MAYBE 843.03/297.14 MAYBE 843.03/297.14 843.03/297.14 We are left with following problem, upon which TcT provides the 843.03/297.14 certificate MAYBE. 843.03/297.14 843.03/297.14 Strict Trs: 843.03/297.14 { active(pairNs()) -> mark(cons(0(), incr(oddNs()))) 843.03/297.14 , active(cons(X1, X2)) -> cons(active(X1), X2) 843.03/297.14 , active(incr(X)) -> incr(active(X)) 843.03/297.14 , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))) 843.03/297.14 , active(oddNs()) -> mark(incr(pairNs())) 843.03/297.14 , active(s(X)) -> s(active(X)) 843.03/297.14 , active(take(X1, X2)) -> take(X1, active(X2)) 843.03/297.14 , active(take(X1, X2)) -> take(active(X1), X2) 843.03/297.14 , active(take(0(), XS)) -> mark(nil()) 843.03/297.14 , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))) 843.03/297.14 , active(zip(X1, X2)) -> zip(X1, active(X2)) 843.03/297.14 , active(zip(X1, X2)) -> zip(active(X1), X2) 843.03/297.14 , active(zip(X, nil())) -> mark(nil()) 843.03/297.14 , active(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.14 mark(cons(pair(X, Y), zip(XS, YS))) 843.03/297.14 , active(zip(nil(), XS)) -> mark(nil()) 843.03/297.14 , active(pair(X1, X2)) -> pair(X1, active(X2)) 843.03/297.14 , active(pair(X1, X2)) -> pair(active(X1), X2) 843.03/297.14 , active(tail(X)) -> tail(active(X)) 843.03/297.14 , active(tail(cons(X, XS))) -> mark(XS) 843.03/297.14 , active(repItems(X)) -> repItems(active(X)) 843.03/297.14 , active(repItems(cons(X, XS))) -> 843.03/297.14 mark(cons(X, cons(X, repItems(XS)))) 843.03/297.14 , active(repItems(nil())) -> mark(nil()) 843.03/297.14 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 843.03/297.14 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 843.03/297.14 , incr(mark(X)) -> mark(incr(X)) 843.03/297.14 , incr(ok(X)) -> ok(incr(X)) 843.03/297.14 , s(mark(X)) -> mark(s(X)) 843.03/297.14 , s(ok(X)) -> ok(s(X)) 843.03/297.14 , take(X1, mark(X2)) -> mark(take(X1, X2)) 843.03/297.14 , take(mark(X1), X2) -> mark(take(X1, X2)) 843.03/297.14 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 843.03/297.14 , zip(X1, mark(X2)) -> mark(zip(X1, X2)) 843.03/297.14 , zip(mark(X1), X2) -> mark(zip(X1, X2)) 843.03/297.14 , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2)) 843.03/297.14 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 843.03/297.14 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 843.03/297.14 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 843.03/297.14 , tail(mark(X)) -> mark(tail(X)) 843.03/297.14 , tail(ok(X)) -> ok(tail(X)) 843.03/297.14 , repItems(mark(X)) -> mark(repItems(X)) 843.03/297.14 , repItems(ok(X)) -> ok(repItems(X)) 843.03/297.14 , proper(pairNs()) -> ok(pairNs()) 843.03/297.14 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 843.03/297.14 , proper(0()) -> ok(0()) 843.03/297.14 , proper(incr(X)) -> incr(proper(X)) 843.03/297.14 , proper(oddNs()) -> ok(oddNs()) 843.03/297.14 , proper(s(X)) -> s(proper(X)) 843.03/297.14 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 843.03/297.14 , proper(nil()) -> ok(nil()) 843.03/297.14 , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2)) 843.03/297.14 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 843.03/297.14 , proper(tail(X)) -> tail(proper(X)) 843.03/297.14 , proper(repItems(X)) -> repItems(proper(X)) 843.03/297.14 , top(mark(X)) -> top(proper(X)) 843.03/297.14 , top(ok(X)) -> top(active(X)) } 843.03/297.14 Obligation: 843.03/297.14 runtime complexity 843.03/297.14 Answer: 843.03/297.14 MAYBE 843.03/297.14 843.03/297.14 None of the processors succeeded. 843.03/297.14 843.03/297.14 Details of failed attempt(s): 843.03/297.14 ----------------------------- 843.03/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 843.03/297.14 following reason: 843.03/297.14 843.03/297.14 Computation stopped due to timeout after 297.0 seconds. 843.03/297.14 843.03/297.14 2) 'Best' failed due to the following reason: 843.03/297.14 843.03/297.14 None of the processors succeeded. 843.03/297.14 843.03/297.14 Details of failed attempt(s): 843.03/297.14 ----------------------------- 843.03/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 843.03/297.14 seconds)' failed due to the following reason: 843.03/297.14 843.03/297.14 Computation stopped due to timeout after 148.0 seconds. 843.03/297.14 843.03/297.14 2) 'Best' failed due to the following reason: 843.03/297.14 843.03/297.14 None of the processors succeeded. 843.03/297.14 843.03/297.14 Details of failed attempt(s): 843.03/297.14 ----------------------------- 843.03/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 843.03/297.14 following reason: 843.03/297.14 843.03/297.14 The processor is inapplicable, reason: 843.03/297.14 Processor only applicable for innermost runtime complexity analysis 843.03/297.14 843.03/297.14 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 843.03/297.14 to the following reason: 843.03/297.14 843.03/297.14 The processor is inapplicable, reason: 843.03/297.14 Processor only applicable for innermost runtime complexity analysis 843.03/297.14 843.03/297.14 843.03/297.14 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 843.03/297.14 failed due to the following reason: 843.03/297.14 843.03/297.14 None of the processors succeeded. 843.03/297.14 843.03/297.14 Details of failed attempt(s): 843.03/297.14 ----------------------------- 843.03/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 843.03/297.14 failed due to the following reason: 843.03/297.14 843.03/297.14 match-boundness of the problem could not be verified. 843.03/297.14 843.03/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 843.03/297.14 failed due to the following reason: 843.03/297.14 843.03/297.14 match-boundness of the problem could not be verified. 843.03/297.14 843.03/297.14 843.03/297.14 843.03/297.14 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 843.03/297.14 the following reason: 843.03/297.14 843.03/297.14 We add the following weak dependency pairs: 843.03/297.14 843.03/297.14 Strict DPs: 843.03/297.14 { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) 843.03/297.14 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 843.03/297.14 , active^#(incr(X)) -> c_3(incr^#(active(X))) 843.03/297.14 , active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS))) 843.03/297.14 , active^#(oddNs()) -> c_5(incr^#(pairNs())) 843.03/297.14 , active^#(s(X)) -> c_6(s^#(active(X))) 843.03/297.14 , active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2))) 843.03/297.14 , active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2)) 843.03/297.14 , active^#(take(0(), XS)) -> c_9() 843.03/297.14 , active^#(take(s(N), cons(X, XS))) -> c_10(cons^#(X, take(N, XS))) 843.03/297.14 , active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2))) 843.03/297.14 , active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2)) 843.03/297.14 , active^#(zip(X, nil())) -> c_13() 843.03/297.14 , active^#(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.14 c_14(cons^#(pair(X, Y), zip(XS, YS))) 843.03/297.14 , active^#(zip(nil(), XS)) -> c_15() 843.03/297.14 , active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2))) 843.03/297.14 , active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2)) 843.03/297.14 , active^#(tail(X)) -> c_18(tail^#(active(X))) 843.03/297.14 , active^#(tail(cons(X, XS))) -> c_19(XS) 843.03/297.14 , active^#(repItems(X)) -> c_20(repItems^#(active(X))) 843.03/297.14 , active^#(repItems(cons(X, XS))) -> 843.03/297.14 c_21(cons^#(X, cons(X, repItems(XS)))) 843.03/297.14 , active^#(repItems(nil())) -> c_22() 843.03/297.14 , cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) 843.03/297.14 , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) 843.03/297.14 , incr^#(mark(X)) -> c_25(incr^#(X)) 843.03/297.14 , incr^#(ok(X)) -> c_26(incr^#(X)) 843.03/297.14 , s^#(mark(X)) -> c_27(s^#(X)) 843.03/297.14 , s^#(ok(X)) -> c_28(s^#(X)) 843.03/297.14 , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) 843.03/297.14 , take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) 843.03/297.14 , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) 843.03/297.14 , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) 843.03/297.14 , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) 843.03/297.14 , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) 843.03/297.14 , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) 843.03/297.14 , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) 843.03/297.14 , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) 843.03/297.14 , tail^#(mark(X)) -> c_38(tail^#(X)) 843.03/297.14 , tail^#(ok(X)) -> c_39(tail^#(X)) 843.03/297.14 , repItems^#(mark(X)) -> c_40(repItems^#(X)) 843.03/297.14 , repItems^#(ok(X)) -> c_41(repItems^#(X)) 843.03/297.14 , proper^#(pairNs()) -> c_42() 843.03/297.14 , proper^#(cons(X1, X2)) -> c_43(cons^#(proper(X1), proper(X2))) 843.03/297.14 , proper^#(0()) -> c_44() 843.03/297.14 , proper^#(incr(X)) -> c_45(incr^#(proper(X))) 843.03/297.14 , proper^#(oddNs()) -> c_46() 843.03/297.14 , proper^#(s(X)) -> c_47(s^#(proper(X))) 843.03/297.14 , proper^#(take(X1, X2)) -> c_48(take^#(proper(X1), proper(X2))) 843.03/297.14 , proper^#(nil()) -> c_49() 843.03/297.14 , proper^#(zip(X1, X2)) -> c_50(zip^#(proper(X1), proper(X2))) 843.03/297.14 , proper^#(pair(X1, X2)) -> c_51(pair^#(proper(X1), proper(X2))) 843.03/297.14 , proper^#(tail(X)) -> c_52(tail^#(proper(X))) 843.03/297.14 , proper^#(repItems(X)) -> c_53(repItems^#(proper(X))) 843.03/297.14 , top^#(mark(X)) -> c_54(top^#(proper(X))) 843.03/297.14 , top^#(ok(X)) -> c_55(top^#(active(X))) } 843.03/297.14 843.03/297.14 and mark the set of starting terms. 843.03/297.14 843.03/297.14 We are left with following problem, upon which TcT provides the 843.03/297.14 certificate MAYBE. 843.03/297.14 843.03/297.14 Strict DPs: 843.03/297.14 { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) 843.03/297.14 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 843.03/297.14 , active^#(incr(X)) -> c_3(incr^#(active(X))) 843.03/297.14 , active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS))) 843.03/297.14 , active^#(oddNs()) -> c_5(incr^#(pairNs())) 843.03/297.14 , active^#(s(X)) -> c_6(s^#(active(X))) 843.03/297.14 , active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2))) 843.03/297.15 , active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2)) 843.03/297.15 , active^#(take(0(), XS)) -> c_9() 843.03/297.15 , active^#(take(s(N), cons(X, XS))) -> c_10(cons^#(X, take(N, XS))) 843.03/297.15 , active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2))) 843.03/297.15 , active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2)) 843.03/297.15 , active^#(zip(X, nil())) -> c_13() 843.03/297.15 , active^#(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.15 c_14(cons^#(pair(X, Y), zip(XS, YS))) 843.03/297.15 , active^#(zip(nil(), XS)) -> c_15() 843.03/297.15 , active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2))) 843.03/297.15 , active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2)) 843.03/297.15 , active^#(tail(X)) -> c_18(tail^#(active(X))) 843.03/297.15 , active^#(tail(cons(X, XS))) -> c_19(XS) 843.03/297.15 , active^#(repItems(X)) -> c_20(repItems^#(active(X))) 843.03/297.15 , active^#(repItems(cons(X, XS))) -> 843.03/297.15 c_21(cons^#(X, cons(X, repItems(XS)))) 843.03/297.15 , active^#(repItems(nil())) -> c_22() 843.03/297.15 , cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) 843.03/297.15 , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) 843.03/297.15 , incr^#(mark(X)) -> c_25(incr^#(X)) 843.03/297.15 , incr^#(ok(X)) -> c_26(incr^#(X)) 843.03/297.15 , s^#(mark(X)) -> c_27(s^#(X)) 843.03/297.15 , s^#(ok(X)) -> c_28(s^#(X)) 843.03/297.15 , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) 843.03/297.15 , take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) 843.03/297.15 , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) 843.03/297.15 , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) 843.03/297.15 , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) 843.03/297.15 , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) 843.03/297.15 , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) 843.03/297.15 , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) 843.03/297.15 , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) 843.03/297.15 , tail^#(mark(X)) -> c_38(tail^#(X)) 843.03/297.15 , tail^#(ok(X)) -> c_39(tail^#(X)) 843.03/297.15 , repItems^#(mark(X)) -> c_40(repItems^#(X)) 843.03/297.15 , repItems^#(ok(X)) -> c_41(repItems^#(X)) 843.03/297.15 , proper^#(pairNs()) -> c_42() 843.03/297.15 , proper^#(cons(X1, X2)) -> c_43(cons^#(proper(X1), proper(X2))) 843.03/297.15 , proper^#(0()) -> c_44() 843.03/297.15 , proper^#(incr(X)) -> c_45(incr^#(proper(X))) 843.03/297.15 , proper^#(oddNs()) -> c_46() 843.03/297.15 , proper^#(s(X)) -> c_47(s^#(proper(X))) 843.03/297.15 , proper^#(take(X1, X2)) -> c_48(take^#(proper(X1), proper(X2))) 843.03/297.15 , proper^#(nil()) -> c_49() 843.03/297.15 , proper^#(zip(X1, X2)) -> c_50(zip^#(proper(X1), proper(X2))) 843.03/297.15 , proper^#(pair(X1, X2)) -> c_51(pair^#(proper(X1), proper(X2))) 843.03/297.15 , proper^#(tail(X)) -> c_52(tail^#(proper(X))) 843.03/297.15 , proper^#(repItems(X)) -> c_53(repItems^#(proper(X))) 843.03/297.15 , top^#(mark(X)) -> c_54(top^#(proper(X))) 843.03/297.15 , top^#(ok(X)) -> c_55(top^#(active(X))) } 843.03/297.15 Strict Trs: 843.03/297.15 { active(pairNs()) -> mark(cons(0(), incr(oddNs()))) 843.03/297.15 , active(cons(X1, X2)) -> cons(active(X1), X2) 843.03/297.15 , active(incr(X)) -> incr(active(X)) 843.03/297.15 , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))) 843.03/297.15 , active(oddNs()) -> mark(incr(pairNs())) 843.03/297.15 , active(s(X)) -> s(active(X)) 843.03/297.15 , active(take(X1, X2)) -> take(X1, active(X2)) 843.03/297.15 , active(take(X1, X2)) -> take(active(X1), X2) 843.03/297.15 , active(take(0(), XS)) -> mark(nil()) 843.03/297.15 , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))) 843.03/297.15 , active(zip(X1, X2)) -> zip(X1, active(X2)) 843.03/297.15 , active(zip(X1, X2)) -> zip(active(X1), X2) 843.03/297.15 , active(zip(X, nil())) -> mark(nil()) 843.03/297.15 , active(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.15 mark(cons(pair(X, Y), zip(XS, YS))) 843.03/297.15 , active(zip(nil(), XS)) -> mark(nil()) 843.03/297.15 , active(pair(X1, X2)) -> pair(X1, active(X2)) 843.03/297.15 , active(pair(X1, X2)) -> pair(active(X1), X2) 843.03/297.15 , active(tail(X)) -> tail(active(X)) 843.03/297.15 , active(tail(cons(X, XS))) -> mark(XS) 843.03/297.15 , active(repItems(X)) -> repItems(active(X)) 843.03/297.15 , active(repItems(cons(X, XS))) -> 843.03/297.15 mark(cons(X, cons(X, repItems(XS)))) 843.03/297.15 , active(repItems(nil())) -> mark(nil()) 843.03/297.15 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 843.03/297.15 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 843.03/297.15 , incr(mark(X)) -> mark(incr(X)) 843.03/297.15 , incr(ok(X)) -> ok(incr(X)) 843.03/297.15 , s(mark(X)) -> mark(s(X)) 843.03/297.15 , s(ok(X)) -> ok(s(X)) 843.03/297.15 , take(X1, mark(X2)) -> mark(take(X1, X2)) 843.03/297.15 , take(mark(X1), X2) -> mark(take(X1, X2)) 843.03/297.15 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 843.03/297.15 , zip(X1, mark(X2)) -> mark(zip(X1, X2)) 843.03/297.15 , zip(mark(X1), X2) -> mark(zip(X1, X2)) 843.03/297.15 , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2)) 843.03/297.15 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 843.03/297.15 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 843.03/297.15 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 843.03/297.15 , tail(mark(X)) -> mark(tail(X)) 843.03/297.15 , tail(ok(X)) -> ok(tail(X)) 843.03/297.15 , repItems(mark(X)) -> mark(repItems(X)) 843.03/297.15 , repItems(ok(X)) -> ok(repItems(X)) 843.03/297.15 , proper(pairNs()) -> ok(pairNs()) 843.03/297.15 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 843.03/297.15 , proper(0()) -> ok(0()) 843.03/297.15 , proper(incr(X)) -> incr(proper(X)) 843.03/297.15 , proper(oddNs()) -> ok(oddNs()) 843.03/297.15 , proper(s(X)) -> s(proper(X)) 843.03/297.15 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 843.03/297.15 , proper(nil()) -> ok(nil()) 843.03/297.15 , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2)) 843.03/297.15 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 843.03/297.15 , proper(tail(X)) -> tail(proper(X)) 843.03/297.15 , proper(repItems(X)) -> repItems(proper(X)) 843.03/297.15 , top(mark(X)) -> top(proper(X)) 843.03/297.15 , top(ok(X)) -> top(active(X)) } 843.03/297.15 Obligation: 843.03/297.15 runtime complexity 843.03/297.15 Answer: 843.03/297.15 MAYBE 843.03/297.15 843.03/297.15 Consider the dependency graph: 843.03/297.15 843.03/297.15 1: active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) 843.03/297.15 843.03/297.15 2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 3: active^#(incr(X)) -> c_3(incr^#(active(X))) 843.03/297.15 -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26 843.03/297.15 -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25 843.03/297.15 843.03/297.15 4: active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS))) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 5: active^#(oddNs()) -> c_5(incr^#(pairNs())) 843.03/297.15 843.03/297.15 6: active^#(s(X)) -> c_6(s^#(active(X))) 843.03/297.15 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 843.03/297.15 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 843.03/297.15 843.03/297.15 7: active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2))) 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 843.03/297.15 8: active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2)) 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 843.03/297.15 9: active^#(take(0(), XS)) -> c_9() 843.03/297.15 843.03/297.15 10: active^#(take(s(N), cons(X, XS))) -> 843.03/297.15 c_10(cons^#(X, take(N, XS))) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 11: active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2))) 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 843.03/297.15 12: active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2)) 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 843.03/297.15 13: active^#(zip(X, nil())) -> c_13() 843.03/297.15 843.03/297.15 14: active^#(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.15 c_14(cons^#(pair(X, Y), zip(XS, YS))) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 15: active^#(zip(nil(), XS)) -> c_15() 843.03/297.15 843.03/297.15 16: active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2))) 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 843.03/297.15 17: active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2)) 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 843.03/297.15 18: active^#(tail(X)) -> c_18(tail^#(active(X))) 843.03/297.15 -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39 843.03/297.15 -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38 843.03/297.15 843.03/297.15 19: active^#(tail(cons(X, XS))) -> c_19(XS) 843.03/297.15 -->_1 top^#(ok(X)) -> c_55(top^#(active(X))) :55 843.03/297.15 -->_1 top^#(mark(X)) -> c_54(top^#(proper(X))) :54 843.03/297.15 -->_1 proper^#(repItems(X)) -> c_53(repItems^#(proper(X))) :53 843.03/297.15 -->_1 proper^#(tail(X)) -> c_52(tail^#(proper(X))) :52 843.03/297.15 -->_1 proper^#(pair(X1, X2)) -> 843.03/297.15 c_51(pair^#(proper(X1), proper(X2))) :51 843.03/297.15 -->_1 proper^#(zip(X1, X2)) -> 843.03/297.15 c_50(zip^#(proper(X1), proper(X2))) :50 843.03/297.15 -->_1 proper^#(take(X1, X2)) -> 843.03/297.15 c_48(take^#(proper(X1), proper(X2))) :48 843.03/297.15 -->_1 proper^#(s(X)) -> c_47(s^#(proper(X))) :47 843.03/297.15 -->_1 proper^#(incr(X)) -> c_45(incr^#(proper(X))) :45 843.03/297.15 -->_1 proper^#(cons(X1, X2)) -> 843.03/297.15 c_43(cons^#(proper(X1), proper(X2))) :43 843.03/297.15 -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41 843.03/297.15 -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40 843.03/297.15 -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39 843.03/297.15 -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 843.03/297.15 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 843.03/297.15 -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26 843.03/297.15 -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 -->_1 active^#(repItems(cons(X, XS))) -> 843.03/297.15 c_21(cons^#(X, cons(X, repItems(XS)))) :21 843.03/297.15 -->_1 active^#(repItems(X)) -> c_20(repItems^#(active(X))) :20 843.03/297.15 -->_1 proper^#(nil()) -> c_49() :49 843.03/297.15 -->_1 proper^#(oddNs()) -> c_46() :46 843.03/297.15 -->_1 proper^#(0()) -> c_44() :44 843.03/297.15 -->_1 proper^#(pairNs()) -> c_42() :42 843.03/297.15 -->_1 active^#(repItems(nil())) -> c_22() :22 843.03/297.15 -->_1 active^#(tail(cons(X, XS))) -> c_19(XS) :19 843.03/297.15 -->_1 active^#(tail(X)) -> c_18(tail^#(active(X))) :18 843.03/297.15 -->_1 active^#(pair(X1, X2)) -> c_17(pair^#(active(X1), X2)) :17 843.03/297.15 -->_1 active^#(pair(X1, X2)) -> c_16(pair^#(X1, active(X2))) :16 843.03/297.15 -->_1 active^#(zip(nil(), XS)) -> c_15() :15 843.03/297.15 -->_1 active^#(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.15 c_14(cons^#(pair(X, Y), zip(XS, YS))) :14 843.03/297.15 -->_1 active^#(zip(X, nil())) -> c_13() :13 843.03/297.15 -->_1 active^#(zip(X1, X2)) -> c_12(zip^#(active(X1), X2)) :12 843.03/297.15 -->_1 active^#(zip(X1, X2)) -> c_11(zip^#(X1, active(X2))) :11 843.03/297.15 -->_1 active^#(take(s(N), cons(X, XS))) -> 843.03/297.15 c_10(cons^#(X, take(N, XS))) :10 843.03/297.15 -->_1 active^#(take(0(), XS)) -> c_9() :9 843.03/297.15 -->_1 active^#(take(X1, X2)) -> c_8(take^#(active(X1), X2)) :8 843.03/297.15 -->_1 active^#(take(X1, X2)) -> c_7(take^#(X1, active(X2))) :7 843.03/297.15 -->_1 active^#(s(X)) -> c_6(s^#(active(X))) :6 843.03/297.15 -->_1 active^#(oddNs()) -> c_5(incr^#(pairNs())) :5 843.03/297.15 -->_1 active^#(incr(cons(X, XS))) -> c_4(cons^#(s(X), incr(XS))) :4 843.03/297.15 -->_1 active^#(incr(X)) -> c_3(incr^#(active(X))) :3 843.03/297.15 -->_1 active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) :2 843.03/297.15 -->_1 active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) :1 843.03/297.15 843.03/297.15 20: active^#(repItems(X)) -> c_20(repItems^#(active(X))) 843.03/297.15 -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41 843.03/297.15 -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40 843.03/297.15 843.03/297.15 21: active^#(repItems(cons(X, XS))) -> 843.03/297.15 c_21(cons^#(X, cons(X, repItems(XS)))) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 22: active^#(repItems(nil())) -> c_22() 843.03/297.15 843.03/297.15 23: cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 24: cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 25: incr^#(mark(X)) -> c_25(incr^#(X)) 843.03/297.15 -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26 843.03/297.15 -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25 843.03/297.15 843.03/297.15 26: incr^#(ok(X)) -> c_26(incr^#(X)) 843.03/297.15 -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26 843.03/297.15 -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25 843.03/297.15 843.03/297.15 27: s^#(mark(X)) -> c_27(s^#(X)) 843.03/297.15 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 843.03/297.15 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 843.03/297.15 843.03/297.15 28: s^#(ok(X)) -> c_28(s^#(X)) 843.03/297.15 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 843.03/297.15 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 843.03/297.15 843.03/297.15 29: take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 843.03/297.15 30: take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 843.03/297.15 31: take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 843.03/297.15 32: zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 843.03/297.15 33: zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 843.03/297.15 34: zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 843.03/297.15 35: pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 843.03/297.15 36: pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 843.03/297.15 37: pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 843.03/297.15 38: tail^#(mark(X)) -> c_38(tail^#(X)) 843.03/297.15 -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39 843.03/297.15 -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38 843.03/297.15 843.03/297.15 39: tail^#(ok(X)) -> c_39(tail^#(X)) 843.03/297.15 -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39 843.03/297.15 -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38 843.03/297.15 843.03/297.15 40: repItems^#(mark(X)) -> c_40(repItems^#(X)) 843.03/297.15 -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41 843.03/297.15 -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40 843.03/297.15 843.03/297.15 41: repItems^#(ok(X)) -> c_41(repItems^#(X)) 843.03/297.15 -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41 843.03/297.15 -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40 843.03/297.15 843.03/297.15 42: proper^#(pairNs()) -> c_42() 843.03/297.15 843.03/297.15 43: proper^#(cons(X1, X2)) -> c_43(cons^#(proper(X1), proper(X2))) 843.03/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) :24 843.03/297.15 -->_1 cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) :23 843.03/297.15 843.03/297.15 44: proper^#(0()) -> c_44() 843.03/297.15 843.03/297.15 45: proper^#(incr(X)) -> c_45(incr^#(proper(X))) 843.03/297.15 -->_1 incr^#(ok(X)) -> c_26(incr^#(X)) :26 843.03/297.15 -->_1 incr^#(mark(X)) -> c_25(incr^#(X)) :25 843.03/297.15 843.03/297.15 46: proper^#(oddNs()) -> c_46() 843.03/297.15 843.03/297.15 47: proper^#(s(X)) -> c_47(s^#(proper(X))) 843.03/297.15 -->_1 s^#(ok(X)) -> c_28(s^#(X)) :28 843.03/297.15 -->_1 s^#(mark(X)) -> c_27(s^#(X)) :27 843.03/297.15 843.03/297.15 48: proper^#(take(X1, X2)) -> c_48(take^#(proper(X1), proper(X2))) 843.03/297.15 -->_1 take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) :31 843.03/297.15 -->_1 take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) :30 843.03/297.15 -->_1 take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) :29 843.03/297.15 843.03/297.15 49: proper^#(nil()) -> c_49() 843.03/297.15 843.03/297.15 50: proper^#(zip(X1, X2)) -> c_50(zip^#(proper(X1), proper(X2))) 843.03/297.15 -->_1 zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) :34 843.03/297.15 -->_1 zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) :33 843.03/297.15 -->_1 zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) :32 843.03/297.15 843.03/297.15 51: proper^#(pair(X1, X2)) -> c_51(pair^#(proper(X1), proper(X2))) 843.03/297.15 -->_1 pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) :37 843.03/297.15 -->_1 pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) :36 843.03/297.15 -->_1 pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) :35 843.03/297.15 843.03/297.15 52: proper^#(tail(X)) -> c_52(tail^#(proper(X))) 843.03/297.15 -->_1 tail^#(ok(X)) -> c_39(tail^#(X)) :39 843.03/297.15 -->_1 tail^#(mark(X)) -> c_38(tail^#(X)) :38 843.03/297.15 843.03/297.15 53: proper^#(repItems(X)) -> c_53(repItems^#(proper(X))) 843.03/297.15 -->_1 repItems^#(ok(X)) -> c_41(repItems^#(X)) :41 843.03/297.15 -->_1 repItems^#(mark(X)) -> c_40(repItems^#(X)) :40 843.03/297.15 843.03/297.15 54: top^#(mark(X)) -> c_54(top^#(proper(X))) 843.03/297.15 -->_1 top^#(ok(X)) -> c_55(top^#(active(X))) :55 843.03/297.15 -->_1 top^#(mark(X)) -> c_54(top^#(proper(X))) :54 843.03/297.15 843.03/297.15 55: top^#(ok(X)) -> c_55(top^#(active(X))) 843.03/297.15 -->_1 top^#(ok(X)) -> c_55(top^#(active(X))) :55 843.03/297.15 -->_1 top^#(mark(X)) -> c_54(top^#(proper(X))) :54 843.03/297.15 843.03/297.15 843.03/297.15 Only the nodes 843.03/297.15 {1,5,23,24,25,26,27,28,29,31,30,32,34,33,35,37,36,38,39,40,41,42,44,46,49,54,55} 843.03/297.15 are reachable from nodes 843.03/297.15 {1,5,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,44,46,49,54,55} 843.03/297.15 that start derivation from marked basic terms. The nodes not 843.03/297.15 reachable are removed from the problem. 843.03/297.15 843.03/297.15 We are left with following problem, upon which TcT provides the 843.03/297.15 certificate MAYBE. 843.03/297.15 843.03/297.15 Strict DPs: 843.03/297.15 { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) 843.03/297.15 , active^#(oddNs()) -> c_5(incr^#(pairNs())) 843.03/297.15 , cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) 843.03/297.15 , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) 843.03/297.15 , incr^#(mark(X)) -> c_25(incr^#(X)) 843.03/297.15 , incr^#(ok(X)) -> c_26(incr^#(X)) 843.03/297.15 , s^#(mark(X)) -> c_27(s^#(X)) 843.03/297.15 , s^#(ok(X)) -> c_28(s^#(X)) 843.03/297.15 , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) 843.03/297.15 , take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) 843.03/297.15 , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) 843.03/297.15 , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) 843.03/297.15 , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) 843.03/297.15 , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) 843.03/297.15 , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) 843.03/297.15 , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) 843.03/297.15 , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) 843.03/297.15 , tail^#(mark(X)) -> c_38(tail^#(X)) 843.03/297.15 , tail^#(ok(X)) -> c_39(tail^#(X)) 843.03/297.15 , repItems^#(mark(X)) -> c_40(repItems^#(X)) 843.03/297.15 , repItems^#(ok(X)) -> c_41(repItems^#(X)) 843.03/297.15 , proper^#(pairNs()) -> c_42() 843.03/297.15 , proper^#(0()) -> c_44() 843.03/297.15 , proper^#(oddNs()) -> c_46() 843.03/297.15 , proper^#(nil()) -> c_49() 843.03/297.15 , top^#(mark(X)) -> c_54(top^#(proper(X))) 843.03/297.15 , top^#(ok(X)) -> c_55(top^#(active(X))) } 843.03/297.15 Strict Trs: 843.03/297.15 { active(pairNs()) -> mark(cons(0(), incr(oddNs()))) 843.03/297.15 , active(cons(X1, X2)) -> cons(active(X1), X2) 843.03/297.15 , active(incr(X)) -> incr(active(X)) 843.03/297.15 , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))) 843.03/297.15 , active(oddNs()) -> mark(incr(pairNs())) 843.03/297.15 , active(s(X)) -> s(active(X)) 843.03/297.15 , active(take(X1, X2)) -> take(X1, active(X2)) 843.03/297.15 , active(take(X1, X2)) -> take(active(X1), X2) 843.03/297.15 , active(take(0(), XS)) -> mark(nil()) 843.03/297.15 , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))) 843.03/297.15 , active(zip(X1, X2)) -> zip(X1, active(X2)) 843.03/297.15 , active(zip(X1, X2)) -> zip(active(X1), X2) 843.03/297.15 , active(zip(X, nil())) -> mark(nil()) 843.03/297.15 , active(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.15 mark(cons(pair(X, Y), zip(XS, YS))) 843.03/297.15 , active(zip(nil(), XS)) -> mark(nil()) 843.03/297.15 , active(pair(X1, X2)) -> pair(X1, active(X2)) 843.03/297.15 , active(pair(X1, X2)) -> pair(active(X1), X2) 843.03/297.15 , active(tail(X)) -> tail(active(X)) 843.03/297.15 , active(tail(cons(X, XS))) -> mark(XS) 843.03/297.15 , active(repItems(X)) -> repItems(active(X)) 843.03/297.15 , active(repItems(cons(X, XS))) -> 843.03/297.15 mark(cons(X, cons(X, repItems(XS)))) 843.03/297.15 , active(repItems(nil())) -> mark(nil()) 843.03/297.15 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 843.03/297.15 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 843.03/297.15 , incr(mark(X)) -> mark(incr(X)) 843.03/297.15 , incr(ok(X)) -> ok(incr(X)) 843.03/297.15 , s(mark(X)) -> mark(s(X)) 843.03/297.15 , s(ok(X)) -> ok(s(X)) 843.03/297.15 , take(X1, mark(X2)) -> mark(take(X1, X2)) 843.03/297.15 , take(mark(X1), X2) -> mark(take(X1, X2)) 843.03/297.15 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 843.03/297.15 , zip(X1, mark(X2)) -> mark(zip(X1, X2)) 843.03/297.15 , zip(mark(X1), X2) -> mark(zip(X1, X2)) 843.03/297.15 , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2)) 843.03/297.15 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 843.03/297.15 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 843.03/297.15 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 843.03/297.15 , tail(mark(X)) -> mark(tail(X)) 843.03/297.15 , tail(ok(X)) -> ok(tail(X)) 843.03/297.15 , repItems(mark(X)) -> mark(repItems(X)) 843.03/297.15 , repItems(ok(X)) -> ok(repItems(X)) 843.03/297.15 , proper(pairNs()) -> ok(pairNs()) 843.03/297.15 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 843.03/297.15 , proper(0()) -> ok(0()) 843.03/297.15 , proper(incr(X)) -> incr(proper(X)) 843.03/297.15 , proper(oddNs()) -> ok(oddNs()) 843.03/297.15 , proper(s(X)) -> s(proper(X)) 843.03/297.15 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 843.03/297.15 , proper(nil()) -> ok(nil()) 843.03/297.15 , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2)) 843.03/297.15 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 843.03/297.15 , proper(tail(X)) -> tail(proper(X)) 843.03/297.15 , proper(repItems(X)) -> repItems(proper(X)) 843.03/297.15 , top(mark(X)) -> top(proper(X)) 843.03/297.15 , top(ok(X)) -> top(active(X)) } 843.03/297.15 Obligation: 843.03/297.15 runtime complexity 843.03/297.15 Answer: 843.03/297.15 MAYBE 843.03/297.15 843.03/297.15 We estimate the number of application of {1,2,22,23,24,25} by 843.03/297.15 applications of Pre({1,2,22,23,24,25}) = {}. Here rules are labeled 843.03/297.15 as follows: 843.03/297.15 843.03/297.15 DPs: 843.03/297.15 { 1: active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) 843.03/297.15 , 2: active^#(oddNs()) -> c_5(incr^#(pairNs())) 843.03/297.15 , 3: cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) 843.03/297.15 , 4: cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) 843.03/297.15 , 5: incr^#(mark(X)) -> c_25(incr^#(X)) 843.03/297.15 , 6: incr^#(ok(X)) -> c_26(incr^#(X)) 843.03/297.15 , 7: s^#(mark(X)) -> c_27(s^#(X)) 843.03/297.15 , 8: s^#(ok(X)) -> c_28(s^#(X)) 843.03/297.15 , 9: take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) 843.03/297.15 , 10: take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) 843.03/297.15 , 11: take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) 843.03/297.15 , 12: zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) 843.03/297.15 , 13: zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) 843.03/297.15 , 14: zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) 843.03/297.15 , 15: pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) 843.03/297.15 , 16: pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) 843.03/297.15 , 17: pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) 843.03/297.15 , 18: tail^#(mark(X)) -> c_38(tail^#(X)) 843.03/297.15 , 19: tail^#(ok(X)) -> c_39(tail^#(X)) 843.03/297.15 , 20: repItems^#(mark(X)) -> c_40(repItems^#(X)) 843.03/297.15 , 21: repItems^#(ok(X)) -> c_41(repItems^#(X)) 843.03/297.15 , 22: proper^#(pairNs()) -> c_42() 843.03/297.15 , 23: proper^#(0()) -> c_44() 843.03/297.15 , 24: proper^#(oddNs()) -> c_46() 843.03/297.16 , 25: proper^#(nil()) -> c_49() 843.03/297.16 , 26: top^#(mark(X)) -> c_54(top^#(proper(X))) 843.03/297.16 , 27: top^#(ok(X)) -> c_55(top^#(active(X))) } 843.03/297.16 843.03/297.16 We are left with following problem, upon which TcT provides the 843.03/297.16 certificate MAYBE. 843.03/297.16 843.03/297.16 Strict DPs: 843.03/297.16 { cons^#(mark(X1), X2) -> c_23(cons^#(X1, X2)) 843.03/297.16 , cons^#(ok(X1), ok(X2)) -> c_24(cons^#(X1, X2)) 843.03/297.16 , incr^#(mark(X)) -> c_25(incr^#(X)) 843.03/297.16 , incr^#(ok(X)) -> c_26(incr^#(X)) 843.03/297.16 , s^#(mark(X)) -> c_27(s^#(X)) 843.03/297.16 , s^#(ok(X)) -> c_28(s^#(X)) 843.03/297.16 , take^#(X1, mark(X2)) -> c_29(take^#(X1, X2)) 843.03/297.16 , take^#(mark(X1), X2) -> c_30(take^#(X1, X2)) 843.03/297.16 , take^#(ok(X1), ok(X2)) -> c_31(take^#(X1, X2)) 843.03/297.16 , zip^#(X1, mark(X2)) -> c_32(zip^#(X1, X2)) 843.03/297.16 , zip^#(mark(X1), X2) -> c_33(zip^#(X1, X2)) 843.03/297.16 , zip^#(ok(X1), ok(X2)) -> c_34(zip^#(X1, X2)) 843.03/297.16 , pair^#(X1, mark(X2)) -> c_35(pair^#(X1, X2)) 843.03/297.16 , pair^#(mark(X1), X2) -> c_36(pair^#(X1, X2)) 843.03/297.16 , pair^#(ok(X1), ok(X2)) -> c_37(pair^#(X1, X2)) 843.03/297.16 , tail^#(mark(X)) -> c_38(tail^#(X)) 843.03/297.16 , tail^#(ok(X)) -> c_39(tail^#(X)) 843.03/297.16 , repItems^#(mark(X)) -> c_40(repItems^#(X)) 843.03/297.16 , repItems^#(ok(X)) -> c_41(repItems^#(X)) 843.03/297.16 , top^#(mark(X)) -> c_54(top^#(proper(X))) 843.03/297.16 , top^#(ok(X)) -> c_55(top^#(active(X))) } 843.03/297.16 Strict Trs: 843.03/297.16 { active(pairNs()) -> mark(cons(0(), incr(oddNs()))) 843.03/297.16 , active(cons(X1, X2)) -> cons(active(X1), X2) 843.03/297.16 , active(incr(X)) -> incr(active(X)) 843.03/297.16 , active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))) 843.03/297.16 , active(oddNs()) -> mark(incr(pairNs())) 843.03/297.16 , active(s(X)) -> s(active(X)) 843.03/297.16 , active(take(X1, X2)) -> take(X1, active(X2)) 843.03/297.16 , active(take(X1, X2)) -> take(active(X1), X2) 843.03/297.16 , active(take(0(), XS)) -> mark(nil()) 843.03/297.16 , active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))) 843.03/297.16 , active(zip(X1, X2)) -> zip(X1, active(X2)) 843.03/297.16 , active(zip(X1, X2)) -> zip(active(X1), X2) 843.03/297.16 , active(zip(X, nil())) -> mark(nil()) 843.03/297.16 , active(zip(cons(X, XS), cons(Y, YS))) -> 843.03/297.16 mark(cons(pair(X, Y), zip(XS, YS))) 843.03/297.16 , active(zip(nil(), XS)) -> mark(nil()) 843.03/297.16 , active(pair(X1, X2)) -> pair(X1, active(X2)) 843.03/297.16 , active(pair(X1, X2)) -> pair(active(X1), X2) 843.03/297.16 , active(tail(X)) -> tail(active(X)) 843.03/297.16 , active(tail(cons(X, XS))) -> mark(XS) 843.03/297.16 , active(repItems(X)) -> repItems(active(X)) 843.03/297.16 , active(repItems(cons(X, XS))) -> 843.03/297.16 mark(cons(X, cons(X, repItems(XS)))) 843.03/297.16 , active(repItems(nil())) -> mark(nil()) 843.03/297.16 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 843.03/297.16 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 843.03/297.16 , incr(mark(X)) -> mark(incr(X)) 843.03/297.16 , incr(ok(X)) -> ok(incr(X)) 843.03/297.16 , s(mark(X)) -> mark(s(X)) 843.03/297.16 , s(ok(X)) -> ok(s(X)) 843.03/297.16 , take(X1, mark(X2)) -> mark(take(X1, X2)) 843.03/297.16 , take(mark(X1), X2) -> mark(take(X1, X2)) 843.03/297.16 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 843.03/297.16 , zip(X1, mark(X2)) -> mark(zip(X1, X2)) 843.03/297.16 , zip(mark(X1), X2) -> mark(zip(X1, X2)) 843.03/297.16 , zip(ok(X1), ok(X2)) -> ok(zip(X1, X2)) 843.03/297.16 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 843.03/297.16 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 843.03/297.16 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 843.03/297.16 , tail(mark(X)) -> mark(tail(X)) 843.03/297.16 , tail(ok(X)) -> ok(tail(X)) 843.03/297.16 , repItems(mark(X)) -> mark(repItems(X)) 843.03/297.16 , repItems(ok(X)) -> ok(repItems(X)) 843.03/297.16 , proper(pairNs()) -> ok(pairNs()) 843.03/297.16 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 843.03/297.16 , proper(0()) -> ok(0()) 843.03/297.16 , proper(incr(X)) -> incr(proper(X)) 843.03/297.16 , proper(oddNs()) -> ok(oddNs()) 843.03/297.16 , proper(s(X)) -> s(proper(X)) 843.03/297.16 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 843.03/297.16 , proper(nil()) -> ok(nil()) 843.03/297.16 , proper(zip(X1, X2)) -> zip(proper(X1), proper(X2)) 843.03/297.16 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 843.03/297.16 , proper(tail(X)) -> tail(proper(X)) 843.03/297.16 , proper(repItems(X)) -> repItems(proper(X)) 843.03/297.16 , top(mark(X)) -> top(proper(X)) 843.03/297.16 , top(ok(X)) -> top(active(X)) } 843.03/297.16 Weak DPs: 843.03/297.16 { active^#(pairNs()) -> c_1(cons^#(0(), incr(oddNs()))) 843.03/297.16 , active^#(oddNs()) -> c_5(incr^#(pairNs())) 843.03/297.16 , proper^#(pairNs()) -> c_42() 843.03/297.16 , proper^#(0()) -> c_44() 843.03/297.16 , proper^#(oddNs()) -> c_46() 843.03/297.16 , proper^#(nil()) -> c_49() } 843.03/297.16 Obligation: 843.03/297.16 runtime complexity 843.03/297.16 Answer: 843.03/297.16 MAYBE 843.03/297.16 843.03/297.16 Empty strict component of the problem is NOT empty. 843.03/297.16 843.03/297.16 843.03/297.16 Arrrr.. 843.26/297.32 EOF