MAYBE 1068.95/297.04 MAYBE 1068.95/297.04 1068.95/297.04 We are left with following problem, upon which TcT provides the 1068.95/297.04 certificate MAYBE. 1068.95/297.04 1068.95/297.04 Strict Trs: 1068.95/297.04 { active(minus(0(), Y)) -> mark(0()) 1068.95/297.04 , active(minus(s(X), s(Y))) -> mark(minus(X, Y)) 1068.95/297.04 , active(s(X)) -> s(active(X)) 1068.95/297.04 , active(geq(X, 0())) -> mark(true()) 1068.95/297.04 , active(geq(0(), s(Y))) -> mark(false()) 1068.95/297.04 , active(geq(s(X), s(Y))) -> mark(geq(X, Y)) 1068.95/297.04 , active(div(X1, X2)) -> div(active(X1), X2) 1068.95/297.04 , active(div(0(), s(Y))) -> mark(0()) 1068.95/297.04 , active(div(s(X), s(Y))) -> 1068.95/297.04 mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.04 , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) 1068.95/297.04 , active(if(true(), X, Y)) -> mark(X) 1068.95/297.04 , active(if(false(), X, Y)) -> mark(Y) 1068.95/297.04 , minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)) 1068.95/297.04 , s(mark(X)) -> mark(s(X)) 1068.95/297.04 , s(ok(X)) -> ok(s(X)) 1068.95/297.04 , geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)) 1068.95/297.04 , div(mark(X1), X2) -> mark(div(X1, X2)) 1068.95/297.04 , div(ok(X1), ok(X2)) -> ok(div(X1, X2)) 1068.95/297.04 , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) 1068.95/297.04 , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) 1068.95/297.04 , proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)) 1068.95/297.04 , proper(0()) -> ok(0()) 1068.95/297.04 , proper(s(X)) -> s(proper(X)) 1068.95/297.04 , proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)) 1068.95/297.04 , proper(true()) -> ok(true()) 1068.95/297.04 , proper(false()) -> ok(false()) 1068.95/297.04 , proper(div(X1, X2)) -> div(proper(X1), proper(X2)) 1068.95/297.04 , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) 1068.95/297.04 , top(mark(X)) -> top(proper(X)) 1068.95/297.04 , top(ok(X)) -> top(active(X)) } 1068.95/297.04 Obligation: 1068.95/297.04 runtime complexity 1068.95/297.04 Answer: 1068.95/297.04 MAYBE 1068.95/297.04 1068.95/297.04 None of the processors succeeded. 1068.95/297.04 1068.95/297.04 Details of failed attempt(s): 1068.95/297.04 ----------------------------- 1068.95/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1068.95/297.04 following reason: 1068.95/297.04 1068.95/297.04 Computation stopped due to timeout after 297.0 seconds. 1068.95/297.04 1068.95/297.04 2) 'Best' failed due to the following reason: 1068.95/297.04 1068.95/297.04 None of the processors succeeded. 1068.95/297.04 1068.95/297.04 Details of failed attempt(s): 1068.95/297.04 ----------------------------- 1068.95/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1068.95/297.04 seconds)' failed due to the following reason: 1068.95/297.04 1068.95/297.04 Computation stopped due to timeout after 148.0 seconds. 1068.95/297.04 1068.95/297.04 2) 'Best' failed due to the following reason: 1068.95/297.04 1068.95/297.04 None of the processors succeeded. 1068.95/297.04 1068.95/297.04 Details of failed attempt(s): 1068.95/297.04 ----------------------------- 1068.95/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1068.95/297.04 following reason: 1068.95/297.04 1068.95/297.04 The processor is inapplicable, reason: 1068.95/297.04 Processor only applicable for innermost runtime complexity analysis 1068.95/297.04 1068.95/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1068.95/297.04 to the following reason: 1068.95/297.04 1068.95/297.04 The processor is inapplicable, reason: 1068.95/297.04 Processor only applicable for innermost runtime complexity analysis 1068.95/297.04 1068.95/297.04 1068.95/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1068.95/297.04 failed due to the following reason: 1068.95/297.04 1068.95/297.04 None of the processors succeeded. 1068.95/297.04 1068.95/297.04 Details of failed attempt(s): 1068.95/297.04 ----------------------------- 1068.95/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1068.95/297.04 failed due to the following reason: 1068.95/297.04 1068.95/297.04 match-boundness of the problem could not be verified. 1068.95/297.04 1068.95/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1068.95/297.04 failed due to the following reason: 1068.95/297.04 1068.95/297.04 match-boundness of the problem could not be verified. 1068.95/297.04 1068.95/297.04 1068.95/297.04 1068.95/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1068.95/297.04 the following reason: 1068.95/297.04 1068.95/297.04 We add the following weak dependency pairs: 1068.95/297.04 1068.95/297.04 Strict DPs: 1068.95/297.04 { active^#(minus(0(), Y)) -> c_1() 1068.95/297.04 , active^#(minus(s(X), s(Y))) -> c_2(minus^#(X, Y)) 1068.95/297.04 , active^#(s(X)) -> c_3(s^#(active(X))) 1068.95/297.04 , active^#(geq(X, 0())) -> c_4() 1068.95/297.04 , active^#(geq(0(), s(Y))) -> c_5() 1068.95/297.04 , active^#(geq(s(X), s(Y))) -> c_6(geq^#(X, Y)) 1068.95/297.04 , active^#(div(X1, X2)) -> c_7(div^#(active(X1), X2)) 1068.95/297.04 , active^#(div(0(), s(Y))) -> c_8() 1068.95/297.04 , active^#(div(s(X), s(Y))) -> 1068.95/297.04 c_9(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.04 , active^#(if(X1, X2, X3)) -> c_10(if^#(active(X1), X2, X3)) 1068.95/297.04 , active^#(if(true(), X, Y)) -> c_11(X) 1068.95/297.04 , active^#(if(false(), X, Y)) -> c_12(Y) 1068.95/297.04 , minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) 1068.95/297.04 , s^#(mark(X)) -> c_14(s^#(X)) 1068.95/297.04 , s^#(ok(X)) -> c_15(s^#(X)) 1068.95/297.04 , geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) 1068.95/297.04 , div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) 1068.95/297.04 , div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) 1068.95/297.04 , if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) 1068.95/297.04 , if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) 1068.95/297.04 , proper^#(minus(X1, X2)) -> c_21(minus^#(proper(X1), proper(X2))) 1068.95/297.04 , proper^#(0()) -> c_22() 1068.95/297.04 , proper^#(s(X)) -> c_23(s^#(proper(X))) 1068.95/297.04 , proper^#(geq(X1, X2)) -> c_24(geq^#(proper(X1), proper(X2))) 1068.95/297.04 , proper^#(true()) -> c_25() 1068.95/297.04 , proper^#(false()) -> c_26() 1068.95/297.04 , proper^#(div(X1, X2)) -> c_27(div^#(proper(X1), proper(X2))) 1068.95/297.04 , proper^#(if(X1, X2, X3)) -> 1068.95/297.04 c_28(if^#(proper(X1), proper(X2), proper(X3))) 1068.95/297.04 , top^#(mark(X)) -> c_29(top^#(proper(X))) 1068.95/297.04 , top^#(ok(X)) -> c_30(top^#(active(X))) } 1068.95/297.04 1068.95/297.04 and mark the set of starting terms. 1068.95/297.04 1068.95/297.04 We are left with following problem, upon which TcT provides the 1068.95/297.04 certificate MAYBE. 1068.95/297.04 1068.95/297.04 Strict DPs: 1068.95/297.04 { active^#(minus(0(), Y)) -> c_1() 1068.95/297.04 , active^#(minus(s(X), s(Y))) -> c_2(minus^#(X, Y)) 1068.95/297.04 , active^#(s(X)) -> c_3(s^#(active(X))) 1068.95/297.04 , active^#(geq(X, 0())) -> c_4() 1068.95/297.04 , active^#(geq(0(), s(Y))) -> c_5() 1068.95/297.04 , active^#(geq(s(X), s(Y))) -> c_6(geq^#(X, Y)) 1068.95/297.04 , active^#(div(X1, X2)) -> c_7(div^#(active(X1), X2)) 1068.95/297.04 , active^#(div(0(), s(Y))) -> c_8() 1068.95/297.04 , active^#(div(s(X), s(Y))) -> 1068.95/297.04 c_9(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.04 , active^#(if(X1, X2, X3)) -> c_10(if^#(active(X1), X2, X3)) 1068.95/297.04 , active^#(if(true(), X, Y)) -> c_11(X) 1068.95/297.04 , active^#(if(false(), X, Y)) -> c_12(Y) 1068.95/297.04 , minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) 1068.95/297.04 , s^#(mark(X)) -> c_14(s^#(X)) 1068.95/297.04 , s^#(ok(X)) -> c_15(s^#(X)) 1068.95/297.04 , geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) 1068.95/297.04 , div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) 1068.95/297.04 , div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) 1068.95/297.04 , if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) 1068.95/297.04 , if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) 1068.95/297.04 , proper^#(minus(X1, X2)) -> c_21(minus^#(proper(X1), proper(X2))) 1068.95/297.04 , proper^#(0()) -> c_22() 1068.95/297.04 , proper^#(s(X)) -> c_23(s^#(proper(X))) 1068.95/297.04 , proper^#(geq(X1, X2)) -> c_24(geq^#(proper(X1), proper(X2))) 1068.95/297.04 , proper^#(true()) -> c_25() 1068.95/297.04 , proper^#(false()) -> c_26() 1068.95/297.04 , proper^#(div(X1, X2)) -> c_27(div^#(proper(X1), proper(X2))) 1068.95/297.04 , proper^#(if(X1, X2, X3)) -> 1068.95/297.04 c_28(if^#(proper(X1), proper(X2), proper(X3))) 1068.95/297.04 , top^#(mark(X)) -> c_29(top^#(proper(X))) 1068.95/297.04 , top^#(ok(X)) -> c_30(top^#(active(X))) } 1068.95/297.04 Strict Trs: 1068.95/297.04 { active(minus(0(), Y)) -> mark(0()) 1068.95/297.04 , active(minus(s(X), s(Y))) -> mark(minus(X, Y)) 1068.95/297.04 , active(s(X)) -> s(active(X)) 1068.95/297.04 , active(geq(X, 0())) -> mark(true()) 1068.95/297.04 , active(geq(0(), s(Y))) -> mark(false()) 1068.95/297.04 , active(geq(s(X), s(Y))) -> mark(geq(X, Y)) 1068.95/297.04 , active(div(X1, X2)) -> div(active(X1), X2) 1068.95/297.04 , active(div(0(), s(Y))) -> mark(0()) 1068.95/297.04 , active(div(s(X), s(Y))) -> 1068.95/297.04 mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.04 , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) 1068.95/297.04 , active(if(true(), X, Y)) -> mark(X) 1068.95/297.04 , active(if(false(), X, Y)) -> mark(Y) 1068.95/297.04 , minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)) 1068.95/297.04 , s(mark(X)) -> mark(s(X)) 1068.95/297.04 , s(ok(X)) -> ok(s(X)) 1068.95/297.04 , geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)) 1068.95/297.04 , div(mark(X1), X2) -> mark(div(X1, X2)) 1068.95/297.04 , div(ok(X1), ok(X2)) -> ok(div(X1, X2)) 1068.95/297.04 , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) 1068.95/297.04 , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) 1068.95/297.04 , proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)) 1068.95/297.04 , proper(0()) -> ok(0()) 1068.95/297.04 , proper(s(X)) -> s(proper(X)) 1068.95/297.04 , proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)) 1068.95/297.04 , proper(true()) -> ok(true()) 1068.95/297.04 , proper(false()) -> ok(false()) 1068.95/297.04 , proper(div(X1, X2)) -> div(proper(X1), proper(X2)) 1068.95/297.05 , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) 1068.95/297.05 , top(mark(X)) -> top(proper(X)) 1068.95/297.05 , top(ok(X)) -> top(active(X)) } 1068.95/297.05 Obligation: 1068.95/297.05 runtime complexity 1068.95/297.05 Answer: 1068.95/297.05 MAYBE 1068.95/297.05 1068.95/297.05 Consider the dependency graph: 1068.95/297.05 1068.95/297.05 1: active^#(minus(0(), Y)) -> c_1() 1068.95/297.05 1068.95/297.05 2: active^#(minus(s(X), s(Y))) -> c_2(minus^#(X, Y)) 1068.95/297.05 -->_1 minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) :13 1068.95/297.05 1068.95/297.05 3: active^#(s(X)) -> c_3(s^#(active(X))) 1068.95/297.05 -->_1 s^#(ok(X)) -> c_15(s^#(X)) :15 1068.95/297.05 -->_1 s^#(mark(X)) -> c_14(s^#(X)) :14 1068.95/297.05 1068.95/297.05 4: active^#(geq(X, 0())) -> c_4() 1068.95/297.05 1068.95/297.05 5: active^#(geq(0(), s(Y))) -> c_5() 1068.95/297.05 1068.95/297.05 6: active^#(geq(s(X), s(Y))) -> c_6(geq^#(X, Y)) 1068.95/297.05 -->_1 geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) :16 1068.95/297.05 1068.95/297.05 7: active^#(div(X1, X2)) -> c_7(div^#(active(X1), X2)) 1068.95/297.05 -->_1 div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) :18 1068.95/297.05 -->_1 div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) :17 1068.95/297.05 1068.95/297.05 8: active^#(div(0(), s(Y))) -> c_8() 1068.95/297.05 1068.95/297.05 9: active^#(div(s(X), s(Y))) -> 1068.95/297.05 c_9(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 1068.95/297.05 10: active^#(if(X1, X2, X3)) -> c_10(if^#(active(X1), X2, X3)) 1068.95/297.05 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) :20 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 1068.95/297.05 11: active^#(if(true(), X, Y)) -> c_11(X) 1068.95/297.05 -->_1 top^#(ok(X)) -> c_30(top^#(active(X))) :30 1068.95/297.05 -->_1 top^#(mark(X)) -> c_29(top^#(proper(X))) :29 1068.95/297.05 -->_1 proper^#(if(X1, X2, X3)) -> 1068.95/297.05 c_28(if^#(proper(X1), proper(X2), proper(X3))) :28 1068.95/297.05 -->_1 proper^#(div(X1, X2)) -> 1068.95/297.05 c_27(div^#(proper(X1), proper(X2))) :27 1068.95/297.05 -->_1 proper^#(geq(X1, X2)) -> 1068.95/297.05 c_24(geq^#(proper(X1), proper(X2))) :24 1068.95/297.05 -->_1 proper^#(s(X)) -> c_23(s^#(proper(X))) :23 1068.95/297.05 -->_1 proper^#(minus(X1, X2)) -> 1068.95/297.05 c_21(minus^#(proper(X1), proper(X2))) :21 1068.95/297.05 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) :20 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 -->_1 div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) :18 1068.95/297.05 -->_1 div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) :17 1068.95/297.05 -->_1 geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) :16 1068.95/297.05 -->_1 s^#(ok(X)) -> c_15(s^#(X)) :15 1068.95/297.05 -->_1 s^#(mark(X)) -> c_14(s^#(X)) :14 1068.95/297.05 -->_1 minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) :13 1068.95/297.05 -->_1 active^#(if(false(), X, Y)) -> c_12(Y) :12 1068.95/297.05 -->_1 proper^#(false()) -> c_26() :26 1068.95/297.05 -->_1 proper^#(true()) -> c_25() :25 1068.95/297.05 -->_1 proper^#(0()) -> c_22() :22 1068.95/297.05 -->_1 active^#(if(true(), X, Y)) -> c_11(X) :11 1068.95/297.05 -->_1 active^#(if(X1, X2, X3)) -> 1068.95/297.05 c_10(if^#(active(X1), X2, X3)) :10 1068.95/297.05 -->_1 active^#(div(s(X), s(Y))) -> 1068.95/297.05 c_9(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) :9 1068.95/297.05 -->_1 active^#(div(0(), s(Y))) -> c_8() :8 1068.95/297.05 -->_1 active^#(div(X1, X2)) -> c_7(div^#(active(X1), X2)) :7 1068.95/297.05 -->_1 active^#(geq(s(X), s(Y))) -> c_6(geq^#(X, Y)) :6 1068.95/297.05 -->_1 active^#(geq(0(), s(Y))) -> c_5() :5 1068.95/297.05 -->_1 active^#(geq(X, 0())) -> c_4() :4 1068.95/297.05 -->_1 active^#(s(X)) -> c_3(s^#(active(X))) :3 1068.95/297.05 -->_1 active^#(minus(s(X), s(Y))) -> c_2(minus^#(X, Y)) :2 1068.95/297.05 -->_1 active^#(minus(0(), Y)) -> c_1() :1 1068.95/297.05 1068.95/297.05 12: active^#(if(false(), X, Y)) -> c_12(Y) 1068.95/297.05 -->_1 top^#(ok(X)) -> c_30(top^#(active(X))) :30 1068.95/297.05 -->_1 top^#(mark(X)) -> c_29(top^#(proper(X))) :29 1068.95/297.05 -->_1 proper^#(if(X1, X2, X3)) -> 1068.95/297.05 c_28(if^#(proper(X1), proper(X2), proper(X3))) :28 1068.95/297.05 -->_1 proper^#(div(X1, X2)) -> 1068.95/297.05 c_27(div^#(proper(X1), proper(X2))) :27 1068.95/297.05 -->_1 proper^#(geq(X1, X2)) -> 1068.95/297.05 c_24(geq^#(proper(X1), proper(X2))) :24 1068.95/297.05 -->_1 proper^#(s(X)) -> c_23(s^#(proper(X))) :23 1068.95/297.05 -->_1 proper^#(minus(X1, X2)) -> 1068.95/297.05 c_21(minus^#(proper(X1), proper(X2))) :21 1068.95/297.05 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) :20 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 -->_1 div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) :18 1068.95/297.05 -->_1 div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) :17 1068.95/297.05 -->_1 geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) :16 1068.95/297.05 -->_1 s^#(ok(X)) -> c_15(s^#(X)) :15 1068.95/297.05 -->_1 s^#(mark(X)) -> c_14(s^#(X)) :14 1068.95/297.05 -->_1 minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) :13 1068.95/297.05 -->_1 proper^#(false()) -> c_26() :26 1068.95/297.05 -->_1 proper^#(true()) -> c_25() :25 1068.95/297.05 -->_1 proper^#(0()) -> c_22() :22 1068.95/297.05 -->_1 active^#(if(false(), X, Y)) -> c_12(Y) :12 1068.95/297.05 -->_1 active^#(if(true(), X, Y)) -> c_11(X) :11 1068.95/297.05 -->_1 active^#(if(X1, X2, X3)) -> 1068.95/297.05 c_10(if^#(active(X1), X2, X3)) :10 1068.95/297.05 -->_1 active^#(div(s(X), s(Y))) -> 1068.95/297.05 c_9(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) :9 1068.95/297.05 -->_1 active^#(div(0(), s(Y))) -> c_8() :8 1068.95/297.05 -->_1 active^#(div(X1, X2)) -> c_7(div^#(active(X1), X2)) :7 1068.95/297.05 -->_1 active^#(geq(s(X), s(Y))) -> c_6(geq^#(X, Y)) :6 1068.95/297.05 -->_1 active^#(geq(0(), s(Y))) -> c_5() :5 1068.95/297.05 -->_1 active^#(geq(X, 0())) -> c_4() :4 1068.95/297.05 -->_1 active^#(s(X)) -> c_3(s^#(active(X))) :3 1068.95/297.05 -->_1 active^#(minus(s(X), s(Y))) -> c_2(minus^#(X, Y)) :2 1068.95/297.05 -->_1 active^#(minus(0(), Y)) -> c_1() :1 1068.95/297.05 1068.95/297.05 13: minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) 1068.95/297.05 -->_1 minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) :13 1068.95/297.05 1068.95/297.05 14: s^#(mark(X)) -> c_14(s^#(X)) 1068.95/297.05 -->_1 s^#(ok(X)) -> c_15(s^#(X)) :15 1068.95/297.05 -->_1 s^#(mark(X)) -> c_14(s^#(X)) :14 1068.95/297.05 1068.95/297.05 15: s^#(ok(X)) -> c_15(s^#(X)) 1068.95/297.05 -->_1 s^#(ok(X)) -> c_15(s^#(X)) :15 1068.95/297.05 -->_1 s^#(mark(X)) -> c_14(s^#(X)) :14 1068.95/297.05 1068.95/297.05 16: geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) 1068.95/297.05 -->_1 geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) :16 1068.95/297.05 1068.95/297.05 17: div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) 1068.95/297.05 -->_1 div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) :18 1068.95/297.05 -->_1 div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) :17 1068.95/297.05 1068.95/297.05 18: div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) 1068.95/297.05 -->_1 div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) :18 1068.95/297.05 -->_1 div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) :17 1068.95/297.05 1068.95/297.05 19: if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) 1068.95/297.05 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) :20 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 1068.95/297.05 20: if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) 1068.95/297.05 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) :20 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 1068.95/297.05 21: proper^#(minus(X1, X2)) -> 1068.95/297.05 c_21(minus^#(proper(X1), proper(X2))) 1068.95/297.05 -->_1 minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) :13 1068.95/297.05 1068.95/297.05 22: proper^#(0()) -> c_22() 1068.95/297.05 1068.95/297.05 23: proper^#(s(X)) -> c_23(s^#(proper(X))) 1068.95/297.05 -->_1 s^#(ok(X)) -> c_15(s^#(X)) :15 1068.95/297.05 -->_1 s^#(mark(X)) -> c_14(s^#(X)) :14 1068.95/297.05 1068.95/297.05 24: proper^#(geq(X1, X2)) -> c_24(geq^#(proper(X1), proper(X2))) 1068.95/297.05 -->_1 geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) :16 1068.95/297.05 1068.95/297.05 25: proper^#(true()) -> c_25() 1068.95/297.05 1068.95/297.05 26: proper^#(false()) -> c_26() 1068.95/297.05 1068.95/297.05 27: proper^#(div(X1, X2)) -> c_27(div^#(proper(X1), proper(X2))) 1068.95/297.05 -->_1 div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) :18 1068.95/297.05 -->_1 div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) :17 1068.95/297.05 1068.95/297.05 28: proper^#(if(X1, X2, X3)) -> 1068.95/297.05 c_28(if^#(proper(X1), proper(X2), proper(X3))) 1068.95/297.05 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) :20 1068.95/297.05 -->_1 if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) :19 1068.95/297.05 1068.95/297.05 29: top^#(mark(X)) -> c_29(top^#(proper(X))) 1068.95/297.05 -->_1 top^#(ok(X)) -> c_30(top^#(active(X))) :30 1068.95/297.05 -->_1 top^#(mark(X)) -> c_29(top^#(proper(X))) :29 1068.95/297.05 1068.95/297.05 30: top^#(ok(X)) -> c_30(top^#(active(X))) 1068.95/297.05 -->_1 top^#(ok(X)) -> c_30(top^#(active(X))) :30 1068.95/297.05 -->_1 top^#(mark(X)) -> c_29(top^#(proper(X))) :29 1068.95/297.05 1068.95/297.05 1068.95/297.05 Only the nodes {13,14,15,16,17,18,19,20,22,25,26,29,30} are 1068.95/297.05 reachable from nodes {13,14,15,16,17,18,19,20,22,25,26,29,30} that 1068.95/297.05 start derivation from marked basic terms. The nodes not reachable 1068.95/297.05 are removed from the problem. 1068.95/297.05 1068.95/297.05 We are left with following problem, upon which TcT provides the 1068.95/297.05 certificate MAYBE. 1068.95/297.05 1068.95/297.05 Strict DPs: 1068.95/297.05 { minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) 1068.95/297.05 , s^#(mark(X)) -> c_14(s^#(X)) 1068.95/297.05 , s^#(ok(X)) -> c_15(s^#(X)) 1068.95/297.05 , geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) 1068.95/297.05 , div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) 1068.95/297.05 , div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) 1068.95/297.05 , if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) 1068.95/297.05 , if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) 1068.95/297.05 , proper^#(0()) -> c_22() 1068.95/297.05 , proper^#(true()) -> c_25() 1068.95/297.05 , proper^#(false()) -> c_26() 1068.95/297.05 , top^#(mark(X)) -> c_29(top^#(proper(X))) 1068.95/297.05 , top^#(ok(X)) -> c_30(top^#(active(X))) } 1068.95/297.05 Strict Trs: 1068.95/297.05 { active(minus(0(), Y)) -> mark(0()) 1068.95/297.05 , active(minus(s(X), s(Y))) -> mark(minus(X, Y)) 1068.95/297.05 , active(s(X)) -> s(active(X)) 1068.95/297.05 , active(geq(X, 0())) -> mark(true()) 1068.95/297.05 , active(geq(0(), s(Y))) -> mark(false()) 1068.95/297.05 , active(geq(s(X), s(Y))) -> mark(geq(X, Y)) 1068.95/297.05 , active(div(X1, X2)) -> div(active(X1), X2) 1068.95/297.05 , active(div(0(), s(Y))) -> mark(0()) 1068.95/297.05 , active(div(s(X), s(Y))) -> 1068.95/297.05 mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.05 , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) 1068.95/297.05 , active(if(true(), X, Y)) -> mark(X) 1068.95/297.05 , active(if(false(), X, Y)) -> mark(Y) 1068.95/297.05 , minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)) 1068.95/297.05 , s(mark(X)) -> mark(s(X)) 1068.95/297.05 , s(ok(X)) -> ok(s(X)) 1068.95/297.05 , geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)) 1068.95/297.05 , div(mark(X1), X2) -> mark(div(X1, X2)) 1068.95/297.05 , div(ok(X1), ok(X2)) -> ok(div(X1, X2)) 1068.95/297.05 , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) 1068.95/297.05 , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) 1068.95/297.05 , proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)) 1068.95/297.05 , proper(0()) -> ok(0()) 1068.95/297.05 , proper(s(X)) -> s(proper(X)) 1068.95/297.05 , proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)) 1068.95/297.05 , proper(true()) -> ok(true()) 1068.95/297.05 , proper(false()) -> ok(false()) 1068.95/297.05 , proper(div(X1, X2)) -> div(proper(X1), proper(X2)) 1068.95/297.05 , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) 1068.95/297.05 , top(mark(X)) -> top(proper(X)) 1068.95/297.05 , top(ok(X)) -> top(active(X)) } 1068.95/297.05 Obligation: 1068.95/297.05 runtime complexity 1068.95/297.05 Answer: 1068.95/297.05 MAYBE 1068.95/297.05 1068.95/297.05 We estimate the number of application of {9,10,11} by applications 1068.95/297.05 of Pre({9,10,11}) = {}. Here rules are labeled as follows: 1068.95/297.05 1068.95/297.05 DPs: 1068.95/297.05 { 1: minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) 1068.95/297.05 , 2: s^#(mark(X)) -> c_14(s^#(X)) 1068.95/297.05 , 3: s^#(ok(X)) -> c_15(s^#(X)) 1068.95/297.05 , 4: geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) 1068.95/297.05 , 5: div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) 1068.95/297.05 , 6: div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) 1068.95/297.05 , 7: if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) 1068.95/297.05 , 8: if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) 1068.95/297.05 , 9: proper^#(0()) -> c_22() 1068.95/297.05 , 10: proper^#(true()) -> c_25() 1068.95/297.05 , 11: proper^#(false()) -> c_26() 1068.95/297.05 , 12: top^#(mark(X)) -> c_29(top^#(proper(X))) 1068.95/297.05 , 13: top^#(ok(X)) -> c_30(top^#(active(X))) } 1068.95/297.05 1068.95/297.05 We are left with following problem, upon which TcT provides the 1068.95/297.05 certificate MAYBE. 1068.95/297.05 1068.95/297.05 Strict DPs: 1068.95/297.05 { minus^#(ok(X1), ok(X2)) -> c_13(minus^#(X1, X2)) 1068.95/297.05 , s^#(mark(X)) -> c_14(s^#(X)) 1068.95/297.05 , s^#(ok(X)) -> c_15(s^#(X)) 1068.95/297.05 , geq^#(ok(X1), ok(X2)) -> c_16(geq^#(X1, X2)) 1068.95/297.05 , div^#(mark(X1), X2) -> c_17(div^#(X1, X2)) 1068.95/297.05 , div^#(ok(X1), ok(X2)) -> c_18(div^#(X1, X2)) 1068.95/297.05 , if^#(mark(X1), X2, X3) -> c_19(if^#(X1, X2, X3)) 1068.95/297.05 , if^#(ok(X1), ok(X2), ok(X3)) -> c_20(if^#(X1, X2, X3)) 1068.95/297.05 , top^#(mark(X)) -> c_29(top^#(proper(X))) 1068.95/297.05 , top^#(ok(X)) -> c_30(top^#(active(X))) } 1068.95/297.05 Strict Trs: 1068.95/297.05 { active(minus(0(), Y)) -> mark(0()) 1068.95/297.05 , active(minus(s(X), s(Y))) -> mark(minus(X, Y)) 1068.95/297.05 , active(s(X)) -> s(active(X)) 1068.95/297.05 , active(geq(X, 0())) -> mark(true()) 1068.95/297.05 , active(geq(0(), s(Y))) -> mark(false()) 1068.95/297.05 , active(geq(s(X), s(Y))) -> mark(geq(X, Y)) 1068.95/297.05 , active(div(X1, X2)) -> div(active(X1), X2) 1068.95/297.05 , active(div(0(), s(Y))) -> mark(0()) 1068.95/297.05 , active(div(s(X), s(Y))) -> 1068.95/297.05 mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) 1068.95/297.05 , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) 1068.95/297.05 , active(if(true(), X, Y)) -> mark(X) 1068.95/297.05 , active(if(false(), X, Y)) -> mark(Y) 1068.95/297.05 , minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)) 1068.95/297.05 , s(mark(X)) -> mark(s(X)) 1068.95/297.05 , s(ok(X)) -> ok(s(X)) 1068.95/297.05 , geq(ok(X1), ok(X2)) -> ok(geq(X1, X2)) 1068.95/297.05 , div(mark(X1), X2) -> mark(div(X1, X2)) 1068.95/297.05 , div(ok(X1), ok(X2)) -> ok(div(X1, X2)) 1068.95/297.05 , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) 1068.95/297.05 , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) 1068.95/297.05 , proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)) 1068.95/297.05 , proper(0()) -> ok(0()) 1068.95/297.05 , proper(s(X)) -> s(proper(X)) 1068.95/297.05 , proper(geq(X1, X2)) -> geq(proper(X1), proper(X2)) 1068.95/297.05 , proper(true()) -> ok(true()) 1068.95/297.05 , proper(false()) -> ok(false()) 1068.95/297.05 , proper(div(X1, X2)) -> div(proper(X1), proper(X2)) 1068.95/297.05 , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) 1068.95/297.05 , top(mark(X)) -> top(proper(X)) 1068.95/297.05 , top(ok(X)) -> top(active(X)) } 1068.95/297.05 Weak DPs: 1068.95/297.05 { proper^#(0()) -> c_22() 1068.95/297.05 , proper^#(true()) -> c_25() 1068.95/297.05 , proper^#(false()) -> c_26() } 1068.95/297.05 Obligation: 1068.95/297.05 runtime complexity 1068.95/297.05 Answer: 1068.95/297.05 MAYBE 1068.95/297.05 1068.95/297.05 Empty strict component of the problem is NOT empty. 1068.95/297.05 1068.95/297.05 1068.95/297.05 Arrrr.. 1069.55/297.56 EOF