MAYBE 992.68/297.06 MAYBE 992.68/297.06 992.68/297.06 We are left with following problem, upon which TcT provides the 992.68/297.06 certificate MAYBE. 992.68/297.06 992.68/297.06 Strict Trs: 992.68/297.06 { active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4) 992.68/297.06 , active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X)) 992.68/297.06 , active(U12(X1, X2)) -> U12(active(X1), X2) 992.68/297.06 , active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) 992.68/297.06 , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) 992.68/297.06 , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) 992.68/297.06 , active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS)) 992.68/297.06 , active(splitAt(0(), XS)) -> mark(pair(nil(), XS)) 992.68/297.06 , active(pair(X1, X2)) -> pair(X1, active(X2)) 992.68/297.06 , active(pair(X1, X2)) -> pair(active(X1), X2) 992.68/297.06 , active(cons(X1, X2)) -> cons(active(X1), X2) 992.68/297.06 , active(afterNth(N, XS)) -> mark(snd(splitAt(N, XS))) 992.68/297.06 , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) 992.68/297.06 , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) 992.68/297.06 , active(snd(X)) -> snd(active(X)) 992.68/297.06 , active(snd(pair(X, Y))) -> mark(Y) 992.68/297.06 , active(and(X1, X2)) -> and(active(X1), X2) 992.68/297.06 , active(and(tt(), X)) -> mark(X) 992.68/297.06 , active(fst(X)) -> fst(active(X)) 992.68/297.06 , active(fst(pair(X, Y))) -> mark(X) 992.68/297.06 , active(head(X)) -> head(active(X)) 992.68/297.06 , active(head(cons(N, XS))) -> mark(N) 992.68/297.06 , active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))) 992.68/297.06 , active(natsFrom(X)) -> natsFrom(active(X)) 992.68/297.06 , active(s(X)) -> s(active(X)) 992.68/297.06 , active(sel(N, XS)) -> mark(head(afterNth(N, XS))) 992.68/297.06 , active(sel(X1, X2)) -> sel(X1, active(X2)) 992.68/297.06 , active(sel(X1, X2)) -> sel(active(X1), X2) 992.68/297.06 , active(tail(X)) -> tail(active(X)) 992.68/297.06 , active(tail(cons(N, XS))) -> mark(XS) 992.68/297.06 , active(take(N, XS)) -> mark(fst(splitAt(N, XS))) 992.68/297.06 , active(take(X1, X2)) -> take(X1, active(X2)) 992.68/297.06 , active(take(X1, X2)) -> take(active(X1), X2) 992.68/297.06 , U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4)) 992.68/297.06 , U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4)) 992.68/297.06 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 992.68/297.06 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 992.68/297.06 , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) 992.68/297.06 , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) 992.68/297.06 , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) 992.68/297.06 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 992.68/297.06 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 992.68/297.06 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 992.68/297.06 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 992.68/297.06 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 992.68/297.06 , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) 992.68/297.06 , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) 992.68/297.06 , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) 992.68/297.06 , snd(mark(X)) -> mark(snd(X)) 992.68/297.06 , snd(ok(X)) -> ok(snd(X)) 992.68/297.06 , and(mark(X1), X2) -> mark(and(X1, X2)) 992.68/297.06 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 992.68/297.06 , fst(mark(X)) -> mark(fst(X)) 992.68/297.06 , fst(ok(X)) -> ok(fst(X)) 992.68/297.06 , head(mark(X)) -> mark(head(X)) 992.68/297.06 , head(ok(X)) -> ok(head(X)) 992.68/297.06 , natsFrom(mark(X)) -> mark(natsFrom(X)) 992.68/297.06 , natsFrom(ok(X)) -> ok(natsFrom(X)) 992.68/297.06 , s(mark(X)) -> mark(s(X)) 992.68/297.06 , s(ok(X)) -> ok(s(X)) 992.68/297.06 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 992.68/297.06 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 992.68/297.06 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 992.68/297.06 , tail(mark(X)) -> mark(tail(X)) 992.68/297.06 , tail(ok(X)) -> ok(tail(X)) 992.68/297.06 , take(X1, mark(X2)) -> mark(take(X1, X2)) 992.68/297.06 , take(mark(X1), X2) -> mark(take(X1, X2)) 992.68/297.06 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 992.68/297.06 , proper(U11(X1, X2, X3, X4)) -> 992.68/297.06 U11(proper(X1), proper(X2), proper(X3), proper(X4)) 992.68/297.06 , proper(tt()) -> ok(tt()) 992.68/297.06 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 992.68/297.06 , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) 992.68/297.06 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 992.68/297.06 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 992.68/297.06 , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) 992.68/297.06 , proper(snd(X)) -> snd(proper(X)) 992.68/297.06 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 992.68/297.06 , proper(fst(X)) -> fst(proper(X)) 992.68/297.06 , proper(head(X)) -> head(proper(X)) 992.68/297.06 , proper(natsFrom(X)) -> natsFrom(proper(X)) 992.68/297.06 , proper(s(X)) -> s(proper(X)) 992.68/297.06 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 992.68/297.06 , proper(0()) -> ok(0()) 992.68/297.06 , proper(nil()) -> ok(nil()) 992.68/297.06 , proper(tail(X)) -> tail(proper(X)) 992.68/297.06 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 992.68/297.06 , top(mark(X)) -> top(proper(X)) 992.68/297.06 , top(ok(X)) -> top(active(X)) } 992.68/297.06 Obligation: 992.68/297.06 runtime complexity 992.68/297.06 Answer: 992.68/297.06 MAYBE 992.68/297.06 992.68/297.06 None of the processors succeeded. 992.68/297.06 992.68/297.06 Details of failed attempt(s): 992.68/297.06 ----------------------------- 992.68/297.06 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 992.68/297.06 following reason: 992.68/297.06 992.68/297.06 Computation stopped due to timeout after 297.0 seconds. 992.68/297.06 992.68/297.06 2) 'Best' failed due to the following reason: 992.68/297.06 992.68/297.06 None of the processors succeeded. 992.68/297.06 992.68/297.06 Details of failed attempt(s): 992.68/297.06 ----------------------------- 992.68/297.06 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 992.68/297.06 seconds)' failed due to the following reason: 992.68/297.06 992.68/297.06 Computation stopped due to timeout after 148.0 seconds. 992.68/297.06 992.68/297.06 2) 'Best' failed due to the following reason: 992.68/297.06 992.68/297.06 None of the processors succeeded. 992.68/297.06 992.68/297.06 Details of failed attempt(s): 992.68/297.06 ----------------------------- 992.68/297.06 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 992.68/297.06 following reason: 992.68/297.06 992.68/297.06 The processor is inapplicable, reason: 992.68/297.06 Processor only applicable for innermost runtime complexity analysis 992.68/297.06 992.68/297.06 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 992.68/297.06 to the following reason: 992.68/297.06 992.68/297.06 The processor is inapplicable, reason: 992.68/297.06 Processor only applicable for innermost runtime complexity analysis 992.68/297.06 992.68/297.06 992.68/297.06 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 992.68/297.06 failed due to the following reason: 992.68/297.06 992.68/297.06 None of the processors succeeded. 992.68/297.06 992.68/297.06 Details of failed attempt(s): 992.68/297.06 ----------------------------- 992.68/297.06 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 992.68/297.06 failed due to the following reason: 992.68/297.06 992.68/297.06 match-boundness of the problem could not be verified. 992.68/297.06 992.68/297.06 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 992.68/297.06 failed due to the following reason: 992.68/297.06 992.68/297.06 match-boundness of the problem could not be verified. 992.68/297.06 992.68/297.06 992.68/297.06 992.68/297.06 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 992.68/297.06 the following reason: 992.68/297.06 992.68/297.06 We add the following weak dependency pairs: 992.68/297.06 992.68/297.06 Strict DPs: 992.68/297.06 { active^#(U11(X1, X2, X3, X4)) -> 992.68/297.06 c_1(U11^#(active(X1), X2, X3, X4)) 992.68/297.06 , active^#(U11(tt(), N, X, XS)) -> c_2(U12^#(splitAt(N, XS), X)) 992.68/297.06 , active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) 992.68/297.06 , active^#(U12(pair(YS, ZS), X)) -> c_4(pair^#(cons(X, YS), ZS)) 992.68/297.06 , active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) 992.68/297.06 , active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) 992.68/297.06 , active^#(splitAt(s(N), cons(X, XS))) -> 992.68/297.06 c_7(U11^#(tt(), N, X, XS)) 992.68/297.06 , active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) 992.68/297.06 , active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) 992.68/297.06 , active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) 992.68/297.06 , active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) 992.68/297.06 , active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) 992.68/297.06 , active^#(afterNth(X1, X2)) -> c_13(afterNth^#(X1, active(X2))) 992.68/297.06 , active^#(afterNth(X1, X2)) -> c_14(afterNth^#(active(X1), X2)) 992.68/297.06 , active^#(snd(X)) -> c_15(snd^#(active(X))) 992.68/297.06 , active^#(snd(pair(X, Y))) -> c_16(Y) 992.68/297.06 , active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) 992.68/297.06 , active^#(and(tt(), X)) -> c_18(X) 992.68/297.06 , active^#(fst(X)) -> c_19(fst^#(active(X))) 992.68/297.06 , active^#(fst(pair(X, Y))) -> c_20(X) 992.68/297.06 , active^#(head(X)) -> c_21(head^#(active(X))) 992.68/297.06 , active^#(head(cons(N, XS))) -> c_22(N) 992.68/297.06 , active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) 992.68/297.06 , active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) 992.68/297.06 , active^#(s(X)) -> c_25(s^#(active(X))) 992.68/297.06 , active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) 992.68/297.06 , active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) 992.68/297.06 , active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) 992.68/297.06 , active^#(tail(X)) -> c_29(tail^#(active(X))) 992.68/297.06 , active^#(tail(cons(N, XS))) -> c_30(XS) 992.68/297.06 , active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) 992.68/297.06 , active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) 992.68/297.06 , active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) 992.68/297.06 , U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4)) 992.68/297.06 , U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.06 c_35(U11^#(X1, X2, X3, X4)) 992.68/297.06 , U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) 992.68/297.06 , U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) 992.68/297.06 , pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) 992.68/297.06 , pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) 992.68/297.06 , pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) 992.68/297.06 , splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) 992.68/297.06 , splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) 992.68/297.06 , splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) 992.68/297.06 , cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) 992.68/297.06 , cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) 992.68/297.06 , snd^#(mark(X)) -> c_49(snd^#(X)) 992.68/297.06 , snd^#(ok(X)) -> c_50(snd^#(X)) 992.68/297.06 , afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) 992.68/297.06 , afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) 992.68/297.06 , afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) 992.68/297.06 , and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) 992.68/297.06 , and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) 992.68/297.06 , fst^#(mark(X)) -> c_53(fst^#(X)) 992.68/297.06 , fst^#(ok(X)) -> c_54(fst^#(X)) 992.68/297.06 , head^#(mark(X)) -> c_55(head^#(X)) 992.68/297.06 , head^#(ok(X)) -> c_56(head^#(X)) 992.68/297.06 , natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) 992.68/297.06 , natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) 992.68/297.06 , s^#(mark(X)) -> c_59(s^#(X)) 992.68/297.06 , s^#(ok(X)) -> c_60(s^#(X)) 992.68/297.06 , sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) 992.68/297.06 , sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) 992.68/297.06 , sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) 992.68/297.06 , tail^#(mark(X)) -> c_64(tail^#(X)) 992.68/297.06 , tail^#(ok(X)) -> c_65(tail^#(X)) 992.68/297.06 , take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) 992.68/297.06 , take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) 992.68/297.06 , take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) 992.68/297.06 , proper^#(U11(X1, X2, X3, X4)) -> 992.68/297.06 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) 992.68/297.06 , proper^#(tt()) -> c_70() 992.68/297.06 , proper^#(U12(X1, X2)) -> c_71(U12^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(splitAt(X1, X2)) -> 992.68/297.06 c_72(splitAt^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(pair(X1, X2)) -> c_73(pair^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(cons(X1, X2)) -> c_74(cons^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(afterNth(X1, X2)) -> 992.68/297.06 c_75(afterNth^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(snd(X)) -> c_76(snd^#(proper(X))) 992.68/297.06 , proper^#(and(X1, X2)) -> c_77(and^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(fst(X)) -> c_78(fst^#(proper(X))) 992.68/297.06 , proper^#(head(X)) -> c_79(head^#(proper(X))) 992.68/297.06 , proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) 992.68/297.06 , proper^#(s(X)) -> c_81(s^#(proper(X))) 992.68/297.06 , proper^#(sel(X1, X2)) -> c_82(sel^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(0()) -> c_83() 992.68/297.06 , proper^#(nil()) -> c_84() 992.68/297.06 , proper^#(tail(X)) -> c_85(tail^#(proper(X))) 992.68/297.06 , proper^#(take(X1, X2)) -> c_86(take^#(proper(X1), proper(X2))) 992.68/297.06 , top^#(mark(X)) -> c_87(top^#(proper(X))) 992.68/297.06 , top^#(ok(X)) -> c_88(top^#(active(X))) } 992.68/297.06 992.68/297.06 and mark the set of starting terms. 992.68/297.06 992.68/297.06 We are left with following problem, upon which TcT provides the 992.68/297.06 certificate MAYBE. 992.68/297.06 992.68/297.06 Strict DPs: 992.68/297.06 { active^#(U11(X1, X2, X3, X4)) -> 992.68/297.06 c_1(U11^#(active(X1), X2, X3, X4)) 992.68/297.06 , active^#(U11(tt(), N, X, XS)) -> c_2(U12^#(splitAt(N, XS), X)) 992.68/297.06 , active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) 992.68/297.06 , active^#(U12(pair(YS, ZS), X)) -> c_4(pair^#(cons(X, YS), ZS)) 992.68/297.06 , active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) 992.68/297.06 , active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) 992.68/297.06 , active^#(splitAt(s(N), cons(X, XS))) -> 992.68/297.06 c_7(U11^#(tt(), N, X, XS)) 992.68/297.06 , active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) 992.68/297.06 , active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) 992.68/297.06 , active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) 992.68/297.06 , active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) 992.68/297.06 , active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) 992.68/297.06 , active^#(afterNth(X1, X2)) -> c_13(afterNth^#(X1, active(X2))) 992.68/297.06 , active^#(afterNth(X1, X2)) -> c_14(afterNth^#(active(X1), X2)) 992.68/297.06 , active^#(snd(X)) -> c_15(snd^#(active(X))) 992.68/297.06 , active^#(snd(pair(X, Y))) -> c_16(Y) 992.68/297.06 , active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) 992.68/297.06 , active^#(and(tt(), X)) -> c_18(X) 992.68/297.06 , active^#(fst(X)) -> c_19(fst^#(active(X))) 992.68/297.06 , active^#(fst(pair(X, Y))) -> c_20(X) 992.68/297.06 , active^#(head(X)) -> c_21(head^#(active(X))) 992.68/297.06 , active^#(head(cons(N, XS))) -> c_22(N) 992.68/297.06 , active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) 992.68/297.06 , active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) 992.68/297.06 , active^#(s(X)) -> c_25(s^#(active(X))) 992.68/297.06 , active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) 992.68/297.06 , active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) 992.68/297.06 , active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) 992.68/297.06 , active^#(tail(X)) -> c_29(tail^#(active(X))) 992.68/297.06 , active^#(tail(cons(N, XS))) -> c_30(XS) 992.68/297.06 , active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) 992.68/297.06 , active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) 992.68/297.06 , active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) 992.68/297.06 , U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4)) 992.68/297.06 , U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.06 c_35(U11^#(X1, X2, X3, X4)) 992.68/297.06 , U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) 992.68/297.06 , U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) 992.68/297.06 , pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) 992.68/297.06 , pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) 992.68/297.06 , pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) 992.68/297.06 , splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) 992.68/297.06 , splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) 992.68/297.06 , splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) 992.68/297.06 , cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) 992.68/297.06 , cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) 992.68/297.06 , snd^#(mark(X)) -> c_49(snd^#(X)) 992.68/297.06 , snd^#(ok(X)) -> c_50(snd^#(X)) 992.68/297.06 , afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) 992.68/297.06 , afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) 992.68/297.06 , afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) 992.68/297.06 , and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) 992.68/297.06 , and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) 992.68/297.06 , fst^#(mark(X)) -> c_53(fst^#(X)) 992.68/297.06 , fst^#(ok(X)) -> c_54(fst^#(X)) 992.68/297.06 , head^#(mark(X)) -> c_55(head^#(X)) 992.68/297.06 , head^#(ok(X)) -> c_56(head^#(X)) 992.68/297.06 , natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) 992.68/297.06 , natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) 992.68/297.06 , s^#(mark(X)) -> c_59(s^#(X)) 992.68/297.06 , s^#(ok(X)) -> c_60(s^#(X)) 992.68/297.06 , sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) 992.68/297.06 , sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) 992.68/297.06 , sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) 992.68/297.06 , tail^#(mark(X)) -> c_64(tail^#(X)) 992.68/297.06 , tail^#(ok(X)) -> c_65(tail^#(X)) 992.68/297.06 , take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) 992.68/297.06 , take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) 992.68/297.06 , take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) 992.68/297.06 , proper^#(U11(X1, X2, X3, X4)) -> 992.68/297.06 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) 992.68/297.06 , proper^#(tt()) -> c_70() 992.68/297.06 , proper^#(U12(X1, X2)) -> c_71(U12^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(splitAt(X1, X2)) -> 992.68/297.06 c_72(splitAt^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(pair(X1, X2)) -> c_73(pair^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(cons(X1, X2)) -> c_74(cons^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(afterNth(X1, X2)) -> 992.68/297.06 c_75(afterNth^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(snd(X)) -> c_76(snd^#(proper(X))) 992.68/297.06 , proper^#(and(X1, X2)) -> c_77(and^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(fst(X)) -> c_78(fst^#(proper(X))) 992.68/297.06 , proper^#(head(X)) -> c_79(head^#(proper(X))) 992.68/297.06 , proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) 992.68/297.06 , proper^#(s(X)) -> c_81(s^#(proper(X))) 992.68/297.06 , proper^#(sel(X1, X2)) -> c_82(sel^#(proper(X1), proper(X2))) 992.68/297.06 , proper^#(0()) -> c_83() 992.68/297.06 , proper^#(nil()) -> c_84() 992.68/297.06 , proper^#(tail(X)) -> c_85(tail^#(proper(X))) 992.68/297.06 , proper^#(take(X1, X2)) -> c_86(take^#(proper(X1), proper(X2))) 992.68/297.06 , top^#(mark(X)) -> c_87(top^#(proper(X))) 992.68/297.07 , top^#(ok(X)) -> c_88(top^#(active(X))) } 992.68/297.07 Strict Trs: 992.68/297.07 { active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4) 992.68/297.07 , active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X)) 992.68/297.07 , active(U12(X1, X2)) -> U12(active(X1), X2) 992.68/297.07 , active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) 992.68/297.07 , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) 992.68/297.07 , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) 992.68/297.07 , active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS)) 992.68/297.07 , active(splitAt(0(), XS)) -> mark(pair(nil(), XS)) 992.68/297.07 , active(pair(X1, X2)) -> pair(X1, active(X2)) 992.68/297.07 , active(pair(X1, X2)) -> pair(active(X1), X2) 992.68/297.07 , active(cons(X1, X2)) -> cons(active(X1), X2) 992.68/297.07 , active(afterNth(N, XS)) -> mark(snd(splitAt(N, XS))) 992.68/297.07 , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) 992.68/297.07 , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) 992.68/297.07 , active(snd(X)) -> snd(active(X)) 992.68/297.07 , active(snd(pair(X, Y))) -> mark(Y) 992.68/297.07 , active(and(X1, X2)) -> and(active(X1), X2) 992.68/297.07 , active(and(tt(), X)) -> mark(X) 992.68/297.07 , active(fst(X)) -> fst(active(X)) 992.68/297.07 , active(fst(pair(X, Y))) -> mark(X) 992.68/297.07 , active(head(X)) -> head(active(X)) 992.68/297.07 , active(head(cons(N, XS))) -> mark(N) 992.68/297.07 , active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))) 992.68/297.07 , active(natsFrom(X)) -> natsFrom(active(X)) 992.68/297.07 , active(s(X)) -> s(active(X)) 992.68/297.07 , active(sel(N, XS)) -> mark(head(afterNth(N, XS))) 992.68/297.07 , active(sel(X1, X2)) -> sel(X1, active(X2)) 992.68/297.07 , active(sel(X1, X2)) -> sel(active(X1), X2) 992.68/297.07 , active(tail(X)) -> tail(active(X)) 992.68/297.07 , active(tail(cons(N, XS))) -> mark(XS) 992.68/297.07 , active(take(N, XS)) -> mark(fst(splitAt(N, XS))) 992.68/297.07 , active(take(X1, X2)) -> take(X1, active(X2)) 992.68/297.07 , active(take(X1, X2)) -> take(active(X1), X2) 992.68/297.07 , U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4)) 992.68/297.07 , U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4)) 992.68/297.07 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 992.68/297.07 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 992.68/297.07 , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) 992.68/297.07 , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) 992.68/297.07 , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) 992.68/297.07 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 992.68/297.07 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 992.68/297.07 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 992.68/297.07 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 992.68/297.07 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 992.68/297.07 , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) 992.68/297.07 , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) 992.68/297.07 , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) 992.68/297.07 , snd(mark(X)) -> mark(snd(X)) 992.68/297.07 , snd(ok(X)) -> ok(snd(X)) 992.68/297.07 , and(mark(X1), X2) -> mark(and(X1, X2)) 992.68/297.07 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 992.68/297.07 , fst(mark(X)) -> mark(fst(X)) 992.68/297.07 , fst(ok(X)) -> ok(fst(X)) 992.68/297.07 , head(mark(X)) -> mark(head(X)) 992.68/297.07 , head(ok(X)) -> ok(head(X)) 992.68/297.07 , natsFrom(mark(X)) -> mark(natsFrom(X)) 992.68/297.07 , natsFrom(ok(X)) -> ok(natsFrom(X)) 992.68/297.07 , s(mark(X)) -> mark(s(X)) 992.68/297.07 , s(ok(X)) -> ok(s(X)) 992.68/297.07 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 992.68/297.07 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 992.68/297.07 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 992.68/297.07 , tail(mark(X)) -> mark(tail(X)) 992.68/297.07 , tail(ok(X)) -> ok(tail(X)) 992.68/297.07 , take(X1, mark(X2)) -> mark(take(X1, X2)) 992.68/297.07 , take(mark(X1), X2) -> mark(take(X1, X2)) 992.68/297.07 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 992.68/297.07 , proper(U11(X1, X2, X3, X4)) -> 992.68/297.07 U11(proper(X1), proper(X2), proper(X3), proper(X4)) 992.68/297.07 , proper(tt()) -> ok(tt()) 992.68/297.07 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 992.68/297.07 , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) 992.68/297.07 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 992.68/297.07 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 992.68/297.07 , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) 992.68/297.07 , proper(snd(X)) -> snd(proper(X)) 992.68/297.07 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 992.68/297.07 , proper(fst(X)) -> fst(proper(X)) 992.68/297.07 , proper(head(X)) -> head(proper(X)) 992.68/297.07 , proper(natsFrom(X)) -> natsFrom(proper(X)) 992.68/297.07 , proper(s(X)) -> s(proper(X)) 992.68/297.07 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 992.68/297.07 , proper(0()) -> ok(0()) 992.68/297.07 , proper(nil()) -> ok(nil()) 992.68/297.07 , proper(tail(X)) -> tail(proper(X)) 992.68/297.07 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 992.68/297.07 , top(mark(X)) -> top(proper(X)) 992.68/297.07 , top(ok(X)) -> top(active(X)) } 992.68/297.07 Obligation: 992.68/297.07 runtime complexity 992.68/297.07 Answer: 992.68/297.07 MAYBE 992.68/297.07 992.68/297.07 Consider the dependency graph: 992.68/297.07 992.68/297.07 1: active^#(U11(X1, X2, X3, X4)) -> 992.68/297.07 c_1(U11^#(active(X1), X2, X3, X4)) 992.68/297.07 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.07 c_35(U11^#(X1, X2, X3, X4)) :35 992.68/297.07 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.68/297.07 c_34(U11^#(X1, X2, X3, X4)) :34 992.68/297.07 992.68/297.07 2: active^#(U11(tt(), N, X, XS)) -> c_2(U12^#(splitAt(N, XS), X)) 992.68/297.07 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.68/297.07 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.68/297.07 992.68/297.07 3: active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) 992.68/297.07 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.68/297.07 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.68/297.07 992.68/297.07 4: active^#(U12(pair(YS, ZS), X)) -> c_4(pair^#(cons(X, YS), ZS)) 992.68/297.07 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.07 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.07 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.07 992.68/297.07 5: active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) 992.68/297.07 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.68/297.07 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.68/297.07 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.68/297.07 992.68/297.07 6: active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) 992.68/297.07 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.68/297.07 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.68/297.07 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.68/297.07 992.68/297.07 7: active^#(splitAt(s(N), cons(X, XS))) -> 992.68/297.07 c_7(U11^#(tt(), N, X, XS)) 992.68/297.07 992.68/297.07 8: active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) 992.68/297.07 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.07 992.68/297.07 9: active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) 992.68/297.07 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.07 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.07 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.07 992.68/297.07 10: active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) 992.68/297.07 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.07 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.07 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.07 992.68/297.07 11: active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) 992.68/297.07 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.68/297.07 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.68/297.07 992.68/297.07 12: active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) 992.68/297.07 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.68/297.07 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.68/297.07 992.68/297.07 13: active^#(afterNth(X1, X2)) -> c_13(afterNth^#(X1, active(X2))) 992.68/297.07 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.68/297.07 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.68/297.07 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.68/297.07 992.68/297.07 14: active^#(afterNth(X1, X2)) -> c_14(afterNth^#(active(X1), X2)) 992.68/297.07 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.68/297.07 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.68/297.07 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.68/297.07 992.68/297.07 15: active^#(snd(X)) -> c_15(snd^#(active(X))) 992.68/297.07 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.68/297.07 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.68/297.07 992.68/297.07 16: active^#(snd(pair(X, Y))) -> c_16(Y) 992.68/297.07 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.68/297.07 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.68/297.07 -->_1 proper^#(take(X1, X2)) -> 992.68/297.07 c_86(take^#(proper(X1), proper(X2))) :86 992.68/297.08 -->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85 992.68/297.08 -->_1 proper^#(sel(X1, X2)) -> 992.68/297.08 c_82(sel^#(proper(X1), proper(X2))) :82 992.68/297.08 -->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81 992.68/297.08 -->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80 992.68/297.08 -->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79 992.68/297.08 -->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78 992.68/297.08 -->_1 proper^#(and(X1, X2)) -> 992.68/297.08 c_77(and^#(proper(X1), proper(X2))) :77 992.68/297.08 -->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76 992.68/297.08 -->_1 proper^#(afterNth(X1, X2)) -> 992.68/297.08 c_75(afterNth^#(proper(X1), proper(X2))) :75 992.68/297.08 -->_1 proper^#(cons(X1, X2)) -> 992.68/297.08 c_74(cons^#(proper(X1), proper(X2))) :74 992.68/297.08 -->_1 proper^#(pair(X1, X2)) -> 992.68/297.08 c_73(pair^#(proper(X1), proper(X2))) :73 992.68/297.08 -->_1 proper^#(splitAt(X1, X2)) -> 992.68/297.08 c_72(splitAt^#(proper(X1), proper(X2))) :72 992.68/297.08 -->_1 proper^#(U12(X1, X2)) -> 992.68/297.08 c_71(U12^#(proper(X1), proper(X2))) :71 992.68/297.08 -->_1 proper^#(U11(X1, X2, X3, X4)) -> 992.68/297.08 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69 992.68/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.68/297.08 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.68/297.08 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.68/297.08 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.68/297.08 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.68/297.08 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.68/297.08 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.68/297.08 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.68/297.08 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.68/297.08 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.68/297.08 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.68/297.08 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.68/297.08 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.68/297.08 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.68/297.08 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.68/297.08 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.68/297.08 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.68/297.08 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.68/297.08 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.68/297.08 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.68/297.08 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.68/297.08 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.68/297.08 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.68/297.08 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.68/297.08 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.68/297.08 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.68/297.08 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.68/297.08 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.68/297.08 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.08 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.08 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.08 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.68/297.08 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.68/297.08 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.08 c_35(U11^#(X1, X2, X3, X4)) :35 992.68/297.08 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.68/297.08 c_34(U11^#(X1, X2, X3, X4)) :34 992.68/297.08 -->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33 992.68/297.08 -->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32 992.68/297.08 -->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31 992.68/297.08 -->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30 992.68/297.08 -->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29 992.68/297.08 -->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28 992.68/297.08 -->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27 992.68/297.08 -->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26 992.68/297.08 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 992.68/297.08 -->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24 992.68/297.08 -->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23 992.68/297.08 -->_1 active^#(head(cons(N, XS))) -> c_22(N) :22 992.68/297.08 -->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21 992.68/297.08 -->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20 992.68/297.08 -->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19 992.68/297.08 -->_1 active^#(and(tt(), X)) -> c_18(X) :18 992.68/297.08 -->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17 992.68/297.08 -->_1 proper^#(nil()) -> c_84() :84 992.68/297.08 -->_1 proper^#(0()) -> c_83() :83 992.68/297.08 -->_1 proper^#(tt()) -> c_70() :70 992.68/297.08 -->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16 992.68/297.08 -->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15 992.68/297.08 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.08 c_14(afterNth^#(active(X1), X2)) :14 992.68/297.08 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.08 c_13(afterNth^#(X1, active(X2))) :13 992.68/297.08 -->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12 992.68/297.08 -->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11 992.68/297.08 -->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10 992.68/297.08 -->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9 992.68/297.08 -->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8 992.68/297.08 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> 992.68/297.08 c_7(U11^#(tt(), N, X, XS)) :7 992.68/297.08 -->_1 active^#(splitAt(X1, X2)) -> 992.68/297.08 c_6(splitAt^#(active(X1), X2)) :6 992.68/297.08 -->_1 active^#(splitAt(X1, X2)) -> 992.68/297.08 c_5(splitAt^#(X1, active(X2))) :5 992.68/297.08 -->_1 active^#(U12(pair(YS, ZS), X)) -> 992.68/297.08 c_4(pair^#(cons(X, YS), ZS)) :4 992.68/297.08 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 992.68/297.08 -->_1 active^#(U11(tt(), N, X, XS)) -> 992.68/297.08 c_2(U12^#(splitAt(N, XS), X)) :2 992.68/297.08 -->_1 active^#(U11(X1, X2, X3, X4)) -> 992.68/297.08 c_1(U11^#(active(X1), X2, X3, X4)) :1 992.68/297.08 992.68/297.08 17: active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) 992.68/297.08 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.68/297.08 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.68/297.08 992.68/297.08 18: active^#(and(tt(), X)) -> c_18(X) 992.68/297.08 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.68/297.08 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.68/297.08 -->_1 proper^#(take(X1, X2)) -> 992.68/297.08 c_86(take^#(proper(X1), proper(X2))) :86 992.68/297.08 -->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85 992.68/297.08 -->_1 proper^#(sel(X1, X2)) -> 992.68/297.08 c_82(sel^#(proper(X1), proper(X2))) :82 992.68/297.08 -->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81 992.68/297.08 -->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80 992.68/297.08 -->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79 992.68/297.08 -->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78 992.68/297.08 -->_1 proper^#(and(X1, X2)) -> 992.68/297.08 c_77(and^#(proper(X1), proper(X2))) :77 992.68/297.08 -->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76 992.68/297.08 -->_1 proper^#(afterNth(X1, X2)) -> 992.68/297.08 c_75(afterNth^#(proper(X1), proper(X2))) :75 992.68/297.08 -->_1 proper^#(cons(X1, X2)) -> 992.68/297.08 c_74(cons^#(proper(X1), proper(X2))) :74 992.68/297.08 -->_1 proper^#(pair(X1, X2)) -> 992.68/297.08 c_73(pair^#(proper(X1), proper(X2))) :73 992.68/297.08 -->_1 proper^#(splitAt(X1, X2)) -> 992.68/297.08 c_72(splitAt^#(proper(X1), proper(X2))) :72 992.68/297.08 -->_1 proper^#(U12(X1, X2)) -> 992.68/297.08 c_71(U12^#(proper(X1), proper(X2))) :71 992.68/297.08 -->_1 proper^#(U11(X1, X2, X3, X4)) -> 992.68/297.08 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69 992.68/297.08 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.68/297.08 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.68/297.08 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.68/297.08 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.68/297.08 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.68/297.08 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.68/297.08 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.68/297.08 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.68/297.08 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.68/297.09 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.68/297.09 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.68/297.09 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.68/297.09 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.68/297.09 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.68/297.09 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.68/297.09 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.68/297.09 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.68/297.09 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.68/297.09 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.68/297.09 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.68/297.09 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.68/297.09 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.68/297.09 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.68/297.09 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.68/297.09 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.68/297.09 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.68/297.09 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.68/297.09 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.68/297.09 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.09 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.09 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.09 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.68/297.09 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.68/297.09 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.09 c_35(U11^#(X1, X2, X3, X4)) :35 992.68/297.09 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.68/297.09 c_34(U11^#(X1, X2, X3, X4)) :34 992.68/297.09 -->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33 992.68/297.09 -->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32 992.68/297.09 -->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31 992.68/297.09 -->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30 992.68/297.09 -->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29 992.68/297.09 -->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28 992.68/297.09 -->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27 992.68/297.09 -->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26 992.68/297.09 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 992.68/297.09 -->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24 992.68/297.09 -->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23 992.68/297.09 -->_1 active^#(head(cons(N, XS))) -> c_22(N) :22 992.68/297.09 -->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21 992.68/297.09 -->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20 992.68/297.09 -->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19 992.68/297.09 -->_1 proper^#(nil()) -> c_84() :84 992.68/297.09 -->_1 proper^#(0()) -> c_83() :83 992.68/297.09 -->_1 proper^#(tt()) -> c_70() :70 992.68/297.09 -->_1 active^#(and(tt(), X)) -> c_18(X) :18 992.68/297.09 -->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17 992.68/297.09 -->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16 992.68/297.09 -->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15 992.68/297.09 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.09 c_14(afterNth^#(active(X1), X2)) :14 992.68/297.09 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.09 c_13(afterNth^#(X1, active(X2))) :13 992.68/297.09 -->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12 992.68/297.09 -->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11 992.68/297.09 -->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10 992.68/297.09 -->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9 992.68/297.09 -->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8 992.68/297.09 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> 992.68/297.09 c_7(U11^#(tt(), N, X, XS)) :7 992.68/297.09 -->_1 active^#(splitAt(X1, X2)) -> 992.68/297.09 c_6(splitAt^#(active(X1), X2)) :6 992.68/297.09 -->_1 active^#(splitAt(X1, X2)) -> 992.68/297.09 c_5(splitAt^#(X1, active(X2))) :5 992.68/297.09 -->_1 active^#(U12(pair(YS, ZS), X)) -> 992.68/297.09 c_4(pair^#(cons(X, YS), ZS)) :4 992.68/297.09 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 992.68/297.09 -->_1 active^#(U11(tt(), N, X, XS)) -> 992.68/297.09 c_2(U12^#(splitAt(N, XS), X)) :2 992.68/297.09 -->_1 active^#(U11(X1, X2, X3, X4)) -> 992.68/297.09 c_1(U11^#(active(X1), X2, X3, X4)) :1 992.68/297.09 992.68/297.09 19: active^#(fst(X)) -> c_19(fst^#(active(X))) 992.68/297.09 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.68/297.09 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.68/297.09 992.68/297.09 20: active^#(fst(pair(X, Y))) -> c_20(X) 992.68/297.09 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.68/297.09 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.68/297.09 -->_1 proper^#(take(X1, X2)) -> 992.68/297.09 c_86(take^#(proper(X1), proper(X2))) :86 992.68/297.09 -->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85 992.68/297.09 -->_1 proper^#(sel(X1, X2)) -> 992.68/297.09 c_82(sel^#(proper(X1), proper(X2))) :82 992.68/297.09 -->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81 992.68/297.09 -->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80 992.68/297.09 -->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79 992.68/297.09 -->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78 992.68/297.09 -->_1 proper^#(and(X1, X2)) -> 992.68/297.09 c_77(and^#(proper(X1), proper(X2))) :77 992.68/297.09 -->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76 992.68/297.09 -->_1 proper^#(afterNth(X1, X2)) -> 992.68/297.09 c_75(afterNth^#(proper(X1), proper(X2))) :75 992.68/297.09 -->_1 proper^#(cons(X1, X2)) -> 992.68/297.09 c_74(cons^#(proper(X1), proper(X2))) :74 992.68/297.09 -->_1 proper^#(pair(X1, X2)) -> 992.68/297.09 c_73(pair^#(proper(X1), proper(X2))) :73 992.68/297.09 -->_1 proper^#(splitAt(X1, X2)) -> 992.68/297.09 c_72(splitAt^#(proper(X1), proper(X2))) :72 992.68/297.09 -->_1 proper^#(U12(X1, X2)) -> 992.68/297.09 c_71(U12^#(proper(X1), proper(X2))) :71 992.68/297.09 -->_1 proper^#(U11(X1, X2, X3, X4)) -> 992.68/297.09 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69 992.68/297.09 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.68/297.09 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.68/297.09 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.68/297.09 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.68/297.09 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.68/297.09 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.68/297.09 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.68/297.09 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.68/297.09 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.68/297.09 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.68/297.09 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.68/297.09 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.68/297.09 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.68/297.09 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.68/297.09 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.68/297.09 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.68/297.09 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.68/297.09 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.68/297.09 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.68/297.09 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.68/297.09 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.68/297.09 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.68/297.09 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.68/297.09 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.68/297.09 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.68/297.09 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.68/297.09 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.68/297.09 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.68/297.09 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.09 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.09 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.09 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.68/297.09 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.68/297.09 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.09 c_35(U11^#(X1, X2, X3, X4)) :35 992.68/297.09 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.68/297.09 c_34(U11^#(X1, X2, X3, X4)) :34 992.68/297.09 -->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33 992.68/297.09 -->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32 992.68/297.09 -->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31 992.68/297.09 -->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30 992.68/297.09 -->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29 992.68/297.09 -->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28 992.68/297.09 -->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27 992.68/297.09 -->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26 992.68/297.09 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 992.68/297.09 -->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24 992.68/297.09 -->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23 992.68/297.09 -->_1 active^#(head(cons(N, XS))) -> c_22(N) :22 992.68/297.09 -->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21 992.68/297.09 -->_1 proper^#(nil()) -> c_84() :84 992.68/297.09 -->_1 proper^#(0()) -> c_83() :83 992.68/297.09 -->_1 proper^#(tt()) -> c_70() :70 992.68/297.09 -->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20 992.68/297.09 -->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19 992.68/297.09 -->_1 active^#(and(tt(), X)) -> c_18(X) :18 992.68/297.09 -->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17 992.68/297.09 -->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16 992.68/297.09 -->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15 992.68/297.09 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.09 c_14(afterNth^#(active(X1), X2)) :14 992.68/297.09 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.09 c_13(afterNth^#(X1, active(X2))) :13 992.68/297.09 -->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12 992.68/297.09 -->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11 992.68/297.09 -->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10 992.68/297.09 -->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9 992.68/297.09 -->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8 992.68/297.09 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> 992.68/297.09 c_7(U11^#(tt(), N, X, XS)) :7 992.68/297.09 -->_1 active^#(splitAt(X1, X2)) -> 992.68/297.09 c_6(splitAt^#(active(X1), X2)) :6 992.68/297.09 -->_1 active^#(splitAt(X1, X2)) -> 992.68/297.09 c_5(splitAt^#(X1, active(X2))) :5 992.68/297.09 -->_1 active^#(U12(pair(YS, ZS), X)) -> 992.68/297.09 c_4(pair^#(cons(X, YS), ZS)) :4 992.68/297.09 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 992.68/297.09 -->_1 active^#(U11(tt(), N, X, XS)) -> 992.68/297.09 c_2(U12^#(splitAt(N, XS), X)) :2 992.68/297.09 -->_1 active^#(U11(X1, X2, X3, X4)) -> 992.68/297.09 c_1(U11^#(active(X1), X2, X3, X4)) :1 992.68/297.09 992.68/297.09 21: active^#(head(X)) -> c_21(head^#(active(X))) 992.68/297.09 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.68/297.09 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.68/297.09 992.68/297.09 22: active^#(head(cons(N, XS))) -> c_22(N) 992.68/297.09 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.68/297.09 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.68/297.09 -->_1 proper^#(take(X1, X2)) -> 992.68/297.09 c_86(take^#(proper(X1), proper(X2))) :86 992.68/297.09 -->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85 992.68/297.09 -->_1 proper^#(sel(X1, X2)) -> 992.68/297.09 c_82(sel^#(proper(X1), proper(X2))) :82 992.68/297.09 -->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81 992.68/297.09 -->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80 992.68/297.09 -->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79 992.68/297.09 -->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78 992.68/297.09 -->_1 proper^#(and(X1, X2)) -> 992.68/297.09 c_77(and^#(proper(X1), proper(X2))) :77 992.68/297.09 -->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76 992.68/297.09 -->_1 proper^#(afterNth(X1, X2)) -> 992.68/297.09 c_75(afterNth^#(proper(X1), proper(X2))) :75 992.68/297.09 -->_1 proper^#(cons(X1, X2)) -> 992.68/297.09 c_74(cons^#(proper(X1), proper(X2))) :74 992.68/297.09 -->_1 proper^#(pair(X1, X2)) -> 992.68/297.09 c_73(pair^#(proper(X1), proper(X2))) :73 992.68/297.09 -->_1 proper^#(splitAt(X1, X2)) -> 992.68/297.09 c_72(splitAt^#(proper(X1), proper(X2))) :72 992.68/297.09 -->_1 proper^#(U12(X1, X2)) -> 992.68/297.09 c_71(U12^#(proper(X1), proper(X2))) :71 992.68/297.09 -->_1 proper^#(U11(X1, X2, X3, X4)) -> 992.68/297.09 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69 992.68/297.09 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.68/297.09 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.68/297.09 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.68/297.09 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.68/297.09 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.68/297.09 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.68/297.09 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.68/297.09 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.68/297.09 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.68/297.09 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.68/297.09 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.68/297.09 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.68/297.09 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.68/297.09 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.68/297.09 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.68/297.09 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.68/297.09 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.68/297.09 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.68/297.09 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.68/297.09 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.68/297.09 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.68/297.09 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.68/297.09 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.68/297.09 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.68/297.09 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.68/297.09 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.68/297.09 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.68/297.09 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.68/297.09 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.68/297.09 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.68/297.09 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.68/297.09 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.68/297.09 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.68/297.09 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.68/297.09 c_35(U11^#(X1, X2, X3, X4)) :35 992.68/297.09 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.68/297.10 c_34(U11^#(X1, X2, X3, X4)) :34 992.68/297.10 -->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33 992.68/297.10 -->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32 992.68/297.10 -->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31 992.68/297.10 -->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30 992.68/297.10 -->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29 992.68/297.10 -->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28 992.68/297.10 -->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27 992.68/297.10 -->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26 992.68/297.10 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 992.68/297.10 -->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24 992.68/297.10 -->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23 992.68/297.10 -->_1 proper^#(nil()) -> c_84() :84 992.68/297.10 -->_1 proper^#(0()) -> c_83() :83 992.68/297.10 -->_1 proper^#(tt()) -> c_70() :70 992.68/297.10 -->_1 active^#(head(cons(N, XS))) -> c_22(N) :22 992.68/297.10 -->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21 992.68/297.10 -->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20 992.68/297.10 -->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19 992.68/297.10 -->_1 active^#(and(tt(), X)) -> c_18(X) :18 992.68/297.10 -->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17 992.68/297.10 -->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16 992.68/297.10 -->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15 992.68/297.10 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.10 c_14(afterNth^#(active(X1), X2)) :14 992.68/297.10 -->_1 active^#(afterNth(X1, X2)) -> 992.68/297.10 c_13(afterNth^#(X1, active(X2))) :13 992.68/297.10 -->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12 992.68/297.10 -->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11 992.68/297.10 -->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10 992.68/297.10 -->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9 992.68/297.10 -->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8 992.87/297.10 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> 992.87/297.10 c_7(U11^#(tt(), N, X, XS)) :7 992.87/297.10 -->_1 active^#(splitAt(X1, X2)) -> 992.87/297.10 c_6(splitAt^#(active(X1), X2)) :6 992.87/297.10 -->_1 active^#(splitAt(X1, X2)) -> 992.87/297.10 c_5(splitAt^#(X1, active(X2))) :5 992.87/297.10 -->_1 active^#(U12(pair(YS, ZS), X)) -> 992.87/297.10 c_4(pair^#(cons(X, YS), ZS)) :4 992.87/297.10 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 992.87/297.10 -->_1 active^#(U11(tt(), N, X, XS)) -> 992.87/297.10 c_2(U12^#(splitAt(N, XS), X)) :2 992.87/297.10 -->_1 active^#(U11(X1, X2, X3, X4)) -> 992.87/297.10 c_1(U11^#(active(X1), X2, X3, X4)) :1 992.87/297.10 992.87/297.10 23: active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) 992.87/297.10 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.87/297.10 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.87/297.10 992.87/297.10 24: active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) 992.87/297.10 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.87/297.10 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.87/297.10 992.87/297.10 25: active^#(s(X)) -> c_25(s^#(active(X))) 992.87/297.10 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.87/297.10 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.87/297.10 992.87/297.10 26: active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) 992.87/297.10 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.87/297.10 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.87/297.10 992.87/297.10 27: active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) 992.87/297.10 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.10 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.10 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.10 992.87/297.10 28: active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) 992.87/297.10 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.10 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.10 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.10 992.87/297.10 29: active^#(tail(X)) -> c_29(tail^#(active(X))) 992.87/297.10 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.87/297.10 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.87/297.10 992.87/297.10 30: active^#(tail(cons(N, XS))) -> c_30(XS) 992.87/297.10 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.87/297.10 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.87/297.10 -->_1 proper^#(take(X1, X2)) -> 992.87/297.10 c_86(take^#(proper(X1), proper(X2))) :86 992.87/297.10 -->_1 proper^#(tail(X)) -> c_85(tail^#(proper(X))) :85 992.87/297.10 -->_1 proper^#(sel(X1, X2)) -> 992.87/297.10 c_82(sel^#(proper(X1), proper(X2))) :82 992.87/297.10 -->_1 proper^#(s(X)) -> c_81(s^#(proper(X))) :81 992.87/297.10 -->_1 proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) :80 992.87/297.10 -->_1 proper^#(head(X)) -> c_79(head^#(proper(X))) :79 992.87/297.10 -->_1 proper^#(fst(X)) -> c_78(fst^#(proper(X))) :78 992.87/297.10 -->_1 proper^#(and(X1, X2)) -> 992.87/297.10 c_77(and^#(proper(X1), proper(X2))) :77 992.87/297.10 -->_1 proper^#(snd(X)) -> c_76(snd^#(proper(X))) :76 992.87/297.10 -->_1 proper^#(afterNth(X1, X2)) -> 992.87/297.10 c_75(afterNth^#(proper(X1), proper(X2))) :75 992.87/297.10 -->_1 proper^#(cons(X1, X2)) -> 992.87/297.10 c_74(cons^#(proper(X1), proper(X2))) :74 992.87/297.10 -->_1 proper^#(pair(X1, X2)) -> 992.87/297.10 c_73(pair^#(proper(X1), proper(X2))) :73 992.87/297.10 -->_1 proper^#(splitAt(X1, X2)) -> 992.87/297.10 c_72(splitAt^#(proper(X1), proper(X2))) :72 992.87/297.10 -->_1 proper^#(U12(X1, X2)) -> 992.87/297.10 c_71(U12^#(proper(X1), proper(X2))) :71 992.87/297.10 -->_1 proper^#(U11(X1, X2, X3, X4)) -> 992.87/297.10 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) :69 992.87/297.10 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.10 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.10 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.10 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.87/297.10 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.87/297.10 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.10 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.10 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.10 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.87/297.10 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.87/297.10 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.87/297.10 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.87/297.10 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.87/297.10 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.87/297.10 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.87/297.10 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.87/297.10 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.87/297.10 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.87/297.10 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.87/297.10 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.87/297.10 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.87/297.10 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.87/297.10 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.87/297.10 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.87/297.10 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.87/297.10 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.87/297.10 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.87/297.10 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.87/297.10 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.87/297.10 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.87/297.10 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.87/297.10 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.87/297.10 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.87/297.10 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.10 c_35(U11^#(X1, X2, X3, X4)) :35 992.87/297.10 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.87/297.10 c_34(U11^#(X1, X2, X3, X4)) :34 992.87/297.10 -->_1 active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) :33 992.87/297.10 -->_1 active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) :32 992.87/297.10 -->_1 active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) :31 992.87/297.10 -->_1 proper^#(nil()) -> c_84() :84 992.87/297.10 -->_1 proper^#(0()) -> c_83() :83 992.87/297.10 -->_1 proper^#(tt()) -> c_70() :70 992.87/297.10 -->_1 active^#(tail(cons(N, XS))) -> c_30(XS) :30 992.87/297.10 -->_1 active^#(tail(X)) -> c_29(tail^#(active(X))) :29 992.87/297.10 -->_1 active^#(sel(X1, X2)) -> c_28(sel^#(active(X1), X2)) :28 992.87/297.10 -->_1 active^#(sel(X1, X2)) -> c_27(sel^#(X1, active(X2))) :27 992.87/297.10 -->_1 active^#(sel(N, XS)) -> c_26(head^#(afterNth(N, XS))) :26 992.87/297.10 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 992.87/297.10 -->_1 active^#(natsFrom(X)) -> c_24(natsFrom^#(active(X))) :24 992.87/297.10 -->_1 active^#(natsFrom(N)) -> c_23(cons^#(N, natsFrom(s(N)))) :23 992.87/297.10 -->_1 active^#(head(cons(N, XS))) -> c_22(N) :22 992.87/297.10 -->_1 active^#(head(X)) -> c_21(head^#(active(X))) :21 992.87/297.10 -->_1 active^#(fst(pair(X, Y))) -> c_20(X) :20 992.87/297.10 -->_1 active^#(fst(X)) -> c_19(fst^#(active(X))) :19 992.87/297.10 -->_1 active^#(and(tt(), X)) -> c_18(X) :18 992.87/297.10 -->_1 active^#(and(X1, X2)) -> c_17(and^#(active(X1), X2)) :17 992.87/297.10 -->_1 active^#(snd(pair(X, Y))) -> c_16(Y) :16 992.87/297.10 -->_1 active^#(snd(X)) -> c_15(snd^#(active(X))) :15 992.87/297.10 -->_1 active^#(afterNth(X1, X2)) -> 992.87/297.10 c_14(afterNth^#(active(X1), X2)) :14 992.87/297.10 -->_1 active^#(afterNth(X1, X2)) -> 992.87/297.10 c_13(afterNth^#(X1, active(X2))) :13 992.87/297.10 -->_1 active^#(afterNth(N, XS)) -> c_12(snd^#(splitAt(N, XS))) :12 992.87/297.10 -->_1 active^#(cons(X1, X2)) -> c_11(cons^#(active(X1), X2)) :11 992.87/297.10 -->_1 active^#(pair(X1, X2)) -> c_10(pair^#(active(X1), X2)) :10 992.87/297.10 -->_1 active^#(pair(X1, X2)) -> c_9(pair^#(X1, active(X2))) :9 992.87/297.10 -->_1 active^#(splitAt(0(), XS)) -> c_8(pair^#(nil(), XS)) :8 992.87/297.10 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> 992.87/297.10 c_7(U11^#(tt(), N, X, XS)) :7 992.87/297.10 -->_1 active^#(splitAt(X1, X2)) -> 992.87/297.10 c_6(splitAt^#(active(X1), X2)) :6 992.87/297.10 -->_1 active^#(splitAt(X1, X2)) -> 992.87/297.10 c_5(splitAt^#(X1, active(X2))) :5 992.87/297.10 -->_1 active^#(U12(pair(YS, ZS), X)) -> 992.87/297.10 c_4(pair^#(cons(X, YS), ZS)) :4 992.87/297.10 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 992.87/297.10 -->_1 active^#(U11(tt(), N, X, XS)) -> 992.87/297.10 c_2(U12^#(splitAt(N, XS), X)) :2 992.87/297.11 -->_1 active^#(U11(X1, X2, X3, X4)) -> 992.87/297.11 c_1(U11^#(active(X1), X2, X3, X4)) :1 992.87/297.11 992.87/297.11 31: active^#(take(N, XS)) -> c_31(fst^#(splitAt(N, XS))) 992.87/297.11 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.87/297.11 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.87/297.11 992.87/297.11 32: active^#(take(X1, X2)) -> c_32(take^#(X1, active(X2))) 992.87/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.11 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.11 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.11 992.87/297.11 33: active^#(take(X1, X2)) -> c_33(take^#(active(X1), X2)) 992.87/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.11 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.11 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.11 992.87/297.11 34: U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4)) 992.87/297.11 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.11 c_35(U11^#(X1, X2, X3, X4)) :35 992.87/297.11 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.87/297.11 c_34(U11^#(X1, X2, X3, X4)) :34 992.87/297.11 992.87/297.11 35: U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.11 c_35(U11^#(X1, X2, X3, X4)) 992.87/297.11 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.11 c_35(U11^#(X1, X2, X3, X4)) :35 992.87/297.11 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.87/297.11 c_34(U11^#(X1, X2, X3, X4)) :34 992.87/297.11 992.87/297.11 36: U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) 992.87/297.11 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.87/297.11 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.87/297.11 992.87/297.11 37: U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) 992.87/297.11 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.87/297.11 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.87/297.11 992.87/297.11 38: pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) 992.87/297.11 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.87/297.11 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.87/297.11 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.87/297.11 992.87/297.11 39: pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) 992.87/297.11 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.87/297.11 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.87/297.11 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.87/297.11 992.87/297.11 40: pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) 992.87/297.11 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.87/297.11 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.87/297.11 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.87/297.11 992.87/297.11 41: splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) 992.87/297.11 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.87/297.11 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.87/297.11 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.87/297.11 992.87/297.11 42: splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) 992.87/297.11 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.87/297.11 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.87/297.11 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.87/297.11 992.87/297.11 43: splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) 992.87/297.11 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.87/297.11 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.87/297.11 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.87/297.11 992.87/297.11 44: cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) 992.87/297.11 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.87/297.11 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.87/297.11 992.87/297.11 45: cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) 992.87/297.11 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.87/297.11 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.87/297.11 992.87/297.11 46: snd^#(mark(X)) -> c_49(snd^#(X)) 992.87/297.11 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.87/297.11 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.87/297.11 992.87/297.11 47: snd^#(ok(X)) -> c_50(snd^#(X)) 992.87/297.11 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.87/297.11 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.87/297.11 992.87/297.11 48: afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) 992.87/297.11 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.87/297.11 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.87/297.11 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.87/297.11 992.87/297.11 49: afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) 992.87/297.11 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.87/297.11 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.87/297.11 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.87/297.11 992.87/297.11 50: afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) 992.87/297.11 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.87/297.11 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.87/297.11 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.87/297.11 992.87/297.11 51: and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) 992.87/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.87/297.11 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.87/297.11 992.87/297.11 52: and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) 992.87/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.87/297.11 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.87/297.11 992.87/297.11 53: fst^#(mark(X)) -> c_53(fst^#(X)) 992.87/297.11 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.87/297.11 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.87/297.11 992.87/297.11 54: fst^#(ok(X)) -> c_54(fst^#(X)) 992.87/297.11 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.87/297.11 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.87/297.11 992.87/297.11 55: head^#(mark(X)) -> c_55(head^#(X)) 992.87/297.11 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.87/297.11 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.87/297.11 992.87/297.11 56: head^#(ok(X)) -> c_56(head^#(X)) 992.87/297.11 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.87/297.11 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.87/297.11 992.87/297.11 57: natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) 992.87/297.11 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.87/297.11 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.87/297.11 992.87/297.11 58: natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) 992.87/297.11 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.87/297.11 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.87/297.11 992.87/297.11 59: s^#(mark(X)) -> c_59(s^#(X)) 992.87/297.11 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.87/297.11 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.87/297.11 992.87/297.11 60: s^#(ok(X)) -> c_60(s^#(X)) 992.87/297.11 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.87/297.11 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.87/297.11 992.87/297.11 61: sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) 992.87/297.11 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.11 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.11 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.11 992.87/297.11 62: sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) 992.87/297.11 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.11 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.11 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.11 992.87/297.11 63: sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) 992.87/297.11 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.11 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.11 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.11 992.87/297.11 64: tail^#(mark(X)) -> c_64(tail^#(X)) 992.87/297.11 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.87/297.11 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.87/297.11 992.87/297.11 65: tail^#(ok(X)) -> c_65(tail^#(X)) 992.87/297.11 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.87/297.11 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.87/297.11 992.87/297.11 66: take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) 992.87/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.11 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.11 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.11 992.87/297.11 67: take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) 992.87/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.11 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.11 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.11 992.87/297.11 68: take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) 992.87/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.11 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.11 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.11 992.87/297.11 69: proper^#(U11(X1, X2, X3, X4)) -> 992.87/297.11 c_69(U11^#(proper(X1), proper(X2), proper(X3), proper(X4))) 992.87/297.11 -->_1 U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.11 c_35(U11^#(X1, X2, X3, X4)) :35 992.87/297.11 -->_1 U11^#(mark(X1), X2, X3, X4) -> 992.87/297.11 c_34(U11^#(X1, X2, X3, X4)) :34 992.87/297.11 992.87/297.11 70: proper^#(tt()) -> c_70() 992.87/297.11 992.87/297.11 71: proper^#(U12(X1, X2)) -> c_71(U12^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) :37 992.87/297.11 -->_1 U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) :36 992.87/297.11 992.87/297.11 72: proper^#(splitAt(X1, X2)) -> 992.87/297.11 c_72(splitAt^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) :43 992.87/297.11 -->_1 splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) :42 992.87/297.11 -->_1 splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) :41 992.87/297.11 992.87/297.11 73: proper^#(pair(X1, X2)) -> c_73(pair^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) :40 992.87/297.11 -->_1 pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) :39 992.87/297.11 -->_1 pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) :38 992.87/297.11 992.87/297.11 74: proper^#(cons(X1, X2)) -> c_74(cons^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) :45 992.87/297.11 -->_1 cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) :44 992.87/297.11 992.87/297.11 75: proper^#(afterNth(X1, X2)) -> 992.87/297.11 c_75(afterNth^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) :50 992.87/297.11 -->_1 afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) :49 992.87/297.11 -->_1 afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) :48 992.87/297.11 992.87/297.11 76: proper^#(snd(X)) -> c_76(snd^#(proper(X))) 992.87/297.11 -->_1 snd^#(ok(X)) -> c_50(snd^#(X)) :47 992.87/297.11 -->_1 snd^#(mark(X)) -> c_49(snd^#(X)) :46 992.87/297.11 992.87/297.11 77: proper^#(and(X1, X2)) -> c_77(and^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) :52 992.87/297.11 -->_1 and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) :51 992.87/297.11 992.87/297.11 78: proper^#(fst(X)) -> c_78(fst^#(proper(X))) 992.87/297.11 -->_1 fst^#(ok(X)) -> c_54(fst^#(X)) :54 992.87/297.11 -->_1 fst^#(mark(X)) -> c_53(fst^#(X)) :53 992.87/297.11 992.87/297.11 79: proper^#(head(X)) -> c_79(head^#(proper(X))) 992.87/297.11 -->_1 head^#(ok(X)) -> c_56(head^#(X)) :56 992.87/297.11 -->_1 head^#(mark(X)) -> c_55(head^#(X)) :55 992.87/297.11 992.87/297.11 80: proper^#(natsFrom(X)) -> c_80(natsFrom^#(proper(X))) 992.87/297.11 -->_1 natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) :58 992.87/297.11 -->_1 natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) :57 992.87/297.11 992.87/297.11 81: proper^#(s(X)) -> c_81(s^#(proper(X))) 992.87/297.11 -->_1 s^#(ok(X)) -> c_60(s^#(X)) :60 992.87/297.11 -->_1 s^#(mark(X)) -> c_59(s^#(X)) :59 992.87/297.11 992.87/297.11 82: proper^#(sel(X1, X2)) -> c_82(sel^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) :63 992.87/297.11 -->_1 sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) :62 992.87/297.11 -->_1 sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) :61 992.87/297.11 992.87/297.11 83: proper^#(0()) -> c_83() 992.87/297.11 992.87/297.11 84: proper^#(nil()) -> c_84() 992.87/297.11 992.87/297.11 85: proper^#(tail(X)) -> c_85(tail^#(proper(X))) 992.87/297.11 -->_1 tail^#(ok(X)) -> c_65(tail^#(X)) :65 992.87/297.11 -->_1 tail^#(mark(X)) -> c_64(tail^#(X)) :64 992.87/297.11 992.87/297.11 86: proper^#(take(X1, X2)) -> c_86(take^#(proper(X1), proper(X2))) 992.87/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) :68 992.87/297.11 -->_1 take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) :67 992.87/297.11 -->_1 take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) :66 992.87/297.11 992.87/297.11 87: top^#(mark(X)) -> c_87(top^#(proper(X))) 992.87/297.11 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.87/297.11 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.87/297.11 992.87/297.11 88: top^#(ok(X)) -> c_88(top^#(active(X))) 992.87/297.11 -->_1 top^#(ok(X)) -> c_88(top^#(active(X))) :88 992.87/297.11 -->_1 top^#(mark(X)) -> c_87(top^#(proper(X))) :87 992.87/297.11 992.87/297.11 992.87/297.11 Only the nodes 992.87/297.11 {34,35,36,37,38,40,39,41,43,42,44,45,46,47,48,50,49,51,52,53,54,55,56,57,58,59,60,61,63,62,64,65,66,68,67,70,83,84,87,88} 992.87/297.11 are reachable from nodes 992.87/297.11 {34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,70,83,84,87,88} 992.87/297.11 that start derivation from marked basic terms. The nodes not 992.87/297.11 reachable are removed from the problem. 992.87/297.11 992.87/297.11 We are left with following problem, upon which TcT provides the 992.87/297.11 certificate MAYBE. 992.87/297.11 992.87/297.11 Strict DPs: 992.87/297.11 { U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4)) 992.87/297.11 , U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.11 c_35(U11^#(X1, X2, X3, X4)) 992.87/297.11 , U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) 992.87/297.11 , U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) 992.87/297.11 , pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) 992.87/297.11 , pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) 992.87/297.11 , pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) 992.87/297.11 , splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) 992.87/297.11 , splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) 992.87/297.11 , splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) 992.87/297.11 , cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) 992.87/297.11 , cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) 992.87/297.11 , snd^#(mark(X)) -> c_49(snd^#(X)) 992.87/297.11 , snd^#(ok(X)) -> c_50(snd^#(X)) 992.87/297.11 , afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) 992.87/297.11 , afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) 992.87/297.11 , afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) 992.87/297.11 , and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) 992.87/297.11 , and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) 992.87/297.11 , fst^#(mark(X)) -> c_53(fst^#(X)) 992.87/297.11 , fst^#(ok(X)) -> c_54(fst^#(X)) 992.87/297.11 , head^#(mark(X)) -> c_55(head^#(X)) 992.87/297.11 , head^#(ok(X)) -> c_56(head^#(X)) 992.87/297.11 , natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) 992.87/297.11 , natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) 992.87/297.11 , s^#(mark(X)) -> c_59(s^#(X)) 992.87/297.11 , s^#(ok(X)) -> c_60(s^#(X)) 992.87/297.11 , sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) 992.87/297.11 , sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) 992.87/297.11 , sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) 992.87/297.11 , tail^#(mark(X)) -> c_64(tail^#(X)) 992.87/297.11 , tail^#(ok(X)) -> c_65(tail^#(X)) 992.87/297.11 , take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) 992.87/297.11 , take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) 992.87/297.11 , take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) 992.87/297.11 , proper^#(tt()) -> c_70() 992.87/297.11 , proper^#(0()) -> c_83() 992.87/297.11 , proper^#(nil()) -> c_84() 992.87/297.11 , top^#(mark(X)) -> c_87(top^#(proper(X))) 992.87/297.11 , top^#(ok(X)) -> c_88(top^#(active(X))) } 992.87/297.11 Strict Trs: 992.87/297.11 { active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4) 992.87/297.11 , active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X)) 992.87/297.11 , active(U12(X1, X2)) -> U12(active(X1), X2) 992.87/297.11 , active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) 992.87/297.11 , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) 992.87/297.11 , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) 992.87/297.11 , active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS)) 992.87/297.11 , active(splitAt(0(), XS)) -> mark(pair(nil(), XS)) 992.87/297.11 , active(pair(X1, X2)) -> pair(X1, active(X2)) 992.87/297.11 , active(pair(X1, X2)) -> pair(active(X1), X2) 992.87/297.11 , active(cons(X1, X2)) -> cons(active(X1), X2) 992.87/297.11 , active(afterNth(N, XS)) -> mark(snd(splitAt(N, XS))) 992.87/297.11 , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) 992.87/297.11 , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) 992.87/297.11 , active(snd(X)) -> snd(active(X)) 992.87/297.11 , active(snd(pair(X, Y))) -> mark(Y) 992.87/297.11 , active(and(X1, X2)) -> and(active(X1), X2) 992.87/297.11 , active(and(tt(), X)) -> mark(X) 992.87/297.11 , active(fst(X)) -> fst(active(X)) 992.87/297.11 , active(fst(pair(X, Y))) -> mark(X) 992.87/297.11 , active(head(X)) -> head(active(X)) 992.87/297.11 , active(head(cons(N, XS))) -> mark(N) 992.87/297.11 , active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))) 992.87/297.11 , active(natsFrom(X)) -> natsFrom(active(X)) 992.87/297.11 , active(s(X)) -> s(active(X)) 992.87/297.11 , active(sel(N, XS)) -> mark(head(afterNth(N, XS))) 992.87/297.11 , active(sel(X1, X2)) -> sel(X1, active(X2)) 992.87/297.11 , active(sel(X1, X2)) -> sel(active(X1), X2) 992.87/297.11 , active(tail(X)) -> tail(active(X)) 992.87/297.11 , active(tail(cons(N, XS))) -> mark(XS) 992.87/297.11 , active(take(N, XS)) -> mark(fst(splitAt(N, XS))) 992.87/297.11 , active(take(X1, X2)) -> take(X1, active(X2)) 992.87/297.11 , active(take(X1, X2)) -> take(active(X1), X2) 992.87/297.12 , U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4)) 992.87/297.12 , U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4)) 992.87/297.12 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 992.87/297.12 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 992.87/297.12 , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) 992.87/297.12 , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) 992.87/297.12 , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) 992.87/297.12 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 992.87/297.12 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 992.87/297.12 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 992.87/297.12 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 992.87/297.12 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 992.87/297.12 , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) 992.87/297.12 , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) 992.87/297.12 , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) 992.87/297.12 , snd(mark(X)) -> mark(snd(X)) 992.87/297.12 , snd(ok(X)) -> ok(snd(X)) 992.87/297.12 , and(mark(X1), X2) -> mark(and(X1, X2)) 992.87/297.12 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 992.87/297.12 , fst(mark(X)) -> mark(fst(X)) 992.87/297.12 , fst(ok(X)) -> ok(fst(X)) 992.87/297.12 , head(mark(X)) -> mark(head(X)) 992.87/297.12 , head(ok(X)) -> ok(head(X)) 992.87/297.12 , natsFrom(mark(X)) -> mark(natsFrom(X)) 992.87/297.12 , natsFrom(ok(X)) -> ok(natsFrom(X)) 992.87/297.12 , s(mark(X)) -> mark(s(X)) 992.87/297.12 , s(ok(X)) -> ok(s(X)) 992.87/297.12 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 992.87/297.12 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 992.87/297.12 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 992.87/297.12 , tail(mark(X)) -> mark(tail(X)) 992.87/297.12 , tail(ok(X)) -> ok(tail(X)) 992.87/297.12 , take(X1, mark(X2)) -> mark(take(X1, X2)) 992.87/297.12 , take(mark(X1), X2) -> mark(take(X1, X2)) 992.87/297.12 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 992.87/297.12 , proper(U11(X1, X2, X3, X4)) -> 992.87/297.12 U11(proper(X1), proper(X2), proper(X3), proper(X4)) 992.87/297.12 , proper(tt()) -> ok(tt()) 992.87/297.12 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 992.87/297.12 , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) 992.87/297.12 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 992.87/297.12 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 992.87/297.12 , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) 992.87/297.12 , proper(snd(X)) -> snd(proper(X)) 992.87/297.12 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 992.87/297.12 , proper(fst(X)) -> fst(proper(X)) 992.87/297.12 , proper(head(X)) -> head(proper(X)) 992.87/297.12 , proper(natsFrom(X)) -> natsFrom(proper(X)) 992.87/297.12 , proper(s(X)) -> s(proper(X)) 992.87/297.12 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 992.87/297.12 , proper(0()) -> ok(0()) 992.87/297.12 , proper(nil()) -> ok(nil()) 992.87/297.12 , proper(tail(X)) -> tail(proper(X)) 992.87/297.12 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 992.87/297.12 , top(mark(X)) -> top(proper(X)) 992.87/297.12 , top(ok(X)) -> top(active(X)) } 992.87/297.12 Obligation: 992.87/297.12 runtime complexity 992.87/297.12 Answer: 992.87/297.12 MAYBE 992.87/297.12 992.87/297.12 We estimate the number of application of {36,37,38} by applications 992.87/297.12 of Pre({36,37,38}) = {}. Here rules are labeled as follows: 992.87/297.12 992.87/297.12 DPs: 992.87/297.12 { 1: U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4)) 992.87/297.12 , 2: U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.12 c_35(U11^#(X1, X2, X3, X4)) 992.87/297.12 , 3: U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) 992.87/297.12 , 4: U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) 992.87/297.12 , 5: pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) 992.87/297.12 , 6: pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) 992.87/297.12 , 7: pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) 992.87/297.12 , 8: splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) 992.87/297.12 , 9: splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) 992.87/297.12 , 10: splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) 992.87/297.12 , 11: cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) 992.87/297.12 , 12: cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) 992.87/297.12 , 13: snd^#(mark(X)) -> c_49(snd^#(X)) 992.87/297.12 , 14: snd^#(ok(X)) -> c_50(snd^#(X)) 992.87/297.12 , 15: afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) 992.87/297.12 , 16: afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) 992.87/297.12 , 17: afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) 992.87/297.12 , 18: and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) 992.87/297.12 , 19: and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) 992.87/297.12 , 20: fst^#(mark(X)) -> c_53(fst^#(X)) 992.87/297.12 , 21: fst^#(ok(X)) -> c_54(fst^#(X)) 992.87/297.12 , 22: head^#(mark(X)) -> c_55(head^#(X)) 992.87/297.12 , 23: head^#(ok(X)) -> c_56(head^#(X)) 992.87/297.12 , 24: natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) 992.87/297.12 , 25: natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) 992.87/297.12 , 26: s^#(mark(X)) -> c_59(s^#(X)) 992.87/297.12 , 27: s^#(ok(X)) -> c_60(s^#(X)) 992.87/297.12 , 28: sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) 992.87/297.12 , 29: sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) 992.87/297.12 , 30: sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) 992.87/297.12 , 31: tail^#(mark(X)) -> c_64(tail^#(X)) 992.87/297.12 , 32: tail^#(ok(X)) -> c_65(tail^#(X)) 992.87/297.12 , 33: take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) 992.87/297.12 , 34: take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) 992.87/297.12 , 35: take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) 992.87/297.12 , 36: proper^#(tt()) -> c_70() 992.87/297.12 , 37: proper^#(0()) -> c_83() 992.87/297.12 , 38: proper^#(nil()) -> c_84() 992.87/297.12 , 39: top^#(mark(X)) -> c_87(top^#(proper(X))) 992.87/297.12 , 40: top^#(ok(X)) -> c_88(top^#(active(X))) } 992.87/297.12 992.87/297.12 We are left with following problem, upon which TcT provides the 992.87/297.12 certificate MAYBE. 992.87/297.12 992.87/297.12 Strict DPs: 992.87/297.12 { U11^#(mark(X1), X2, X3, X4) -> c_34(U11^#(X1, X2, X3, X4)) 992.87/297.12 , U11^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 992.87/297.12 c_35(U11^#(X1, X2, X3, X4)) 992.87/297.12 , U12^#(mark(X1), X2) -> c_36(U12^#(X1, X2)) 992.87/297.12 , U12^#(ok(X1), ok(X2)) -> c_37(U12^#(X1, X2)) 992.87/297.12 , pair^#(X1, mark(X2)) -> c_41(pair^#(X1, X2)) 992.87/297.12 , pair^#(mark(X1), X2) -> c_42(pair^#(X1, X2)) 992.87/297.12 , pair^#(ok(X1), ok(X2)) -> c_43(pair^#(X1, X2)) 992.87/297.12 , splitAt^#(X1, mark(X2)) -> c_38(splitAt^#(X1, X2)) 992.87/297.12 , splitAt^#(mark(X1), X2) -> c_39(splitAt^#(X1, X2)) 992.87/297.12 , splitAt^#(ok(X1), ok(X2)) -> c_40(splitAt^#(X1, X2)) 992.87/297.12 , cons^#(mark(X1), X2) -> c_44(cons^#(X1, X2)) 992.87/297.12 , cons^#(ok(X1), ok(X2)) -> c_45(cons^#(X1, X2)) 992.87/297.12 , snd^#(mark(X)) -> c_49(snd^#(X)) 992.87/297.12 , snd^#(ok(X)) -> c_50(snd^#(X)) 992.87/297.12 , afterNth^#(X1, mark(X2)) -> c_46(afterNth^#(X1, X2)) 992.87/297.12 , afterNth^#(mark(X1), X2) -> c_47(afterNth^#(X1, X2)) 992.87/297.12 , afterNth^#(ok(X1), ok(X2)) -> c_48(afterNth^#(X1, X2)) 992.87/297.12 , and^#(mark(X1), X2) -> c_51(and^#(X1, X2)) 992.87/297.12 , and^#(ok(X1), ok(X2)) -> c_52(and^#(X1, X2)) 992.87/297.12 , fst^#(mark(X)) -> c_53(fst^#(X)) 992.87/297.12 , fst^#(ok(X)) -> c_54(fst^#(X)) 992.87/297.12 , head^#(mark(X)) -> c_55(head^#(X)) 992.87/297.12 , head^#(ok(X)) -> c_56(head^#(X)) 992.87/297.12 , natsFrom^#(mark(X)) -> c_57(natsFrom^#(X)) 992.87/297.12 , natsFrom^#(ok(X)) -> c_58(natsFrom^#(X)) 992.87/297.12 , s^#(mark(X)) -> c_59(s^#(X)) 992.87/297.12 , s^#(ok(X)) -> c_60(s^#(X)) 992.87/297.12 , sel^#(X1, mark(X2)) -> c_61(sel^#(X1, X2)) 992.87/297.12 , sel^#(mark(X1), X2) -> c_62(sel^#(X1, X2)) 992.87/297.12 , sel^#(ok(X1), ok(X2)) -> c_63(sel^#(X1, X2)) 992.87/297.12 , tail^#(mark(X)) -> c_64(tail^#(X)) 992.87/297.12 , tail^#(ok(X)) -> c_65(tail^#(X)) 992.87/297.12 , take^#(X1, mark(X2)) -> c_66(take^#(X1, X2)) 992.87/297.12 , take^#(mark(X1), X2) -> c_67(take^#(X1, X2)) 992.87/297.12 , take^#(ok(X1), ok(X2)) -> c_68(take^#(X1, X2)) 992.87/297.12 , top^#(mark(X)) -> c_87(top^#(proper(X))) 992.87/297.12 , top^#(ok(X)) -> c_88(top^#(active(X))) } 992.87/297.12 Strict Trs: 992.87/297.12 { active(U11(X1, X2, X3, X4)) -> U11(active(X1), X2, X3, X4) 992.87/297.12 , active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X)) 992.87/297.12 , active(U12(X1, X2)) -> U12(active(X1), X2) 992.87/297.12 , active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) 992.87/297.12 , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) 992.87/297.12 , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) 992.87/297.12 , active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS)) 992.87/297.12 , active(splitAt(0(), XS)) -> mark(pair(nil(), XS)) 992.87/297.12 , active(pair(X1, X2)) -> pair(X1, active(X2)) 992.87/297.12 , active(pair(X1, X2)) -> pair(active(X1), X2) 992.87/297.12 , active(cons(X1, X2)) -> cons(active(X1), X2) 992.87/297.12 , active(afterNth(N, XS)) -> mark(snd(splitAt(N, XS))) 992.87/297.12 , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) 992.87/297.12 , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) 992.87/297.12 , active(snd(X)) -> snd(active(X)) 992.87/297.12 , active(snd(pair(X, Y))) -> mark(Y) 992.87/297.12 , active(and(X1, X2)) -> and(active(X1), X2) 992.87/297.12 , active(and(tt(), X)) -> mark(X) 992.87/297.12 , active(fst(X)) -> fst(active(X)) 992.87/297.12 , active(fst(pair(X, Y))) -> mark(X) 992.87/297.12 , active(head(X)) -> head(active(X)) 992.87/297.12 , active(head(cons(N, XS))) -> mark(N) 992.87/297.12 , active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))) 992.87/297.12 , active(natsFrom(X)) -> natsFrom(active(X)) 992.87/297.12 , active(s(X)) -> s(active(X)) 992.87/297.12 , active(sel(N, XS)) -> mark(head(afterNth(N, XS))) 992.87/297.12 , active(sel(X1, X2)) -> sel(X1, active(X2)) 992.87/297.12 , active(sel(X1, X2)) -> sel(active(X1), X2) 992.87/297.12 , active(tail(X)) -> tail(active(X)) 992.87/297.12 , active(tail(cons(N, XS))) -> mark(XS) 992.87/297.12 , active(take(N, XS)) -> mark(fst(splitAt(N, XS))) 992.87/297.12 , active(take(X1, X2)) -> take(X1, active(X2)) 992.87/297.12 , active(take(X1, X2)) -> take(active(X1), X2) 992.87/297.12 , U11(mark(X1), X2, X3, X4) -> mark(U11(X1, X2, X3, X4)) 992.87/297.12 , U11(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U11(X1, X2, X3, X4)) 992.87/297.12 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 992.87/297.12 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 992.87/297.12 , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) 992.87/297.12 , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) 992.87/297.12 , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) 992.87/297.12 , pair(X1, mark(X2)) -> mark(pair(X1, X2)) 992.87/297.12 , pair(mark(X1), X2) -> mark(pair(X1, X2)) 992.87/297.12 , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) 992.87/297.12 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 992.87/297.12 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 992.87/297.12 , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) 992.87/297.12 , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) 992.87/297.12 , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) 992.87/297.12 , snd(mark(X)) -> mark(snd(X)) 992.87/297.12 , snd(ok(X)) -> ok(snd(X)) 992.87/297.12 , and(mark(X1), X2) -> mark(and(X1, X2)) 992.87/297.12 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 992.87/297.12 , fst(mark(X)) -> mark(fst(X)) 992.87/297.12 , fst(ok(X)) -> ok(fst(X)) 992.87/297.12 , head(mark(X)) -> mark(head(X)) 992.87/297.12 , head(ok(X)) -> ok(head(X)) 992.87/297.12 , natsFrom(mark(X)) -> mark(natsFrom(X)) 992.87/297.12 , natsFrom(ok(X)) -> ok(natsFrom(X)) 992.87/297.12 , s(mark(X)) -> mark(s(X)) 992.87/297.12 , s(ok(X)) -> ok(s(X)) 992.87/297.12 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 992.87/297.12 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 992.87/297.12 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 992.87/297.12 , tail(mark(X)) -> mark(tail(X)) 992.87/297.12 , tail(ok(X)) -> ok(tail(X)) 992.87/297.12 , take(X1, mark(X2)) -> mark(take(X1, X2)) 992.87/297.12 , take(mark(X1), X2) -> mark(take(X1, X2)) 992.87/297.12 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 992.87/297.12 , proper(U11(X1, X2, X3, X4)) -> 992.87/297.12 U11(proper(X1), proper(X2), proper(X3), proper(X4)) 992.87/297.12 , proper(tt()) -> ok(tt()) 992.87/297.12 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 992.87/297.12 , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) 992.87/297.12 , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) 992.87/297.12 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 992.87/297.12 , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) 992.87/297.12 , proper(snd(X)) -> snd(proper(X)) 992.87/297.12 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 992.87/297.12 , proper(fst(X)) -> fst(proper(X)) 992.87/297.12 , proper(head(X)) -> head(proper(X)) 992.87/297.12 , proper(natsFrom(X)) -> natsFrom(proper(X)) 992.87/297.12 , proper(s(X)) -> s(proper(X)) 992.87/297.12 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 992.87/297.12 , proper(0()) -> ok(0()) 992.87/297.12 , proper(nil()) -> ok(nil()) 992.87/297.12 , proper(tail(X)) -> tail(proper(X)) 992.87/297.12 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 992.87/297.12 , top(mark(X)) -> top(proper(X)) 992.87/297.12 , top(ok(X)) -> top(active(X)) } 992.87/297.12 Weak DPs: 992.87/297.12 { proper^#(tt()) -> c_70() 992.87/297.12 , proper^#(0()) -> c_83() 992.87/297.12 , proper^#(nil()) -> c_84() } 992.87/297.12 Obligation: 992.87/297.12 runtime complexity 992.87/297.12 Answer: 992.87/297.12 MAYBE 992.87/297.12 992.87/297.12 Empty strict component of the problem is NOT empty. 992.87/297.12 992.87/297.12 992.87/297.12 Arrrr.. 993.21/297.40 EOF