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