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