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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(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(0(), XS) -> U191(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(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(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , 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__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(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() , s(X) -> n__s(X) , 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) '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: { 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_77() , U41^#(tt(), V2) -> c_72(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_76() , U81^#(tt()) -> c_78() , U91^#(tt()) -> c_79() , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_13(s^#(activate(X))) , activate^#(n__nil()) -> c_14(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_21(0^#()) , activate^#(n__head(X)) -> c_22(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_83(X) , s^#(X) -> c_87(X) , nil^#() -> c_53() , afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_48(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_68(X) , fst^#(pair(X, Y)) -> c_69(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_86() , head^#(X) -> c_45(X) , head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_85(X1, X2) , pair^#(X1, X2) -> c_52(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), 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(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_50(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_63(activate^#(X)) , U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_65(activate^#(XS)) , U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_71(activate^#(N)) , U42^#(tt()) -> c_73() , U52^#(tt()) -> c_75() , isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_81(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_77() , U41^#(tt(), V2) -> c_72(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_76() , U81^#(tt()) -> c_78() , U91^#(tt()) -> c_79() , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_13(s^#(activate(X))) , activate^#(n__nil()) -> c_14(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_21(0^#()) , activate^#(n__head(X)) -> c_22(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_83(X) , s^#(X) -> c_87(X) , nil^#() -> c_53() , afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_48(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_68(X) , fst^#(pair(X, Y)) -> c_69(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_86() , head^#(X) -> c_45(X) , head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_85(X1, X2) , pair^#(X1, X2) -> c_52(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), 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(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_50(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_63(activate^#(X)) , U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_65(activate^#(XS)) , U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_71(activate^#(N)) , U42^#(tt()) -> c_73() , U52^#(tt()) -> c_75() , isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_81(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(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(0(), XS) -> U191(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(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(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , 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__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(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() , s(X) -> n__s(X) , 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,35,47,58,62,64,66,68,77,88,89} by applications of Pre({2,4,11,14,15,16,35,47,58,62,64,66,68,77,88,89}) = {1,3,7,8,9,12,13,17,20,27,33,34,37,38,39,41,43,46,48,51,52,53,63,65,67,76,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_77() , 12: U41^#(tt(), V2) -> c_72(U42^#(isLNat(activate(V2)))) , 13: U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , 14: U61^#(tt()) -> c_76() , 15: U81^#(tt()) -> c_78() , 16: U91^#(tt()) -> c_79() , 17: activate^#(X) -> c_11(X) , 18: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(activate(X))) , 19: activate^#(n__s(X)) -> c_13(s^#(activate(X))) , 20: activate^#(n__nil()) -> c_14(nil^#()) , 21: activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , 22: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , 23: activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , 24: activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , 25: activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , 26: activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , 27: activate^#(n__0()) -> c_21(0^#()) , 28: activate^#(n__head(X)) -> c_22(head^#(activate(X))) , 29: activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , 30: activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , 31: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , 32: natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , 33: natsFrom^#(X) -> c_83(X) , 34: s^#(X) -> c_87(X) , 35: nil^#() -> c_53() , 36: afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , 37: afterNth^#(X1, X2) -> c_48(X1, X2) , 38: cons^#(X1, X2) -> c_42(X1, X2) , 39: fst^#(X) -> c_68(X) , 40: fst^#(pair(X, Y)) -> c_69(U21^#(isLNat(X), X, Y)) , 41: snd^#(X) -> c_29(X) , 42: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , 43: tail^#(X) -> c_88(X) , 44: tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , 45: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , 46: take^#(X1, X2) -> c_91(X1, X2) , 47: 0^#() -> c_86() , 48: head^#(X) -> c_45(X) , 49: head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , 50: sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , 51: sel^#(X1, X2) -> c_85(X1, X2) , 52: pair^#(X1, X2) -> c_52(X1, X2) , 53: splitAt^#(X1, X2) -> c_31(X1, X2) , 54: splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , 55: splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , 60: U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , 61: U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), 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(n__s(activate(N))))) , 70: U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , 71: U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , 72: U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , 73: U182^#(tt(), Y) -> c_50(activate^#(Y)) , 74: U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , 75: U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , 76: isNatural^#(n__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , 77: isNatural^#(n__0()) -> c_57() , 78: isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , 79: isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , 80: U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , 81: U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , 82: U22^#(tt(), X) -> c_63(activate^#(X)) , 83: U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , 84: U212^#(tt(), XS) -> c_65(activate^#(XS)) , 85: U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , 86: U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , 87: U32^#(tt(), N) -> c_71(activate^#(N)) , 88: U42^#(tt()) -> c_73() , 89: U52^#(tt()) -> c_75() , 90: isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , 91: isPLNat^#(n__splitAt(V1, V2)) -> c_81(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_72(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , activate^#(X) -> c_11(X) , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_13(s^#(activate(X))) , activate^#(n__nil()) -> c_14(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_21(0^#()) , activate^#(n__head(X)) -> c_22(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_83(X) , s^#(X) -> c_87(X) , afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_48(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_68(X) , fst^#(pair(X, Y)) -> c_69(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_45(X) , head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_85(X1, X2) , pair^#(X1, X2) -> c_52(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), 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(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_50(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_63(activate^#(X)) , U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_65(activate^#(XS)) , U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_71(activate^#(N)) , isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_81(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(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(0(), XS) -> U191(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(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(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , 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__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(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() , s(X) -> n__s(X) , 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_77() , U61^#(tt()) -> c_76() , U81^#(tt()) -> c_78() , U91^#(tt()) -> c_79() , nil^#() -> c_53() , 0^#() -> c_86() , 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_73() , U52^#(tt()) -> c_75() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,5,6,7,9,10,14,21,53,54,55,63,64} by applications of Pre({1,2,5,6,7,9,10,14,21,53,54,55,63,64}) = {3,4,8,11,27,28,30,31,32,34,36,39,40,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_72(U42^#(isLNat(activate(V2)))) , 10: U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , 11: activate^#(X) -> c_11(X) , 12: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(activate(X))) , 13: activate^#(n__s(X)) -> c_13(s^#(activate(X))) , 14: activate^#(n__nil()) -> c_14(nil^#()) , 15: activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , 16: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , 17: activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , 18: activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , 19: activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , 20: activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , 21: activate^#(n__0()) -> c_21(0^#()) , 22: activate^#(n__head(X)) -> c_22(head^#(activate(X))) , 23: activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , 24: activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , 25: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , 26: natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , 27: natsFrom^#(X) -> c_83(X) , 28: s^#(X) -> c_87(X) , 29: afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , 30: afterNth^#(X1, X2) -> c_48(X1, X2) , 31: cons^#(X1, X2) -> c_42(X1, X2) , 32: fst^#(X) -> c_68(X) , 33: fst^#(pair(X, Y)) -> c_69(U21^#(isLNat(X), X, Y)) , 34: snd^#(X) -> c_29(X) , 35: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , 36: tail^#(X) -> c_88(X) , 37: tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , 38: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , 39: take^#(X1, X2) -> c_91(X1, X2) , 40: head^#(X) -> c_45(X) , 41: head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , 42: sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , 43: sel^#(X1, X2) -> c_85(X1, X2) , 44: pair^#(X1, X2) -> c_52(X1, X2) , 45: splitAt^#(X1, X2) -> c_31(X1, X2) , 46: splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , 47: splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , 51: U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , 52: U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), 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(n__s(activate(N))))) , 57: U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , 58: U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , 59: U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , 60: U182^#(tt(), Y) -> c_50(activate^#(Y)) , 61: U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , 62: U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , 63: isNatural^#(n__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , 64: isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , 65: isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , 66: U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , 67: U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , 68: U22^#(tt(), X) -> c_63(activate^#(X)) , 69: U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , 70: U212^#(tt(), XS) -> c_65(activate^#(XS)) , 71: U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , 72: U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , 73: U32^#(tt(), N) -> c_71(activate^#(N)) , 74: isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , 75: isPLNat^#(n__splitAt(V1, V2)) -> c_81(U151^#(isNatural(activate(V1)), activate(V2))) , 76: U102^#(tt()) -> c_2() , 77: isLNat^#(n__nil()) -> c_4() , 78: U71^#(tt()) -> c_77() , 79: U61^#(tt()) -> c_76() , 80: U81^#(tt()) -> c_78() , 81: U91^#(tt()) -> c_79() , 82: nil^#() -> c_53() , 83: 0^#() -> c_86() , 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_73() , 91: U52^#(tt()) -> c_75() } 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^#(activate(X))) , activate^#(n__s(X)) -> c_13(s^#(activate(X))) , activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , activate^#(n__head(X)) -> c_22(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_83(X) , s^#(X) -> c_87(X) , afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_48(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_68(X) , fst^#(pair(X, Y)) -> c_69(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_45(X) , head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_85(X1, X2) , pair^#(X1, X2) -> c_52(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_50(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_63(activate^#(X)) , U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_65(activate^#(XS)) , U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_71(activate^#(N)) , isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_81(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(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(0(), XS) -> U191(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(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(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , 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__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(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() , s(X) -> n__s(X) , 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_77() , U41^#(tt(), V2) -> c_72(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_76() , U81^#(tt()) -> c_78() , U91^#(tt()) -> c_79() , activate^#(n__nil()) -> c_14(nil^#()) , activate^#(n__0()) -> c_21(0^#()) , nil^#() -> c_53() , 0^#() -> c_86() , 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__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , U42^#(tt()) -> c_73() , U52^#(tt()) -> c_75() } 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,19,21,22,23,25,27,30,31,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^#(activate(X))) , 6: activate^#(n__s(X)) -> c_13(s^#(activate(X))) , 7: activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , 8: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , 9: activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , 10: activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , 11: activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , 12: activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , 13: activate^#(n__head(X)) -> c_22(head^#(activate(X))) , 14: activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , 15: activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , 16: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , 17: natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , 18: natsFrom^#(X) -> c_83(X) , 19: s^#(X) -> c_87(X) , 20: afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , 21: afterNth^#(X1, X2) -> c_48(X1, X2) , 22: cons^#(X1, X2) -> c_42(X1, X2) , 23: fst^#(X) -> c_68(X) , 24: fst^#(pair(X, Y)) -> c_69(U21^#(isLNat(X), X, Y)) , 25: snd^#(X) -> c_29(X) , 26: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y)) , 27: tail^#(X) -> c_88(X) , 28: tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS))) , 29: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS)) , 30: take^#(X1, X2) -> c_91(X1, X2) , 31: head^#(X) -> c_45(X) , 32: head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , 33: sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , 34: sel^#(X1, X2) -> c_85(X1, X2) , 35: pair^#(X1, X2) -> c_52(X1, X2) , 36: splitAt^#(X1, X2) -> c_31(X1, X2) , 37: splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , 38: splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , 42: U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , 43: U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , 44: U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 45: U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , 46: U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , 47: U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , 48: U182^#(tt(), Y) -> c_50(activate^#(Y)) , 49: U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , 50: U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , 51: isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , 52: U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , 53: U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , 54: U22^#(tt(), X) -> c_63(activate^#(X)) , 55: U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , 56: U212^#(tt(), XS) -> c_65(activate^#(XS)) , 57: U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , 58: U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , 59: U32^#(tt(), N) -> c_71(activate^#(N)) , 60: isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , 61: isPLNat^#(n__splitAt(V1, V2)) -> c_81(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_77() , 70: U41^#(tt(), V2) -> c_72(U42^#(isLNat(activate(V2)))) , 71: U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , 72: U61^#(tt()) -> c_76() , 73: U81^#(tt()) -> c_78() , 74: U91^#(tt()) -> c_79() , 75: activate^#(n__nil()) -> c_14(nil^#()) , 76: activate^#(n__0()) -> c_21(0^#()) , 77: nil^#() -> c_53() , 78: 0^#() -> c_86() , 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__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , 88: isNatural^#(n__0()) -> c_57() , 89: isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , 90: U42^#(tt()) -> c_73() , 91: U52^#(tt()) -> c_75() } 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^#(activate(X))) , activate^#(n__s(X)) -> c_13(s^#(activate(X))) , activate^#(n__afterNth(X1, X2)) -> c_15(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_17(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_18(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_19(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_20(take^#(activate(X1), activate(X2))) , activate^#(n__head(X)) -> c_22(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_23(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_24(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(activate(X1), activate(X2))) , natsFrom^#(N) -> c_82(U161^#(isNatural(N), N)) , natsFrom^#(X) -> c_83(X) , s^#(X) -> c_87(X) , afterNth^#(N, XS) -> c_47(U11^#(isNatural(N), N, XS)) , afterNth^#(X1, X2) -> c_48(X1, X2) , cons^#(X1, X2) -> c_42(X1, X2) , fst^#(X) -> c_68(X) , fst^#(pair(X, Y)) -> c_69(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_45(X) , head^#(cons(N, XS)) -> c_46(U31^#(isNatural(N), N, activate(XS))) , sel^#(N, XS) -> c_84(U171^#(isNatural(N), N, XS)) , sel^#(X1, X2) -> c_85(X1, X2) , pair^#(X1, X2) -> c_52(X1, X2) , splitAt^#(X1, X2) -> c_31(X1, X2) , splitAt^#(0(), XS) -> c_32(U191^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_33(U201^#(isNatural(N), N, X, activate(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_49(U182^#(isLNat(activate(Y)), activate(Y))) , U191^#(tt(), XS) -> c_51(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_54(U202^#(isNatural(activate(X)), activate(N), activate(X), activate(XS))) , U161^#(tt(), N) -> c_41(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_43(U172^#(isLNat(activate(XS)), activate(N), activate(XS))) , U172^#(tt(), N, XS) -> c_44(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N, XS) -> c_70(U32^#(isLNat(activate(XS)), activate(N))) , U182^#(tt(), Y) -> c_50(activate^#(Y)) , U202^#(tt(), N, X, XS) -> c_55(U203^#(isLNat(activate(XS)), activate(N), activate(X), activate(XS))) , U203^#(tt(), N, X, XS) -> c_60(U204^#(splitAt(activate(N), activate(XS)), activate(X))) , U204^#(pair(YS, ZS), X) -> c_61(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X, Y) -> c_62(U22^#(isLNat(activate(Y)), activate(X))) , U22^#(tt(), X) -> c_63(activate^#(X)) , U211^#(tt(), XS) -> c_64(U212^#(isLNat(activate(XS)), activate(XS))) , U212^#(tt(), XS) -> c_65(activate^#(XS)) , U221^#(tt(), N, XS) -> c_66(U222^#(isLNat(activate(XS)), activate(N), activate(XS))) , U222^#(tt(), N, XS) -> c_67(fst^#(splitAt(activate(N), activate(XS)))) , U32^#(tt(), N) -> c_71(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(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(0(), XS) -> U191(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(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(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , 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__s(V1)) -> U121(isNatural(activate(V1))) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNat(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() , s(X) -> n__s(X) , 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_77() , U41^#(tt(), V2) -> c_72(U42^#(isLNat(activate(V2)))) , U51^#(tt(), V2) -> c_74(U52^#(isLNat(activate(V2)))) , U61^#(tt()) -> c_76() , U81^#(tt()) -> c_78() , U91^#(tt()) -> c_79() , activate^#(n__nil()) -> c_14(nil^#()) , activate^#(n__0()) -> c_21(0^#()) , nil^#() -> c_53() , 0^#() -> c_86() , 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__s(V1)) -> c_56(U121^#(isNatural(activate(V1)))) , isNatural^#(n__0()) -> c_57() , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1)))) , isNatural^#(n__sel(V1, V2)) -> c_59(U131^#(isNatural(activate(V1)), activate(V2))) , U42^#(tt()) -> c_73() , U52^#(tt()) -> c_75() , isPLNat^#(n__pair(V1, V2)) -> c_80(U141^#(isLNat(activate(V1)), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_81(U151^#(isNatural(activate(V1)), activate(V2))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..