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