MAYBE 893.46/297.11 MAYBE 893.46/297.11 893.46/297.11 We are left with following problem, upon which TcT provides the 893.46/297.11 certificate MAYBE. 893.46/297.11 893.46/297.11 Strict Trs: 893.46/297.11 { zeros() -> cons(0(), n__zeros()) 893.46/297.11 , zeros() -> n__zeros() 893.46/297.11 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.11 , 0() -> n__0() 893.46/297.11 , U101(tt(), V1, V2) -> 893.46/297.11 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.11 , U102(tt(), V1, V2) -> 893.46/297.11 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.11 , isNatKind(n__0()) -> tt() 893.46/297.11 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.11 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.11 , activate(X) -> X 893.46/297.11 , activate(n__zeros()) -> zeros() 893.46/297.11 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.11 , activate(n__0()) -> 0() 893.46/297.11 , activate(n__length(X)) -> length(activate(X)) 893.46/297.11 , activate(n__s(X)) -> s(activate(X)) 893.46/297.11 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.11 , activate(n__nil()) -> nil() 893.46/297.11 , U103(tt(), V1, V2) -> 893.46/297.11 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.11 , isNatIListKind(n__zeros()) -> tt() 893.46/297.11 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.11 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.11 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.11 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.11 , isNatIListKind(n__nil()) -> tt() 893.46/297.11 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.11 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.11 , isNat(n__0()) -> tt() 893.46/297.11 , isNat(n__length(V1)) -> 893.46/297.11 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.11 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.11 , U106(tt()) -> tt() 893.46/297.11 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.11 , isNatIList(n__zeros()) -> tt() 893.46/297.11 , isNatIList(n__cons(V1, V2)) -> 893.46/297.11 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.11 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.11 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.11 , U111(tt(), L, N) -> 893.46/297.11 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.11 , U112(tt(), L, N) -> 893.46/297.11 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.11 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.11 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.11 , s(X) -> n__s(X) 893.46/297.11 , length(X) -> n__length(X) 893.46/297.11 , length(cons(N, L)) -> 893.46/297.11 U111(isNatList(activate(L)), activate(L), N) 893.46/297.11 , length(nil()) -> 0() 893.46/297.11 , U13(tt()) -> tt() 893.46/297.11 , isNatList(n__take(V1, V2)) -> 893.46/297.11 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.11 , isNatList(n__cons(V1, V2)) -> 893.46/297.11 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.11 , isNatList(n__nil()) -> tt() 893.46/297.11 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.11 , U122(tt()) -> nil() 893.46/297.11 , nil() -> n__nil() 893.46/297.11 , U131(tt(), IL, M, N) -> 893.46/297.11 U132(isNatIListKind(activate(IL)), 893.46/297.11 activate(IL), 893.46/297.11 activate(M), 893.46/297.11 activate(N)) 893.46/297.11 , U132(tt(), IL, M, N) -> 893.46/297.11 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.11 , U133(tt(), IL, M, N) -> 893.46/297.11 U134(isNatKind(activate(M)), 893.46/297.11 activate(IL), 893.46/297.11 activate(M), 893.46/297.11 activate(N)) 893.46/297.11 , U134(tt(), IL, M, N) -> 893.46/297.11 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.11 , U135(tt(), IL, M, N) -> 893.46/297.11 U136(isNatKind(activate(N)), 893.46/297.11 activate(IL), 893.46/297.11 activate(M), 893.46/297.11 activate(N)) 893.46/297.11 , U136(tt(), IL, M, N) -> 893.46/297.11 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.11 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.11 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.11 , U23(tt()) -> tt() 893.46/297.11 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.11 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.11 , U33(tt()) -> tt() 893.46/297.11 , U41(tt(), V1, V2) -> 893.46/297.11 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.11 , U42(tt(), V1, V2) -> 893.46/297.11 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.11 , U43(tt(), V1, V2) -> 893.46/297.11 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.11 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.11 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.11 , U46(tt()) -> tt() 893.46/297.11 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.11 , U52(tt()) -> tt() 893.46/297.11 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.11 , U62(tt()) -> tt() 893.46/297.11 , U71(tt()) -> tt() 893.46/297.11 , U81(tt()) -> tt() 893.46/297.11 , U91(tt(), V1, V2) -> 893.46/297.11 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.11 , U92(tt(), V1, V2) -> 893.46/297.11 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.11 , U93(tt(), V1, V2) -> 893.46/297.11 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.11 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.11 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.11 , U96(tt()) -> tt() 893.46/297.11 , take(X1, X2) -> n__take(X1, X2) 893.46/297.11 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.11 , take(s(M), cons(N, IL)) -> 893.46/297.11 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.11 Obligation: 893.46/297.11 runtime complexity 893.46/297.11 Answer: 893.46/297.11 MAYBE 893.46/297.11 893.46/297.11 None of the processors succeeded. 893.46/297.11 893.46/297.11 Details of failed attempt(s): 893.46/297.11 ----------------------------- 893.46/297.11 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 893.46/297.11 following reason: 893.46/297.11 893.46/297.11 Computation stopped due to timeout after 297.0 seconds. 893.46/297.11 893.46/297.11 2) 'Best' failed due to the following reason: 893.46/297.11 893.46/297.11 None of the processors succeeded. 893.46/297.11 893.46/297.11 Details of failed attempt(s): 893.46/297.11 ----------------------------- 893.46/297.11 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 893.46/297.11 seconds)' failed due to the following reason: 893.46/297.11 893.46/297.11 Computation stopped due to timeout after 148.0 seconds. 893.46/297.11 893.46/297.11 2) 'Best' failed due to the following reason: 893.46/297.11 893.46/297.11 None of the processors succeeded. 893.46/297.11 893.46/297.11 Details of failed attempt(s): 893.46/297.11 ----------------------------- 893.46/297.11 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 893.46/297.11 to the following reason: 893.46/297.11 893.46/297.11 The processor is inapplicable, reason: 893.46/297.11 Processor only applicable for innermost runtime complexity analysis 893.46/297.11 893.46/297.11 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 893.46/297.11 following reason: 893.46/297.11 893.46/297.11 The processor is inapplicable, reason: 893.46/297.11 Processor only applicable for innermost runtime complexity analysis 893.46/297.11 893.46/297.11 893.46/297.11 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 893.46/297.11 failed due to the following reason: 893.46/297.11 893.46/297.11 None of the processors succeeded. 893.46/297.11 893.46/297.11 Details of failed attempt(s): 893.46/297.11 ----------------------------- 893.46/297.11 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 893.46/297.11 failed due to the following reason: 893.46/297.11 893.46/297.11 match-boundness of the problem could not be verified. 893.46/297.11 893.46/297.11 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 893.46/297.11 failed due to the following reason: 893.46/297.11 893.46/297.11 match-boundness of the problem could not be verified. 893.46/297.11 893.46/297.11 893.46/297.11 893.46/297.11 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 893.46/297.11 the following reason: 893.46/297.11 893.46/297.11 We add the following weak dependency pairs: 893.46/297.11 893.46/297.11 Strict DPs: 893.46/297.11 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.11 , zeros^#() -> c_2() 893.46/297.11 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.11 , 0^#() -> c_4() 893.46/297.11 , U101^#(tt(), V1, V2) -> 893.46/297.11 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.11 , U102^#(tt(), V1, V2) -> 893.46/297.11 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.11 activate(V1), 893.46/297.11 activate(V2))) 893.46/297.11 , U103^#(tt(), V1, V2) -> 893.46/297.11 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.11 activate(V1), 893.46/297.11 activate(V2))) 893.46/297.11 , isNatKind^#(n__0()) -> c_7() 893.46/297.11 , isNatKind^#(n__length(V1)) -> 893.46/297.11 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.11 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.11 , U71^#(tt()) -> c_71() 893.46/297.11 , U81^#(tt()) -> c_72() 893.46/297.11 , activate^#(X) -> c_10(X) 893.46/297.11 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.11 , activate^#(n__take(X1, X2)) -> 893.46/297.11 c_12(take^#(activate(X1), activate(X2))) 893.46/297.11 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.11 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.11 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.11 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.11 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.11 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.12 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.12 , take^#(s(M), cons(N, IL)) -> 893.46/297.12 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.12 , length^#(X) -> c_39(X) 893.46/297.12 , length^#(cons(N, L)) -> 893.46/297.12 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.12 , length^#(nil()) -> c_41(0^#()) 893.46/297.12 , s^#(X) -> c_38(X) 893.46/297.12 , nil^#() -> c_48() 893.46/297.12 , U104^#(tt(), V1, V2) -> 893.46/297.12 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.12 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.12 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.12 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.12 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.12 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.12 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.12 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.12 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.12 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.12 , U106^#(tt()) -> c_28() 893.46/297.12 , isNat^#(n__0()) -> c_25() 893.46/297.12 , isNat^#(n__length(V1)) -> 893.46/297.12 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.12 , isNat^#(n__s(V1)) -> 893.46/297.12 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.12 , U11^#(tt(), V1) -> 893.46/297.12 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.12 , U21^#(tt(), V1) -> 893.46/297.12 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.12 , isNatIList^#(V) -> 893.46/297.12 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.12 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.12 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.12 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U31^#(tt(), V) -> 893.46/297.12 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.12 , U41^#(tt(), V1, V2) -> 893.46/297.12 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.12 , U13^#(tt()) -> c_42() 893.46/297.12 , U111^#(tt(), L, N) -> 893.46/297.12 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.12 , U112^#(tt(), L, N) -> 893.46/297.12 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.12 , U113^#(tt(), L, N) -> 893.46/297.12 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.12 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.12 , isNatList^#(n__take(V1, V2)) -> 893.46/297.12 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.12 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , isNatList^#(n__nil()) -> c_45() 893.46/297.12 , U91^#(tt(), V1, V2) -> 893.46/297.12 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.12 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.12 , U131^#(tt(), IL, M, N) -> 893.46/297.12 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U132^#(tt(), IL, M, N) -> 893.46/297.12 c_50(U133^#(isNat(activate(M)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U133^#(tt(), IL, M, N) -> 893.46/297.12 c_51(U134^#(isNatKind(activate(M)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U134^#(tt(), IL, M, N) -> 893.46/297.12 c_52(U135^#(isNat(activate(N)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U135^#(tt(), IL, M, N) -> 893.46/297.12 c_53(U136^#(isNatKind(activate(N)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U136^#(tt(), IL, M, N) -> 893.46/297.12 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.12 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.12 , U23^#(tt()) -> c_57() 893.46/297.12 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.12 , U33^#(tt()) -> c_60() 893.46/297.12 , U42^#(tt(), V1, V2) -> 893.46/297.12 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U43^#(tt(), V1, V2) -> 893.46/297.12 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U44^#(tt(), V1, V2) -> 893.46/297.12 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.12 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.12 , U46^#(tt()) -> c_66() 893.46/297.12 , U52^#(tt()) -> c_68() 893.46/297.12 , U62^#(tt()) -> c_70() 893.46/297.12 , U92^#(tt(), V1, V2) -> 893.46/297.12 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U93^#(tt(), V1, V2) -> 893.46/297.12 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U94^#(tt(), V1, V2) -> 893.46/297.12 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.12 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.12 , U96^#(tt()) -> c_78() } 893.46/297.12 893.46/297.12 and mark the set of starting terms. 893.46/297.12 893.46/297.12 We are left with following problem, upon which TcT provides the 893.46/297.12 certificate MAYBE. 893.46/297.12 893.46/297.12 Strict DPs: 893.46/297.12 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.12 , zeros^#() -> c_2() 893.46/297.12 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.12 , 0^#() -> c_4() 893.46/297.12 , U101^#(tt(), V1, V2) -> 893.46/297.12 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U102^#(tt(), V1, V2) -> 893.46/297.12 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U103^#(tt(), V1, V2) -> 893.46/297.12 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , isNatKind^#(n__0()) -> c_7() 893.46/297.12 , isNatKind^#(n__length(V1)) -> 893.46/297.12 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.12 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.12 , U71^#(tt()) -> c_71() 893.46/297.12 , U81^#(tt()) -> c_72() 893.46/297.12 , activate^#(X) -> c_10(X) 893.46/297.12 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.12 , activate^#(n__take(X1, X2)) -> 893.46/297.12 c_12(take^#(activate(X1), activate(X2))) 893.46/297.12 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.12 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.12 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.12 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.12 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.12 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.12 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.12 , take^#(s(M), cons(N, IL)) -> 893.46/297.12 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.12 , length^#(X) -> c_39(X) 893.46/297.12 , length^#(cons(N, L)) -> 893.46/297.12 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.12 , length^#(nil()) -> c_41(0^#()) 893.46/297.12 , s^#(X) -> c_38(X) 893.46/297.12 , nil^#() -> c_48() 893.46/297.12 , U104^#(tt(), V1, V2) -> 893.46/297.12 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.12 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.12 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.12 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.12 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.12 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.12 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.12 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.12 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.12 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.12 , U106^#(tt()) -> c_28() 893.46/297.12 , isNat^#(n__0()) -> c_25() 893.46/297.12 , isNat^#(n__length(V1)) -> 893.46/297.12 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.12 , isNat^#(n__s(V1)) -> 893.46/297.12 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.12 , U11^#(tt(), V1) -> 893.46/297.12 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.12 , U21^#(tt(), V1) -> 893.46/297.12 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.12 , isNatIList^#(V) -> 893.46/297.12 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.12 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.12 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.12 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U31^#(tt(), V) -> 893.46/297.12 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.12 , U41^#(tt(), V1, V2) -> 893.46/297.12 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.12 , U13^#(tt()) -> c_42() 893.46/297.12 , U111^#(tt(), L, N) -> 893.46/297.12 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.12 , U112^#(tt(), L, N) -> 893.46/297.12 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.12 , U113^#(tt(), L, N) -> 893.46/297.12 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.12 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.12 , isNatList^#(n__take(V1, V2)) -> 893.46/297.12 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.12 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , isNatList^#(n__nil()) -> c_45() 893.46/297.12 , U91^#(tt(), V1, V2) -> 893.46/297.12 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.12 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.12 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.12 , U131^#(tt(), IL, M, N) -> 893.46/297.12 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U132^#(tt(), IL, M, N) -> 893.46/297.12 c_50(U133^#(isNat(activate(M)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U133^#(tt(), IL, M, N) -> 893.46/297.12 c_51(U134^#(isNatKind(activate(M)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U134^#(tt(), IL, M, N) -> 893.46/297.12 c_52(U135^#(isNat(activate(N)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U135^#(tt(), IL, M, N) -> 893.46/297.12 c_53(U136^#(isNatKind(activate(N)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N))) 893.46/297.12 , U136^#(tt(), IL, M, N) -> 893.46/297.12 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.12 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.12 , U23^#(tt()) -> c_57() 893.46/297.12 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.12 , U33^#(tt()) -> c_60() 893.46/297.12 , U42^#(tt(), V1, V2) -> 893.46/297.12 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U43^#(tt(), V1, V2) -> 893.46/297.12 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U44^#(tt(), V1, V2) -> 893.46/297.12 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.12 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.12 , U46^#(tt()) -> c_66() 893.46/297.12 , U52^#(tt()) -> c_68() 893.46/297.12 , U62^#(tt()) -> c_70() 893.46/297.12 , U92^#(tt(), V1, V2) -> 893.46/297.12 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U93^#(tt(), V1, V2) -> 893.46/297.12 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.12 activate(V1), 893.46/297.12 activate(V2))) 893.46/297.12 , U94^#(tt(), V1, V2) -> 893.46/297.12 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.12 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.12 , U96^#(tt()) -> c_78() } 893.46/297.12 Strict Trs: 893.46/297.12 { zeros() -> cons(0(), n__zeros()) 893.46/297.12 , zeros() -> n__zeros() 893.46/297.12 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.12 , 0() -> n__0() 893.46/297.12 , U101(tt(), V1, V2) -> 893.46/297.12 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.12 , U102(tt(), V1, V2) -> 893.46/297.12 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.12 , isNatKind(n__0()) -> tt() 893.46/297.12 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.12 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.12 , activate(X) -> X 893.46/297.12 , activate(n__zeros()) -> zeros() 893.46/297.12 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.12 , activate(n__0()) -> 0() 893.46/297.12 , activate(n__length(X)) -> length(activate(X)) 893.46/297.12 , activate(n__s(X)) -> s(activate(X)) 893.46/297.12 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.12 , activate(n__nil()) -> nil() 893.46/297.12 , U103(tt(), V1, V2) -> 893.46/297.12 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.12 , isNatIListKind(n__zeros()) -> tt() 893.46/297.12 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.12 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.12 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.12 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.12 , isNatIListKind(n__nil()) -> tt() 893.46/297.12 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.12 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.12 , isNat(n__0()) -> tt() 893.46/297.12 , isNat(n__length(V1)) -> 893.46/297.12 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.12 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.12 , U106(tt()) -> tt() 893.46/297.12 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.12 , isNatIList(n__zeros()) -> tt() 893.46/297.12 , isNatIList(n__cons(V1, V2)) -> 893.46/297.12 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.12 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.12 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.12 , U111(tt(), L, N) -> 893.46/297.12 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.12 , U112(tt(), L, N) -> 893.46/297.12 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.12 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.12 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.12 , s(X) -> n__s(X) 893.46/297.12 , length(X) -> n__length(X) 893.46/297.12 , length(cons(N, L)) -> 893.46/297.12 U111(isNatList(activate(L)), activate(L), N) 893.46/297.12 , length(nil()) -> 0() 893.46/297.12 , U13(tt()) -> tt() 893.46/297.12 , isNatList(n__take(V1, V2)) -> 893.46/297.12 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.12 , isNatList(n__cons(V1, V2)) -> 893.46/297.12 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.12 , isNatList(n__nil()) -> tt() 893.46/297.12 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.12 , U122(tt()) -> nil() 893.46/297.12 , nil() -> n__nil() 893.46/297.12 , U131(tt(), IL, M, N) -> 893.46/297.12 U132(isNatIListKind(activate(IL)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N)) 893.46/297.12 , U132(tt(), IL, M, N) -> 893.46/297.12 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.12 , U133(tt(), IL, M, N) -> 893.46/297.12 U134(isNatKind(activate(M)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N)) 893.46/297.12 , U134(tt(), IL, M, N) -> 893.46/297.12 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.12 , U135(tt(), IL, M, N) -> 893.46/297.12 U136(isNatKind(activate(N)), 893.46/297.12 activate(IL), 893.46/297.12 activate(M), 893.46/297.12 activate(N)) 893.46/297.12 , U136(tt(), IL, M, N) -> 893.46/297.12 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.12 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.12 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.12 , U23(tt()) -> tt() 893.46/297.12 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.12 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.12 , U33(tt()) -> tt() 893.46/297.12 , U41(tt(), V1, V2) -> 893.46/297.12 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.12 , U42(tt(), V1, V2) -> 893.46/297.12 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.12 , U43(tt(), V1, V2) -> 893.46/297.12 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.12 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.12 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.12 , U46(tt()) -> tt() 893.46/297.12 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.12 , U52(tt()) -> tt() 893.46/297.12 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.12 , U62(tt()) -> tt() 893.46/297.12 , U71(tt()) -> tt() 893.46/297.12 , U81(tt()) -> tt() 893.46/297.12 , U91(tt(), V1, V2) -> 893.46/297.12 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.12 , U92(tt(), V1, V2) -> 893.46/297.12 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.12 , U93(tt(), V1, V2) -> 893.46/297.12 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.12 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.12 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.12 , U96(tt()) -> tt() 893.46/297.12 , take(X1, X2) -> n__take(X1, X2) 893.46/297.12 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.12 , take(s(M), cons(N, IL)) -> 893.46/297.12 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.12 Obligation: 893.46/297.12 runtime complexity 893.46/297.12 Answer: 893.46/297.12 MAYBE 893.46/297.12 893.46/297.12 We estimate the number of application of 893.46/297.13 {2,4,8,11,12,28,30,33,37,38,44,49,56,67,69,74,75,76,81} by 893.46/297.13 applications of 893.46/297.13 Pre({2,4,8,11,12,28,30,33,37,38,44,49,56,67,69,74,75,76,81}) = 893.46/297.13 {3,9,10,13,14,16,20,21,24,26,27,34,35,36,48,59,66,68,73,80}. Here 893.46/297.13 rules are labeled as follows: 893.46/297.13 893.46/297.13 DPs: 893.46/297.13 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.13 , 2: zeros^#() -> c_2() 893.46/297.13 , 3: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.13 , 4: 0^#() -> c_4() 893.46/297.13 , 5: U101^#(tt(), V1, V2) -> 893.46/297.13 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , 6: U102^#(tt(), V1, V2) -> 893.46/297.13 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , 7: U103^#(tt(), V1, V2) -> 893.46/297.13 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , 8: isNatKind^#(n__0()) -> c_7() 893.46/297.13 , 9: isNatKind^#(n__length(V1)) -> 893.46/297.13 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.13 , 10: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.13 , 11: U71^#(tt()) -> c_71() 893.46/297.13 , 12: U81^#(tt()) -> c_72() 893.46/297.13 , 13: activate^#(X) -> c_10(X) 893.46/297.13 , 14: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.13 , 15: activate^#(n__take(X1, X2)) -> 893.46/297.13 c_12(take^#(activate(X1), activate(X2))) 893.46/297.13 , 16: activate^#(n__0()) -> c_13(0^#()) 893.46/297.13 , 17: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.13 , 18: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.13 , 19: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.13 , 20: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.13 , 21: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.13 , 22: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.13 , 23: take^#(s(M), cons(N, IL)) -> 893.46/297.13 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.13 , 24: length^#(X) -> c_39(X) 893.46/297.13 , 25: length^#(cons(N, L)) -> 893.46/297.13 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.13 , 26: length^#(nil()) -> c_41(0^#()) 893.46/297.13 , 27: s^#(X) -> c_38(X) 893.46/297.13 , 28: nil^#() -> c_48() 893.46/297.13 , 29: U104^#(tt(), V1, V2) -> 893.46/297.13 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.13 , 30: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.13 , 31: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.13 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.13 , 32: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.13 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.13 , 33: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.13 , 34: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.13 , 35: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.13 , 36: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.13 , 37: U106^#(tt()) -> c_28() 893.46/297.13 , 38: isNat^#(n__0()) -> c_25() 893.46/297.13 , 39: isNat^#(n__length(V1)) -> 893.46/297.13 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.13 , 40: isNat^#(n__s(V1)) -> 893.46/297.13 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.13 , 41: U11^#(tt(), V1) -> 893.46/297.13 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.13 , 42: U21^#(tt(), V1) -> 893.46/297.13 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.13 , 43: isNatIList^#(V) -> 893.46/297.13 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.13 , 44: isNatIList^#(n__zeros()) -> c_30() 893.46/297.13 , 45: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.13 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , 46: U31^#(tt(), V) -> 893.46/297.13 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.13 , 47: U41^#(tt(), V1, V2) -> 893.46/297.13 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , 48: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.13 , 49: U13^#(tt()) -> c_42() 893.46/297.13 , 50: U111^#(tt(), L, N) -> 893.46/297.13 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.13 , 51: U112^#(tt(), L, N) -> 893.46/297.13 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.13 , 52: U113^#(tt(), L, N) -> 893.46/297.13 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.13 , 53: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.13 , 54: isNatList^#(n__take(V1, V2)) -> 893.46/297.13 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , 55: isNatList^#(n__cons(V1, V2)) -> 893.46/297.13 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , 56: isNatList^#(n__nil()) -> c_45() 893.46/297.13 , 57: U91^#(tt(), V1, V2) -> 893.46/297.13 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , 58: U121^#(tt(), IL) -> 893.46/297.13 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.13 , 59: U122^#(tt()) -> c_47(nil^#()) 893.46/297.13 , 60: U131^#(tt(), IL, M, N) -> 893.46/297.13 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , 61: U132^#(tt(), IL, M, N) -> 893.46/297.13 c_50(U133^#(isNat(activate(M)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , 62: U133^#(tt(), IL, M, N) -> 893.46/297.13 c_51(U134^#(isNatKind(activate(M)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , 63: U134^#(tt(), IL, M, N) -> 893.46/297.13 c_52(U135^#(isNat(activate(N)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , 64: U135^#(tt(), IL, M, N) -> 893.46/297.13 c_53(U136^#(isNatKind(activate(N)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , 65: U136^#(tt(), IL, M, N) -> 893.46/297.13 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.13 , 66: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.13 , 67: U23^#(tt()) -> c_57() 893.46/297.13 , 68: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.13 , 69: U33^#(tt()) -> c_60() 893.46/297.13 , 70: U42^#(tt(), V1, V2) -> 893.46/297.13 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , 71: U43^#(tt(), V1, V2) -> 893.46/297.13 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , 72: U44^#(tt(), V1, V2) -> 893.46/297.13 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.13 , 73: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.13 , 74: U46^#(tt()) -> c_66() 893.46/297.13 , 75: U52^#(tt()) -> c_68() 893.46/297.13 , 76: U62^#(tt()) -> c_70() 893.46/297.13 , 77: U92^#(tt(), V1, V2) -> 893.46/297.13 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , 78: U93^#(tt(), V1, V2) -> 893.46/297.13 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , 79: U94^#(tt(), V1, V2) -> 893.46/297.13 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.13 , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.13 , 81: U96^#(tt()) -> c_78() } 893.46/297.13 893.46/297.13 We are left with following problem, upon which TcT provides the 893.46/297.13 certificate MAYBE. 893.46/297.13 893.46/297.13 Strict DPs: 893.46/297.13 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.13 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.13 , U101^#(tt(), V1, V2) -> 893.46/297.13 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , U102^#(tt(), V1, V2) -> 893.46/297.13 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , U103^#(tt(), V1, V2) -> 893.46/297.13 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , isNatKind^#(n__length(V1)) -> 893.46/297.13 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.13 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.13 , activate^#(X) -> c_10(X) 893.46/297.13 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.13 , activate^#(n__take(X1, X2)) -> 893.46/297.13 c_12(take^#(activate(X1), activate(X2))) 893.46/297.13 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.13 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.13 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.13 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.13 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.13 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.13 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.13 , take^#(s(M), cons(N, IL)) -> 893.46/297.13 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.13 , length^#(X) -> c_39(X) 893.46/297.13 , length^#(cons(N, L)) -> 893.46/297.13 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.13 , length^#(nil()) -> c_41(0^#()) 893.46/297.13 , s^#(X) -> c_38(X) 893.46/297.13 , U104^#(tt(), V1, V2) -> 893.46/297.13 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.13 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.13 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.13 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.13 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.13 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.13 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.13 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.13 , isNat^#(n__length(V1)) -> 893.46/297.13 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.13 , isNat^#(n__s(V1)) -> 893.46/297.13 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.13 , U11^#(tt(), V1) -> 893.46/297.13 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.13 , U21^#(tt(), V1) -> 893.46/297.13 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.13 , isNatIList^#(V) -> 893.46/297.13 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.13 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.13 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , U31^#(tt(), V) -> 893.46/297.13 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.13 , U41^#(tt(), V1, V2) -> 893.46/297.13 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.13 , U111^#(tt(), L, N) -> 893.46/297.13 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.13 , U112^#(tt(), L, N) -> 893.46/297.13 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.13 , U113^#(tt(), L, N) -> 893.46/297.13 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.13 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.13 , isNatList^#(n__take(V1, V2)) -> 893.46/297.13 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.13 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , U91^#(tt(), V1, V2) -> 893.46/297.13 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.13 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.13 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.13 , U131^#(tt(), IL, M, N) -> 893.46/297.13 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , U132^#(tt(), IL, M, N) -> 893.46/297.13 c_50(U133^#(isNat(activate(M)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , U133^#(tt(), IL, M, N) -> 893.46/297.13 c_51(U134^#(isNatKind(activate(M)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , U134^#(tt(), IL, M, N) -> 893.46/297.13 c_52(U135^#(isNat(activate(N)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , U135^#(tt(), IL, M, N) -> 893.46/297.13 c_53(U136^#(isNatKind(activate(N)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N))) 893.46/297.13 , U136^#(tt(), IL, M, N) -> 893.46/297.13 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.13 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.13 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.13 , U42^#(tt(), V1, V2) -> 893.46/297.13 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , U43^#(tt(), V1, V2) -> 893.46/297.13 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , U44^#(tt(), V1, V2) -> 893.46/297.13 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.13 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.13 , U92^#(tt(), V1, V2) -> 893.46/297.13 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , U93^#(tt(), V1, V2) -> 893.46/297.13 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.13 activate(V1), 893.46/297.13 activate(V2))) 893.46/297.13 , U94^#(tt(), V1, V2) -> 893.46/297.13 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.13 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) } 893.46/297.13 Strict Trs: 893.46/297.13 { zeros() -> cons(0(), n__zeros()) 893.46/297.13 , zeros() -> n__zeros() 893.46/297.13 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.13 , 0() -> n__0() 893.46/297.13 , U101(tt(), V1, V2) -> 893.46/297.13 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.13 , U102(tt(), V1, V2) -> 893.46/297.13 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.13 , isNatKind(n__0()) -> tt() 893.46/297.13 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.13 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.13 , activate(X) -> X 893.46/297.13 , activate(n__zeros()) -> zeros() 893.46/297.13 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.13 , activate(n__0()) -> 0() 893.46/297.13 , activate(n__length(X)) -> length(activate(X)) 893.46/297.13 , activate(n__s(X)) -> s(activate(X)) 893.46/297.13 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.13 , activate(n__nil()) -> nil() 893.46/297.13 , U103(tt(), V1, V2) -> 893.46/297.13 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.13 , isNatIListKind(n__zeros()) -> tt() 893.46/297.13 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.13 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.13 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.13 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.13 , isNatIListKind(n__nil()) -> tt() 893.46/297.13 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.13 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.13 , isNat(n__0()) -> tt() 893.46/297.13 , isNat(n__length(V1)) -> 893.46/297.13 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.13 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.13 , U106(tt()) -> tt() 893.46/297.13 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.13 , isNatIList(n__zeros()) -> tt() 893.46/297.13 , isNatIList(n__cons(V1, V2)) -> 893.46/297.13 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.13 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.13 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.13 , U111(tt(), L, N) -> 893.46/297.13 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.13 , U112(tt(), L, N) -> 893.46/297.13 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.13 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.13 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.13 , s(X) -> n__s(X) 893.46/297.13 , length(X) -> n__length(X) 893.46/297.13 , length(cons(N, L)) -> 893.46/297.13 U111(isNatList(activate(L)), activate(L), N) 893.46/297.13 , length(nil()) -> 0() 893.46/297.13 , U13(tt()) -> tt() 893.46/297.13 , isNatList(n__take(V1, V2)) -> 893.46/297.13 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.13 , isNatList(n__cons(V1, V2)) -> 893.46/297.13 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.13 , isNatList(n__nil()) -> tt() 893.46/297.13 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.13 , U122(tt()) -> nil() 893.46/297.13 , nil() -> n__nil() 893.46/297.13 , U131(tt(), IL, M, N) -> 893.46/297.13 U132(isNatIListKind(activate(IL)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N)) 893.46/297.13 , U132(tt(), IL, M, N) -> 893.46/297.13 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.13 , U133(tt(), IL, M, N) -> 893.46/297.13 U134(isNatKind(activate(M)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N)) 893.46/297.13 , U134(tt(), IL, M, N) -> 893.46/297.13 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.13 , U135(tt(), IL, M, N) -> 893.46/297.13 U136(isNatKind(activate(N)), 893.46/297.13 activate(IL), 893.46/297.13 activate(M), 893.46/297.13 activate(N)) 893.46/297.13 , U136(tt(), IL, M, N) -> 893.46/297.14 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.14 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.14 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.14 , U23(tt()) -> tt() 893.46/297.14 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.14 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.14 , U33(tt()) -> tt() 893.46/297.14 , U41(tt(), V1, V2) -> 893.46/297.14 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , U42(tt(), V1, V2) -> 893.46/297.14 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U43(tt(), V1, V2) -> 893.46/297.14 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.14 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.14 , U46(tt()) -> tt() 893.46/297.14 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.14 , U52(tt()) -> tt() 893.46/297.14 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.14 , U62(tt()) -> tt() 893.46/297.14 , U71(tt()) -> tt() 893.46/297.14 , U81(tt()) -> tt() 893.46/297.14 , U91(tt(), V1, V2) -> 893.46/297.14 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , U92(tt(), V1, V2) -> 893.46/297.14 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U93(tt(), V1, V2) -> 893.46/297.14 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.14 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.14 , U96(tt()) -> tt() 893.46/297.14 , take(X1, X2) -> n__take(X1, X2) 893.46/297.14 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.14 , take(s(M), cons(N, IL)) -> 893.46/297.14 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.14 Weak DPs: 893.46/297.14 { zeros^#() -> c_2() 893.46/297.14 , 0^#() -> c_4() 893.46/297.14 , isNatKind^#(n__0()) -> c_7() 893.46/297.14 , U71^#(tt()) -> c_71() 893.46/297.14 , U81^#(tt()) -> c_72() 893.46/297.14 , nil^#() -> c_48() 893.46/297.14 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.14 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.14 , U106^#(tt()) -> c_28() 893.46/297.14 , isNat^#(n__0()) -> c_25() 893.46/297.14 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.14 , U13^#(tt()) -> c_42() 893.46/297.14 , isNatList^#(n__nil()) -> c_45() 893.46/297.14 , U23^#(tt()) -> c_57() 893.46/297.14 , U33^#(tt()) -> c_60() 893.46/297.14 , U46^#(tt()) -> c_66() 893.46/297.14 , U52^#(tt()) -> c_68() 893.46/297.14 , U62^#(tt()) -> c_70() 893.46/297.14 , U96^#(tt()) -> c_78() } 893.46/297.14 Obligation: 893.46/297.14 runtime complexity 893.46/297.14 Answer: 893.46/297.14 MAYBE 893.46/297.14 893.46/297.14 We estimate the number of application of 893.46/297.14 {6,7,11,15,21,26,27,28,37,46,53,54,58,62} by applications of 893.46/297.14 Pre({6,7,11,15,21,26,27,28,37,46,53,54,58,62}) = 893.46/297.14 {2,8,12,16,19,22,23,24,25,31,32,35,45,57,61}. Here rules are 893.46/297.14 labeled as follows: 893.46/297.14 893.46/297.14 DPs: 893.46/297.14 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.14 , 2: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.14 , 3: U101^#(tt(), V1, V2) -> 893.46/297.14 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 4: U102^#(tt(), V1, V2) -> 893.46/297.14 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 5: U103^#(tt(), V1, V2) -> 893.46/297.14 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 6: isNatKind^#(n__length(V1)) -> 893.46/297.14 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.14 , 7: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.14 , 8: activate^#(X) -> c_10(X) 893.46/297.14 , 9: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.14 , 10: activate^#(n__take(X1, X2)) -> 893.46/297.14 c_12(take^#(activate(X1), activate(X2))) 893.46/297.14 , 11: activate^#(n__0()) -> c_13(0^#()) 893.46/297.14 , 12: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.14 , 13: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.14 , 14: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.14 , 15: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.14 , 16: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.14 , 17: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.14 , 18: take^#(s(M), cons(N, IL)) -> 893.46/297.14 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.14 , 19: length^#(X) -> c_39(X) 893.46/297.14 , 20: length^#(cons(N, L)) -> 893.46/297.14 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.14 , 21: length^#(nil()) -> c_41(0^#()) 893.46/297.14 , 22: s^#(X) -> c_38(X) 893.46/297.14 , 23: U104^#(tt(), V1, V2) -> 893.46/297.14 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.14 , 24: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.14 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.14 , 25: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.14 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.14 , 26: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.14 , 27: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.14 , 28: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.14 , 29: isNat^#(n__length(V1)) -> 893.46/297.14 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.14 , 30: isNat^#(n__s(V1)) -> 893.46/297.14 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.14 , 31: U11^#(tt(), V1) -> 893.46/297.14 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.14 , 32: U21^#(tt(), V1) -> 893.46/297.14 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.14 , 33: isNatIList^#(V) -> 893.46/297.14 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.14 , 34: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.14 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 35: U31^#(tt(), V) -> 893.46/297.14 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.14 , 36: U41^#(tt(), V1, V2) -> 893.46/297.14 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 37: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.14 , 38: U111^#(tt(), L, N) -> 893.46/297.14 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.14 , 39: U112^#(tt(), L, N) -> 893.46/297.14 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.14 , 40: U113^#(tt(), L, N) -> 893.46/297.14 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.14 , 41: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.14 , 42: isNatList^#(n__take(V1, V2)) -> 893.46/297.14 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 43: isNatList^#(n__cons(V1, V2)) -> 893.46/297.14 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 44: U91^#(tt(), V1, V2) -> 893.46/297.14 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 45: U121^#(tt(), IL) -> 893.46/297.14 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.14 , 46: U122^#(tt()) -> c_47(nil^#()) 893.46/297.14 , 47: U131^#(tt(), IL, M, N) -> 893.46/297.14 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , 48: U132^#(tt(), IL, M, N) -> 893.46/297.14 c_50(U133^#(isNat(activate(M)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , 49: U133^#(tt(), IL, M, N) -> 893.46/297.14 c_51(U134^#(isNatKind(activate(M)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , 50: U134^#(tt(), IL, M, N) -> 893.46/297.14 c_52(U135^#(isNat(activate(N)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , 51: U135^#(tt(), IL, M, N) -> 893.46/297.14 c_53(U136^#(isNatKind(activate(N)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , 52: U136^#(tt(), IL, M, N) -> 893.46/297.14 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.14 , 53: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.14 , 54: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.14 , 55: U42^#(tt(), V1, V2) -> 893.46/297.14 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 56: U43^#(tt(), V1, V2) -> 893.46/297.14 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 57: U44^#(tt(), V1, V2) -> 893.46/297.14 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.14 , 58: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.14 , 59: U92^#(tt(), V1, V2) -> 893.46/297.14 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 60: U93^#(tt(), V1, V2) -> 893.46/297.14 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 61: U94^#(tt(), V1, V2) -> 893.46/297.14 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.14 , 62: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.14 , 63: zeros^#() -> c_2() 893.46/297.14 , 64: 0^#() -> c_4() 893.46/297.14 , 65: isNatKind^#(n__0()) -> c_7() 893.46/297.14 , 66: U71^#(tt()) -> c_71() 893.46/297.14 , 67: U81^#(tt()) -> c_72() 893.46/297.14 , 68: nil^#() -> c_48() 893.46/297.14 , 69: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.14 , 70: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.14 , 71: U106^#(tt()) -> c_28() 893.46/297.14 , 72: isNat^#(n__0()) -> c_25() 893.46/297.14 , 73: isNatIList^#(n__zeros()) -> c_30() 893.46/297.14 , 74: U13^#(tt()) -> c_42() 893.46/297.14 , 75: isNatList^#(n__nil()) -> c_45() 893.46/297.14 , 76: U23^#(tt()) -> c_57() 893.46/297.14 , 77: U33^#(tt()) -> c_60() 893.46/297.14 , 78: U46^#(tt()) -> c_66() 893.46/297.14 , 79: U52^#(tt()) -> c_68() 893.46/297.14 , 80: U62^#(tt()) -> c_70() 893.46/297.14 , 81: U96^#(tt()) -> c_78() } 893.46/297.14 893.46/297.14 We are left with following problem, upon which TcT provides the 893.46/297.14 certificate MAYBE. 893.46/297.14 893.46/297.14 Strict DPs: 893.46/297.14 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.14 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.14 , U101^#(tt(), V1, V2) -> 893.46/297.14 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , U102^#(tt(), V1, V2) -> 893.46/297.14 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , U103^#(tt(), V1, V2) -> 893.46/297.14 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , activate^#(X) -> c_10(X) 893.46/297.14 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.14 , activate^#(n__take(X1, X2)) -> 893.46/297.14 c_12(take^#(activate(X1), activate(X2))) 893.46/297.14 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.14 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.14 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.14 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.14 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.14 , take^#(s(M), cons(N, IL)) -> 893.46/297.14 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.14 , length^#(X) -> c_39(X) 893.46/297.14 , length^#(cons(N, L)) -> 893.46/297.14 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.14 , s^#(X) -> c_38(X) 893.46/297.14 , U104^#(tt(), V1, V2) -> 893.46/297.14 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.14 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.14 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.14 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.14 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.14 , isNat^#(n__length(V1)) -> 893.46/297.14 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.14 , isNat^#(n__s(V1)) -> 893.46/297.14 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.14 , U11^#(tt(), V1) -> 893.46/297.14 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.14 , U21^#(tt(), V1) -> 893.46/297.14 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.14 , isNatIList^#(V) -> 893.46/297.14 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.14 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.14 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , U31^#(tt(), V) -> 893.46/297.14 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.14 , U41^#(tt(), V1, V2) -> 893.46/297.14 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , U111^#(tt(), L, N) -> 893.46/297.14 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.14 , U112^#(tt(), L, N) -> 893.46/297.14 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.14 , U113^#(tt(), L, N) -> 893.46/297.14 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.14 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.14 , isNatList^#(n__take(V1, V2)) -> 893.46/297.14 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.14 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , U91^#(tt(), V1, V2) -> 893.46/297.14 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.14 , U131^#(tt(), IL, M, N) -> 893.46/297.14 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , U132^#(tt(), IL, M, N) -> 893.46/297.14 c_50(U133^#(isNat(activate(M)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , U133^#(tt(), IL, M, N) -> 893.46/297.14 c_51(U134^#(isNatKind(activate(M)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , U134^#(tt(), IL, M, N) -> 893.46/297.14 c_52(U135^#(isNat(activate(N)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , U135^#(tt(), IL, M, N) -> 893.46/297.14 c_53(U136^#(isNatKind(activate(N)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N))) 893.46/297.14 , U136^#(tt(), IL, M, N) -> 893.46/297.14 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.14 , U42^#(tt(), V1, V2) -> 893.46/297.14 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , U43^#(tt(), V1, V2) -> 893.46/297.14 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , U44^#(tt(), V1, V2) -> 893.46/297.14 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.14 , U92^#(tt(), V1, V2) -> 893.46/297.14 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , U93^#(tt(), V1, V2) -> 893.46/297.14 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , U94^#(tt(), V1, V2) -> 893.46/297.14 c_76(U95^#(isNat(activate(V1)), activate(V2))) } 893.46/297.14 Strict Trs: 893.46/297.14 { zeros() -> cons(0(), n__zeros()) 893.46/297.14 , zeros() -> n__zeros() 893.46/297.14 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.14 , 0() -> n__0() 893.46/297.14 , U101(tt(), V1, V2) -> 893.46/297.14 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , U102(tt(), V1, V2) -> 893.46/297.14 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , isNatKind(n__0()) -> tt() 893.46/297.14 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.14 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.14 , activate(X) -> X 893.46/297.14 , activate(n__zeros()) -> zeros() 893.46/297.14 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.14 , activate(n__0()) -> 0() 893.46/297.14 , activate(n__length(X)) -> length(activate(X)) 893.46/297.14 , activate(n__s(X)) -> s(activate(X)) 893.46/297.14 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.14 , activate(n__nil()) -> nil() 893.46/297.14 , U103(tt(), V1, V2) -> 893.46/297.14 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , isNatIListKind(n__zeros()) -> tt() 893.46/297.14 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.14 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.14 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.14 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.14 , isNatIListKind(n__nil()) -> tt() 893.46/297.14 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.14 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.14 , isNat(n__0()) -> tt() 893.46/297.14 , isNat(n__length(V1)) -> 893.46/297.14 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.14 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.14 , U106(tt()) -> tt() 893.46/297.14 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.14 , isNatIList(n__zeros()) -> tt() 893.46/297.14 , isNatIList(n__cons(V1, V2)) -> 893.46/297.14 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.14 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.14 , U111(tt(), L, N) -> 893.46/297.14 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.14 , U112(tt(), L, N) -> 893.46/297.14 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.14 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.14 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.14 , s(X) -> n__s(X) 893.46/297.14 , length(X) -> n__length(X) 893.46/297.14 , length(cons(N, L)) -> 893.46/297.14 U111(isNatList(activate(L)), activate(L), N) 893.46/297.14 , length(nil()) -> 0() 893.46/297.14 , U13(tt()) -> tt() 893.46/297.14 , isNatList(n__take(V1, V2)) -> 893.46/297.14 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , isNatList(n__cons(V1, V2)) -> 893.46/297.14 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , isNatList(n__nil()) -> tt() 893.46/297.14 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.14 , U122(tt()) -> nil() 893.46/297.14 , nil() -> n__nil() 893.46/297.14 , U131(tt(), IL, M, N) -> 893.46/297.14 U132(isNatIListKind(activate(IL)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N)) 893.46/297.14 , U132(tt(), IL, M, N) -> 893.46/297.14 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.14 , U133(tt(), IL, M, N) -> 893.46/297.14 U134(isNatKind(activate(M)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N)) 893.46/297.14 , U134(tt(), IL, M, N) -> 893.46/297.14 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.14 , U135(tt(), IL, M, N) -> 893.46/297.14 U136(isNatKind(activate(N)), 893.46/297.14 activate(IL), 893.46/297.14 activate(M), 893.46/297.14 activate(N)) 893.46/297.14 , U136(tt(), IL, M, N) -> 893.46/297.14 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.14 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.14 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.14 , U23(tt()) -> tt() 893.46/297.14 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.14 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.14 , U33(tt()) -> tt() 893.46/297.14 , U41(tt(), V1, V2) -> 893.46/297.14 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , U42(tt(), V1, V2) -> 893.46/297.14 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U43(tt(), V1, V2) -> 893.46/297.14 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.14 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.14 , U46(tt()) -> tt() 893.46/297.14 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.14 , U52(tt()) -> tt() 893.46/297.14 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.14 , U62(tt()) -> tt() 893.46/297.14 , U71(tt()) -> tt() 893.46/297.14 , U81(tt()) -> tt() 893.46/297.14 , U91(tt(), V1, V2) -> 893.46/297.14 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.14 , U92(tt(), V1, V2) -> 893.46/297.14 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U93(tt(), V1, V2) -> 893.46/297.14 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.14 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.14 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.14 , U96(tt()) -> tt() 893.46/297.14 , take(X1, X2) -> n__take(X1, X2) 893.46/297.14 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.14 , take(s(M), cons(N, IL)) -> 893.46/297.14 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.14 Weak DPs: 893.46/297.14 { zeros^#() -> c_2() 893.46/297.14 , 0^#() -> c_4() 893.46/297.14 , isNatKind^#(n__0()) -> c_7() 893.46/297.14 , isNatKind^#(n__length(V1)) -> 893.46/297.14 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.14 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.14 , U71^#(tt()) -> c_71() 893.46/297.14 , U81^#(tt()) -> c_72() 893.46/297.14 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.14 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.14 , length^#(nil()) -> c_41(0^#()) 893.46/297.14 , nil^#() -> c_48() 893.46/297.14 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.14 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.14 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.14 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.14 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.14 , U106^#(tt()) -> c_28() 893.46/297.14 , isNat^#(n__0()) -> c_25() 893.46/297.14 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.14 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.14 , U13^#(tt()) -> c_42() 893.46/297.14 , isNatList^#(n__nil()) -> c_45() 893.46/297.14 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.14 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.14 , U23^#(tt()) -> c_57() 893.46/297.14 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.14 , U33^#(tt()) -> c_60() 893.46/297.14 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.14 , U46^#(tt()) -> c_66() 893.46/297.14 , U52^#(tt()) -> c_68() 893.46/297.14 , U62^#(tt()) -> c_70() 893.46/297.14 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.14 , U96^#(tt()) -> c_78() } 893.46/297.14 Obligation: 893.46/297.14 runtime complexity 893.46/297.14 Answer: 893.46/297.14 MAYBE 893.46/297.14 893.46/297.14 We estimate the number of application of 893.46/297.14 {18,19,20,23,24,27,36,45,48} by applications of 893.46/297.14 Pre({18,19,20,23,24,27,36,45,48}) = 893.46/297.14 {2,5,6,12,13,15,17,21,22,25,44,47}. Here rules are labeled as 893.46/297.14 follows: 893.46/297.14 893.46/297.14 DPs: 893.46/297.14 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.14 , 2: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.14 , 3: U101^#(tt(), V1, V2) -> 893.46/297.14 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 4: U102^#(tt(), V1, V2) -> 893.46/297.14 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 5: U103^#(tt(), V1, V2) -> 893.46/297.14 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.14 activate(V1), 893.46/297.14 activate(V2))) 893.46/297.14 , 6: activate^#(X) -> c_10(X) 893.46/297.14 , 7: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.14 , 8: activate^#(n__take(X1, X2)) -> 893.46/297.14 c_12(take^#(activate(X1), activate(X2))) 893.46/297.14 , 9: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.14 , 10: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.14 , 11: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.14 , 12: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.14 , 13: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.14 , 14: take^#(s(M), cons(N, IL)) -> 893.46/297.14 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.14 , 15: length^#(X) -> c_39(X) 893.46/297.14 , 16: length^#(cons(N, L)) -> 893.46/297.14 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.14 , 17: s^#(X) -> c_38(X) 893.46/297.14 , 18: U104^#(tt(), V1, V2) -> 893.46/297.14 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.14 , 19: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.14 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.14 , 20: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.14 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.14 , 21: isNat^#(n__length(V1)) -> 893.46/297.14 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.14 , 22: isNat^#(n__s(V1)) -> 893.46/297.14 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.14 , 23: U11^#(tt(), V1) -> 893.46/297.14 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.14 , 24: U21^#(tt(), V1) -> 893.46/297.14 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.14 , 25: isNatIList^#(V) -> 893.46/297.14 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.14 , 26: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.14 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 27: U31^#(tt(), V) -> 893.46/297.14 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.14 , 28: U41^#(tt(), V1, V2) -> 893.46/297.14 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 29: U111^#(tt(), L, N) -> 893.46/297.14 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.14 , 30: U112^#(tt(), L, N) -> 893.46/297.14 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.14 , 31: U113^#(tt(), L, N) -> 893.46/297.14 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.14 , 32: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.14 , 33: isNatList^#(n__take(V1, V2)) -> 893.46/297.14 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 34: isNatList^#(n__cons(V1, V2)) -> 893.46/297.14 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 35: U91^#(tt(), V1, V2) -> 893.46/297.14 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.14 , 36: U121^#(tt(), IL) -> 893.46/297.14 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.15 , 37: U131^#(tt(), IL, M, N) -> 893.46/297.15 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , 38: U132^#(tt(), IL, M, N) -> 893.46/297.15 c_50(U133^#(isNat(activate(M)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , 39: U133^#(tt(), IL, M, N) -> 893.46/297.15 c_51(U134^#(isNatKind(activate(M)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , 40: U134^#(tt(), IL, M, N) -> 893.46/297.15 c_52(U135^#(isNat(activate(N)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , 41: U135^#(tt(), IL, M, N) -> 893.46/297.15 c_53(U136^#(isNatKind(activate(N)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , 42: U136^#(tt(), IL, M, N) -> 893.46/297.15 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.15 , 43: U42^#(tt(), V1, V2) -> 893.46/297.15 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , 44: U43^#(tt(), V1, V2) -> 893.46/297.15 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , 45: U44^#(tt(), V1, V2) -> 893.46/297.15 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.15 , 46: U92^#(tt(), V1, V2) -> 893.46/297.15 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , 47: U93^#(tt(), V1, V2) -> 893.46/297.15 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , 48: U94^#(tt(), V1, V2) -> 893.46/297.15 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.15 , 49: zeros^#() -> c_2() 893.46/297.15 , 50: 0^#() -> c_4() 893.46/297.15 , 51: isNatKind^#(n__0()) -> c_7() 893.46/297.15 , 52: isNatKind^#(n__length(V1)) -> 893.46/297.15 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.15 , 53: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.15 , 54: U71^#(tt()) -> c_71() 893.46/297.15 , 55: U81^#(tt()) -> c_72() 893.46/297.15 , 56: activate^#(n__0()) -> c_13(0^#()) 893.46/297.15 , 57: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.15 , 58: length^#(nil()) -> c_41(0^#()) 893.46/297.15 , 59: nil^#() -> c_48() 893.46/297.15 , 60: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.15 , 61: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.15 , 62: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.15 , 63: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.15 , 64: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.15 , 65: U106^#(tt()) -> c_28() 893.46/297.15 , 66: isNat^#(n__0()) -> c_25() 893.46/297.15 , 67: isNatIList^#(n__zeros()) -> c_30() 893.46/297.15 , 68: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.15 , 69: U13^#(tt()) -> c_42() 893.46/297.15 , 70: isNatList^#(n__nil()) -> c_45() 893.46/297.15 , 71: U122^#(tt()) -> c_47(nil^#()) 893.46/297.15 , 72: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.15 , 73: U23^#(tt()) -> c_57() 893.46/297.15 , 74: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.15 , 75: U33^#(tt()) -> c_60() 893.46/297.15 , 76: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.15 , 77: U46^#(tt()) -> c_66() 893.46/297.15 , 78: U52^#(tt()) -> c_68() 893.46/297.15 , 79: U62^#(tt()) -> c_70() 893.46/297.15 , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.15 , 81: U96^#(tt()) -> c_78() } 893.46/297.15 893.46/297.15 We are left with following problem, upon which TcT provides the 893.46/297.15 certificate MAYBE. 893.46/297.15 893.46/297.15 Strict DPs: 893.46/297.15 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.15 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.15 , U101^#(tt(), V1, V2) -> 893.46/297.15 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , U102^#(tt(), V1, V2) -> 893.46/297.15 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , U103^#(tt(), V1, V2) -> 893.46/297.15 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , activate^#(X) -> c_10(X) 893.46/297.15 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.15 , activate^#(n__take(X1, X2)) -> 893.46/297.15 c_12(take^#(activate(X1), activate(X2))) 893.46/297.15 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.15 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.15 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.15 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.15 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.15 , take^#(s(M), cons(N, IL)) -> 893.46/297.15 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.15 , length^#(X) -> c_39(X) 893.46/297.15 , length^#(cons(N, L)) -> 893.46/297.15 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.15 , s^#(X) -> c_38(X) 893.46/297.15 , isNat^#(n__length(V1)) -> 893.46/297.15 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.15 , isNat^#(n__s(V1)) -> 893.46/297.15 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.15 , isNatIList^#(V) -> 893.46/297.15 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.15 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.15 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , U41^#(tt(), V1, V2) -> 893.46/297.15 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , U111^#(tt(), L, N) -> 893.46/297.15 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.15 , U112^#(tt(), L, N) -> 893.46/297.15 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.15 , U113^#(tt(), L, N) -> 893.46/297.15 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.15 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.15 , isNatList^#(n__take(V1, V2)) -> 893.46/297.15 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.15 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , U91^#(tt(), V1, V2) -> 893.46/297.15 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , U131^#(tt(), IL, M, N) -> 893.46/297.15 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , U132^#(tt(), IL, M, N) -> 893.46/297.15 c_50(U133^#(isNat(activate(M)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , U133^#(tt(), IL, M, N) -> 893.46/297.15 c_51(U134^#(isNatKind(activate(M)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , U134^#(tt(), IL, M, N) -> 893.46/297.15 c_52(U135^#(isNat(activate(N)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , U135^#(tt(), IL, M, N) -> 893.46/297.15 c_53(U136^#(isNatKind(activate(N)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N))) 893.46/297.15 , U136^#(tt(), IL, M, N) -> 893.46/297.15 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.15 , U42^#(tt(), V1, V2) -> 893.46/297.15 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , U43^#(tt(), V1, V2) -> 893.46/297.15 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , U92^#(tt(), V1, V2) -> 893.46/297.15 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , U93^#(tt(), V1, V2) -> 893.46/297.15 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) } 893.46/297.15 Strict Trs: 893.46/297.15 { zeros() -> cons(0(), n__zeros()) 893.46/297.15 , zeros() -> n__zeros() 893.46/297.15 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.15 , 0() -> n__0() 893.46/297.15 , U101(tt(), V1, V2) -> 893.46/297.15 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.15 , U102(tt(), V1, V2) -> 893.46/297.15 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.15 , isNatKind(n__0()) -> tt() 893.46/297.15 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.15 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.15 , activate(X) -> X 893.46/297.15 , activate(n__zeros()) -> zeros() 893.46/297.15 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.15 , activate(n__0()) -> 0() 893.46/297.15 , activate(n__length(X)) -> length(activate(X)) 893.46/297.15 , activate(n__s(X)) -> s(activate(X)) 893.46/297.15 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.15 , activate(n__nil()) -> nil() 893.46/297.15 , U103(tt(), V1, V2) -> 893.46/297.15 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.15 , isNatIListKind(n__zeros()) -> tt() 893.46/297.15 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.15 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.15 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.15 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.15 , isNatIListKind(n__nil()) -> tt() 893.46/297.15 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.15 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.15 , isNat(n__0()) -> tt() 893.46/297.15 , isNat(n__length(V1)) -> 893.46/297.15 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.15 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.15 , U106(tt()) -> tt() 893.46/297.15 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.15 , isNatIList(n__zeros()) -> tt() 893.46/297.15 , isNatIList(n__cons(V1, V2)) -> 893.46/297.15 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.15 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.15 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.15 , U111(tt(), L, N) -> 893.46/297.15 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.15 , U112(tt(), L, N) -> 893.46/297.15 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.15 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.15 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.15 , s(X) -> n__s(X) 893.46/297.15 , length(X) -> n__length(X) 893.46/297.15 , length(cons(N, L)) -> 893.46/297.15 U111(isNatList(activate(L)), activate(L), N) 893.46/297.15 , length(nil()) -> 0() 893.46/297.15 , U13(tt()) -> tt() 893.46/297.15 , isNatList(n__take(V1, V2)) -> 893.46/297.15 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.15 , isNatList(n__cons(V1, V2)) -> 893.46/297.15 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.15 , isNatList(n__nil()) -> tt() 893.46/297.15 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.15 , U122(tt()) -> nil() 893.46/297.15 , nil() -> n__nil() 893.46/297.15 , U131(tt(), IL, M, N) -> 893.46/297.15 U132(isNatIListKind(activate(IL)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N)) 893.46/297.15 , U132(tt(), IL, M, N) -> 893.46/297.15 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.15 , U133(tt(), IL, M, N) -> 893.46/297.15 U134(isNatKind(activate(M)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N)) 893.46/297.15 , U134(tt(), IL, M, N) -> 893.46/297.15 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.15 , U135(tt(), IL, M, N) -> 893.46/297.15 U136(isNatKind(activate(N)), 893.46/297.15 activate(IL), 893.46/297.15 activate(M), 893.46/297.15 activate(N)) 893.46/297.15 , U136(tt(), IL, M, N) -> 893.46/297.15 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.15 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.15 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.15 , U23(tt()) -> tt() 893.46/297.15 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.15 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.15 , U33(tt()) -> tt() 893.46/297.15 , U41(tt(), V1, V2) -> 893.46/297.15 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.15 , U42(tt(), V1, V2) -> 893.46/297.15 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.15 , U43(tt(), V1, V2) -> 893.46/297.15 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.15 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.15 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.15 , U46(tt()) -> tt() 893.46/297.15 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.15 , U52(tt()) -> tt() 893.46/297.15 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.15 , U62(tt()) -> tt() 893.46/297.15 , U71(tt()) -> tt() 893.46/297.15 , U81(tt()) -> tt() 893.46/297.15 , U91(tt(), V1, V2) -> 893.46/297.15 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.15 , U92(tt(), V1, V2) -> 893.46/297.15 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.15 , U93(tt(), V1, V2) -> 893.46/297.15 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.15 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.15 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.15 , U96(tt()) -> tt() 893.46/297.15 , take(X1, X2) -> n__take(X1, X2) 893.46/297.15 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.15 , take(s(M), cons(N, IL)) -> 893.46/297.15 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.15 Weak DPs: 893.46/297.15 { zeros^#() -> c_2() 893.46/297.15 , 0^#() -> c_4() 893.46/297.15 , isNatKind^#(n__0()) -> c_7() 893.46/297.15 , isNatKind^#(n__length(V1)) -> 893.46/297.15 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.15 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.15 , U71^#(tt()) -> c_71() 893.46/297.15 , U81^#(tt()) -> c_72() 893.46/297.15 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.15 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.15 , length^#(nil()) -> c_41(0^#()) 893.46/297.15 , nil^#() -> c_48() 893.46/297.15 , U104^#(tt(), V1, V2) -> 893.46/297.15 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.15 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.15 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.15 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.15 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.15 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.15 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.15 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.15 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.15 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.15 , U106^#(tt()) -> c_28() 893.46/297.15 , isNat^#(n__0()) -> c_25() 893.46/297.15 , U11^#(tt(), V1) -> 893.46/297.15 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.15 , U21^#(tt(), V1) -> 893.46/297.15 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.15 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.15 , U31^#(tt(), V) -> 893.46/297.15 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.15 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.15 , U13^#(tt()) -> c_42() 893.46/297.15 , isNatList^#(n__nil()) -> c_45() 893.46/297.15 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.15 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.15 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.15 , U23^#(tt()) -> c_57() 893.46/297.15 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.15 , U33^#(tt()) -> c_60() 893.46/297.15 , U44^#(tt(), V1, V2) -> 893.46/297.15 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.15 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.15 , U46^#(tt()) -> c_66() 893.46/297.15 , U52^#(tt()) -> c_68() 893.46/297.15 , U62^#(tt()) -> c_70() 893.46/297.15 , U94^#(tt(), V1, V2) -> 893.46/297.15 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.15 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.15 , U96^#(tt()) -> c_78() } 893.46/297.15 Obligation: 893.46/297.15 runtime complexity 893.46/297.15 Answer: 893.46/297.15 MAYBE 893.46/297.15 893.46/297.15 We estimate the number of application of {5,13,18,19,20,37,39} by 893.46/297.15 applications of Pre({5,13,18,19,20,37,39}) = 893.46/297.15 {2,4,6,8,12,15,17,36,38}. Here rules are labeled as follows: 893.46/297.15 893.46/297.15 DPs: 893.46/297.15 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.15 , 2: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.15 , 3: U101^#(tt(), V1, V2) -> 893.46/297.15 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.15 , 4: U102^#(tt(), V1, V2) -> 893.46/297.15 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , 5: U103^#(tt(), V1, V2) -> 893.46/297.15 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.15 activate(V1), 893.46/297.15 activate(V2))) 893.46/297.15 , 6: activate^#(X) -> c_10(X) 893.46/297.15 , 7: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.15 , 8: activate^#(n__take(X1, X2)) -> 893.46/297.15 c_12(take^#(activate(X1), activate(X2))) 893.46/297.15 , 9: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.15 , 10: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.15 , 11: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.15 , 12: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.15 , 13: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.16 , 14: take^#(s(M), cons(N, IL)) -> 893.46/297.16 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.16 , 15: length^#(X) -> c_39(X) 893.46/297.16 , 16: length^#(cons(N, L)) -> 893.46/297.16 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.16 , 17: s^#(X) -> c_38(X) 893.46/297.16 , 18: isNat^#(n__length(V1)) -> 893.46/297.16 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.16 , 19: isNat^#(n__s(V1)) -> 893.46/297.16 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.16 , 20: isNatIList^#(V) -> 893.46/297.16 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.16 , 21: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.16 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , 22: U41^#(tt(), V1, V2) -> 893.46/297.16 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , 23: U111^#(tt(), L, N) -> 893.46/297.16 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.16 , 24: U112^#(tt(), L, N) -> 893.46/297.16 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.16 , 25: U113^#(tt(), L, N) -> 893.46/297.16 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.16 , 26: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.16 , 27: isNatList^#(n__take(V1, V2)) -> 893.46/297.16 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , 28: isNatList^#(n__cons(V1, V2)) -> 893.46/297.16 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , 29: U91^#(tt(), V1, V2) -> 893.46/297.16 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , 30: U131^#(tt(), IL, M, N) -> 893.46/297.16 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , 31: U132^#(tt(), IL, M, N) -> 893.46/297.16 c_50(U133^#(isNat(activate(M)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , 32: U133^#(tt(), IL, M, N) -> 893.46/297.16 c_51(U134^#(isNatKind(activate(M)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , 33: U134^#(tt(), IL, M, N) -> 893.46/297.16 c_52(U135^#(isNat(activate(N)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , 34: U135^#(tt(), IL, M, N) -> 893.46/297.16 c_53(U136^#(isNatKind(activate(N)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , 35: U136^#(tt(), IL, M, N) -> 893.46/297.16 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.16 , 36: U42^#(tt(), V1, V2) -> 893.46/297.16 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , 37: U43^#(tt(), V1, V2) -> 893.46/297.16 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , 38: U92^#(tt(), V1, V2) -> 893.46/297.16 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , 39: U93^#(tt(), V1, V2) -> 893.46/297.16 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , 40: zeros^#() -> c_2() 893.46/297.16 , 41: 0^#() -> c_4() 893.46/297.16 , 42: isNatKind^#(n__0()) -> c_7() 893.46/297.16 , 43: isNatKind^#(n__length(V1)) -> 893.46/297.16 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.16 , 44: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.16 , 45: U71^#(tt()) -> c_71() 893.46/297.16 , 46: U81^#(tt()) -> c_72() 893.46/297.16 , 47: activate^#(n__0()) -> c_13(0^#()) 893.46/297.16 , 48: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.16 , 49: length^#(nil()) -> c_41(0^#()) 893.46/297.16 , 50: nil^#() -> c_48() 893.46/297.16 , 51: U104^#(tt(), V1, V2) -> 893.46/297.16 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.16 , 52: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.16 , 53: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.16 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.16 , 54: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.16 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.16 , 55: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.16 , 56: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.16 , 57: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.16 , 58: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.16 , 59: U106^#(tt()) -> c_28() 893.46/297.16 , 60: isNat^#(n__0()) -> c_25() 893.46/297.16 , 61: U11^#(tt(), V1) -> 893.46/297.16 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.16 , 62: U21^#(tt(), V1) -> 893.46/297.16 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.16 , 63: isNatIList^#(n__zeros()) -> c_30() 893.46/297.16 , 64: U31^#(tt(), V) -> 893.46/297.16 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.16 , 65: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.16 , 66: U13^#(tt()) -> c_42() 893.46/297.16 , 67: isNatList^#(n__nil()) -> c_45() 893.46/297.16 , 68: U121^#(tt(), IL) -> 893.46/297.16 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.16 , 69: U122^#(tt()) -> c_47(nil^#()) 893.46/297.16 , 70: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.16 , 71: U23^#(tt()) -> c_57() 893.46/297.16 , 72: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.16 , 73: U33^#(tt()) -> c_60() 893.46/297.16 , 74: U44^#(tt(), V1, V2) -> 893.46/297.16 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.16 , 75: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.16 , 76: U46^#(tt()) -> c_66() 893.46/297.16 , 77: U52^#(tt()) -> c_68() 893.46/297.16 , 78: U62^#(tt()) -> c_70() 893.46/297.16 , 79: U94^#(tt(), V1, V2) -> 893.46/297.16 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.16 , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.16 , 81: U96^#(tt()) -> c_78() } 893.46/297.16 893.46/297.16 We are left with following problem, upon which TcT provides the 893.46/297.16 certificate MAYBE. 893.46/297.16 893.46/297.16 Strict DPs: 893.46/297.16 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.16 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.16 , U101^#(tt(), V1, V2) -> 893.46/297.16 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , U102^#(tt(), V1, V2) -> 893.46/297.16 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , activate^#(X) -> c_10(X) 893.46/297.16 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.16 , activate^#(n__take(X1, X2)) -> 893.46/297.16 c_12(take^#(activate(X1), activate(X2))) 893.46/297.16 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.16 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.16 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.16 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.16 , take^#(s(M), cons(N, IL)) -> 893.46/297.16 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.16 , length^#(X) -> c_39(X) 893.46/297.16 , length^#(cons(N, L)) -> 893.46/297.16 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.16 , s^#(X) -> c_38(X) 893.46/297.16 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.16 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , U41^#(tt(), V1, V2) -> 893.46/297.16 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , U111^#(tt(), L, N) -> 893.46/297.16 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.16 , U112^#(tt(), L, N) -> 893.46/297.16 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.16 , U113^#(tt(), L, N) -> 893.46/297.16 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.16 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.16 , isNatList^#(n__take(V1, V2)) -> 893.46/297.16 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.16 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , U91^#(tt(), V1, V2) -> 893.46/297.16 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.16 , U131^#(tt(), IL, M, N) -> 893.46/297.16 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , U132^#(tt(), IL, M, N) -> 893.46/297.16 c_50(U133^#(isNat(activate(M)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , U133^#(tt(), IL, M, N) -> 893.46/297.16 c_51(U134^#(isNatKind(activate(M)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , U134^#(tt(), IL, M, N) -> 893.46/297.16 c_52(U135^#(isNat(activate(N)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , U135^#(tt(), IL, M, N) -> 893.46/297.16 c_53(U136^#(isNatKind(activate(N)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N))) 893.46/297.16 , U136^#(tt(), IL, M, N) -> 893.46/297.16 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.16 , U42^#(tt(), V1, V2) -> 893.46/297.16 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , U92^#(tt(), V1, V2) -> 893.46/297.16 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) } 893.46/297.16 Strict Trs: 893.46/297.16 { zeros() -> cons(0(), n__zeros()) 893.46/297.16 , zeros() -> n__zeros() 893.46/297.16 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.16 , 0() -> n__0() 893.46/297.16 , U101(tt(), V1, V2) -> 893.46/297.16 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.16 , U102(tt(), V1, V2) -> 893.46/297.16 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.16 , isNatKind(n__0()) -> tt() 893.46/297.16 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.16 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.16 , activate(X) -> X 893.46/297.16 , activate(n__zeros()) -> zeros() 893.46/297.16 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.16 , activate(n__0()) -> 0() 893.46/297.16 , activate(n__length(X)) -> length(activate(X)) 893.46/297.16 , activate(n__s(X)) -> s(activate(X)) 893.46/297.16 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.16 , activate(n__nil()) -> nil() 893.46/297.16 , U103(tt(), V1, V2) -> 893.46/297.16 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.16 , isNatIListKind(n__zeros()) -> tt() 893.46/297.16 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.16 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.16 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.16 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.16 , isNatIListKind(n__nil()) -> tt() 893.46/297.16 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.16 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.16 , isNat(n__0()) -> tt() 893.46/297.16 , isNat(n__length(V1)) -> 893.46/297.16 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.16 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.16 , U106(tt()) -> tt() 893.46/297.16 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.16 , isNatIList(n__zeros()) -> tt() 893.46/297.16 , isNatIList(n__cons(V1, V2)) -> 893.46/297.16 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.16 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.16 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.16 , U111(tt(), L, N) -> 893.46/297.16 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.16 , U112(tt(), L, N) -> 893.46/297.16 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.16 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.16 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.16 , s(X) -> n__s(X) 893.46/297.16 , length(X) -> n__length(X) 893.46/297.16 , length(cons(N, L)) -> 893.46/297.16 U111(isNatList(activate(L)), activate(L), N) 893.46/297.16 , length(nil()) -> 0() 893.46/297.16 , U13(tt()) -> tt() 893.46/297.16 , isNatList(n__take(V1, V2)) -> 893.46/297.16 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.16 , isNatList(n__cons(V1, V2)) -> 893.46/297.16 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.16 , isNatList(n__nil()) -> tt() 893.46/297.16 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.16 , U122(tt()) -> nil() 893.46/297.16 , nil() -> n__nil() 893.46/297.16 , U131(tt(), IL, M, N) -> 893.46/297.16 U132(isNatIListKind(activate(IL)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N)) 893.46/297.16 , U132(tt(), IL, M, N) -> 893.46/297.16 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.16 , U133(tt(), IL, M, N) -> 893.46/297.16 U134(isNatKind(activate(M)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N)) 893.46/297.16 , U134(tt(), IL, M, N) -> 893.46/297.16 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.16 , U135(tt(), IL, M, N) -> 893.46/297.16 U136(isNatKind(activate(N)), 893.46/297.16 activate(IL), 893.46/297.16 activate(M), 893.46/297.16 activate(N)) 893.46/297.16 , U136(tt(), IL, M, N) -> 893.46/297.16 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.16 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.16 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.16 , U23(tt()) -> tt() 893.46/297.16 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.16 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.16 , U33(tt()) -> tt() 893.46/297.16 , U41(tt(), V1, V2) -> 893.46/297.16 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.16 , U42(tt(), V1, V2) -> 893.46/297.16 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.16 , U43(tt(), V1, V2) -> 893.46/297.16 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.16 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.16 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.16 , U46(tt()) -> tt() 893.46/297.16 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.16 , U52(tt()) -> tt() 893.46/297.16 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.16 , U62(tt()) -> tt() 893.46/297.16 , U71(tt()) -> tt() 893.46/297.16 , U81(tt()) -> tt() 893.46/297.16 , U91(tt(), V1, V2) -> 893.46/297.16 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.16 , U92(tt(), V1, V2) -> 893.46/297.16 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.16 , U93(tt(), V1, V2) -> 893.46/297.16 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.16 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.16 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.16 , U96(tt()) -> tt() 893.46/297.16 , take(X1, X2) -> n__take(X1, X2) 893.46/297.16 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.16 , take(s(M), cons(N, IL)) -> 893.46/297.16 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.16 Weak DPs: 893.46/297.16 { zeros^#() -> c_2() 893.46/297.16 , 0^#() -> c_4() 893.46/297.16 , U103^#(tt(), V1, V2) -> 893.46/297.16 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , isNatKind^#(n__0()) -> c_7() 893.46/297.16 , isNatKind^#(n__length(V1)) -> 893.46/297.16 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.16 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.16 , U71^#(tt()) -> c_71() 893.46/297.16 , U81^#(tt()) -> c_72() 893.46/297.16 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.16 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.16 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.16 , length^#(nil()) -> c_41(0^#()) 893.46/297.16 , nil^#() -> c_48() 893.46/297.16 , U104^#(tt(), V1, V2) -> 893.46/297.16 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.16 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.16 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.16 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.16 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.16 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.16 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.16 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.16 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.16 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.16 , U106^#(tt()) -> c_28() 893.46/297.16 , isNat^#(n__0()) -> c_25() 893.46/297.16 , isNat^#(n__length(V1)) -> 893.46/297.16 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.16 , isNat^#(n__s(V1)) -> 893.46/297.16 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.16 , U11^#(tt(), V1) -> 893.46/297.16 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.16 , U21^#(tt(), V1) -> 893.46/297.16 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.16 , isNatIList^#(V) -> 893.46/297.16 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.16 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.16 , U31^#(tt(), V) -> 893.46/297.16 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.16 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.16 , U13^#(tt()) -> c_42() 893.46/297.16 , isNatList^#(n__nil()) -> c_45() 893.46/297.16 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.16 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.16 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.16 , U23^#(tt()) -> c_57() 893.46/297.16 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.16 , U33^#(tt()) -> c_60() 893.46/297.16 , U43^#(tt(), V1, V2) -> 893.46/297.16 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , U44^#(tt(), V1, V2) -> 893.46/297.16 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.16 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.16 , U46^#(tt()) -> c_66() 893.46/297.16 , U52^#(tt()) -> c_68() 893.46/297.16 , U62^#(tt()) -> c_70() 893.46/297.16 , U93^#(tt(), V1, V2) -> 893.46/297.16 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.16 activate(V1), 893.46/297.16 activate(V2))) 893.46/297.16 , U94^#(tt(), V1, V2) -> 893.46/297.16 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.16 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.16 , U96^#(tt()) -> c_78() } 893.46/297.16 Obligation: 893.46/297.16 runtime complexity 893.46/297.16 Answer: 893.46/297.16 MAYBE 893.46/297.16 893.46/297.16 We estimate the number of application of {4,31,32} by applications 893.46/297.17 of Pre({4,31,32}) = {2,3,5,11,13,15,17,24}. Here rules are labeled 893.46/297.17 as follows: 893.46/297.17 893.46/297.17 DPs: 893.46/297.17 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.17 , 2: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.17 , 3: U101^#(tt(), V1, V2) -> 893.46/297.17 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 4: U102^#(tt(), V1, V2) -> 893.46/297.17 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 5: activate^#(X) -> c_10(X) 893.46/297.17 , 6: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.17 , 7: activate^#(n__take(X1, X2)) -> 893.46/297.17 c_12(take^#(activate(X1), activate(X2))) 893.46/297.17 , 8: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.17 , 9: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.17 , 10: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.17 , 11: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.17 , 12: take^#(s(M), cons(N, IL)) -> 893.46/297.17 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.17 , 13: length^#(X) -> c_39(X) 893.46/297.17 , 14: length^#(cons(N, L)) -> 893.46/297.17 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.17 , 15: s^#(X) -> c_38(X) 893.46/297.17 , 16: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.17 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 17: U41^#(tt(), V1, V2) -> 893.46/297.17 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 18: U111^#(tt(), L, N) -> 893.46/297.17 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.17 , 19: U112^#(tt(), L, N) -> 893.46/297.17 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.17 , 20: U113^#(tt(), L, N) -> 893.46/297.17 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.17 , 21: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.17 , 22: isNatList^#(n__take(V1, V2)) -> 893.46/297.17 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 23: isNatList^#(n__cons(V1, V2)) -> 893.46/297.17 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 24: U91^#(tt(), V1, V2) -> 893.46/297.17 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 25: U131^#(tt(), IL, M, N) -> 893.46/297.17 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 26: U132^#(tt(), IL, M, N) -> 893.46/297.17 c_50(U133^#(isNat(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 27: U133^#(tt(), IL, M, N) -> 893.46/297.17 c_51(U134^#(isNatKind(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 28: U134^#(tt(), IL, M, N) -> 893.46/297.17 c_52(U135^#(isNat(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 29: U135^#(tt(), IL, M, N) -> 893.46/297.17 c_53(U136^#(isNatKind(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 30: U136^#(tt(), IL, M, N) -> 893.46/297.17 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.17 , 31: U42^#(tt(), V1, V2) -> 893.46/297.17 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 32: U92^#(tt(), V1, V2) -> 893.46/297.17 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 33: zeros^#() -> c_2() 893.46/297.17 , 34: 0^#() -> c_4() 893.46/297.17 , 35: U103^#(tt(), V1, V2) -> 893.46/297.17 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 36: isNatKind^#(n__0()) -> c_7() 893.46/297.17 , 37: isNatKind^#(n__length(V1)) -> 893.46/297.17 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.17 , 38: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.17 , 39: U71^#(tt()) -> c_71() 893.46/297.17 , 40: U81^#(tt()) -> c_72() 893.46/297.17 , 41: activate^#(n__0()) -> c_13(0^#()) 893.46/297.17 , 42: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.17 , 43: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.17 , 44: length^#(nil()) -> c_41(0^#()) 893.46/297.17 , 45: nil^#() -> c_48() 893.46/297.17 , 46: U104^#(tt(), V1, V2) -> 893.46/297.17 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , 47: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.17 , 48: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.17 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.17 , 49: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.17 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.17 , 50: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.17 , 51: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.17 , 52: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.17 , 53: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.17 , 54: U106^#(tt()) -> c_28() 893.46/297.17 , 55: isNat^#(n__0()) -> c_25() 893.46/297.17 , 56: isNat^#(n__length(V1)) -> 893.46/297.17 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.17 , 57: isNat^#(n__s(V1)) -> 893.46/297.17 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.17 , 58: U11^#(tt(), V1) -> 893.46/297.17 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.17 , 59: U21^#(tt(), V1) -> 893.46/297.17 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.17 , 60: isNatIList^#(V) -> 893.46/297.17 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.17 , 61: isNatIList^#(n__zeros()) -> c_30() 893.46/297.17 , 62: U31^#(tt(), V) -> 893.46/297.17 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.17 , 63: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.17 , 64: U13^#(tt()) -> c_42() 893.46/297.17 , 65: isNatList^#(n__nil()) -> c_45() 893.46/297.17 , 66: U121^#(tt(), IL) -> 893.46/297.17 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.17 , 67: U122^#(tt()) -> c_47(nil^#()) 893.46/297.17 , 68: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.17 , 69: U23^#(tt()) -> c_57() 893.46/297.17 , 70: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.17 , 71: U33^#(tt()) -> c_60() 893.46/297.17 , 72: U43^#(tt(), V1, V2) -> 893.46/297.17 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 73: U44^#(tt(), V1, V2) -> 893.46/297.17 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , 74: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.17 , 75: U46^#(tt()) -> c_66() 893.46/297.17 , 76: U52^#(tt()) -> c_68() 893.46/297.17 , 77: U62^#(tt()) -> c_70() 893.46/297.17 , 78: U93^#(tt(), V1, V2) -> 893.46/297.17 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 79: U94^#(tt(), V1, V2) -> 893.46/297.17 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.17 , 81: U96^#(tt()) -> c_78() } 893.46/297.17 893.46/297.17 We are left with following problem, upon which TcT provides the 893.46/297.17 certificate MAYBE. 893.46/297.17 893.46/297.17 Strict DPs: 893.46/297.17 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.17 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.17 , U101^#(tt(), V1, V2) -> 893.46/297.17 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , activate^#(X) -> c_10(X) 893.46/297.17 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.17 , activate^#(n__take(X1, X2)) -> 893.46/297.17 c_12(take^#(activate(X1), activate(X2))) 893.46/297.17 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.17 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.17 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.17 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.17 , take^#(s(M), cons(N, IL)) -> 893.46/297.17 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.17 , length^#(X) -> c_39(X) 893.46/297.17 , length^#(cons(N, L)) -> 893.46/297.17 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.17 , s^#(X) -> c_38(X) 893.46/297.17 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.17 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , U41^#(tt(), V1, V2) -> 893.46/297.17 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , U111^#(tt(), L, N) -> 893.46/297.17 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.17 , U112^#(tt(), L, N) -> 893.46/297.17 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.17 , U113^#(tt(), L, N) -> 893.46/297.17 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.17 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.17 , isNatList^#(n__take(V1, V2)) -> 893.46/297.17 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.17 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , U91^#(tt(), V1, V2) -> 893.46/297.17 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , U131^#(tt(), IL, M, N) -> 893.46/297.17 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , U132^#(tt(), IL, M, N) -> 893.46/297.17 c_50(U133^#(isNat(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , U133^#(tt(), IL, M, N) -> 893.46/297.17 c_51(U134^#(isNatKind(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , U134^#(tt(), IL, M, N) -> 893.46/297.17 c_52(U135^#(isNat(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , U135^#(tt(), IL, M, N) -> 893.46/297.17 c_53(U136^#(isNatKind(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , U136^#(tt(), IL, M, N) -> 893.46/297.17 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 893.46/297.17 Strict Trs: 893.46/297.17 { zeros() -> cons(0(), n__zeros()) 893.46/297.17 , zeros() -> n__zeros() 893.46/297.17 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.17 , 0() -> n__0() 893.46/297.17 , U101(tt(), V1, V2) -> 893.46/297.17 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.17 , U102(tt(), V1, V2) -> 893.46/297.17 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.17 , isNatKind(n__0()) -> tt() 893.46/297.17 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.17 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.17 , activate(X) -> X 893.46/297.17 , activate(n__zeros()) -> zeros() 893.46/297.17 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.17 , activate(n__0()) -> 0() 893.46/297.17 , activate(n__length(X)) -> length(activate(X)) 893.46/297.17 , activate(n__s(X)) -> s(activate(X)) 893.46/297.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.17 , activate(n__nil()) -> nil() 893.46/297.17 , U103(tt(), V1, V2) -> 893.46/297.17 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.17 , isNatIListKind(n__zeros()) -> tt() 893.46/297.17 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.17 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.17 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.17 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.17 , isNatIListKind(n__nil()) -> tt() 893.46/297.17 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.17 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.17 , isNat(n__0()) -> tt() 893.46/297.17 , isNat(n__length(V1)) -> 893.46/297.17 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.17 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.17 , U106(tt()) -> tt() 893.46/297.17 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.17 , isNatIList(n__zeros()) -> tt() 893.46/297.17 , isNatIList(n__cons(V1, V2)) -> 893.46/297.17 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.17 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.17 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.17 , U111(tt(), L, N) -> 893.46/297.17 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.17 , U112(tt(), L, N) -> 893.46/297.17 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.17 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.17 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.17 , s(X) -> n__s(X) 893.46/297.17 , length(X) -> n__length(X) 893.46/297.17 , length(cons(N, L)) -> 893.46/297.17 U111(isNatList(activate(L)), activate(L), N) 893.46/297.17 , length(nil()) -> 0() 893.46/297.17 , U13(tt()) -> tt() 893.46/297.17 , isNatList(n__take(V1, V2)) -> 893.46/297.17 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.17 , isNatList(n__cons(V1, V2)) -> 893.46/297.17 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.17 , isNatList(n__nil()) -> tt() 893.46/297.17 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.17 , U122(tt()) -> nil() 893.46/297.17 , nil() -> n__nil() 893.46/297.17 , U131(tt(), IL, M, N) -> 893.46/297.17 U132(isNatIListKind(activate(IL)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N)) 893.46/297.17 , U132(tt(), IL, M, N) -> 893.46/297.17 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.17 , U133(tt(), IL, M, N) -> 893.46/297.17 U134(isNatKind(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N)) 893.46/297.17 , U134(tt(), IL, M, N) -> 893.46/297.17 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.17 , U135(tt(), IL, M, N) -> 893.46/297.17 U136(isNatKind(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N)) 893.46/297.17 , U136(tt(), IL, M, N) -> 893.46/297.17 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.17 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.17 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.17 , U23(tt()) -> tt() 893.46/297.17 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.17 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.17 , U33(tt()) -> tt() 893.46/297.17 , U41(tt(), V1, V2) -> 893.46/297.17 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.17 , U42(tt(), V1, V2) -> 893.46/297.17 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.17 , U43(tt(), V1, V2) -> 893.46/297.17 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.17 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.17 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.17 , U46(tt()) -> tt() 893.46/297.17 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.17 , U52(tt()) -> tt() 893.46/297.17 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.17 , U62(tt()) -> tt() 893.46/297.17 , U71(tt()) -> tt() 893.46/297.17 , U81(tt()) -> tt() 893.46/297.17 , U91(tt(), V1, V2) -> 893.46/297.17 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.17 , U92(tt(), V1, V2) -> 893.46/297.17 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.17 , U93(tt(), V1, V2) -> 893.46/297.17 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.17 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.17 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.17 , U96(tt()) -> tt() 893.46/297.17 , take(X1, X2) -> n__take(X1, X2) 893.46/297.17 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.17 , take(s(M), cons(N, IL)) -> 893.46/297.17 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.17 Weak DPs: 893.46/297.17 { zeros^#() -> c_2() 893.46/297.17 , 0^#() -> c_4() 893.46/297.17 , U102^#(tt(), V1, V2) -> 893.46/297.17 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , U103^#(tt(), V1, V2) -> 893.46/297.17 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , isNatKind^#(n__0()) -> c_7() 893.46/297.17 , isNatKind^#(n__length(V1)) -> 893.46/297.17 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.17 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.17 , U71^#(tt()) -> c_71() 893.46/297.17 , U81^#(tt()) -> c_72() 893.46/297.17 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.17 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.17 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.17 , length^#(nil()) -> c_41(0^#()) 893.46/297.17 , nil^#() -> c_48() 893.46/297.17 , U104^#(tt(), V1, V2) -> 893.46/297.17 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.17 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.17 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.17 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.17 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.17 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.17 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.17 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.17 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.17 , U106^#(tt()) -> c_28() 893.46/297.17 , isNat^#(n__0()) -> c_25() 893.46/297.17 , isNat^#(n__length(V1)) -> 893.46/297.17 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.17 , isNat^#(n__s(V1)) -> 893.46/297.17 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.17 , U11^#(tt(), V1) -> 893.46/297.17 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.17 , U21^#(tt(), V1) -> 893.46/297.17 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.17 , isNatIList^#(V) -> 893.46/297.17 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.17 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.17 , U31^#(tt(), V) -> 893.46/297.17 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.17 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.17 , U13^#(tt()) -> c_42() 893.46/297.17 , isNatList^#(n__nil()) -> c_45() 893.46/297.17 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.17 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.17 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.17 , U23^#(tt()) -> c_57() 893.46/297.17 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.17 , U33^#(tt()) -> c_60() 893.46/297.17 , U42^#(tt(), V1, V2) -> 893.46/297.17 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , U43^#(tt(), V1, V2) -> 893.46/297.17 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , U44^#(tt(), V1, V2) -> 893.46/297.17 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.17 , U46^#(tt()) -> c_66() 893.46/297.17 , U52^#(tt()) -> c_68() 893.46/297.17 , U62^#(tt()) -> c_70() 893.46/297.17 , U92^#(tt(), V1, V2) -> 893.46/297.17 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , U93^#(tt(), V1, V2) -> 893.46/297.17 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , U94^#(tt(), V1, V2) -> 893.46/297.17 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.17 , U96^#(tt()) -> c_78() } 893.46/297.17 Obligation: 893.46/297.17 runtime complexity 893.46/297.17 Answer: 893.46/297.17 MAYBE 893.46/297.17 893.46/297.17 We estimate the number of application of {3,16,23} by applications 893.46/297.17 of Pre({3,16,23}) = {2,4,10,12,14,15,21,22}. Here rules are labeled 893.46/297.17 as follows: 893.46/297.17 893.46/297.17 DPs: 893.46/297.17 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.17 , 2: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.17 , 3: U101^#(tt(), V1, V2) -> 893.46/297.17 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 4: activate^#(X) -> c_10(X) 893.46/297.17 , 5: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.17 , 6: activate^#(n__take(X1, X2)) -> 893.46/297.17 c_12(take^#(activate(X1), activate(X2))) 893.46/297.17 , 7: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.17 , 8: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.17 , 9: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.17 , 10: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.17 , 11: take^#(s(M), cons(N, IL)) -> 893.46/297.17 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.17 , 12: length^#(X) -> c_39(X) 893.46/297.17 , 13: length^#(cons(N, L)) -> 893.46/297.17 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.17 , 14: s^#(X) -> c_38(X) 893.46/297.17 , 15: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.17 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 16: U41^#(tt(), V1, V2) -> 893.46/297.17 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 17: U111^#(tt(), L, N) -> 893.46/297.17 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.17 , 18: U112^#(tt(), L, N) -> 893.46/297.17 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.17 , 19: U113^#(tt(), L, N) -> 893.46/297.17 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.17 , 20: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.17 , 21: isNatList^#(n__take(V1, V2)) -> 893.46/297.17 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 22: isNatList^#(n__cons(V1, V2)) -> 893.46/297.17 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 23: U91^#(tt(), V1, V2) -> 893.46/297.17 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.17 , 24: U131^#(tt(), IL, M, N) -> 893.46/297.17 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 25: U132^#(tt(), IL, M, N) -> 893.46/297.17 c_50(U133^#(isNat(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 26: U133^#(tt(), IL, M, N) -> 893.46/297.17 c_51(U134^#(isNatKind(activate(M)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 27: U134^#(tt(), IL, M, N) -> 893.46/297.17 c_52(U135^#(isNat(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 28: U135^#(tt(), IL, M, N) -> 893.46/297.17 c_53(U136^#(isNatKind(activate(N)), 893.46/297.17 activate(IL), 893.46/297.17 activate(M), 893.46/297.17 activate(N))) 893.46/297.17 , 29: U136^#(tt(), IL, M, N) -> 893.46/297.17 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.17 , 30: zeros^#() -> c_2() 893.46/297.17 , 31: 0^#() -> c_4() 893.46/297.17 , 32: U102^#(tt(), V1, V2) -> 893.46/297.17 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 33: U103^#(tt(), V1, V2) -> 893.46/297.17 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.17 activate(V1), 893.46/297.17 activate(V2))) 893.46/297.17 , 34: isNatKind^#(n__0()) -> c_7() 893.46/297.17 , 35: isNatKind^#(n__length(V1)) -> 893.46/297.17 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.17 , 36: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.17 , 37: U71^#(tt()) -> c_71() 893.46/297.17 , 38: U81^#(tt()) -> c_72() 893.46/297.17 , 39: activate^#(n__0()) -> c_13(0^#()) 893.46/297.17 , 40: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.17 , 41: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.17 , 42: length^#(nil()) -> c_41(0^#()) 893.46/297.17 , 43: nil^#() -> c_48() 893.46/297.17 , 44: U104^#(tt(), V1, V2) -> 893.46/297.17 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.17 , 45: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.17 , 46: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.17 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.17 , 47: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.17 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.17 , 48: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.17 , 49: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.17 , 50: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.17 , 51: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.17 , 52: U106^#(tt()) -> c_28() 893.46/297.17 , 53: isNat^#(n__0()) -> c_25() 893.46/297.17 , 54: isNat^#(n__length(V1)) -> 893.46/297.18 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.18 , 55: isNat^#(n__s(V1)) -> 893.46/297.18 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.18 , 56: U11^#(tt(), V1) -> 893.46/297.18 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.18 , 57: U21^#(tt(), V1) -> 893.46/297.18 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.18 , 58: isNatIList^#(V) -> 893.46/297.18 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.18 , 59: isNatIList^#(n__zeros()) -> c_30() 893.46/297.18 , 60: U31^#(tt(), V) -> 893.46/297.18 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.18 , 61: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.18 , 62: U13^#(tt()) -> c_42() 893.46/297.18 , 63: isNatList^#(n__nil()) -> c_45() 893.46/297.18 , 64: U121^#(tt(), IL) -> 893.46/297.18 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.18 , 65: U122^#(tt()) -> c_47(nil^#()) 893.46/297.18 , 66: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.18 , 67: U23^#(tt()) -> c_57() 893.46/297.18 , 68: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.18 , 69: U33^#(tt()) -> c_60() 893.46/297.18 , 70: U42^#(tt(), V1, V2) -> 893.46/297.18 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , 71: U43^#(tt(), V1, V2) -> 893.46/297.18 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , 72: U44^#(tt(), V1, V2) -> 893.46/297.18 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.18 , 73: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.18 , 74: U46^#(tt()) -> c_66() 893.46/297.18 , 75: U52^#(tt()) -> c_68() 893.46/297.18 , 76: U62^#(tt()) -> c_70() 893.46/297.18 , 77: U92^#(tt(), V1, V2) -> 893.46/297.18 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , 78: U93^#(tt(), V1, V2) -> 893.46/297.18 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , 79: U94^#(tt(), V1, V2) -> 893.46/297.18 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.18 , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.18 , 81: U96^#(tt()) -> c_78() } 893.46/297.18 893.46/297.18 We are left with following problem, upon which TcT provides the 893.46/297.18 certificate MAYBE. 893.46/297.18 893.46/297.18 Strict DPs: 893.46/297.18 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.18 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.18 , activate^#(X) -> c_10(X) 893.46/297.18 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.18 , activate^#(n__take(X1, X2)) -> 893.46/297.18 c_12(take^#(activate(X1), activate(X2))) 893.46/297.18 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.18 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.18 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.18 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.18 , take^#(s(M), cons(N, IL)) -> 893.46/297.18 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.18 , length^#(X) -> c_39(X) 893.46/297.18 , length^#(cons(N, L)) -> 893.46/297.18 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.18 , s^#(X) -> c_38(X) 893.46/297.18 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.18 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , U111^#(tt(), L, N) -> 893.46/297.18 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.18 , U112^#(tt(), L, N) -> 893.46/297.18 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.18 , U113^#(tt(), L, N) -> 893.46/297.18 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.18 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.18 , isNatList^#(n__take(V1, V2)) -> 893.46/297.18 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.18 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , U131^#(tt(), IL, M, N) -> 893.46/297.18 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , U132^#(tt(), IL, M, N) -> 893.46/297.18 c_50(U133^#(isNat(activate(M)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , U133^#(tt(), IL, M, N) -> 893.46/297.18 c_51(U134^#(isNatKind(activate(M)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , U134^#(tt(), IL, M, N) -> 893.46/297.18 c_52(U135^#(isNat(activate(N)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , U135^#(tt(), IL, M, N) -> 893.46/297.18 c_53(U136^#(isNatKind(activate(N)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , U136^#(tt(), IL, M, N) -> 893.46/297.18 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 893.46/297.18 Strict Trs: 893.46/297.18 { zeros() -> cons(0(), n__zeros()) 893.46/297.18 , zeros() -> n__zeros() 893.46/297.18 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.18 , 0() -> n__0() 893.46/297.18 , U101(tt(), V1, V2) -> 893.46/297.18 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.18 , U102(tt(), V1, V2) -> 893.46/297.18 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.18 , isNatKind(n__0()) -> tt() 893.46/297.18 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.18 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.18 , activate(X) -> X 893.46/297.18 , activate(n__zeros()) -> zeros() 893.46/297.18 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.18 , activate(n__0()) -> 0() 893.46/297.18 , activate(n__length(X)) -> length(activate(X)) 893.46/297.18 , activate(n__s(X)) -> s(activate(X)) 893.46/297.18 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.18 , activate(n__nil()) -> nil() 893.46/297.18 , U103(tt(), V1, V2) -> 893.46/297.18 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.18 , isNatIListKind(n__zeros()) -> tt() 893.46/297.18 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.18 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.18 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.18 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.18 , isNatIListKind(n__nil()) -> tt() 893.46/297.18 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.18 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.18 , isNat(n__0()) -> tt() 893.46/297.18 , isNat(n__length(V1)) -> 893.46/297.18 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.18 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.18 , U106(tt()) -> tt() 893.46/297.18 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.18 , isNatIList(n__zeros()) -> tt() 893.46/297.18 , isNatIList(n__cons(V1, V2)) -> 893.46/297.18 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.18 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.18 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.18 , U111(tt(), L, N) -> 893.46/297.18 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.18 , U112(tt(), L, N) -> 893.46/297.18 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.18 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.18 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.18 , s(X) -> n__s(X) 893.46/297.18 , length(X) -> n__length(X) 893.46/297.18 , length(cons(N, L)) -> 893.46/297.18 U111(isNatList(activate(L)), activate(L), N) 893.46/297.18 , length(nil()) -> 0() 893.46/297.18 , U13(tt()) -> tt() 893.46/297.18 , isNatList(n__take(V1, V2)) -> 893.46/297.18 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.18 , isNatList(n__cons(V1, V2)) -> 893.46/297.18 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.18 , isNatList(n__nil()) -> tt() 893.46/297.18 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.18 , U122(tt()) -> nil() 893.46/297.18 , nil() -> n__nil() 893.46/297.18 , U131(tt(), IL, M, N) -> 893.46/297.18 U132(isNatIListKind(activate(IL)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N)) 893.46/297.18 , U132(tt(), IL, M, N) -> 893.46/297.18 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.18 , U133(tt(), IL, M, N) -> 893.46/297.18 U134(isNatKind(activate(M)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N)) 893.46/297.18 , U134(tt(), IL, M, N) -> 893.46/297.18 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.18 , U135(tt(), IL, M, N) -> 893.46/297.18 U136(isNatKind(activate(N)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N)) 893.46/297.18 , U136(tt(), IL, M, N) -> 893.46/297.18 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.18 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.18 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.18 , U23(tt()) -> tt() 893.46/297.18 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.18 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.18 , U33(tt()) -> tt() 893.46/297.18 , U41(tt(), V1, V2) -> 893.46/297.18 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.18 , U42(tt(), V1, V2) -> 893.46/297.18 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.18 , U43(tt(), V1, V2) -> 893.46/297.18 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.18 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.18 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.18 , U46(tt()) -> tt() 893.46/297.18 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.18 , U52(tt()) -> tt() 893.46/297.18 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.18 , U62(tt()) -> tt() 893.46/297.18 , U71(tt()) -> tt() 893.46/297.18 , U81(tt()) -> tt() 893.46/297.18 , U91(tt(), V1, V2) -> 893.46/297.18 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.18 , U92(tt(), V1, V2) -> 893.46/297.18 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.18 , U93(tt(), V1, V2) -> 893.46/297.18 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.18 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.18 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.18 , U96(tt()) -> tt() 893.46/297.18 , take(X1, X2) -> n__take(X1, X2) 893.46/297.18 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.18 , take(s(M), cons(N, IL)) -> 893.46/297.18 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.18 Weak DPs: 893.46/297.18 { zeros^#() -> c_2() 893.46/297.18 , 0^#() -> c_4() 893.46/297.18 , U101^#(tt(), V1, V2) -> 893.46/297.18 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , U102^#(tt(), V1, V2) -> 893.46/297.18 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , U103^#(tt(), V1, V2) -> 893.46/297.18 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , isNatKind^#(n__0()) -> c_7() 893.46/297.18 , isNatKind^#(n__length(V1)) -> 893.46/297.18 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.18 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.18 , U71^#(tt()) -> c_71() 893.46/297.18 , U81^#(tt()) -> c_72() 893.46/297.18 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.18 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.18 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.18 , length^#(nil()) -> c_41(0^#()) 893.46/297.18 , nil^#() -> c_48() 893.46/297.18 , U104^#(tt(), V1, V2) -> 893.46/297.18 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.18 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.18 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.18 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.18 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.18 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.18 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.18 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.18 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.18 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.18 , U106^#(tt()) -> c_28() 893.46/297.18 , isNat^#(n__0()) -> c_25() 893.46/297.18 , isNat^#(n__length(V1)) -> 893.46/297.18 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.18 , isNat^#(n__s(V1)) -> 893.46/297.18 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.18 , U11^#(tt(), V1) -> 893.46/297.18 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.18 , U21^#(tt(), V1) -> 893.46/297.18 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.18 , isNatIList^#(V) -> 893.46/297.18 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.18 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.18 , U31^#(tt(), V) -> 893.46/297.18 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.18 , U41^#(tt(), V1, V2) -> 893.46/297.18 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.18 , U13^#(tt()) -> c_42() 893.46/297.18 , isNatList^#(n__nil()) -> c_45() 893.46/297.18 , U91^#(tt(), V1, V2) -> 893.46/297.18 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.18 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.18 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.18 , U23^#(tt()) -> c_57() 893.46/297.18 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.18 , U33^#(tt()) -> c_60() 893.46/297.18 , U42^#(tt(), V1, V2) -> 893.46/297.18 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , U43^#(tt(), V1, V2) -> 893.46/297.18 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , U44^#(tt(), V1, V2) -> 893.46/297.18 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.18 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.18 , U46^#(tt()) -> c_66() 893.46/297.18 , U52^#(tt()) -> c_68() 893.46/297.18 , U62^#(tt()) -> c_70() 893.46/297.18 , U92^#(tt(), V1, V2) -> 893.46/297.18 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , U93^#(tt(), V1, V2) -> 893.46/297.18 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.18 activate(V1), 893.46/297.18 activate(V2))) 893.46/297.18 , U94^#(tt(), V1, V2) -> 893.46/297.18 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.18 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.18 , U96^#(tt()) -> c_78() } 893.46/297.18 Obligation: 893.46/297.18 runtime complexity 893.46/297.18 Answer: 893.46/297.18 MAYBE 893.46/297.18 893.46/297.18 We estimate the number of application of {14,19,20} by applications 893.46/297.18 of Pre({14,19,20}) = {2,3,9,11,13}. Here rules are labeled as 893.46/297.18 follows: 893.46/297.18 893.46/297.18 DPs: 893.46/297.18 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.18 , 2: cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.18 , 3: activate^#(X) -> c_10(X) 893.46/297.18 , 4: activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.18 , 5: activate^#(n__take(X1, X2)) -> 893.46/297.18 c_12(take^#(activate(X1), activate(X2))) 893.46/297.18 , 6: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.18 , 7: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.18 , 8: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.18 , 9: take^#(X1, X2) -> c_79(X1, X2) 893.46/297.18 , 10: take^#(s(M), cons(N, IL)) -> 893.46/297.18 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.18 , 11: length^#(X) -> c_39(X) 893.46/297.18 , 12: length^#(cons(N, L)) -> 893.46/297.18 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.18 , 13: s^#(X) -> c_38(X) 893.46/297.18 , 14: isNatIList^#(n__cons(V1, V2)) -> 893.46/297.18 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , 15: U111^#(tt(), L, N) -> 893.46/297.18 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.18 , 16: U112^#(tt(), L, N) -> 893.46/297.18 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.18 , 17: U113^#(tt(), L, N) -> 893.46/297.18 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.18 , 18: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.18 , 19: isNatList^#(n__take(V1, V2)) -> 893.46/297.18 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , 20: isNatList^#(n__cons(V1, V2)) -> 893.46/297.18 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.18 , 21: U131^#(tt(), IL, M, N) -> 893.46/297.18 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , 22: U132^#(tt(), IL, M, N) -> 893.46/297.18 c_50(U133^#(isNat(activate(M)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , 23: U133^#(tt(), IL, M, N) -> 893.46/297.18 c_51(U134^#(isNatKind(activate(M)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , 24: U134^#(tt(), IL, M, N) -> 893.46/297.18 c_52(U135^#(isNat(activate(N)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.18 activate(N))) 893.46/297.18 , 25: U135^#(tt(), IL, M, N) -> 893.46/297.18 c_53(U136^#(isNatKind(activate(N)), 893.46/297.18 activate(IL), 893.46/297.18 activate(M), 893.46/297.19 activate(N))) 893.46/297.19 , 26: U136^#(tt(), IL, M, N) -> 893.46/297.19 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) 893.46/297.19 , 27: zeros^#() -> c_2() 893.46/297.19 , 28: 0^#() -> c_4() 893.46/297.19 , 29: U101^#(tt(), V1, V2) -> 893.46/297.19 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , 30: U102^#(tt(), V1, V2) -> 893.46/297.19 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , 31: U103^#(tt(), V1, V2) -> 893.46/297.19 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , 32: isNatKind^#(n__0()) -> c_7() 893.46/297.19 , 33: isNatKind^#(n__length(V1)) -> 893.46/297.19 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.19 , 34: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.19 , 35: U71^#(tt()) -> c_71() 893.46/297.19 , 36: U81^#(tt()) -> c_72() 893.46/297.19 , 37: activate^#(n__0()) -> c_13(0^#()) 893.46/297.19 , 38: activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.19 , 39: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.19 , 40: length^#(nil()) -> c_41(0^#()) 893.46/297.19 , 41: nil^#() -> c_48() 893.46/297.19 , 42: U104^#(tt(), V1, V2) -> 893.46/297.19 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.19 , 43: isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.19 , 44: isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.19 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.19 , 45: isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.19 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.19 , 46: isNatIListKind^#(n__nil()) -> c_22() 893.46/297.19 , 47: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.19 , 48: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.19 , 49: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.19 , 50: U106^#(tt()) -> c_28() 893.46/297.19 , 51: isNat^#(n__0()) -> c_25() 893.46/297.19 , 52: isNat^#(n__length(V1)) -> 893.46/297.19 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.19 , 53: isNat^#(n__s(V1)) -> 893.46/297.19 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.19 , 54: U11^#(tt(), V1) -> 893.46/297.19 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.19 , 55: U21^#(tt(), V1) -> 893.46/297.19 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.19 , 56: isNatIList^#(V) -> 893.46/297.19 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.19 , 57: isNatIList^#(n__zeros()) -> c_30() 893.46/297.19 , 58: U31^#(tt(), V) -> 893.46/297.19 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.19 , 59: U41^#(tt(), V1, V2) -> 893.46/297.19 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , 60: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.19 , 61: U13^#(tt()) -> c_42() 893.46/297.19 , 62: isNatList^#(n__nil()) -> c_45() 893.46/297.19 , 63: U91^#(tt(), V1, V2) -> 893.46/297.19 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , 64: U121^#(tt(), IL) -> 893.46/297.19 c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.19 , 65: U122^#(tt()) -> c_47(nil^#()) 893.46/297.19 , 66: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.19 , 67: U23^#(tt()) -> c_57() 893.46/297.19 , 68: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.19 , 69: U33^#(tt()) -> c_60() 893.46/297.19 , 70: U42^#(tt(), V1, V2) -> 893.46/297.19 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , 71: U43^#(tt(), V1, V2) -> 893.46/297.19 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , 72: U44^#(tt(), V1, V2) -> 893.46/297.19 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.19 , 73: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.19 , 74: U46^#(tt()) -> c_66() 893.46/297.19 , 75: U52^#(tt()) -> c_68() 893.46/297.19 , 76: U62^#(tt()) -> c_70() 893.46/297.19 , 77: U92^#(tt(), V1, V2) -> 893.46/297.19 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , 78: U93^#(tt(), V1, V2) -> 893.46/297.19 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , 79: U94^#(tt(), V1, V2) -> 893.46/297.19 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.19 , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.19 , 81: U96^#(tt()) -> c_78() } 893.46/297.19 893.46/297.19 We are left with following problem, upon which TcT provides the 893.46/297.19 certificate MAYBE. 893.46/297.19 893.46/297.19 Strict DPs: 893.46/297.19 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 893.46/297.19 , cons^#(X1, X2) -> c_3(X1, X2) 893.46/297.19 , activate^#(X) -> c_10(X) 893.46/297.19 , activate^#(n__zeros()) -> c_11(zeros^#()) 893.46/297.19 , activate^#(n__take(X1, X2)) -> 893.46/297.19 c_12(take^#(activate(X1), activate(X2))) 893.46/297.19 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 893.46/297.19 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 893.46/297.19 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 893.46/297.19 , take^#(X1, X2) -> c_79(X1, X2) 893.46/297.19 , take^#(s(M), cons(N, IL)) -> 893.46/297.19 c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) 893.46/297.19 , length^#(X) -> c_39(X) 893.46/297.19 , length^#(cons(N, L)) -> 893.46/297.19 c_40(U111^#(isNatList(activate(L)), activate(L), N)) 893.46/297.19 , s^#(X) -> c_38(X) 893.46/297.19 , U111^#(tt(), L, N) -> 893.46/297.19 c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) 893.46/297.19 , U112^#(tt(), L, N) -> 893.46/297.19 c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) 893.46/297.19 , U113^#(tt(), L, N) -> 893.46/297.19 c_36(U114^#(isNatKind(activate(N)), activate(L))) 893.46/297.19 , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) 893.46/297.19 , U131^#(tt(), IL, M, N) -> 893.46/297.19 c_49(U132^#(isNatIListKind(activate(IL)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N))) 893.46/297.19 , U132^#(tt(), IL, M, N) -> 893.46/297.19 c_50(U133^#(isNat(activate(M)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N))) 893.46/297.19 , U133^#(tt(), IL, M, N) -> 893.46/297.19 c_51(U134^#(isNatKind(activate(M)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N))) 893.46/297.19 , U134^#(tt(), IL, M, N) -> 893.46/297.19 c_52(U135^#(isNat(activate(N)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N))) 893.46/297.19 , U135^#(tt(), IL, M, N) -> 893.46/297.19 c_53(U136^#(isNatKind(activate(N)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N))) 893.46/297.19 , U136^#(tt(), IL, M, N) -> 893.46/297.19 c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 893.46/297.19 Strict Trs: 893.46/297.19 { zeros() -> cons(0(), n__zeros()) 893.46/297.19 , zeros() -> n__zeros() 893.46/297.19 , cons(X1, X2) -> n__cons(X1, X2) 893.46/297.19 , 0() -> n__0() 893.46/297.19 , U101(tt(), V1, V2) -> 893.46/297.19 U102(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.19 , U102(tt(), V1, V2) -> 893.46/297.19 U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.19 , isNatKind(n__0()) -> tt() 893.46/297.19 , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) 893.46/297.19 , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) 893.46/297.19 , activate(X) -> X 893.46/297.19 , activate(n__zeros()) -> zeros() 893.46/297.19 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 893.46/297.19 , activate(n__0()) -> 0() 893.46/297.19 , activate(n__length(X)) -> length(activate(X)) 893.46/297.19 , activate(n__s(X)) -> s(activate(X)) 893.46/297.19 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 893.46/297.19 , activate(n__nil()) -> nil() 893.46/297.19 , U103(tt(), V1, V2) -> 893.46/297.19 U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.19 , isNatIListKind(n__zeros()) -> tt() 893.46/297.19 , isNatIListKind(n__take(V1, V2)) -> 893.46/297.19 U61(isNatKind(activate(V1)), activate(V2)) 893.46/297.19 , isNatIListKind(n__cons(V1, V2)) -> 893.46/297.19 U51(isNatKind(activate(V1)), activate(V2)) 893.46/297.19 , isNatIListKind(n__nil()) -> tt() 893.46/297.19 , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) 893.46/297.19 , U105(tt(), V2) -> U106(isNatIList(activate(V2))) 893.46/297.19 , isNat(n__0()) -> tt() 893.46/297.19 , isNat(n__length(V1)) -> 893.46/297.19 U11(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.19 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 893.46/297.19 , U106(tt()) -> tt() 893.46/297.19 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 893.46/297.19 , isNatIList(n__zeros()) -> tt() 893.46/297.19 , isNatIList(n__cons(V1, V2)) -> 893.46/297.19 U41(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.19 , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) 893.46/297.19 , U12(tt(), V1) -> U13(isNatList(activate(V1))) 893.46/297.19 , U111(tt(), L, N) -> 893.46/297.19 U112(isNatIListKind(activate(L)), activate(L), activate(N)) 893.46/297.19 , U112(tt(), L, N) -> 893.46/297.19 U113(isNat(activate(N)), activate(L), activate(N)) 893.46/297.19 , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) 893.46/297.19 , U114(tt(), L) -> s(length(activate(L))) 893.46/297.19 , s(X) -> n__s(X) 893.46/297.19 , length(X) -> n__length(X) 893.46/297.19 , length(cons(N, L)) -> 893.46/297.19 U111(isNatList(activate(L)), activate(L), N) 893.46/297.19 , length(nil()) -> 0() 893.46/297.19 , U13(tt()) -> tt() 893.46/297.19 , isNatList(n__take(V1, V2)) -> 893.46/297.19 U101(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.19 , isNatList(n__cons(V1, V2)) -> 893.46/297.19 U91(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.19 , isNatList(n__nil()) -> tt() 893.46/297.19 , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) 893.46/297.19 , U122(tt()) -> nil() 893.46/297.19 , nil() -> n__nil() 893.46/297.19 , U131(tt(), IL, M, N) -> 893.46/297.19 U132(isNatIListKind(activate(IL)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N)) 893.46/297.19 , U132(tt(), IL, M, N) -> 893.46/297.19 U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) 893.46/297.19 , U133(tt(), IL, M, N) -> 893.46/297.19 U134(isNatKind(activate(M)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N)) 893.46/297.19 , U134(tt(), IL, M, N) -> 893.46/297.19 U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) 893.46/297.19 , U135(tt(), IL, M, N) -> 893.46/297.19 U136(isNatKind(activate(N)), 893.46/297.19 activate(IL), 893.46/297.19 activate(M), 893.46/297.19 activate(N)) 893.46/297.19 , U136(tt(), IL, M, N) -> 893.46/297.19 cons(activate(N), n__take(activate(M), activate(IL))) 893.46/297.19 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 893.46/297.19 , U22(tt(), V1) -> U23(isNat(activate(V1))) 893.46/297.19 , U23(tt()) -> tt() 893.46/297.19 , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) 893.46/297.19 , U32(tt(), V) -> U33(isNatList(activate(V))) 893.46/297.19 , U33(tt()) -> tt() 893.46/297.19 , U41(tt(), V1, V2) -> 893.46/297.19 U42(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.19 , U42(tt(), V1, V2) -> 893.46/297.19 U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.19 , U43(tt(), V1, V2) -> 893.46/297.19 U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.19 , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) 893.46/297.19 , U45(tt(), V2) -> U46(isNatIList(activate(V2))) 893.46/297.19 , U46(tt()) -> tt() 893.46/297.19 , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) 893.46/297.19 , U52(tt()) -> tt() 893.46/297.19 , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) 893.46/297.19 , U62(tt()) -> tt() 893.46/297.19 , U71(tt()) -> tt() 893.46/297.19 , U81(tt()) -> tt() 893.46/297.19 , U91(tt(), V1, V2) -> 893.46/297.19 U92(isNatKind(activate(V1)), activate(V1), activate(V2)) 893.46/297.19 , U92(tt(), V1, V2) -> 893.46/297.19 U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.19 , U93(tt(), V1, V2) -> 893.46/297.19 U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) 893.46/297.19 , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) 893.46/297.19 , U95(tt(), V2) -> U96(isNatList(activate(V2))) 893.46/297.19 , U96(tt()) -> tt() 893.46/297.19 , take(X1, X2) -> n__take(X1, X2) 893.46/297.19 , take(0(), IL) -> U121(isNatIList(IL), IL) 893.46/297.19 , take(s(M), cons(N, IL)) -> 893.46/297.19 U131(isNatIList(activate(IL)), activate(IL), M, N) } 893.46/297.19 Weak DPs: 893.46/297.19 { zeros^#() -> c_2() 893.46/297.19 , 0^#() -> c_4() 893.46/297.19 , U101^#(tt(), V1, V2) -> 893.46/297.19 c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , U102^#(tt(), V1, V2) -> 893.46/297.19 c_6(U103^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , U103^#(tt(), V1, V2) -> 893.46/297.19 c_18(U104^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , isNatKind^#(n__0()) -> c_7() 893.46/297.19 , isNatKind^#(n__length(V1)) -> 893.46/297.19 c_8(U71^#(isNatIListKind(activate(V1)))) 893.46/297.19 , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) 893.46/297.19 , U71^#(tt()) -> c_71() 893.46/297.19 , U81^#(tt()) -> c_72() 893.46/297.19 , activate^#(n__0()) -> c_13(0^#()) 893.46/297.19 , activate^#(n__nil()) -> c_17(nil^#()) 893.46/297.19 , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) 893.46/297.19 , length^#(nil()) -> c_41(0^#()) 893.46/297.19 , nil^#() -> c_48() 893.46/297.19 , U104^#(tt(), V1, V2) -> 893.46/297.19 c_23(U105^#(isNat(activate(V1)), activate(V2))) 893.46/297.19 , isNatIListKind^#(n__zeros()) -> c_19() 893.46/297.19 , isNatIListKind^#(n__take(V1, V2)) -> 893.46/297.19 c_20(U61^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.19 , isNatIListKind^#(n__cons(V1, V2)) -> 893.46/297.19 c_21(U51^#(isNatKind(activate(V1)), activate(V2))) 893.46/297.19 , isNatIListKind^#(n__nil()) -> c_22() 893.46/297.19 , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) 893.46/297.19 , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) 893.46/297.19 , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) 893.46/297.19 , U106^#(tt()) -> c_28() 893.46/297.19 , isNat^#(n__0()) -> c_25() 893.46/297.19 , isNat^#(n__length(V1)) -> 893.46/297.19 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.19 , isNat^#(n__s(V1)) -> 893.46/297.19 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.19 , U11^#(tt(), V1) -> 893.46/297.19 c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) 893.46/297.19 , U21^#(tt(), V1) -> 893.46/297.19 c_55(U22^#(isNatKind(activate(V1)), activate(V1))) 893.46/297.19 , isNatIList^#(V) -> 893.46/297.19 c_29(U31^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.19 , isNatIList^#(n__zeros()) -> c_30() 893.46/297.19 , isNatIList^#(n__cons(V1, V2)) -> 893.46/297.19 c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , U31^#(tt(), V) -> 893.46/297.19 c_58(U32^#(isNatIListKind(activate(V)), activate(V))) 893.46/297.19 , U41^#(tt(), V1, V2) -> 893.46/297.19 c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) 893.46/297.19 , U13^#(tt()) -> c_42() 893.46/297.19 , isNatList^#(n__take(V1, V2)) -> 893.46/297.19 c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , isNatList^#(n__cons(V1, V2)) -> 893.46/297.19 c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , isNatList^#(n__nil()) -> c_45() 893.46/297.19 , U91^#(tt(), V1, V2) -> 893.46/297.19 c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) 893.46/297.19 , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) 893.46/297.19 , U122^#(tt()) -> c_47(nil^#()) 893.46/297.19 , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) 893.46/297.19 , U23^#(tt()) -> c_57() 893.46/297.19 , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) 893.46/297.19 , U33^#(tt()) -> c_60() 893.46/297.19 , U42^#(tt(), V1, V2) -> 893.46/297.19 c_62(U43^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , U43^#(tt(), V1, V2) -> 893.46/297.19 c_63(U44^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , U44^#(tt(), V1, V2) -> 893.46/297.19 c_64(U45^#(isNat(activate(V1)), activate(V2))) 893.46/297.19 , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) 893.46/297.19 , U46^#(tt()) -> c_66() 893.46/297.19 , U52^#(tt()) -> c_68() 893.46/297.19 , U62^#(tt()) -> c_70() 893.46/297.19 , U92^#(tt(), V1, V2) -> 893.46/297.19 c_74(U93^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , U93^#(tt(), V1, V2) -> 893.46/297.19 c_75(U94^#(isNatIListKind(activate(V2)), 893.46/297.19 activate(V1), 893.46/297.19 activate(V2))) 893.46/297.19 , U94^#(tt(), V1, V2) -> 893.46/297.19 c_76(U95^#(isNat(activate(V1)), activate(V2))) 893.46/297.19 , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) 893.46/297.19 , U96^#(tt()) -> c_78() } 893.46/297.19 Obligation: 893.46/297.19 runtime complexity 893.46/297.19 Answer: 893.46/297.19 MAYBE 893.46/297.19 893.46/297.19 Empty strict component of the problem is NOT empty. 893.46/297.19 893.46/297.19 893.46/297.19 Arrrr.. 893.68/297.26 EOF