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