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