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