MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), N, XS)) -> mark(fst(splitAt(N, XS))) , active(fst(X)) -> fst(active(X)) , active(fst(pair(X, Y))) -> mark(U21(and(isLNat(X), isLNat(Y)), X)) , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) , active(splitAt(s(N), cons(X, XS))) -> mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) , active(splitAt(0(), XS)) -> mark(U71(isLNat(XS), XS)) , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))) , active(snd(X)) -> snd(active(X)) , active(snd(pair(X, Y))) -> mark(U61(and(isLNat(X), isLNat(Y)), Y)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), X)) -> mark(X) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), N)) -> mark(N) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(cons(N, natsFrom(s(N)))) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(natsFrom(N)) -> mark(U41(isNatural(N), N)) , active(natsFrom(X)) -> natsFrom(active(X)) , active(s(X)) -> s(active(X)) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), N, XS)) -> mark(head(afterNth(N, XS))) , active(head(X)) -> head(active(X)) , active(head(cons(N, XS))) -> mark(U31(and(isNatural(N), isLNat(XS)), N)) , active(afterNth(N, XS)) -> mark(U11(and(isNatural(N), isLNat(XS)), N, XS)) , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), Y)) -> mark(Y) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), XS)) -> mark(pair(nil(), XS)) , active(pair(X1, X2)) -> pair(X1, active(X2)) , active(pair(X1, X2)) -> pair(active(X1), X2) , active(U81(X1, X2, X3, X4)) -> U81(active(X1), X2, X3, X4) , active(U81(tt(), N, X, XS)) -> mark(U82(splitAt(N, XS), X)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), XS)) -> mark(XS) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatural(s(V1))) -> mark(isNatural(V1)) , active(isNatural(head(V1))) -> mark(isLNat(V1)) , active(isNatural(0())) -> mark(tt()) , active(isNatural(sel(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(fst(V1))) -> mark(isPLNat(V1)) , active(isLNat(snd(V1))) -> mark(isPLNat(V1)) , active(isLNat(cons(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)) , active(isLNat(afterNth(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(nil())) -> mark(tt()) , active(isLNat(tail(V1))) -> mark(isLNat(V1)) , active(isLNat(take(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(splitAt(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(pair(V1, V2))) -> mark(and(isLNat(V1), isLNat(V2))) , active(tail(X)) -> tail(active(X)) , active(tail(cons(N, XS))) -> mark(U91(and(isNatural(N), isLNat(XS)), XS)) , active(take(N, XS)) -> mark(U101(and(isNatural(N), isLNat(XS)), N, XS)) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(sel(N, XS)) -> mark(U51(and(isNatural(N), isLNat(XS)), N, XS)) , active(sel(X1, X2)) -> sel(X1, active(X2)) , active(sel(X1, X2)) -> sel(active(X1), X2) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , fst(mark(X)) -> mark(fst(X)) , fst(ok(X)) -> ok(fst(X)) , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , snd(mark(X)) -> mark(snd(X)) , snd(ok(X)) -> ok(snd(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , natsFrom(mark(X)) -> mark(natsFrom(X)) , natsFrom(ok(X)) -> ok(natsFrom(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , pair(X1, mark(X2)) -> mark(pair(X1, X2)) , pair(mark(X1), X2) -> mark(pair(X1, X2)) , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) , U81(mark(X1), X2, X3, X4) -> mark(U81(X1, X2, X3, X4)) , U81(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U81(X1, X2, X3, X4)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatural(ok(X)) -> ok(isNatural(X)) , isLNat(ok(X)) -> ok(isLNat(X)) , isPLNat(ok(X)) -> ok(isPLNat(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , sel(X1, mark(X2)) -> mark(sel(X1, X2)) , sel(mark(X1), X2) -> mark(sel(X1, X2)) , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(fst(X)) -> fst(proper(X)) , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(snd(X)) -> snd(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(natsFrom(X)) -> natsFrom(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(head(X)) -> head(proper(X)) , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U81(X1, X2, X3, X4)) -> U81(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatural(X)) -> isNatural(proper(X)) , proper(isLNat(X)) -> isLNat(proper(X)) , proper(isPLNat(X)) -> isPLNat(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) , active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) , active^#(fst(X)) -> c_3(fst^#(active(X))) , active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) , active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) , active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) , active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) , active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) , active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) , active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) , active^#(snd(X)) -> c_11(snd^#(active(X))) , active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) , active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) , active^#(U21(tt(), X)) -> c_14(X) , active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) , active^#(U31(tt(), N)) -> c_16(N) , active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) , active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) , active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) , active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) , active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) , active^#(s(X)) -> c_22(s^#(active(X))) , active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) , active^#(head(X)) -> c_25(head^#(active(X))) , active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) , active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) , active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) , active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) , active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) , active^#(U61(tt(), Y)) -> c_31(Y) , active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) , active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) , active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) , active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) , active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) , active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) , active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) , active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) , active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) , active^#(U91(tt(), XS)) -> c_41(XS) , active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) , active^#(and(tt(), X)) -> c_43(X) , active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) , active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) , active^#(isNatural(0())) -> c_46() , active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) , active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) , active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) , active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) , active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) , active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) , active^#(isLNat(nil())) -> c_53() , active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) , active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) , active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) , active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) , active^#(tail(X)) -> c_58(tail^#(active(X))) , active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) , active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) , active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) , active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) , active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) , active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) , active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) , U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) , fst^#(mark(X)) -> c_68(fst^#(X)) , fst^#(ok(X)) -> c_69(fst^#(X)) , U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) , splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) , splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) , splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) , U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) , U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) , U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) , U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) , snd^#(mark(X)) -> c_75(snd^#(X)) , snd^#(ok(X)) -> c_76(snd^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) , cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) , natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) , natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) , s^#(mark(X)) -> c_87(s^#(X)) , s^#(ok(X)) -> c_88(s^#(X)) , U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) , head^#(mark(X)) -> c_91(head^#(X)) , head^#(ok(X)) -> c_92(head^#(X)) , afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) , afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) , afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) , pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) , pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) , pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) , U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) , U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) , and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) , isNatural^#(ok(X)) -> c_111(isNatural^#(X)) , isLNat^#(ok(X)) -> c_112(isLNat^#(X)) , isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) , tail^#(mark(X)) -> c_114(tail^#(X)) , tail^#(ok(X)) -> c_115(tail^#(X)) , take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) , sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) , sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) , sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) , proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) , proper^#(tt()) -> c_123() , proper^#(fst(X)) -> c_124(fst^#(proper(X))) , proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) , proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) , proper^#(snd(X)) -> c_127(snd^#(proper(X))) , proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) , proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) , proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) , proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) , proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) , proper^#(s(X)) -> c_133(s^#(proper(X))) , proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(head(X)) -> c_135(head^#(proper(X))) , proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) , proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) , proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) , proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_140() , proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) , proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) , proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) , proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) , proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) , proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) , proper^#(tail(X)) -> c_148(tail^#(proper(X))) , proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) , proper^#(0()) -> c_150() , proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) , top^#(mark(X)) -> c_152(top^#(proper(X))) , top^#(ok(X)) -> c_153(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) , active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) , active^#(fst(X)) -> c_3(fst^#(active(X))) , active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) , active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) , active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) , active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) , active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) , active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) , active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) , active^#(snd(X)) -> c_11(snd^#(active(X))) , active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) , active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) , active^#(U21(tt(), X)) -> c_14(X) , active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) , active^#(U31(tt(), N)) -> c_16(N) , active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) , active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) , active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) , active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) , active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) , active^#(s(X)) -> c_22(s^#(active(X))) , active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) , active^#(head(X)) -> c_25(head^#(active(X))) , active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) , active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) , active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) , active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) , active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) , active^#(U61(tt(), Y)) -> c_31(Y) , active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) , active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) , active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) , active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) , active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) , active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) , active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) , active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) , active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) , active^#(U91(tt(), XS)) -> c_41(XS) , active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) , active^#(and(tt(), X)) -> c_43(X) , active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) , active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) , active^#(isNatural(0())) -> c_46() , active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) , active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) , active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) , active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) , active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) , active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) , active^#(isLNat(nil())) -> c_53() , active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) , active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) , active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) , active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) , active^#(tail(X)) -> c_58(tail^#(active(X))) , active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) , active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) , active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) , active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) , active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) , active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) , active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) , U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) , fst^#(mark(X)) -> c_68(fst^#(X)) , fst^#(ok(X)) -> c_69(fst^#(X)) , U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) , splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) , splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) , splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) , U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) , U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) , U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) , U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) , snd^#(mark(X)) -> c_75(snd^#(X)) , snd^#(ok(X)) -> c_76(snd^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) , cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) , natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) , natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) , s^#(mark(X)) -> c_87(s^#(X)) , s^#(ok(X)) -> c_88(s^#(X)) , U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) , head^#(mark(X)) -> c_91(head^#(X)) , head^#(ok(X)) -> c_92(head^#(X)) , afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) , afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) , afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) , pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) , pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) , pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) , U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) , U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) , and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) , isNatural^#(ok(X)) -> c_111(isNatural^#(X)) , isLNat^#(ok(X)) -> c_112(isLNat^#(X)) , isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) , tail^#(mark(X)) -> c_114(tail^#(X)) , tail^#(ok(X)) -> c_115(tail^#(X)) , take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) , sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) , sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) , sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) , proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) , proper^#(tt()) -> c_123() , proper^#(fst(X)) -> c_124(fst^#(proper(X))) , proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) , proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) , proper^#(snd(X)) -> c_127(snd^#(proper(X))) , proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) , proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) , proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) , proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) , proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) , proper^#(s(X)) -> c_133(s^#(proper(X))) , proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(head(X)) -> c_135(head^#(proper(X))) , proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) , proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) , proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) , proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) , proper^#(nil()) -> c_140() , proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) , proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) , proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) , proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) , proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) , proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) , proper^#(tail(X)) -> c_148(tail^#(proper(X))) , proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) , proper^#(0()) -> c_150() , proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) , top^#(mark(X)) -> c_152(top^#(proper(X))) , top^#(ok(X)) -> c_153(top^#(active(X))) } Strict Trs: { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), N, XS)) -> mark(fst(splitAt(N, XS))) , active(fst(X)) -> fst(active(X)) , active(fst(pair(X, Y))) -> mark(U21(and(isLNat(X), isLNat(Y)), X)) , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) , active(splitAt(s(N), cons(X, XS))) -> mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) , active(splitAt(0(), XS)) -> mark(U71(isLNat(XS), XS)) , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))) , active(snd(X)) -> snd(active(X)) , active(snd(pair(X, Y))) -> mark(U61(and(isLNat(X), isLNat(Y)), Y)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), X)) -> mark(X) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), N)) -> mark(N) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(cons(N, natsFrom(s(N)))) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(natsFrom(N)) -> mark(U41(isNatural(N), N)) , active(natsFrom(X)) -> natsFrom(active(X)) , active(s(X)) -> s(active(X)) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), N, XS)) -> mark(head(afterNth(N, XS))) , active(head(X)) -> head(active(X)) , active(head(cons(N, XS))) -> mark(U31(and(isNatural(N), isLNat(XS)), N)) , active(afterNth(N, XS)) -> mark(U11(and(isNatural(N), isLNat(XS)), N, XS)) , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), Y)) -> mark(Y) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), XS)) -> mark(pair(nil(), XS)) , active(pair(X1, X2)) -> pair(X1, active(X2)) , active(pair(X1, X2)) -> pair(active(X1), X2) , active(U81(X1, X2, X3, X4)) -> U81(active(X1), X2, X3, X4) , active(U81(tt(), N, X, XS)) -> mark(U82(splitAt(N, XS), X)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), XS)) -> mark(XS) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatural(s(V1))) -> mark(isNatural(V1)) , active(isNatural(head(V1))) -> mark(isLNat(V1)) , active(isNatural(0())) -> mark(tt()) , active(isNatural(sel(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(fst(V1))) -> mark(isPLNat(V1)) , active(isLNat(snd(V1))) -> mark(isPLNat(V1)) , active(isLNat(cons(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)) , active(isLNat(afterNth(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(nil())) -> mark(tt()) , active(isLNat(tail(V1))) -> mark(isLNat(V1)) , active(isLNat(take(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(splitAt(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(pair(V1, V2))) -> mark(and(isLNat(V1), isLNat(V2))) , active(tail(X)) -> tail(active(X)) , active(tail(cons(N, XS))) -> mark(U91(and(isNatural(N), isLNat(XS)), XS)) , active(take(N, XS)) -> mark(U101(and(isNatural(N), isLNat(XS)), N, XS)) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(sel(N, XS)) -> mark(U51(and(isNatural(N), isLNat(XS)), N, XS)) , active(sel(X1, X2)) -> sel(X1, active(X2)) , active(sel(X1, X2)) -> sel(active(X1), X2) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , fst(mark(X)) -> mark(fst(X)) , fst(ok(X)) -> ok(fst(X)) , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , snd(mark(X)) -> mark(snd(X)) , snd(ok(X)) -> ok(snd(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , natsFrom(mark(X)) -> mark(natsFrom(X)) , natsFrom(ok(X)) -> ok(natsFrom(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , pair(X1, mark(X2)) -> mark(pair(X1, X2)) , pair(mark(X1), X2) -> mark(pair(X1, X2)) , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) , U81(mark(X1), X2, X3, X4) -> mark(U81(X1, X2, X3, X4)) , U81(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U81(X1, X2, X3, X4)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatural(ok(X)) -> ok(isNatural(X)) , isLNat(ok(X)) -> ok(isLNat(X)) , isPLNat(ok(X)) -> ok(isPLNat(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , sel(X1, mark(X2)) -> mark(sel(X1, X2)) , sel(mark(X1), X2) -> mark(sel(X1, X2)) , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(fst(X)) -> fst(proper(X)) , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(snd(X)) -> snd(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(natsFrom(X)) -> natsFrom(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(head(X)) -> head(proper(X)) , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U81(X1, X2, X3, X4)) -> U81(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatural(X)) -> isNatural(proper(X)) , proper(isLNat(X)) -> isLNat(proper(X)) , proper(isPLNat(X)) -> isPLNat(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 2: active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 3: active^#(fst(X)) -> c_3(fst^#(active(X))) -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 4: active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 5: active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 6: active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 7: active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 8: active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 9: active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 10: active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 11: active^#(snd(X)) -> c_11(snd^#(active(X))) -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 12: active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 13: active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 14: active^#(U21(tt(), X)) -> c_14(X) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 -->_1 proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) :151 -->_1 proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) :149 -->_1 proper^#(tail(X)) -> c_148(tail^#(proper(X))) :148 -->_1 proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) :147 -->_1 proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) :146 -->_1 proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) :145 -->_1 proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) :144 -->_1 proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) :143 -->_1 proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) :142 -->_1 proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) :141 -->_1 proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) :139 -->_1 proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) :138 -->_1 proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) :137 -->_1 proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) :136 -->_1 proper^#(head(X)) -> c_135(head^#(proper(X))) :135 -->_1 proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) :134 -->_1 proper^#(s(X)) -> c_133(s^#(proper(X))) :133 -->_1 proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) :132 -->_1 proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) :131 -->_1 proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) :129 -->_1 proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) :128 -->_1 proper^#(snd(X)) -> c_127(snd^#(proper(X))) :127 -->_1 proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) :126 -->_1 proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) :125 -->_1 proper^#(fst(X)) -> c_124(fst^#(proper(X))) :124 -->_1 proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 -->_1 active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) :65 -->_1 active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) :64 -->_1 active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) :63 -->_1 active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) :62 -->_1 active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) :61 -->_1 active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) :60 -->_1 active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) :59 -->_1 active^#(tail(X)) -> c_58(tail^#(active(X))) :58 -->_1 active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) :57 -->_1 active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) :56 -->_1 active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) :55 -->_1 active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) :54 -->_1 active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) :52 -->_1 active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) :51 -->_1 active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) :50 -->_1 active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) :49 -->_1 active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) :48 -->_1 active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) :47 -->_1 active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) :45 -->_1 active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) :44 -->_1 active^#(and(tt(), X)) -> c_43(X) :43 -->_1 active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) :42 -->_1 active^#(U91(tt(), XS)) -> c_41(XS) :41 -->_1 active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) :40 -->_1 active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) :39 -->_1 active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) :38 -->_1 active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) :37 -->_1 active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) :36 -->_1 active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) :35 -->_1 active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) :33 -->_1 active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) :32 -->_1 active^#(U61(tt(), Y)) -> c_31(Y) :31 -->_1 active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) :30 -->_1 active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) :29 -->_1 active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) :28 -->_1 active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) :27 -->_1 active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) :26 -->_1 active^#(head(X)) -> c_25(head^#(active(X))) :25 -->_1 active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 active^#(s(X)) -> c_22(s^#(active(X))) :22 -->_1 active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) :21 -->_1 active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) :20 -->_1 active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) :19 -->_1 active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) :18 -->_1 active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) :17 -->_1 active^#(U31(tt(), N)) -> c_16(N) :16 -->_1 active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) :15 -->_1 proper^#(0()) -> c_150() :150 -->_1 proper^#(nil()) -> c_140() :140 -->_1 proper^#(tt()) -> c_123() :123 -->_1 active^#(isLNat(nil())) -> c_53() :53 -->_1 active^#(isNatural(0())) -> c_46() :46 -->_1 active^#(U21(tt(), X)) -> c_14(X) :14 -->_1 active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) :13 -->_1 active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) :12 -->_1 active^#(snd(X)) -> c_11(snd^#(active(X))) :11 -->_1 active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) :10 -->_1 active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) :9 -->_1 active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) :8 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) :7 -->_1 active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) :6 -->_1 active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) :5 -->_1 active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) :4 -->_1 active^#(fst(X)) -> c_3(fst^#(active(X))) :3 -->_1 active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) :2 -->_1 active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) :1 15: active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 16: active^#(U31(tt(), N)) -> c_16(N) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 -->_1 proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) :151 -->_1 proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) :149 -->_1 proper^#(tail(X)) -> c_148(tail^#(proper(X))) :148 -->_1 proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) :147 -->_1 proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) :146 -->_1 proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) :145 -->_1 proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) :144 -->_1 proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) :143 -->_1 proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) :142 -->_1 proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) :141 -->_1 proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) :139 -->_1 proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) :138 -->_1 proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) :137 -->_1 proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) :136 -->_1 proper^#(head(X)) -> c_135(head^#(proper(X))) :135 -->_1 proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) :134 -->_1 proper^#(s(X)) -> c_133(s^#(proper(X))) :133 -->_1 proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) :132 -->_1 proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) :131 -->_1 proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) :129 -->_1 proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) :128 -->_1 proper^#(snd(X)) -> c_127(snd^#(proper(X))) :127 -->_1 proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) :126 -->_1 proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) :125 -->_1 proper^#(fst(X)) -> c_124(fst^#(proper(X))) :124 -->_1 proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 -->_1 active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) :65 -->_1 active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) :64 -->_1 active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) :63 -->_1 active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) :62 -->_1 active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) :61 -->_1 active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) :60 -->_1 active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) :59 -->_1 active^#(tail(X)) -> c_58(tail^#(active(X))) :58 -->_1 active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) :57 -->_1 active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) :56 -->_1 active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) :55 -->_1 active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) :54 -->_1 active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) :52 -->_1 active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) :51 -->_1 active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) :50 -->_1 active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) :49 -->_1 active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) :48 -->_1 active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) :47 -->_1 active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) :45 -->_1 active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) :44 -->_1 active^#(and(tt(), X)) -> c_43(X) :43 -->_1 active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) :42 -->_1 active^#(U91(tt(), XS)) -> c_41(XS) :41 -->_1 active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) :40 -->_1 active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) :39 -->_1 active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) :38 -->_1 active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) :37 -->_1 active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) :36 -->_1 active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) :35 -->_1 active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) :33 -->_1 active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) :32 -->_1 active^#(U61(tt(), Y)) -> c_31(Y) :31 -->_1 active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) :30 -->_1 active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) :29 -->_1 active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) :28 -->_1 active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) :27 -->_1 active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) :26 -->_1 active^#(head(X)) -> c_25(head^#(active(X))) :25 -->_1 active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 active^#(s(X)) -> c_22(s^#(active(X))) :22 -->_1 active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) :21 -->_1 active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) :20 -->_1 active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) :19 -->_1 active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) :18 -->_1 active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) :17 -->_1 proper^#(0()) -> c_150() :150 -->_1 proper^#(nil()) -> c_140() :140 -->_1 proper^#(tt()) -> c_123() :123 -->_1 active^#(isLNat(nil())) -> c_53() :53 -->_1 active^#(isNatural(0())) -> c_46() :46 -->_1 active^#(U31(tt(), N)) -> c_16(N) :16 -->_1 active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), X)) -> c_14(X) :14 -->_1 active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) :13 -->_1 active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) :12 -->_1 active^#(snd(X)) -> c_11(snd^#(active(X))) :11 -->_1 active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) :10 -->_1 active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) :9 -->_1 active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) :8 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) :7 -->_1 active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) :6 -->_1 active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) :5 -->_1 active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) :4 -->_1 active^#(fst(X)) -> c_3(fst^#(active(X))) :3 -->_1 active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) :2 -->_1 active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) :1 17: active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 18: active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 19: active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 20: active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 21: active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 22: active^#(s(X)) -> c_22(s^#(active(X))) -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 23: active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 24: active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 25: active^#(head(X)) -> c_25(head^#(active(X))) -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 26: active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 27: active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 28: active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 29: active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 30: active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 31: active^#(U61(tt(), Y)) -> c_31(Y) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 -->_1 proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) :151 -->_1 proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) :149 -->_1 proper^#(tail(X)) -> c_148(tail^#(proper(X))) :148 -->_1 proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) :147 -->_1 proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) :146 -->_1 proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) :145 -->_1 proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) :144 -->_1 proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) :143 -->_1 proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) :142 -->_1 proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) :141 -->_1 proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) :139 -->_1 proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) :138 -->_1 proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) :137 -->_1 proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) :136 -->_1 proper^#(head(X)) -> c_135(head^#(proper(X))) :135 -->_1 proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) :134 -->_1 proper^#(s(X)) -> c_133(s^#(proper(X))) :133 -->_1 proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) :132 -->_1 proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) :131 -->_1 proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) :129 -->_1 proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) :128 -->_1 proper^#(snd(X)) -> c_127(snd^#(proper(X))) :127 -->_1 proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) :126 -->_1 proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) :125 -->_1 proper^#(fst(X)) -> c_124(fst^#(proper(X))) :124 -->_1 proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 -->_1 active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) :65 -->_1 active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) :64 -->_1 active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) :63 -->_1 active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) :62 -->_1 active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) :61 -->_1 active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) :60 -->_1 active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) :59 -->_1 active^#(tail(X)) -> c_58(tail^#(active(X))) :58 -->_1 active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) :57 -->_1 active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) :56 -->_1 active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) :55 -->_1 active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) :54 -->_1 active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) :52 -->_1 active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) :51 -->_1 active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) :50 -->_1 active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) :49 -->_1 active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) :48 -->_1 active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) :47 -->_1 active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) :45 -->_1 active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) :44 -->_1 active^#(and(tt(), X)) -> c_43(X) :43 -->_1 active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) :42 -->_1 active^#(U91(tt(), XS)) -> c_41(XS) :41 -->_1 active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) :40 -->_1 active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) :39 -->_1 active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) :38 -->_1 active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) :37 -->_1 active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) :36 -->_1 active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) :35 -->_1 active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) :33 -->_1 active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) :32 -->_1 proper^#(0()) -> c_150() :150 -->_1 proper^#(nil()) -> c_140() :140 -->_1 proper^#(tt()) -> c_123() :123 -->_1 active^#(isLNat(nil())) -> c_53() :53 -->_1 active^#(isNatural(0())) -> c_46() :46 -->_1 active^#(U61(tt(), Y)) -> c_31(Y) :31 -->_1 active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) :30 -->_1 active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) :29 -->_1 active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) :28 -->_1 active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) :27 -->_1 active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) :26 -->_1 active^#(head(X)) -> c_25(head^#(active(X))) :25 -->_1 active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 active^#(s(X)) -> c_22(s^#(active(X))) :22 -->_1 active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) :21 -->_1 active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) :20 -->_1 active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) :19 -->_1 active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) :18 -->_1 active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) :17 -->_1 active^#(U31(tt(), N)) -> c_16(N) :16 -->_1 active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), X)) -> c_14(X) :14 -->_1 active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) :13 -->_1 active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) :12 -->_1 active^#(snd(X)) -> c_11(snd^#(active(X))) :11 -->_1 active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) :10 -->_1 active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) :9 -->_1 active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) :8 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) :7 -->_1 active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) :6 -->_1 active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) :5 -->_1 active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) :4 -->_1 active^#(fst(X)) -> c_3(fst^#(active(X))) :3 -->_1 active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) :2 -->_1 active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) :1 32: active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 33: active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 34: active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 35: active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 36: active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 37: active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 38: active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 39: active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 40: active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 41: active^#(U91(tt(), XS)) -> c_41(XS) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 -->_1 proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) :151 -->_1 proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) :149 -->_1 proper^#(tail(X)) -> c_148(tail^#(proper(X))) :148 -->_1 proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) :147 -->_1 proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) :146 -->_1 proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) :145 -->_1 proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) :144 -->_1 proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) :143 -->_1 proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) :142 -->_1 proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) :141 -->_1 proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) :139 -->_1 proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) :138 -->_1 proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) :137 -->_1 proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) :136 -->_1 proper^#(head(X)) -> c_135(head^#(proper(X))) :135 -->_1 proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) :134 -->_1 proper^#(s(X)) -> c_133(s^#(proper(X))) :133 -->_1 proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) :132 -->_1 proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) :131 -->_1 proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) :129 -->_1 proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) :128 -->_1 proper^#(snd(X)) -> c_127(snd^#(proper(X))) :127 -->_1 proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) :126 -->_1 proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) :125 -->_1 proper^#(fst(X)) -> c_124(fst^#(proper(X))) :124 -->_1 proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 -->_1 active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) :65 -->_1 active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) :64 -->_1 active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) :63 -->_1 active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) :62 -->_1 active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) :61 -->_1 active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) :60 -->_1 active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) :59 -->_1 active^#(tail(X)) -> c_58(tail^#(active(X))) :58 -->_1 active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) :57 -->_1 active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) :56 -->_1 active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) :55 -->_1 active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) :54 -->_1 active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) :52 -->_1 active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) :51 -->_1 active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) :50 -->_1 active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) :49 -->_1 active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) :48 -->_1 active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) :47 -->_1 active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) :45 -->_1 active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) :44 -->_1 active^#(and(tt(), X)) -> c_43(X) :43 -->_1 active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) :42 -->_1 proper^#(0()) -> c_150() :150 -->_1 proper^#(nil()) -> c_140() :140 -->_1 proper^#(tt()) -> c_123() :123 -->_1 active^#(isLNat(nil())) -> c_53() :53 -->_1 active^#(isNatural(0())) -> c_46() :46 -->_1 active^#(U91(tt(), XS)) -> c_41(XS) :41 -->_1 active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) :40 -->_1 active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) :39 -->_1 active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) :38 -->_1 active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) :37 -->_1 active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) :36 -->_1 active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) :35 -->_1 active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) :33 -->_1 active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) :32 -->_1 active^#(U61(tt(), Y)) -> c_31(Y) :31 -->_1 active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) :30 -->_1 active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) :29 -->_1 active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) :28 -->_1 active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) :27 -->_1 active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) :26 -->_1 active^#(head(X)) -> c_25(head^#(active(X))) :25 -->_1 active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 active^#(s(X)) -> c_22(s^#(active(X))) :22 -->_1 active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) :21 -->_1 active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) :20 -->_1 active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) :19 -->_1 active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) :18 -->_1 active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) :17 -->_1 active^#(U31(tt(), N)) -> c_16(N) :16 -->_1 active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), X)) -> c_14(X) :14 -->_1 active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) :13 -->_1 active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) :12 -->_1 active^#(snd(X)) -> c_11(snd^#(active(X))) :11 -->_1 active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) :10 -->_1 active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) :9 -->_1 active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) :8 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) :7 -->_1 active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) :6 -->_1 active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) :5 -->_1 active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) :4 -->_1 active^#(fst(X)) -> c_3(fst^#(active(X))) :3 -->_1 active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) :2 -->_1 active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) :1 42: active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 43: active^#(and(tt(), X)) -> c_43(X) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 -->_1 proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) :151 -->_1 proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) :149 -->_1 proper^#(tail(X)) -> c_148(tail^#(proper(X))) :148 -->_1 proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) :147 -->_1 proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) :146 -->_1 proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) :145 -->_1 proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) :144 -->_1 proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) :143 -->_1 proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) :142 -->_1 proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) :141 -->_1 proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) :139 -->_1 proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) :138 -->_1 proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) :137 -->_1 proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) :136 -->_1 proper^#(head(X)) -> c_135(head^#(proper(X))) :135 -->_1 proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) :134 -->_1 proper^#(s(X)) -> c_133(s^#(proper(X))) :133 -->_1 proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) :132 -->_1 proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) :131 -->_1 proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) :130 -->_1 proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) :129 -->_1 proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) :128 -->_1 proper^#(snd(X)) -> c_127(snd^#(proper(X))) :127 -->_1 proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) :126 -->_1 proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) :125 -->_1 proper^#(fst(X)) -> c_124(fst^#(proper(X))) :124 -->_1 proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) :122 -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 -->_1 active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) :65 -->_1 active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) :64 -->_1 active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) :63 -->_1 active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) :62 -->_1 active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) :61 -->_1 active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) :60 -->_1 active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) :59 -->_1 active^#(tail(X)) -> c_58(tail^#(active(X))) :58 -->_1 active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) :57 -->_1 active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) :56 -->_1 active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) :55 -->_1 active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) :54 -->_1 active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) :52 -->_1 active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) :51 -->_1 active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) :50 -->_1 active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) :49 -->_1 active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) :48 -->_1 active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) :47 -->_1 active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) :45 -->_1 active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) :44 -->_1 proper^#(0()) -> c_150() :150 -->_1 proper^#(nil()) -> c_140() :140 -->_1 proper^#(tt()) -> c_123() :123 -->_1 active^#(isLNat(nil())) -> c_53() :53 -->_1 active^#(isNatural(0())) -> c_46() :46 -->_1 active^#(and(tt(), X)) -> c_43(X) :43 -->_1 active^#(and(X1, X2)) -> c_42(and^#(active(X1), X2)) :42 -->_1 active^#(U91(tt(), XS)) -> c_41(XS) :41 -->_1 active^#(U91(X1, X2)) -> c_40(U91^#(active(X1), X2)) :40 -->_1 active^#(U82(pair(YS, ZS), X)) -> c_39(pair^#(cons(X, YS), ZS)) :39 -->_1 active^#(U82(X1, X2)) -> c_38(U82^#(active(X1), X2)) :38 -->_1 active^#(U81(tt(), N, X, XS)) -> c_37(U82^#(splitAt(N, XS), X)) :37 -->_1 active^#(U81(X1, X2, X3, X4)) -> c_36(U81^#(active(X1), X2, X3, X4)) :36 -->_1 active^#(pair(X1, X2)) -> c_35(pair^#(active(X1), X2)) :35 -->_1 active^#(pair(X1, X2)) -> c_34(pair^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), XS)) -> c_33(pair^#(nil(), XS)) :33 -->_1 active^#(U71(X1, X2)) -> c_32(U71^#(active(X1), X2)) :32 -->_1 active^#(U61(tt(), Y)) -> c_31(Y) :31 -->_1 active^#(U61(X1, X2)) -> c_30(U61^#(active(X1), X2)) :30 -->_1 active^#(afterNth(X1, X2)) -> c_29(afterNth^#(active(X1), X2)) :29 -->_1 active^#(afterNth(X1, X2)) -> c_28(afterNth^#(X1, active(X2))) :28 -->_1 active^#(afterNth(N, XS)) -> c_27(U11^#(and(isNatural(N), isLNat(XS)), N, XS)) :27 -->_1 active^#(head(cons(N, XS))) -> c_26(U31^#(and(isNatural(N), isLNat(XS)), N)) :26 -->_1 active^#(head(X)) -> c_25(head^#(active(X))) :25 -->_1 active^#(U51(tt(), N, XS)) -> c_24(head^#(afterNth(N, XS))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 active^#(s(X)) -> c_22(s^#(active(X))) :22 -->_1 active^#(natsFrom(X)) -> c_21(natsFrom^#(active(X))) :21 -->_1 active^#(natsFrom(N)) -> c_20(U41^#(isNatural(N), N)) :20 -->_1 active^#(cons(X1, X2)) -> c_19(cons^#(active(X1), X2)) :19 -->_1 active^#(U41(tt(), N)) -> c_18(cons^#(N, natsFrom(s(N)))) :18 -->_1 active^#(U41(X1, X2)) -> c_17(U41^#(active(X1), X2)) :17 -->_1 active^#(U31(tt(), N)) -> c_16(N) :16 -->_1 active^#(U31(X1, X2)) -> c_15(U31^#(active(X1), X2)) :15 -->_1 active^#(U21(tt(), X)) -> c_14(X) :14 -->_1 active^#(U21(X1, X2)) -> c_13(U21^#(active(X1), X2)) :13 -->_1 active^#(snd(pair(X, Y))) -> c_12(U61^#(and(isLNat(X), isLNat(Y)), Y)) :12 -->_1 active^#(snd(X)) -> c_11(snd^#(active(X))) :11 -->_1 active^#(U11(tt(), N, XS)) -> c_10(snd^#(splitAt(N, XS))) :10 -->_1 active^#(U11(X1, X2, X3)) -> c_9(U11^#(active(X1), X2, X3)) :9 -->_1 active^#(splitAt(0(), XS)) -> c_8(U71^#(isLNat(XS), XS)) :8 -->_1 active^#(splitAt(s(N), cons(X, XS))) -> c_7(U81^#(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) :7 -->_1 active^#(splitAt(X1, X2)) -> c_6(splitAt^#(active(X1), X2)) :6 -->_1 active^#(splitAt(X1, X2)) -> c_5(splitAt^#(X1, active(X2))) :5 -->_1 active^#(fst(pair(X, Y))) -> c_4(U21^#(and(isLNat(X), isLNat(Y)), X)) :4 -->_1 active^#(fst(X)) -> c_3(fst^#(active(X))) :3 -->_1 active^#(U101(tt(), N, XS)) -> c_2(fst^#(splitAt(N, XS))) :2 -->_1 active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) :1 44: active^#(isNatural(s(V1))) -> c_44(isNatural^#(V1)) -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 45: active^#(isNatural(head(V1))) -> c_45(isLNat^#(V1)) -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 46: active^#(isNatural(0())) -> c_46() 47: active^#(isNatural(sel(V1, V2))) -> c_47(and^#(isNatural(V1), isLNat(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 48: active^#(isLNat(fst(V1))) -> c_48(isPLNat^#(V1)) -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 49: active^#(isLNat(snd(V1))) -> c_49(isPLNat^#(V1)) -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 50: active^#(isLNat(cons(V1, V2))) -> c_50(and^#(isNatural(V1), isLNat(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 51: active^#(isLNat(natsFrom(V1))) -> c_51(isNatural^#(V1)) -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 52: active^#(isLNat(afterNth(V1, V2))) -> c_52(and^#(isNatural(V1), isLNat(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 53: active^#(isLNat(nil())) -> c_53() 54: active^#(isLNat(tail(V1))) -> c_54(isLNat^#(V1)) -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 55: active^#(isLNat(take(V1, V2))) -> c_55(and^#(isNatural(V1), isLNat(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 56: active^#(isPLNat(splitAt(V1, V2))) -> c_56(and^#(isNatural(V1), isLNat(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 57: active^#(isPLNat(pair(V1, V2))) -> c_57(and^#(isLNat(V1), isLNat(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 58: active^#(tail(X)) -> c_58(tail^#(active(X))) -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 59: active^#(tail(cons(N, XS))) -> c_59(U91^#(and(isNatural(N), isLNat(XS)), XS)) -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 60: active^#(take(N, XS)) -> c_60(U101^#(and(isNatural(N), isLNat(XS)), N, XS)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 61: active^#(take(X1, X2)) -> c_61(take^#(X1, active(X2))) -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 62: active^#(take(X1, X2)) -> c_62(take^#(active(X1), X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 63: active^#(sel(N, XS)) -> c_63(U51^#(and(isNatural(N), isLNat(XS)), N, XS)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 64: active^#(sel(X1, X2)) -> c_64(sel^#(X1, active(X2))) -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 65: active^#(sel(X1, X2)) -> c_65(sel^#(active(X1), X2)) -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 66: U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 67: U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 68: fst^#(mark(X)) -> c_68(fst^#(X)) -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 69: fst^#(ok(X)) -> c_69(fst^#(X)) -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 70: U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 71: U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 72: splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 73: splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 74: splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 75: U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 76: U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 77: U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 78: U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 79: U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 80: U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 81: snd^#(mark(X)) -> c_75(snd^#(X)) -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 82: snd^#(ok(X)) -> c_76(snd^#(X)) -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 83: U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 84: U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 85: U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 86: U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 87: U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 88: U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 89: cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 90: cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 91: natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 92: natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 93: s^#(mark(X)) -> c_87(s^#(X)) -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 94: s^#(ok(X)) -> c_88(s^#(X)) -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 95: U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 96: U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 97: head^#(mark(X)) -> c_91(head^#(X)) -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 98: head^#(ok(X)) -> c_92(head^#(X)) -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 99: afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 100: afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 101: afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 102: pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 103: pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 104: pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 105: U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 106: U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 107: U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 108: U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 109: and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 110: and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 111: isNatural^#(ok(X)) -> c_111(isNatural^#(X)) -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 112: isLNat^#(ok(X)) -> c_112(isLNat^#(X)) -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 113: isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 114: tail^#(mark(X)) -> c_114(tail^#(X)) -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 115: tail^#(ok(X)) -> c_115(tail^#(X)) -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 116: take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 117: take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 118: take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 119: sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 120: sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 121: sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 122: proper^#(U101(X1, X2, X3)) -> c_122(U101^#(proper(X1), proper(X2), proper(X3))) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) :67 -->_1 U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) :66 123: proper^#(tt()) -> c_123() 124: proper^#(fst(X)) -> c_124(fst^#(proper(X))) -->_1 fst^#(ok(X)) -> c_69(fst^#(X)) :69 -->_1 fst^#(mark(X)) -> c_68(fst^#(X)) :68 125: proper^#(splitAt(X1, X2)) -> c_125(splitAt^#(proper(X1), proper(X2))) -->_1 splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) :74 -->_1 splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) :73 -->_1 splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) :72 126: proper^#(U11(X1, X2, X3)) -> c_126(U11^#(proper(X1), proper(X2), proper(X3))) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) :80 -->_1 U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) :79 127: proper^#(snd(X)) -> c_127(snd^#(proper(X))) -->_1 snd^#(ok(X)) -> c_76(snd^#(X)) :82 -->_1 snd^#(mark(X)) -> c_75(snd^#(X)) :81 128: proper^#(U21(X1, X2)) -> c_128(U21^#(proper(X1), proper(X2))) -->_1 U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) :71 -->_1 U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) :70 129: proper^#(U31(X1, X2)) -> c_129(U31^#(proper(X1), proper(X2))) -->_1 U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) :86 -->_1 U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) :85 130: proper^#(U41(X1, X2)) -> c_130(U41^#(proper(X1), proper(X2))) -->_1 U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) :88 -->_1 U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) :87 131: proper^#(cons(X1, X2)) -> c_131(cons^#(proper(X1), proper(X2))) -->_1 cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) :90 -->_1 cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) :89 132: proper^#(natsFrom(X)) -> c_132(natsFrom^#(proper(X))) -->_1 natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) :92 -->_1 natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) :91 133: proper^#(s(X)) -> c_133(s^#(proper(X))) -->_1 s^#(ok(X)) -> c_88(s^#(X)) :94 -->_1 s^#(mark(X)) -> c_87(s^#(X)) :93 134: proper^#(U51(X1, X2, X3)) -> c_134(U51^#(proper(X1), proper(X2), proper(X3))) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) :96 -->_1 U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) :95 135: proper^#(head(X)) -> c_135(head^#(proper(X))) -->_1 head^#(ok(X)) -> c_92(head^#(X)) :98 -->_1 head^#(mark(X)) -> c_91(head^#(X)) :97 136: proper^#(afterNth(X1, X2)) -> c_136(afterNth^#(proper(X1), proper(X2))) -->_1 afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) :101 -->_1 afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) :100 -->_1 afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) :99 137: proper^#(U61(X1, X2)) -> c_137(U61^#(proper(X1), proper(X2))) -->_1 U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) :84 -->_1 U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) :83 138: proper^#(U71(X1, X2)) -> c_138(U71^#(proper(X1), proper(X2))) -->_1 U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) :78 -->_1 U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) :77 139: proper^#(pair(X1, X2)) -> c_139(pair^#(proper(X1), proper(X2))) -->_1 pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) :104 -->_1 pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) :103 -->_1 pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) :102 140: proper^#(nil()) -> c_140() 141: proper^#(U81(X1, X2, X3, X4)) -> c_141(U81^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) :76 -->_1 U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) :75 142: proper^#(U82(X1, X2)) -> c_142(U82^#(proper(X1), proper(X2))) -->_1 U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) :106 -->_1 U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) :105 143: proper^#(U91(X1, X2)) -> c_143(U91^#(proper(X1), proper(X2))) -->_1 U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) :108 -->_1 U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) :107 144: proper^#(and(X1, X2)) -> c_144(and^#(proper(X1), proper(X2))) -->_1 and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) :110 -->_1 and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) :109 145: proper^#(isNatural(X)) -> c_145(isNatural^#(proper(X))) -->_1 isNatural^#(ok(X)) -> c_111(isNatural^#(X)) :111 146: proper^#(isLNat(X)) -> c_146(isLNat^#(proper(X))) -->_1 isLNat^#(ok(X)) -> c_112(isLNat^#(X)) :112 147: proper^#(isPLNat(X)) -> c_147(isPLNat^#(proper(X))) -->_1 isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) :113 148: proper^#(tail(X)) -> c_148(tail^#(proper(X))) -->_1 tail^#(ok(X)) -> c_115(tail^#(X)) :115 -->_1 tail^#(mark(X)) -> c_114(tail^#(X)) :114 149: proper^#(take(X1, X2)) -> c_149(take^#(proper(X1), proper(X2))) -->_1 take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) :118 -->_1 take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) :117 -->_1 take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) :116 150: proper^#(0()) -> c_150() 151: proper^#(sel(X1, X2)) -> c_151(sel^#(proper(X1), proper(X2))) -->_1 sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) :121 -->_1 sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) :120 -->_1 sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) :119 152: top^#(mark(X)) -> c_152(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 153: top^#(ok(X)) -> c_153(top^#(active(X))) -->_1 top^#(ok(X)) -> c_153(top^#(active(X))) :153 -->_1 top^#(mark(X)) -> c_152(top^#(proper(X))) :152 Only the nodes {66,67,68,69,70,71,72,74,73,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,101,100,102,104,103,105,106,107,108,109,110,111,112,113,114,115,116,118,117,119,121,120,123,140,150,152,153} are reachable from nodes {66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,123,140,150,152,153} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) , fst^#(mark(X)) -> c_68(fst^#(X)) , fst^#(ok(X)) -> c_69(fst^#(X)) , U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) , splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) , splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) , splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) , U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) , U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) , U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) , U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) , snd^#(mark(X)) -> c_75(snd^#(X)) , snd^#(ok(X)) -> c_76(snd^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) , cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) , natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) , natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) , s^#(mark(X)) -> c_87(s^#(X)) , s^#(ok(X)) -> c_88(s^#(X)) , U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) , head^#(mark(X)) -> c_91(head^#(X)) , head^#(ok(X)) -> c_92(head^#(X)) , afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) , afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) , afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) , pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) , pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) , pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) , U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) , U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) , and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) , isNatural^#(ok(X)) -> c_111(isNatural^#(X)) , isLNat^#(ok(X)) -> c_112(isLNat^#(X)) , isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) , tail^#(mark(X)) -> c_114(tail^#(X)) , tail^#(ok(X)) -> c_115(tail^#(X)) , take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) , sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) , sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) , sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) , proper^#(tt()) -> c_123() , proper^#(nil()) -> c_140() , proper^#(0()) -> c_150() , top^#(mark(X)) -> c_152(top^#(proper(X))) , top^#(ok(X)) -> c_153(top^#(active(X))) } Strict Trs: { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), N, XS)) -> mark(fst(splitAt(N, XS))) , active(fst(X)) -> fst(active(X)) , active(fst(pair(X, Y))) -> mark(U21(and(isLNat(X), isLNat(Y)), X)) , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) , active(splitAt(s(N), cons(X, XS))) -> mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) , active(splitAt(0(), XS)) -> mark(U71(isLNat(XS), XS)) , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))) , active(snd(X)) -> snd(active(X)) , active(snd(pair(X, Y))) -> mark(U61(and(isLNat(X), isLNat(Y)), Y)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), X)) -> mark(X) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), N)) -> mark(N) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(cons(N, natsFrom(s(N)))) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(natsFrom(N)) -> mark(U41(isNatural(N), N)) , active(natsFrom(X)) -> natsFrom(active(X)) , active(s(X)) -> s(active(X)) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), N, XS)) -> mark(head(afterNth(N, XS))) , active(head(X)) -> head(active(X)) , active(head(cons(N, XS))) -> mark(U31(and(isNatural(N), isLNat(XS)), N)) , active(afterNth(N, XS)) -> mark(U11(and(isNatural(N), isLNat(XS)), N, XS)) , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), Y)) -> mark(Y) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), XS)) -> mark(pair(nil(), XS)) , active(pair(X1, X2)) -> pair(X1, active(X2)) , active(pair(X1, X2)) -> pair(active(X1), X2) , active(U81(X1, X2, X3, X4)) -> U81(active(X1), X2, X3, X4) , active(U81(tt(), N, X, XS)) -> mark(U82(splitAt(N, XS), X)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), XS)) -> mark(XS) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatural(s(V1))) -> mark(isNatural(V1)) , active(isNatural(head(V1))) -> mark(isLNat(V1)) , active(isNatural(0())) -> mark(tt()) , active(isNatural(sel(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(fst(V1))) -> mark(isPLNat(V1)) , active(isLNat(snd(V1))) -> mark(isPLNat(V1)) , active(isLNat(cons(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)) , active(isLNat(afterNth(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(nil())) -> mark(tt()) , active(isLNat(tail(V1))) -> mark(isLNat(V1)) , active(isLNat(take(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(splitAt(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(pair(V1, V2))) -> mark(and(isLNat(V1), isLNat(V2))) , active(tail(X)) -> tail(active(X)) , active(tail(cons(N, XS))) -> mark(U91(and(isNatural(N), isLNat(XS)), XS)) , active(take(N, XS)) -> mark(U101(and(isNatural(N), isLNat(XS)), N, XS)) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(sel(N, XS)) -> mark(U51(and(isNatural(N), isLNat(XS)), N, XS)) , active(sel(X1, X2)) -> sel(X1, active(X2)) , active(sel(X1, X2)) -> sel(active(X1), X2) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , fst(mark(X)) -> mark(fst(X)) , fst(ok(X)) -> ok(fst(X)) , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , snd(mark(X)) -> mark(snd(X)) , snd(ok(X)) -> ok(snd(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , natsFrom(mark(X)) -> mark(natsFrom(X)) , natsFrom(ok(X)) -> ok(natsFrom(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , pair(X1, mark(X2)) -> mark(pair(X1, X2)) , pair(mark(X1), X2) -> mark(pair(X1, X2)) , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) , U81(mark(X1), X2, X3, X4) -> mark(U81(X1, X2, X3, X4)) , U81(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U81(X1, X2, X3, X4)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatural(ok(X)) -> ok(isNatural(X)) , isLNat(ok(X)) -> ok(isLNat(X)) , isPLNat(ok(X)) -> ok(isPLNat(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , sel(X1, mark(X2)) -> mark(sel(X1, X2)) , sel(mark(X1), X2) -> mark(sel(X1, X2)) , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(fst(X)) -> fst(proper(X)) , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(snd(X)) -> snd(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(natsFrom(X)) -> natsFrom(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(head(X)) -> head(proper(X)) , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U81(X1, X2, X3, X4)) -> U81(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatural(X)) -> isNatural(proper(X)) , proper(isLNat(X)) -> isLNat(proper(X)) , proper(isPLNat(X)) -> isPLNat(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {57,58,59} by applications of Pre({57,58,59}) = {}. Here rules are labeled as follows: DPs: { 1: U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) , 2: U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) , 3: fst^#(mark(X)) -> c_68(fst^#(X)) , 4: fst^#(ok(X)) -> c_69(fst^#(X)) , 5: U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) , 6: U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) , 7: splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) , 8: splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) , 9: splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) , 10: U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) , 11: U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) , 12: U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) , 13: U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) , 14: U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) , 15: U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) , 16: snd^#(mark(X)) -> c_75(snd^#(X)) , 17: snd^#(ok(X)) -> c_76(snd^#(X)) , 18: U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , 19: U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , 20: U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , 21: U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , 22: U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) , 23: U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) , 24: cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) , 25: cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) , 26: natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) , 27: natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) , 28: s^#(mark(X)) -> c_87(s^#(X)) , 29: s^#(ok(X)) -> c_88(s^#(X)) , 30: U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) , 31: U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) , 32: head^#(mark(X)) -> c_91(head^#(X)) , 33: head^#(ok(X)) -> c_92(head^#(X)) , 34: afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) , 35: afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) , 36: afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) , 37: pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) , 38: pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) , 39: pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) , 40: U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) , 41: U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) , 42: U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) , 43: U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) , 44: and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) , 45: and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) , 46: isNatural^#(ok(X)) -> c_111(isNatural^#(X)) , 47: isLNat^#(ok(X)) -> c_112(isLNat^#(X)) , 48: isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) , 49: tail^#(mark(X)) -> c_114(tail^#(X)) , 50: tail^#(ok(X)) -> c_115(tail^#(X)) , 51: take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) , 52: take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) , 53: take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) , 54: sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) , 55: sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) , 56: sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) , 57: proper^#(tt()) -> c_123() , 58: proper^#(nil()) -> c_140() , 59: proper^#(0()) -> c_150() , 60: top^#(mark(X)) -> c_152(top^#(proper(X))) , 61: top^#(ok(X)) -> c_153(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(mark(X1), X2, X3) -> c_66(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_67(U101^#(X1, X2, X3)) , fst^#(mark(X)) -> c_68(fst^#(X)) , fst^#(ok(X)) -> c_69(fst^#(X)) , U21^#(mark(X1), X2) -> c_77(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_78(U21^#(X1, X2)) , splitAt^#(X1, mark(X2)) -> c_70(splitAt^#(X1, X2)) , splitAt^#(mark(X1), X2) -> c_71(splitAt^#(X1, X2)) , splitAt^#(ok(X1), ok(X2)) -> c_72(splitAt^#(X1, X2)) , U81^#(mark(X1), X2, X3, X4) -> c_103(U81^#(X1, X2, X3, X4)) , U81^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_104(U81^#(X1, X2, X3, X4)) , U71^#(mark(X1), X2) -> c_98(U71^#(X1, X2)) , U71^#(ok(X1), ok(X2)) -> c_99(U71^#(X1, X2)) , U11^#(mark(X1), X2, X3) -> c_73(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_74(U11^#(X1, X2, X3)) , snd^#(mark(X)) -> c_75(snd^#(X)) , snd^#(ok(X)) -> c_76(snd^#(X)) , U61^#(mark(X1), X2) -> c_96(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_97(U61^#(X1, X2)) , U31^#(mark(X1), X2) -> c_79(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_80(U31^#(X1, X2)) , U41^#(mark(X1), X2) -> c_81(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_82(U41^#(X1, X2)) , cons^#(mark(X1), X2) -> c_83(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_84(cons^#(X1, X2)) , natsFrom^#(mark(X)) -> c_85(natsFrom^#(X)) , natsFrom^#(ok(X)) -> c_86(natsFrom^#(X)) , s^#(mark(X)) -> c_87(s^#(X)) , s^#(ok(X)) -> c_88(s^#(X)) , U51^#(mark(X1), X2, X3) -> c_89(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_90(U51^#(X1, X2, X3)) , head^#(mark(X)) -> c_91(head^#(X)) , head^#(ok(X)) -> c_92(head^#(X)) , afterNth^#(X1, mark(X2)) -> c_93(afterNth^#(X1, X2)) , afterNth^#(mark(X1), X2) -> c_94(afterNth^#(X1, X2)) , afterNth^#(ok(X1), ok(X2)) -> c_95(afterNth^#(X1, X2)) , pair^#(X1, mark(X2)) -> c_100(pair^#(X1, X2)) , pair^#(mark(X1), X2) -> c_101(pair^#(X1, X2)) , pair^#(ok(X1), ok(X2)) -> c_102(pair^#(X1, X2)) , U82^#(mark(X1), X2) -> c_105(U82^#(X1, X2)) , U82^#(ok(X1), ok(X2)) -> c_106(U82^#(X1, X2)) , U91^#(mark(X1), X2) -> c_107(U91^#(X1, X2)) , U91^#(ok(X1), ok(X2)) -> c_108(U91^#(X1, X2)) , and^#(mark(X1), X2) -> c_109(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_110(and^#(X1, X2)) , isNatural^#(ok(X)) -> c_111(isNatural^#(X)) , isLNat^#(ok(X)) -> c_112(isLNat^#(X)) , isPLNat^#(ok(X)) -> c_113(isPLNat^#(X)) , tail^#(mark(X)) -> c_114(tail^#(X)) , tail^#(ok(X)) -> c_115(tail^#(X)) , take^#(X1, mark(X2)) -> c_116(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_117(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_118(take^#(X1, X2)) , sel^#(X1, mark(X2)) -> c_119(sel^#(X1, X2)) , sel^#(mark(X1), X2) -> c_120(sel^#(X1, X2)) , sel^#(ok(X1), ok(X2)) -> c_121(sel^#(X1, X2)) , top^#(mark(X)) -> c_152(top^#(proper(X))) , top^#(ok(X)) -> c_153(top^#(active(X))) } Strict Trs: { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), N, XS)) -> mark(fst(splitAt(N, XS))) , active(fst(X)) -> fst(active(X)) , active(fst(pair(X, Y))) -> mark(U21(and(isLNat(X), isLNat(Y)), X)) , active(splitAt(X1, X2)) -> splitAt(X1, active(X2)) , active(splitAt(X1, X2)) -> splitAt(active(X1), X2) , active(splitAt(s(N), cons(X, XS))) -> mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)) , active(splitAt(0(), XS)) -> mark(U71(isLNat(XS), XS)) , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))) , active(snd(X)) -> snd(active(X)) , active(snd(pair(X, Y))) -> mark(U61(and(isLNat(X), isLNat(Y)), Y)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), X)) -> mark(X) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), N)) -> mark(N) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(cons(N, natsFrom(s(N)))) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(natsFrom(N)) -> mark(U41(isNatural(N), N)) , active(natsFrom(X)) -> natsFrom(active(X)) , active(s(X)) -> s(active(X)) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), N, XS)) -> mark(head(afterNth(N, XS))) , active(head(X)) -> head(active(X)) , active(head(cons(N, XS))) -> mark(U31(and(isNatural(N), isLNat(XS)), N)) , active(afterNth(N, XS)) -> mark(U11(and(isNatural(N), isLNat(XS)), N, XS)) , active(afterNth(X1, X2)) -> afterNth(X1, active(X2)) , active(afterNth(X1, X2)) -> afterNth(active(X1), X2) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), Y)) -> mark(Y) , active(U71(X1, X2)) -> U71(active(X1), X2) , active(U71(tt(), XS)) -> mark(pair(nil(), XS)) , active(pair(X1, X2)) -> pair(X1, active(X2)) , active(pair(X1, X2)) -> pair(active(X1), X2) , active(U81(X1, X2, X3, X4)) -> U81(active(X1), X2, X3, X4) , active(U81(tt(), N, X, XS)) -> mark(U82(splitAt(N, XS), X)) , active(U82(X1, X2)) -> U82(active(X1), X2) , active(U82(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)) , active(U91(X1, X2)) -> U91(active(X1), X2) , active(U91(tt(), XS)) -> mark(XS) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatural(s(V1))) -> mark(isNatural(V1)) , active(isNatural(head(V1))) -> mark(isLNat(V1)) , active(isNatural(0())) -> mark(tt()) , active(isNatural(sel(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(fst(V1))) -> mark(isPLNat(V1)) , active(isLNat(snd(V1))) -> mark(isPLNat(V1)) , active(isLNat(cons(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)) , active(isLNat(afterNth(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isLNat(nil())) -> mark(tt()) , active(isLNat(tail(V1))) -> mark(isLNat(V1)) , active(isLNat(take(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(splitAt(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))) , active(isPLNat(pair(V1, V2))) -> mark(and(isLNat(V1), isLNat(V2))) , active(tail(X)) -> tail(active(X)) , active(tail(cons(N, XS))) -> mark(U91(and(isNatural(N), isLNat(XS)), XS)) , active(take(N, XS)) -> mark(U101(and(isNatural(N), isLNat(XS)), N, XS)) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(sel(N, XS)) -> mark(U51(and(isNatural(N), isLNat(XS)), N, XS)) , active(sel(X1, X2)) -> sel(X1, active(X2)) , active(sel(X1, X2)) -> sel(active(X1), X2) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , fst(mark(X)) -> mark(fst(X)) , fst(ok(X)) -> ok(fst(X)) , splitAt(X1, mark(X2)) -> mark(splitAt(X1, X2)) , splitAt(mark(X1), X2) -> mark(splitAt(X1, X2)) , splitAt(ok(X1), ok(X2)) -> ok(splitAt(X1, X2)) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , snd(mark(X)) -> mark(snd(X)) , snd(ok(X)) -> ok(snd(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , natsFrom(mark(X)) -> mark(natsFrom(X)) , natsFrom(ok(X)) -> ok(natsFrom(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , afterNth(X1, mark(X2)) -> mark(afterNth(X1, X2)) , afterNth(mark(X1), X2) -> mark(afterNth(X1, X2)) , afterNth(ok(X1), ok(X2)) -> ok(afterNth(X1, X2)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U71(mark(X1), X2) -> mark(U71(X1, X2)) , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) , pair(X1, mark(X2)) -> mark(pair(X1, X2)) , pair(mark(X1), X2) -> mark(pair(X1, X2)) , pair(ok(X1), ok(X2)) -> ok(pair(X1, X2)) , U81(mark(X1), X2, X3, X4) -> mark(U81(X1, X2, X3, X4)) , U81(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U81(X1, X2, X3, X4)) , U82(mark(X1), X2) -> mark(U82(X1, X2)) , U82(ok(X1), ok(X2)) -> ok(U82(X1, X2)) , U91(mark(X1), X2) -> mark(U91(X1, X2)) , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatural(ok(X)) -> ok(isNatural(X)) , isLNat(ok(X)) -> ok(isLNat(X)) , isPLNat(ok(X)) -> ok(isPLNat(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , sel(X1, mark(X2)) -> mark(sel(X1, X2)) , sel(mark(X1), X2) -> mark(sel(X1, X2)) , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(fst(X)) -> fst(proper(X)) , proper(splitAt(X1, X2)) -> splitAt(proper(X1), proper(X2)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(snd(X)) -> snd(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(natsFrom(X)) -> natsFrom(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(head(X)) -> head(proper(X)) , proper(afterNth(X1, X2)) -> afterNth(proper(X1), proper(X2)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) , proper(pair(X1, X2)) -> pair(proper(X1), proper(X2)) , proper(nil()) -> ok(nil()) , proper(U81(X1, X2, X3, X4)) -> U81(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U82(X1, X2)) -> U82(proper(X1), proper(X2)) , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatural(X)) -> isNatural(proper(X)) , proper(isLNat(X)) -> isLNat(proper(X)) , proper(isPLNat(X)) -> isPLNat(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { proper^#(tt()) -> c_123() , proper^#(nil()) -> c_140() , proper^#(0()) -> c_150() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..