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