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