MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { U101(tt(), V2) -> U102(isLNat(activate(V2))) , U102(tt()) -> tt() , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(isNatural(activate(V1)), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(isNatural(activate(V1)), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) , isLNat(n__take(V1, V2)) -> U101(isNatural(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__fst(X)) -> fst(X) , activate(n__snd(X)) -> snd(X) , activate(n__tail(X)) -> tail(X) , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(X) , activate(n__s(X)) -> s(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__pair(X1, X2)) -> pair(X1, X2) , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2) , U11(tt(), N, XS) -> U12(isLNat(activate(XS)), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , U111(tt()) -> tt() , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(isLNat(X), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(XS)) , splitAt(0(), XS) -> U191(isLNat(XS), XS) , U121(tt()) -> tt() , U131(tt(), V2) -> U132(isLNat(activate(V2))) , U132(tt()) -> tt() , U141(tt(), V2) -> U142(isLNat(activate(V2))) , U142(tt()) -> tt() , U151(tt(), V2) -> U152(isLNat(activate(V2))) , U152(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , s(X) -> n__s(X) , U171(tt(), N, XS) -> U172(isLNat(activate(XS)), activate(N), activate(XS)) , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) , afterNth(N, XS) -> U11(isNatural(N), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) , U182(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) , U202(tt(), N, X, XS) -> U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__sel(V1, V2)) -> U131(isNatural(activate(V1)), activate(V2)) , U203(tt(), N, X, XS) -> U204(splitAt(activate(N), activate(XS)), activate(X)) , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) , U22(tt(), X) -> activate(X) , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) , U212(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> U222(isLNat(activate(XS)), activate(N), activate(XS)) , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), V2) -> U42(isLNat(activate(V2))) , U42(tt()) -> tt() , U51(tt(), V2) -> U52(isLNat(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(isLNat(activate(V1)), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(isNatural(activate(V1)), activate(V2)) , natsFrom(N) -> U161(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(isNatural(N), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) , take(N, XS) -> U221(isNatural(N), N, XS) , take(X1, X2) -> n__take(X1, X2) } 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) '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 minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 2) '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 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , U102^#(tt()) -> c_2() , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , isLNat^#(n__nil()) -> c_4() , isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , U71^#(tt()) -> c_78() , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_77() , U81^#(tt()) -> c_79() , U91^#(tt()) -> c_80() , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , activate^#(n__fst(X)) -> c_16(fst^#(X)) , activate^#(n__snd(X)) -> c_17(snd^#(X)) , activate^#(n__tail(X)) -> c_18(tail^#(X)) , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , activate^#(n__0()) -> c_20(0^#()) , activate^#(n__head(X)) -> c_21(head^#(X)) , activate^#(n__s(X)) -> c_22(s^#(X)) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_84(X) , nil^#() -> c_54() , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_49(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_69(X) , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , snd^#(X) -> c_29(X) , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , tail^#(X) -> c_88(X) , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , take^#(X1, X2) -> c_91(X1, X2) , 0^#() -> c_87() , head^#(X) -> c_46(X) , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , s^#(X) -> c_43(X) , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_86(X1, X2) , pair^#(X1, X2) -> c_53(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , U111^#(tt()) -> c_28() , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , U121^#(tt()) -> c_34() , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , U132^#(tt()) -> c_36() , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , U142^#(tt()) -> c_38() , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , U152^#(tt()) -> c_40() , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_51(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_64(activate^#(X)) , U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_66(activate^#(XS)) , U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_72(activate^#(N)) , U42^#(tt()) -> c_74() , U52^#(tt()) -> c_76() , isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , U102^#(tt()) -> c_2() , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , isLNat^#(n__nil()) -> c_4() , isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , U71^#(tt()) -> c_78() , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_77() , U81^#(tt()) -> c_79() , U91^#(tt()) -> c_80() , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , activate^#(n__fst(X)) -> c_16(fst^#(X)) , activate^#(n__snd(X)) -> c_17(snd^#(X)) , activate^#(n__tail(X)) -> c_18(tail^#(X)) , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , activate^#(n__0()) -> c_20(0^#()) , activate^#(n__head(X)) -> c_21(head^#(X)) , activate^#(n__s(X)) -> c_22(s^#(X)) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_84(X) , nil^#() -> c_54() , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_49(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_69(X) , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , snd^#(X) -> c_29(X) , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , tail^#(X) -> c_88(X) , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , take^#(X1, X2) -> c_91(X1, X2) , 0^#() -> c_87() , head^#(X) -> c_46(X) , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , s^#(X) -> c_43(X) , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_86(X1, X2) , pair^#(X1, X2) -> c_53(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , U111^#(tt()) -> c_28() , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , U121^#(tt()) -> c_34() , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , U132^#(tt()) -> c_36() , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , U142^#(tt()) -> c_38() , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , U152^#(tt()) -> c_40() , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_51(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_64(activate^#(X)) , U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_66(activate^#(XS)) , U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_72(activate^#(N)) , U42^#(tt()) -> c_74() , U52^#(tt()) -> c_76() , isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) } Strict Trs: { U101(tt(), V2) -> U102(isLNat(activate(V2))) , U102(tt()) -> tt() , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(isNatural(activate(V1)), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(isNatural(activate(V1)), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) , isLNat(n__take(V1, V2)) -> U101(isNatural(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__fst(X)) -> fst(X) , activate(n__snd(X)) -> snd(X) , activate(n__tail(X)) -> tail(X) , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(X) , activate(n__s(X)) -> s(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__pair(X1, X2)) -> pair(X1, X2) , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2) , U11(tt(), N, XS) -> U12(isLNat(activate(XS)), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , U111(tt()) -> tt() , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(isLNat(X), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(XS)) , splitAt(0(), XS) -> U191(isLNat(XS), XS) , U121(tt()) -> tt() , U131(tt(), V2) -> U132(isLNat(activate(V2))) , U132(tt()) -> tt() , U141(tt(), V2) -> U142(isLNat(activate(V2))) , U142(tt()) -> tt() , U151(tt(), V2) -> U152(isLNat(activate(V2))) , U152(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , s(X) -> n__s(X) , U171(tt(), N, XS) -> U172(isLNat(activate(XS)), activate(N), activate(XS)) , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) , afterNth(N, XS) -> U11(isNatural(N), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) , U182(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) , U202(tt(), N, X, XS) -> U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__sel(V1, V2)) -> U131(isNatural(activate(V1)), activate(V2)) , U203(tt(), N, X, XS) -> U204(splitAt(activate(N), activate(XS)), activate(X)) , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) , U22(tt(), X) -> activate(X) , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) , U212(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> U222(isLNat(activate(XS)), activate(N), activate(XS)) , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), V2) -> U42(isLNat(activate(V2))) , U42(tt()) -> tt() , U51(tt(), V2) -> U52(isLNat(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(isLNat(activate(V1)), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(isNatural(activate(V1)), activate(V2)) , natsFrom(N) -> U161(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(isNatural(N), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) , take(N, XS) -> U221(isNatural(N), N, XS) , take(X1, X2) -> n__take(X1, X2) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,4,11,14,15,16,34,46,58,62,64,66,68,76,88,89} by applications of Pre({2,4,11,14,15,16,34,46,58,62,64,66,68,76,88,89}) = {1,3,7,8,9,12,13,17,19,26,33,36,37,38,40,42,45,47,49,51,52,53,63,65,67,77,78}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , 2: U102^#(tt()) -> c_2() , 3: isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , 4: isLNat^#(n__nil()) -> c_4() , 5: isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , 6: isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , 7: isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , 8: isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , 9: isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , 10: isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , 11: U71^#(tt()) -> c_78() , 12: U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , 13: U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , 14: U61^#(tt()) -> c_77() , 15: U81^#(tt()) -> c_79() , 16: U91^#(tt()) -> c_80() , 17: activate^#(X) -> c_11(X) , 18: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , 19: activate^#(n__nil()) -> c_13(nil^#()) , 20: activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , 21: activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , 22: activate^#(n__fst(X)) -> c_16(fst^#(X)) , 23: activate^#(n__snd(X)) -> c_17(snd^#(X)) , 24: activate^#(n__tail(X)) -> c_18(tail^#(X)) , 25: activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , 26: activate^#(n__0()) -> c_20(0^#()) , 27: activate^#(n__head(X)) -> c_21(head^#(X)) , 28: activate^#(n__s(X)) -> c_22(s^#(X)) , 29: activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , 30: activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , 31: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , 32: natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , 33: natsFrom^#(X) -> c_84(X) , 34: nil^#() -> c_54() , 35: afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , 36: afterNth^#(X1, X2) -> c_49(X1, X2) , 37: cons^#(X1, X2) -> c_42(X1, X2) , 38: fst^#(X) -> c_69(X) , 39: fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , 40: snd^#(X) -> c_29(X) , 41: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , 42: tail^#(X) -> c_88(X) , 43: tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , 44: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , 45: take^#(X1, X2) -> c_91(X1, X2) , 46: 0^#() -> c_87() , 47: head^#(X) -> c_46(X) , 48: head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , 49: s^#(X) -> c_43(X) , 50: sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , 51: sel^#(X1, X2) -> c_86(X1, X2) , 52: pair^#(X1, X2) -> c_53(X1, X2) , 53: splitAt^#(X1, X2) -> c_31(X1, X2) , 54: splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , 55: splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , 56: U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , 57: U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , 58: U111^#(tt()) -> c_28() , 59: U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , 60: U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , 61: U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , 62: U121^#(tt()) -> c_34() , 63: U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , 64: U132^#(tt()) -> c_36() , 65: U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , 66: U142^#(tt()) -> c_38() , 67: U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , 68: U152^#(tt()) -> c_40() , 69: U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , 70: U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , 71: U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , 72: U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , 73: U182^#(tt(), Y) -> c_51(activate^#(Y)) , 74: U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , 75: U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , 76: isNatural^#(n__0()) -> c_57() , 77: isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , 78: isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , 79: isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , 80: U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , 81: U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , 82: U22^#(tt(), X) -> c_64(activate^#(X)) , 83: U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , 84: U212^#(tt(), XS) -> c_66(activate^#(XS)) , 85: U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , 86: U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , 87: U32^#(tt(), N) -> c_72(activate^#(N)) , 88: U42^#(tt()) -> c_74() , 89: U52^#(tt()) -> c_76() , 90: isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , 91: isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , activate^#(n__fst(X)) -> c_16(fst^#(X)) , activate^#(n__snd(X)) -> c_17(snd^#(X)) , activate^#(n__tail(X)) -> c_18(tail^#(X)) , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , activate^#(n__0()) -> c_20(0^#()) , activate^#(n__head(X)) -> c_21(head^#(X)) , activate^#(n__s(X)) -> c_22(s^#(X)) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_84(X) , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_49(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_69(X) , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , snd^#(X) -> c_29(X) , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , tail^#(X) -> c_88(X) , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , take^#(X1, X2) -> c_91(X1, X2) , head^#(X) -> c_46(X) , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , s^#(X) -> c_43(X) , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_86(X1, X2) , pair^#(X1, X2) -> c_53(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_51(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_64(activate^#(X)) , U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_66(activate^#(XS)) , U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_72(activate^#(N)) , isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) } Strict Trs: { U101(tt(), V2) -> U102(isLNat(activate(V2))) , U102(tt()) -> tt() , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(isNatural(activate(V1)), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(isNatural(activate(V1)), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) , isLNat(n__take(V1, V2)) -> U101(isNatural(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__fst(X)) -> fst(X) , activate(n__snd(X)) -> snd(X) , activate(n__tail(X)) -> tail(X) , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(X) , activate(n__s(X)) -> s(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__pair(X1, X2)) -> pair(X1, X2) , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2) , U11(tt(), N, XS) -> U12(isLNat(activate(XS)), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , U111(tt()) -> tt() , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(isLNat(X), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(XS)) , splitAt(0(), XS) -> U191(isLNat(XS), XS) , U121(tt()) -> tt() , U131(tt(), V2) -> U132(isLNat(activate(V2))) , U132(tt()) -> tt() , U141(tt(), V2) -> U142(isLNat(activate(V2))) , U142(tt()) -> tt() , U151(tt(), V2) -> U152(isLNat(activate(V2))) , U152(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , s(X) -> n__s(X) , U171(tt(), N, XS) -> U172(isLNat(activate(XS)), activate(N), activate(XS)) , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) , afterNth(N, XS) -> U11(isNatural(N), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) , U182(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) , U202(tt(), N, X, XS) -> U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__sel(V1, V2)) -> U131(isNatural(activate(V1)), activate(V2)) , U203(tt(), N, X, XS) -> U204(splitAt(activate(N), activate(XS)), activate(X)) , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) , U22(tt(), X) -> activate(X) , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) , U212(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> U222(isLNat(activate(XS)), activate(N), activate(XS)) , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), V2) -> U42(isLNat(activate(V2))) , U42(tt()) -> tt() , U51(tt(), V2) -> U52(isLNat(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(isLNat(activate(V1)), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(isNatural(activate(V1)), activate(V2)) , natsFrom(N) -> U161(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(isNatural(N), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) , take(N, XS) -> U221(isNatural(N), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U102^#(tt()) -> c_2() , isLNat^#(n__nil()) -> c_4() , U71^#(tt()) -> c_78() , U61^#(tt()) -> c_77() , U81^#(tt()) -> c_79() , U91^#(tt()) -> c_80() , nil^#() -> c_54() , 0^#() -> c_87() , U111^#(tt()) -> c_28() , U121^#(tt()) -> c_34() , U132^#(tt()) -> c_36() , U142^#(tt()) -> c_38() , U152^#(tt()) -> c_40() , isNatural^#(n__0()) -> c_57() , U42^#(tt()) -> c_74() , U52^#(tt()) -> c_76() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,5,6,7,9,10,13,20,53,54,55,63,64} by applications of Pre({1,2,5,6,7,9,10,13,20,53,54,55,63,64}) = {3,4,8,11,27,29,30,31,33,35,38,39,41,43,44,45,60,65,68,70,73,74,75}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , 2: isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , 3: isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , 4: isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , 5: isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , 6: isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , 7: isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , 8: isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , 9: U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , 10: U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , 11: activate^#(X) -> c_11(X) , 12: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , 13: activate^#(n__nil()) -> c_13(nil^#()) , 14: activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , 15: activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , 16: activate^#(n__fst(X)) -> c_16(fst^#(X)) , 17: activate^#(n__snd(X)) -> c_17(snd^#(X)) , 18: activate^#(n__tail(X)) -> c_18(tail^#(X)) , 19: activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , 20: activate^#(n__0()) -> c_20(0^#()) , 21: activate^#(n__head(X)) -> c_21(head^#(X)) , 22: activate^#(n__s(X)) -> c_22(s^#(X)) , 23: activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , 24: activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , 25: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , 26: natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , 27: natsFrom^#(X) -> c_84(X) , 28: afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , 29: afterNth^#(X1, X2) -> c_49(X1, X2) , 30: cons^#(X1, X2) -> c_42(X1, X2) , 31: fst^#(X) -> c_69(X) , 32: fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , 33: snd^#(X) -> c_29(X) , 34: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , 35: tail^#(X) -> c_88(X) , 36: tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , 37: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , 38: take^#(X1, X2) -> c_91(X1, X2) , 39: head^#(X) -> c_46(X) , 40: head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , 41: s^#(X) -> c_43(X) , 42: sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , 43: sel^#(X1, X2) -> c_86(X1, X2) , 44: pair^#(X1, X2) -> c_53(X1, X2) , 45: splitAt^#(X1, X2) -> c_31(X1, X2) , 46: splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , 47: splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , 48: U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , 49: U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , 50: U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , 51: U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , 52: U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , 53: U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , 54: U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , 55: U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , 56: U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , 57: U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , 58: U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , 59: U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , 60: U182^#(tt(), Y) -> c_51(activate^#(Y)) , 61: U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , 62: U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , 63: isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , 64: isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , 65: isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , 66: U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , 67: U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , 68: U22^#(tt(), X) -> c_64(activate^#(X)) , 69: U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , 70: U212^#(tt(), XS) -> c_66(activate^#(XS)) , 71: U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , 72: U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , 73: U32^#(tt(), N) -> c_72(activate^#(N)) , 74: isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , 75: isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) , 76: U102^#(tt()) -> c_2() , 77: isLNat^#(n__nil()) -> c_4() , 78: U71^#(tt()) -> c_78() , 79: U61^#(tt()) -> c_77() , 80: U81^#(tt()) -> c_79() , 81: U91^#(tt()) -> c_80() , 82: nil^#() -> c_54() , 83: 0^#() -> c_87() , 84: U111^#(tt()) -> c_28() , 85: U121^#(tt()) -> c_34() , 86: U132^#(tt()) -> c_36() , 87: U142^#(tt()) -> c_38() , 88: U152^#(tt()) -> c_40() , 89: isNatural^#(n__0()) -> c_57() , 90: U42^#(tt()) -> c_74() , 91: U52^#(tt()) -> c_76() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , activate^#(n__fst(X)) -> c_16(fst^#(X)) , activate^#(n__snd(X)) -> c_17(snd^#(X)) , activate^#(n__tail(X)) -> c_18(tail^#(X)) , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , activate^#(n__head(X)) -> c_21(head^#(X)) , activate^#(n__s(X)) -> c_22(s^#(X)) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_84(X) , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_49(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_69(X) , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , snd^#(X) -> c_29(X) , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , tail^#(X) -> c_88(X) , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , take^#(X1, X2) -> c_91(X1, X2) , head^#(X) -> c_46(X) , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , s^#(X) -> c_43(X) , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_86(X1, X2) , pair^#(X1, X2) -> c_53(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_51(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_64(activate^#(X)) , U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_66(activate^#(XS)) , U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_72(activate^#(N)) , isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) } Strict Trs: { U101(tt(), V2) -> U102(isLNat(activate(V2))) , U102(tt()) -> tt() , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(isNatural(activate(V1)), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(isNatural(activate(V1)), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) , isLNat(n__take(V1, V2)) -> U101(isNatural(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__fst(X)) -> fst(X) , activate(n__snd(X)) -> snd(X) , activate(n__tail(X)) -> tail(X) , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(X) , activate(n__s(X)) -> s(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__pair(X1, X2)) -> pair(X1, X2) , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2) , U11(tt(), N, XS) -> U12(isLNat(activate(XS)), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , U111(tt()) -> tt() , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(isLNat(X), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(XS)) , splitAt(0(), XS) -> U191(isLNat(XS), XS) , U121(tt()) -> tt() , U131(tt(), V2) -> U132(isLNat(activate(V2))) , U132(tt()) -> tt() , U141(tt(), V2) -> U142(isLNat(activate(V2))) , U142(tt()) -> tt() , U151(tt(), V2) -> U152(isLNat(activate(V2))) , U152(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , s(X) -> n__s(X) , U171(tt(), N, XS) -> U172(isLNat(activate(XS)), activate(N), activate(XS)) , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) , afterNth(N, XS) -> U11(isNatural(N), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) , U182(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) , U202(tt(), N, X, XS) -> U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__sel(V1, V2)) -> U131(isNatural(activate(V1)), activate(V2)) , U203(tt(), N, X, XS) -> U204(splitAt(activate(N), activate(XS)), activate(X)) , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) , U22(tt(), X) -> activate(X) , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) , U212(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> U222(isLNat(activate(XS)), activate(N), activate(XS)) , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), V2) -> U42(isLNat(activate(V2))) , U42(tt()) -> tt() , U51(tt(), V2) -> U52(isLNat(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(isLNat(activate(V1)), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(isNatural(activate(V1)), activate(V2)) , natsFrom(N) -> U161(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(isNatural(N), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) , take(N, XS) -> U221(isNatural(N), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , U102^#(tt()) -> c_2() , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , isLNat^#(n__nil()) -> c_4() , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , U71^#(tt()) -> c_78() , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_77() , U81^#(tt()) -> c_79() , U91^#(tt()) -> c_80() , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__0()) -> c_20(0^#()) , nil^#() -> c_54() , 0^#() -> c_87() , U111^#(tt()) -> c_28() , U121^#(tt()) -> c_34() , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , U132^#(tt()) -> c_36() , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , U142^#(tt()) -> c_38() , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , U152^#(tt()) -> c_40() , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , U42^#(tt()) -> c_74() , U52^#(tt()) -> c_76() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,51,60,61} by applications of Pre({1,2,3,51,60,61}) = {4,18,20,21,22,24,26,29,30,32,34,35,36}. Here rules are labeled as follows: DPs: { 1: isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , 2: isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , 3: isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , 4: activate^#(X) -> c_11(X) , 5: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , 6: activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , 7: activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , 8: activate^#(n__fst(X)) -> c_16(fst^#(X)) , 9: activate^#(n__snd(X)) -> c_17(snd^#(X)) , 10: activate^#(n__tail(X)) -> c_18(tail^#(X)) , 11: activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , 12: activate^#(n__head(X)) -> c_21(head^#(X)) , 13: activate^#(n__s(X)) -> c_22(s^#(X)) , 14: activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , 15: activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , 16: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , 17: natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , 18: natsFrom^#(X) -> c_84(X) , 19: afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , 20: afterNth^#(X1, X2) -> c_49(X1, X2) , 21: cons^#(X1, X2) -> c_42(X1, X2) , 22: fst^#(X) -> c_69(X) , 23: fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , 24: snd^#(X) -> c_29(X) , 25: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , 26: tail^#(X) -> c_88(X) , 27: tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , 28: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , 29: take^#(X1, X2) -> c_91(X1, X2) , 30: head^#(X) -> c_46(X) , 31: head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , 32: s^#(X) -> c_43(X) , 33: sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , 34: sel^#(X1, X2) -> c_86(X1, X2) , 35: pair^#(X1, X2) -> c_53(X1, X2) , 36: splitAt^#(X1, X2) -> c_31(X1, X2) , 37: splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , 38: splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , 39: U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , 40: U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , 41: U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , 42: U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , 43: U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , 44: U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , 45: U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , 46: U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , 47: U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , 48: U182^#(tt(), Y) -> c_51(activate^#(Y)) , 49: U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , 50: U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , 51: isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , 52: U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , 53: U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , 54: U22^#(tt(), X) -> c_64(activate^#(X)) , 55: U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , 56: U212^#(tt(), XS) -> c_66(activate^#(XS)) , 57: U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , 58: U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , 59: U32^#(tt(), N) -> c_72(activate^#(N)) , 60: isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , 61: isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) , 62: U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , 63: U102^#(tt()) -> c_2() , 64: isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , 65: isLNat^#(n__nil()) -> c_4() , 66: isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , 67: isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , 68: isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , 69: U71^#(tt()) -> c_78() , 70: U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , 71: U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , 72: U61^#(tt()) -> c_77() , 73: U81^#(tt()) -> c_79() , 74: U91^#(tt()) -> c_80() , 75: activate^#(n__nil()) -> c_13(nil^#()) , 76: activate^#(n__0()) -> c_20(0^#()) , 77: nil^#() -> c_54() , 78: 0^#() -> c_87() , 79: U111^#(tt()) -> c_28() , 80: U121^#(tt()) -> c_34() , 81: U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , 82: U132^#(tt()) -> c_36() , 83: U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , 84: U142^#(tt()) -> c_38() , 85: U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , 86: U152^#(tt()) -> c_40() , 87: isNatural^#(n__0()) -> c_57() , 88: isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , 89: isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , 90: U42^#(tt()) -> c_74() , 91: U52^#(tt()) -> c_76() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X)) , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2)) , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2)) , activate^#(n__fst(X)) -> c_16(fst^#(X)) , activate^#(n__snd(X)) -> c_17(snd^#(X)) , activate^#(n__tail(X)) -> c_18(tail^#(X)) , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2)) , activate^#(n__head(X)) -> c_21(head^#(X)) , activate^#(n__s(X)) -> c_22(s^#(X)) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2)) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2)) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2)) , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_84(X) , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_49(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_69(X) , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y)) , snd^#(X) -> c_29(X) , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , tail^#(X) -> c_88(X) , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , take^#(X1, X2) -> c_91(X1, X2) , head^#(X) -> c_46(X) , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS))) , s^#(X) -> c_43(X) , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_86(X1, X2) , pair^#(X1, X2) -> c_53(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(s(N), cons(X, XS)) -> c_32(U201^#(isNatural(N), N, X, activate(XS))) , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS)) , U11^#(tt(), N, XS) -> c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_27(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y))) , U201^#(tt(), N, X, XS) -> c_55(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS))) , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(s(activate(N))))) , U171^#(tt(), N, XS) -> c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_45(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_71(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_51(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_56(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , U204^#(pair(YS, ZS), X) -> c_62(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_63(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_64(activate^#(X)) , U211^#(tt(), XS) -> c_65(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_66(activate^#(XS)) , U221^#(tt(), N, XS) -> c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_68(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_72(activate^#(N)) } Strict Trs: { U101(tt(), V2) -> U102(isLNat(activate(V2))) , U102(tt()) -> tt() , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(isNatural(activate(V1)), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(isNatural(activate(V1)), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) , isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) , isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) , isLNat(n__take(V1, V2)) -> U101(isNatural(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(X1, X2) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__fst(X)) -> fst(X) , activate(n__snd(X)) -> snd(X) , activate(n__tail(X)) -> tail(X) , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(X) , activate(n__s(X)) -> s(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__pair(X1, X2)) -> pair(X1, X2) , activate(n__splitAt(X1, X2)) -> splitAt(X1, X2) , U11(tt(), N, XS) -> U12(isLNat(activate(XS)), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , U111(tt()) -> tt() , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(isLNat(X), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(XS)) , splitAt(0(), XS) -> U191(isLNat(XS), XS) , U121(tt()) -> tt() , U131(tt(), V2) -> U132(isLNat(activate(V2))) , U132(tt()) -> tt() , U141(tt(), V2) -> U142(isLNat(activate(V2))) , U142(tt()) -> tt() , U151(tt(), V2) -> U152(isLNat(activate(V2))) , U152(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , s(X) -> n__s(X) , U171(tt(), N, XS) -> U172(isLNat(activate(XS)), activate(N), activate(XS)) , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS)) , afterNth(N, XS) -> U11(isNatural(N), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y)) , U182(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(isNatural(activate(X)), activate(N), activate(X), activate(XS)) , U202(tt(), N, X, XS) -> U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) , isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__sel(V1, V2)) -> U131(isNatural(activate(V1)), activate(V2)) , U203(tt(), N, X, XS) -> U204(splitAt(activate(N), activate(XS)), activate(X)) , U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X, Y) -> U22(isLNat(activate(Y)), activate(X)) , U22(tt(), X) -> activate(X) , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS)) , U212(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> U222(isLNat(activate(XS)), activate(N), activate(XS)) , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(isLNat(X), X, Y) , U31(tt(), N, XS) -> U32(isLNat(activate(XS)), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), V2) -> U42(isLNat(activate(V2))) , U42(tt()) -> tt() , U51(tt(), V2) -> U52(isLNat(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(isLNat(activate(V1)), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(isNatural(activate(V1)), activate(V2)) , natsFrom(N) -> U161(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(isNatural(N), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS)) , take(N, XS) -> U221(isNatural(N), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2)))) , U102^#(tt()) -> c_2() , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1)))) , isLNat^#(n__nil()) -> c_4() , isLNat^#(n__afterNth(V1, V2)) -> c_5(U41^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_6(U51^#(isNatural(activate(V1)), activate(V2))) , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1)))) , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1)))) , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1)))) , isLNat^#(n__take(V1, V2)) -> c_10(U101^#(isNatural(activate(V1)), activate(V2))) , U71^#(tt()) -> c_78() , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_77() , U81^#(tt()) -> c_79() , U91^#(tt()) -> c_80() , activate^#(n__nil()) -> c_13(nil^#()) , activate^#(n__0()) -> c_20(0^#()) , nil^#() -> c_54() , 0^#() -> c_87() , U111^#(tt()) -> c_28() , U121^#(tt()) -> c_34() , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2)))) , U132^#(tt()) -> c_36() , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2)))) , U142^#(tt()) -> c_38() , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2)))) , U152^#(tt()) -> c_40() , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_60(U131^#(isNatural(activate(V1)), activate(V2))) , U42^#(tt()) -> c_74() , U52^#(tt()) -> c_76() , isPLNat^#(n__pair(V1, V2)) -> c_81(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_82(U151^#(isNatural(activate(V1)), activate(V2))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..