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