MAYBE 920.38/297.14 MAYBE 920.38/297.14 920.38/297.14 We are left with following problem, upon which TcT provides the 920.38/297.14 certificate MAYBE. 920.38/297.14 920.38/297.14 Strict Trs: 920.38/297.14 { zeros() -> cons(0(), n__zeros()) 920.38/297.14 , zeros() -> n__zeros() 920.38/297.14 , cons(X1, X2) -> n__cons(X1, X2) 920.38/297.14 , 0() -> n__0() 920.38/297.14 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 920.38/297.14 , U12(tt()) -> tt() 920.38/297.14 , isNatList(n__take(V1, V2)) -> 920.38/297.14 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2)) 920.38/297.14 , isNatList(n__cons(V1, V2)) -> 920.38/297.14 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2)) 920.38/297.14 , isNatList(n__nil()) -> tt() 920.38/297.14 , activate(X) -> X 920.38/297.14 , activate(n__zeros()) -> zeros() 920.38/297.14 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 920.38/297.14 , activate(n__0()) -> 0() 920.38/297.14 , activate(n__length(X)) -> length(activate(X)) 920.38/297.14 , activate(n__s(X)) -> s(activate(X)) 920.38/297.14 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 920.38/297.14 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 920.38/297.14 , activate(n__nil()) -> nil() 920.38/297.14 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 920.38/297.14 , activate(n__isNat(X)) -> isNat(X) 920.38/297.14 , activate(n__isNatKind(X)) -> isNatKind(X) 920.38/297.14 , U21(tt(), V1) -> U22(isNat(activate(V1))) 920.38/297.14 , U22(tt()) -> tt() 920.38/297.14 , isNat(X) -> n__isNat(X) 920.38/297.14 , isNat(n__0()) -> tt() 920.38/297.14 , isNat(n__length(V1)) -> 920.38/297.14 U11(isNatIListKind(activate(V1)), activate(V1)) 920.38/297.14 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 920.38/297.14 , U31(tt(), V) -> U32(isNatList(activate(V))) 920.38/297.14 , U32(tt()) -> tt() 920.38/297.14 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 920.38/297.14 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 920.38/297.14 , U43(tt()) -> tt() 920.38/297.14 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 920.38/297.14 , isNatIList(n__zeros()) -> tt() 920.38/297.14 , isNatIList(n__cons(V1, V2)) -> 920.38/297.14 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2)) 920.38/297.14 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 920.38/297.14 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 920.38/297.14 , U53(tt()) -> tt() 920.38/297.14 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 920.38/297.14 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 920.38/297.14 , U63(tt()) -> tt() 920.38/297.14 , U71(tt(), L) -> s(length(activate(L))) 920.38/297.14 , s(X) -> n__s(X) 920.38/297.14 , length(X) -> n__length(X) 920.38/297.14 , length(cons(N, L)) -> 920.38/297.14 U71(and(and(isNatList(activate(L)), 920.38/297.14 n__isNatIListKind(activate(L))), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.14 activate(L)) 920.38/297.14 , length(nil()) -> 0() 920.38/297.14 , U81(tt()) -> nil() 920.38/297.14 , nil() -> n__nil() 920.38/297.14 , U91(tt(), IL, M, N) -> 920.38/297.14 cons(activate(N), n__take(activate(M), activate(IL))) 920.38/297.14 , and(X1, X2) -> n__and(X1, X2) 920.38/297.14 , and(tt(), X) -> activate(X) 920.38/297.14 , isNatIListKind(X) -> n__isNatIListKind(X) 920.38/297.14 , isNatIListKind(n__zeros()) -> tt() 920.38/297.14 , isNatIListKind(n__take(V1, V2)) -> 920.38/297.14 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.14 , isNatIListKind(n__cons(V1, V2)) -> 920.38/297.14 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.14 , isNatIListKind(n__nil()) -> tt() 920.38/297.14 , isNatKind(X) -> n__isNatKind(X) 920.38/297.14 , isNatKind(n__0()) -> tt() 920.38/297.14 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 920.38/297.14 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 920.38/297.14 , take(X1, X2) -> n__take(X1, X2) 920.38/297.14 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 920.38/297.14 , take(s(M), cons(N, IL)) -> 920.38/297.14 U91(and(and(isNatIList(activate(IL)), 920.38/297.14 n__isNatIListKind(activate(IL))), 920.38/297.14 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.14 activate(IL), 920.38/297.14 M, 920.38/297.14 N) } 920.38/297.14 Obligation: 920.38/297.14 runtime complexity 920.38/297.14 Answer: 920.38/297.14 MAYBE 920.38/297.14 920.38/297.14 None of the processors succeeded. 920.38/297.14 920.38/297.14 Details of failed attempt(s): 920.38/297.14 ----------------------------- 920.38/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 920.38/297.14 following reason: 920.38/297.14 920.38/297.14 Computation stopped due to timeout after 297.0 seconds. 920.38/297.14 920.38/297.14 2) 'Best' failed due to the following reason: 920.38/297.14 920.38/297.14 None of the processors succeeded. 920.38/297.14 920.38/297.14 Details of failed attempt(s): 920.38/297.14 ----------------------------- 920.38/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 920.38/297.14 seconds)' failed due to the following reason: 920.38/297.14 920.38/297.14 Computation stopped due to timeout after 148.0 seconds. 920.38/297.14 920.38/297.14 2) 'Best' failed due to the following reason: 920.38/297.14 920.38/297.14 None of the processors succeeded. 920.38/297.14 920.38/297.14 Details of failed attempt(s): 920.38/297.14 ----------------------------- 920.38/297.14 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 920.38/297.14 following reason: 920.38/297.14 920.38/297.14 The processor is inapplicable, reason: 920.38/297.14 Processor only applicable for innermost runtime complexity analysis 920.38/297.14 920.38/297.14 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 920.38/297.14 to the following reason: 920.38/297.14 920.38/297.14 The processor is inapplicable, reason: 920.38/297.14 Processor only applicable for innermost runtime complexity analysis 920.38/297.14 920.38/297.14 920.38/297.14 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 920.38/297.14 failed due to the following reason: 920.38/297.14 920.38/297.14 None of the processors succeeded. 920.38/297.14 920.38/297.14 Details of failed attempt(s): 920.38/297.14 ----------------------------- 920.38/297.14 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 920.38/297.14 failed due to the following reason: 920.38/297.14 920.38/297.14 match-boundness of the problem could not be verified. 920.38/297.14 920.38/297.14 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 920.38/297.14 failed due to the following reason: 920.38/297.14 920.38/297.14 match-boundness of the problem could not be verified. 920.38/297.14 920.38/297.14 920.38/297.14 920.38/297.14 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 920.38/297.14 the following reason: 920.38/297.14 920.38/297.14 We add the following weak dependency pairs: 920.38/297.14 920.38/297.14 Strict DPs: 920.38/297.14 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.14 , zeros^#() -> c_2() 920.38/297.14 , cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.14 , 0^#() -> c_4() 920.38/297.14 , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.14 , U12^#(tt()) -> c_6() 920.38/297.14 , isNatList^#(n__take(V1, V2)) -> 920.38/297.14 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2))) 920.38/297.14 , isNatList^#(n__cons(V1, V2)) -> 920.38/297.14 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2))) 920.38/297.14 , isNatList^#(n__nil()) -> c_9() 920.38/297.14 , U61^#(tt(), V1, V2) -> 920.38/297.14 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.14 , U51^#(tt(), V1, V2) -> 920.38/297.14 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.14 , activate^#(X) -> c_10(X) 920.38/297.14 , activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.14 , activate^#(n__take(X1, X2)) -> 920.38/297.14 c_12(take^#(activate(X1), activate(X2))) 920.38/297.14 , activate^#(n__0()) -> c_13(0^#()) 920.38/297.14 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.14 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.14 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.14 , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.14 , activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.14 , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.14 , activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.14 , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.14 , take^#(X1, X2) -> c_61(X1, X2) 920.38/297.14 , take^#(0(), IL) -> 920.38/297.14 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.14 , take^#(s(M), cons(N, IL)) -> 920.38/297.14 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.14 n__isNatIListKind(activate(IL))), 920.38/297.14 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.14 activate(IL), 920.38/297.14 M, 920.38/297.14 N)) 920.38/297.14 , length^#(X) -> c_44(X) 920.38/297.14 , length^#(cons(N, L)) -> 920.38/297.14 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.14 n__isNatIListKind(activate(L))), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.14 activate(L))) 920.38/297.14 , length^#(nil()) -> c_46(0^#()) 920.38/297.14 , s^#(X) -> c_43(X) 920.38/297.14 , isNatIListKind^#(X) -> c_52(X) 920.38/297.14 , isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.14 , isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.14 c_54(and^#(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2)))) 920.38/297.14 , isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.14 c_55(and^#(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2)))) 920.38/297.14 , isNatIListKind^#(n__nil()) -> c_56() 920.38/297.14 , nil^#() -> c_48() 920.38/297.14 , and^#(X1, X2) -> c_50(X1, X2) 920.38/297.14 , and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.14 , isNat^#(X) -> c_24(X) 920.38/297.14 , isNat^#(n__0()) -> c_25() 920.38/297.14 , isNat^#(n__length(V1)) -> 920.38/297.14 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.14 , isNat^#(n__s(V1)) -> 920.38/297.14 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.14 , isNatKind^#(X) -> c_57(X) 920.38/297.14 , isNatKind^#(n__0()) -> c_58() 920.38/297.14 , isNatKind^#(n__length(V1)) -> 920.38/297.14 c_59(isNatIListKind^#(activate(V1))) 920.38/297.14 , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.14 , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.14 , U22^#(tt()) -> c_23() 920.38/297.14 , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.14 , U32^#(tt()) -> c_29() 920.38/297.14 , U41^#(tt(), V1, V2) -> 920.38/297.14 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.14 , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.14 , U43^#(tt()) -> c_32() 920.38/297.14 , isNatIList^#(V) -> 920.38/297.14 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.14 , isNatIList^#(n__zeros()) -> c_34() 920.38/297.14 , isNatIList^#(n__cons(V1, V2)) -> 920.38/297.14 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2))) 920.38/297.14 , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.14 , U53^#(tt()) -> c_38() 920.38/297.14 , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.14 , U63^#(tt()) -> c_41() 920.38/297.14 , U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.14 , U81^#(tt()) -> c_47(nil^#()) 920.38/297.14 , U91^#(tt(), IL, M, N) -> 920.38/297.14 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.14 920.38/297.14 and mark the set of starting terms. 920.38/297.14 920.38/297.14 We are left with following problem, upon which TcT provides the 920.38/297.14 certificate MAYBE. 920.38/297.14 920.38/297.14 Strict DPs: 920.38/297.14 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.14 , zeros^#() -> c_2() 920.38/297.14 , cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.14 , 0^#() -> c_4() 920.38/297.14 , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.14 , U12^#(tt()) -> c_6() 920.38/297.14 , isNatList^#(n__take(V1, V2)) -> 920.38/297.14 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2))) 920.38/297.14 , isNatList^#(n__cons(V1, V2)) -> 920.38/297.14 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2))) 920.38/297.14 , isNatList^#(n__nil()) -> c_9() 920.38/297.14 , U61^#(tt(), V1, V2) -> 920.38/297.14 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.14 , U51^#(tt(), V1, V2) -> 920.38/297.14 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.14 , activate^#(X) -> c_10(X) 920.38/297.14 , activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.14 , activate^#(n__take(X1, X2)) -> 920.38/297.14 c_12(take^#(activate(X1), activate(X2))) 920.38/297.14 , activate^#(n__0()) -> c_13(0^#()) 920.38/297.14 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.14 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.14 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.14 , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.14 , activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.14 , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.14 , activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.14 , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.14 , take^#(X1, X2) -> c_61(X1, X2) 920.38/297.14 , take^#(0(), IL) -> 920.38/297.14 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.14 , take^#(s(M), cons(N, IL)) -> 920.38/297.14 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.14 n__isNatIListKind(activate(IL))), 920.38/297.14 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.14 activate(IL), 920.38/297.14 M, 920.38/297.14 N)) 920.38/297.14 , length^#(X) -> c_44(X) 920.38/297.14 , length^#(cons(N, L)) -> 920.38/297.14 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.14 n__isNatIListKind(activate(L))), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.14 activate(L))) 920.38/297.14 , length^#(nil()) -> c_46(0^#()) 920.38/297.14 , s^#(X) -> c_43(X) 920.38/297.14 , isNatIListKind^#(X) -> c_52(X) 920.38/297.14 , isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.14 , isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.14 c_54(and^#(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2)))) 920.38/297.14 , isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.14 c_55(and^#(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2)))) 920.38/297.14 , isNatIListKind^#(n__nil()) -> c_56() 920.38/297.14 , nil^#() -> c_48() 920.38/297.14 , and^#(X1, X2) -> c_50(X1, X2) 920.38/297.14 , and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.14 , isNat^#(X) -> c_24(X) 920.38/297.14 , isNat^#(n__0()) -> c_25() 920.38/297.14 , isNat^#(n__length(V1)) -> 920.38/297.14 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.14 , isNat^#(n__s(V1)) -> 920.38/297.14 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.14 , isNatKind^#(X) -> c_57(X) 920.38/297.14 , isNatKind^#(n__0()) -> c_58() 920.38/297.14 , isNatKind^#(n__length(V1)) -> 920.38/297.14 c_59(isNatIListKind^#(activate(V1))) 920.38/297.14 , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.14 , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.14 , U22^#(tt()) -> c_23() 920.38/297.14 , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.14 , U32^#(tt()) -> c_29() 920.38/297.14 , U41^#(tt(), V1, V2) -> 920.38/297.14 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.14 , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.14 , U43^#(tt()) -> c_32() 920.38/297.14 , isNatIList^#(V) -> 920.38/297.14 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.14 , isNatIList^#(n__zeros()) -> c_34() 920.38/297.14 , isNatIList^#(n__cons(V1, V2)) -> 920.38/297.14 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.14 n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2))) 920.38/297.14 , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.14 , U53^#(tt()) -> c_38() 920.38/297.14 , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.14 , U63^#(tt()) -> c_41() 920.38/297.14 , U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.14 , U81^#(tt()) -> c_47(nil^#()) 920.38/297.14 , U91^#(tt(), IL, M, N) -> 920.38/297.14 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.14 Strict Trs: 920.38/297.14 { zeros() -> cons(0(), n__zeros()) 920.38/297.14 , zeros() -> n__zeros() 920.38/297.14 , cons(X1, X2) -> n__cons(X1, X2) 920.38/297.14 , 0() -> n__0() 920.38/297.14 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 920.38/297.14 , U12(tt()) -> tt() 920.38/297.14 , isNatList(n__take(V1, V2)) -> 920.38/297.14 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2)) 920.38/297.14 , isNatList(n__cons(V1, V2)) -> 920.38/297.14 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2)) 920.38/297.14 , isNatList(n__nil()) -> tt() 920.38/297.14 , activate(X) -> X 920.38/297.14 , activate(n__zeros()) -> zeros() 920.38/297.14 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 920.38/297.14 , activate(n__0()) -> 0() 920.38/297.14 , activate(n__length(X)) -> length(activate(X)) 920.38/297.14 , activate(n__s(X)) -> s(activate(X)) 920.38/297.14 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 920.38/297.14 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 920.38/297.14 , activate(n__nil()) -> nil() 920.38/297.14 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 920.38/297.14 , activate(n__isNat(X)) -> isNat(X) 920.38/297.14 , activate(n__isNatKind(X)) -> isNatKind(X) 920.38/297.14 , U21(tt(), V1) -> U22(isNat(activate(V1))) 920.38/297.14 , U22(tt()) -> tt() 920.38/297.14 , isNat(X) -> n__isNat(X) 920.38/297.14 , isNat(n__0()) -> tt() 920.38/297.14 , isNat(n__length(V1)) -> 920.38/297.14 U11(isNatIListKind(activate(V1)), activate(V1)) 920.38/297.14 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 920.38/297.14 , U31(tt(), V) -> U32(isNatList(activate(V))) 920.38/297.14 , U32(tt()) -> tt() 920.38/297.14 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 920.38/297.14 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 920.38/297.14 , U43(tt()) -> tt() 920.38/297.14 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 920.38/297.14 , isNatIList(n__zeros()) -> tt() 920.38/297.14 , isNatIList(n__cons(V1, V2)) -> 920.38/297.14 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.14 activate(V1), 920.38/297.14 activate(V2)) 920.38/297.14 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 920.38/297.14 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 920.38/297.14 , U53(tt()) -> tt() 920.38/297.14 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 920.38/297.14 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 920.38/297.14 , U63(tt()) -> tt() 920.38/297.14 , U71(tt(), L) -> s(length(activate(L))) 920.38/297.14 , s(X) -> n__s(X) 920.38/297.14 , length(X) -> n__length(X) 920.38/297.14 , length(cons(N, L)) -> 920.38/297.14 U71(and(and(isNatList(activate(L)), 920.38/297.14 n__isNatIListKind(activate(L))), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.14 activate(L)) 920.38/297.14 , length(nil()) -> 0() 920.38/297.14 , U81(tt()) -> nil() 920.38/297.14 , nil() -> n__nil() 920.38/297.14 , U91(tt(), IL, M, N) -> 920.38/297.14 cons(activate(N), n__take(activate(M), activate(IL))) 920.38/297.14 , and(X1, X2) -> n__and(X1, X2) 920.38/297.14 , and(tt(), X) -> activate(X) 920.38/297.14 , isNatIListKind(X) -> n__isNatIListKind(X) 920.38/297.14 , isNatIListKind(n__zeros()) -> tt() 920.38/297.14 , isNatIListKind(n__take(V1, V2)) -> 920.38/297.14 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.14 , isNatIListKind(n__cons(V1, V2)) -> 920.38/297.14 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.14 , isNatIListKind(n__nil()) -> tt() 920.38/297.14 , isNatKind(X) -> n__isNatKind(X) 920.38/297.14 , isNatKind(n__0()) -> tt() 920.38/297.14 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 920.38/297.14 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 920.38/297.14 , take(X1, X2) -> n__take(X1, X2) 920.38/297.14 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 920.38/297.14 , take(s(M), cons(N, IL)) -> 920.38/297.14 U91(and(and(isNatIList(activate(IL)), 920.38/297.14 n__isNatIListKind(activate(IL))), 920.38/297.14 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.14 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.14 activate(IL), 920.38/297.15 M, 920.38/297.15 N) } 920.38/297.15 Obligation: 920.38/297.15 runtime complexity 920.38/297.15 Answer: 920.38/297.15 MAYBE 920.38/297.15 920.38/297.15 We estimate the number of application of 920.38/297.15 {2,4,6,9,32,35,36,40,44,48,50,53,55,58,60} by applications of 920.38/297.15 Pre({2,4,6,9,32,35,36,40,44,48,50,53,55,58,60}) = 920.38/297.15 {3,5,12,13,15,19,20,22,23,24,27,29,30,31,37,39,43,45,46,47,49,52,57,59,62}. 920.38/297.15 Here rules are labeled as follows: 920.38/297.15 920.38/297.15 DPs: 920.38/297.15 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.15 , 2: zeros^#() -> c_2() 920.38/297.15 , 3: cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.15 , 4: 0^#() -> c_4() 920.38/297.15 , 5: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.15 , 6: U12^#(tt()) -> c_6() 920.38/297.15 , 7: isNatList^#(n__take(V1, V2)) -> 920.38/297.15 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , 8: isNatList^#(n__cons(V1, V2)) -> 920.38/297.15 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , 9: isNatList^#(n__nil()) -> c_9() 920.38/297.15 , 10: U61^#(tt(), V1, V2) -> 920.38/297.15 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , 11: U51^#(tt(), V1, V2) -> 920.38/297.15 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , 12: activate^#(X) -> c_10(X) 920.38/297.15 , 13: activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.15 , 14: activate^#(n__take(X1, X2)) -> 920.38/297.15 c_12(take^#(activate(X1), activate(X2))) 920.38/297.15 , 15: activate^#(n__0()) -> c_13(0^#()) 920.38/297.15 , 16: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.15 , 17: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.15 , 18: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.15 , 19: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.15 , 20: activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.15 , 21: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.15 , 22: activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.15 , 23: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.15 , 24: take^#(X1, X2) -> c_61(X1, X2) 920.38/297.15 , 25: take^#(0(), IL) -> 920.38/297.15 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.15 , 26: take^#(s(M), cons(N, IL)) -> 920.38/297.15 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.15 n__isNatIListKind(activate(IL))), 920.38/297.15 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.15 activate(IL), 920.38/297.15 M, 920.38/297.15 N)) 920.38/297.15 , 27: length^#(X) -> c_44(X) 920.38/297.15 , 28: length^#(cons(N, L)) -> 920.38/297.15 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.15 n__isNatIListKind(activate(L))), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.15 activate(L))) 920.38/297.15 , 29: length^#(nil()) -> c_46(0^#()) 920.38/297.15 , 30: s^#(X) -> c_43(X) 920.38/297.15 , 31: isNatIListKind^#(X) -> c_52(X) 920.38/297.15 , 32: isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.15 , 33: isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.15 c_54(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , 34: isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.15 c_55(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , 35: isNatIListKind^#(n__nil()) -> c_56() 920.38/297.15 , 36: nil^#() -> c_48() 920.38/297.15 , 37: and^#(X1, X2) -> c_50(X1, X2) 920.38/297.15 , 38: and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.15 , 39: isNat^#(X) -> c_24(X) 920.38/297.15 , 40: isNat^#(n__0()) -> c_25() 920.38/297.15 , 41: isNat^#(n__length(V1)) -> 920.38/297.15 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.15 , 42: isNat^#(n__s(V1)) -> 920.38/297.15 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.15 , 43: isNatKind^#(X) -> c_57(X) 920.38/297.15 , 44: isNatKind^#(n__0()) -> c_58() 920.38/297.15 , 45: isNatKind^#(n__length(V1)) -> 920.38/297.15 c_59(isNatIListKind^#(activate(V1))) 920.38/297.15 , 46: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.15 , 47: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.15 , 48: U22^#(tt()) -> c_23() 920.38/297.15 , 49: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.15 , 50: U32^#(tt()) -> c_29() 920.38/297.15 , 51: U41^#(tt(), V1, V2) -> 920.38/297.15 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , 52: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.15 , 53: U43^#(tt()) -> c_32() 920.38/297.15 , 54: isNatIList^#(V) -> 920.38/297.15 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.15 , 55: isNatIList^#(n__zeros()) -> c_34() 920.38/297.15 , 56: isNatIList^#(n__cons(V1, V2)) -> 920.38/297.15 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , 57: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.15 , 58: U53^#(tt()) -> c_38() 920.38/297.15 , 59: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.15 , 60: U63^#(tt()) -> c_41() 920.38/297.15 , 61: U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.15 , 62: U81^#(tt()) -> c_47(nil^#()) 920.38/297.15 , 63: U91^#(tt(), IL, M, N) -> 920.38/297.15 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.15 920.38/297.15 We are left with following problem, upon which TcT provides the 920.38/297.15 certificate MAYBE. 920.38/297.15 920.38/297.15 Strict DPs: 920.38/297.15 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.15 , cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.15 , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.15 , isNatList^#(n__take(V1, V2)) -> 920.38/297.15 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , isNatList^#(n__cons(V1, V2)) -> 920.38/297.15 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , U61^#(tt(), V1, V2) -> 920.38/297.15 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , U51^#(tt(), V1, V2) -> 920.38/297.15 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , activate^#(X) -> c_10(X) 920.38/297.15 , activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.15 , activate^#(n__take(X1, X2)) -> 920.38/297.15 c_12(take^#(activate(X1), activate(X2))) 920.38/297.15 , activate^#(n__0()) -> c_13(0^#()) 920.38/297.15 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.15 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.15 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.15 , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.15 , activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.15 , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.15 , activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.15 , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.15 , take^#(X1, X2) -> c_61(X1, X2) 920.38/297.15 , take^#(0(), IL) -> 920.38/297.15 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.15 , take^#(s(M), cons(N, IL)) -> 920.38/297.15 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.15 n__isNatIListKind(activate(IL))), 920.38/297.15 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.15 activate(IL), 920.38/297.15 M, 920.38/297.15 N)) 920.38/297.15 , length^#(X) -> c_44(X) 920.38/297.15 , length^#(cons(N, L)) -> 920.38/297.15 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.15 n__isNatIListKind(activate(L))), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.15 activate(L))) 920.38/297.15 , length^#(nil()) -> c_46(0^#()) 920.38/297.15 , s^#(X) -> c_43(X) 920.38/297.15 , isNatIListKind^#(X) -> c_52(X) 920.38/297.15 , isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.15 c_54(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.15 c_55(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , and^#(X1, X2) -> c_50(X1, X2) 920.38/297.15 , and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.15 , isNat^#(X) -> c_24(X) 920.38/297.15 , isNat^#(n__length(V1)) -> 920.38/297.15 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.15 , isNat^#(n__s(V1)) -> 920.38/297.15 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.15 , isNatKind^#(X) -> c_57(X) 920.38/297.15 , isNatKind^#(n__length(V1)) -> 920.38/297.15 c_59(isNatIListKind^#(activate(V1))) 920.38/297.15 , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.15 , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.15 , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.15 , U41^#(tt(), V1, V2) -> 920.38/297.15 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.15 , isNatIList^#(V) -> 920.38/297.15 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.15 , isNatIList^#(n__cons(V1, V2)) -> 920.38/297.15 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.15 , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.15 , U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.15 , U81^#(tt()) -> c_47(nil^#()) 920.38/297.15 , U91^#(tt(), IL, M, N) -> 920.38/297.15 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.15 Strict Trs: 920.38/297.15 { zeros() -> cons(0(), n__zeros()) 920.38/297.15 , zeros() -> n__zeros() 920.38/297.15 , cons(X1, X2) -> n__cons(X1, X2) 920.38/297.15 , 0() -> n__0() 920.38/297.15 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 920.38/297.15 , U12(tt()) -> tt() 920.38/297.15 , isNatList(n__take(V1, V2)) -> 920.38/297.15 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2)) 920.38/297.15 , isNatList(n__cons(V1, V2)) -> 920.38/297.15 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2)) 920.38/297.15 , isNatList(n__nil()) -> tt() 920.38/297.15 , activate(X) -> X 920.38/297.15 , activate(n__zeros()) -> zeros() 920.38/297.15 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 920.38/297.15 , activate(n__0()) -> 0() 920.38/297.15 , activate(n__length(X)) -> length(activate(X)) 920.38/297.15 , activate(n__s(X)) -> s(activate(X)) 920.38/297.15 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 920.38/297.15 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 920.38/297.15 , activate(n__nil()) -> nil() 920.38/297.15 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 920.38/297.15 , activate(n__isNat(X)) -> isNat(X) 920.38/297.15 , activate(n__isNatKind(X)) -> isNatKind(X) 920.38/297.15 , U21(tt(), V1) -> U22(isNat(activate(V1))) 920.38/297.15 , U22(tt()) -> tt() 920.38/297.15 , isNat(X) -> n__isNat(X) 920.38/297.15 , isNat(n__0()) -> tt() 920.38/297.15 , isNat(n__length(V1)) -> 920.38/297.15 U11(isNatIListKind(activate(V1)), activate(V1)) 920.38/297.15 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 920.38/297.15 , U31(tt(), V) -> U32(isNatList(activate(V))) 920.38/297.15 , U32(tt()) -> tt() 920.38/297.15 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 920.38/297.15 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 920.38/297.15 , U43(tt()) -> tt() 920.38/297.15 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 920.38/297.15 , isNatIList(n__zeros()) -> tt() 920.38/297.15 , isNatIList(n__cons(V1, V2)) -> 920.38/297.15 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2)) 920.38/297.15 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 920.38/297.15 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 920.38/297.15 , U53(tt()) -> tt() 920.38/297.15 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 920.38/297.15 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 920.38/297.15 , U63(tt()) -> tt() 920.38/297.15 , U71(tt(), L) -> s(length(activate(L))) 920.38/297.15 , s(X) -> n__s(X) 920.38/297.15 , length(X) -> n__length(X) 920.38/297.15 , length(cons(N, L)) -> 920.38/297.15 U71(and(and(isNatList(activate(L)), 920.38/297.15 n__isNatIListKind(activate(L))), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.15 activate(L)) 920.38/297.15 , length(nil()) -> 0() 920.38/297.15 , U81(tt()) -> nil() 920.38/297.15 , nil() -> n__nil() 920.38/297.15 , U91(tt(), IL, M, N) -> 920.38/297.15 cons(activate(N), n__take(activate(M), activate(IL))) 920.38/297.15 , and(X1, X2) -> n__and(X1, X2) 920.38/297.15 , and(tt(), X) -> activate(X) 920.38/297.15 , isNatIListKind(X) -> n__isNatIListKind(X) 920.38/297.15 , isNatIListKind(n__zeros()) -> tt() 920.38/297.15 , isNatIListKind(n__take(V1, V2)) -> 920.38/297.15 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.15 , isNatIListKind(n__cons(V1, V2)) -> 920.38/297.15 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.15 , isNatIListKind(n__nil()) -> tt() 920.38/297.15 , isNatKind(X) -> n__isNatKind(X) 920.38/297.15 , isNatKind(n__0()) -> tt() 920.38/297.15 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 920.38/297.15 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 920.38/297.15 , take(X1, X2) -> n__take(X1, X2) 920.38/297.15 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 920.38/297.15 , take(s(M), cons(N, IL)) -> 920.38/297.15 U91(and(and(isNatIList(activate(IL)), 920.38/297.15 n__isNatIListKind(activate(IL))), 920.38/297.15 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.15 activate(IL), 920.38/297.15 M, 920.38/297.15 N) } 920.38/297.15 Weak DPs: 920.38/297.15 { zeros^#() -> c_2() 920.38/297.15 , 0^#() -> c_4() 920.38/297.15 , U12^#(tt()) -> c_6() 920.38/297.15 , isNatList^#(n__nil()) -> c_9() 920.38/297.15 , isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.15 , isNatIListKind^#(n__nil()) -> c_56() 920.38/297.15 , nil^#() -> c_48() 920.38/297.15 , isNat^#(n__0()) -> c_25() 920.38/297.15 , isNatKind^#(n__0()) -> c_58() 920.38/297.15 , U22^#(tt()) -> c_23() 920.38/297.15 , U32^#(tt()) -> c_29() 920.38/297.15 , U43^#(tt()) -> c_32() 920.38/297.15 , isNatIList^#(n__zeros()) -> c_34() 920.38/297.15 , U53^#(tt()) -> c_38() 920.38/297.15 , U63^#(tt()) -> c_41() } 920.38/297.15 Obligation: 920.38/297.15 runtime complexity 920.38/297.15 Answer: 920.38/297.15 MAYBE 920.38/297.15 920.38/297.15 We estimate the number of application of 920.38/297.15 {3,11,16,25,38,39,41,44,45,47} by applications of 920.38/297.15 Pre({3,11,16,25,38,39,41,44,45,47}) = 920.38/297.15 {2,6,7,8,12,20,21,23,26,27,30,31,32,33,34,35,40,42}. Here rules are 920.38/297.15 labeled as follows: 920.38/297.15 920.38/297.15 DPs: 920.38/297.15 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.15 , 2: cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.15 , 3: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.15 , 4: isNatList^#(n__take(V1, V2)) -> 920.38/297.15 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , 5: isNatList^#(n__cons(V1, V2)) -> 920.38/297.15 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , 6: U61^#(tt(), V1, V2) -> 920.38/297.15 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , 7: U51^#(tt(), V1, V2) -> 920.38/297.15 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , 8: activate^#(X) -> c_10(X) 920.38/297.15 , 9: activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.15 , 10: activate^#(n__take(X1, X2)) -> 920.38/297.15 c_12(take^#(activate(X1), activate(X2))) 920.38/297.15 , 11: activate^#(n__0()) -> c_13(0^#()) 920.38/297.15 , 12: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.15 , 13: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.15 , 14: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.15 , 15: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.15 , 16: activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.15 , 17: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.15 , 18: activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.15 , 19: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.15 , 20: take^#(X1, X2) -> c_61(X1, X2) 920.38/297.15 , 21: take^#(0(), IL) -> 920.38/297.15 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.15 , 22: take^#(s(M), cons(N, IL)) -> 920.38/297.15 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.15 n__isNatIListKind(activate(IL))), 920.38/297.15 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.15 activate(IL), 920.38/297.15 M, 920.38/297.15 N)) 920.38/297.15 , 23: length^#(X) -> c_44(X) 920.38/297.15 , 24: length^#(cons(N, L)) -> 920.38/297.15 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.15 n__isNatIListKind(activate(L))), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.15 activate(L))) 920.38/297.15 , 25: length^#(nil()) -> c_46(0^#()) 920.38/297.15 , 26: s^#(X) -> c_43(X) 920.38/297.15 , 27: isNatIListKind^#(X) -> c_52(X) 920.38/297.15 , 28: isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.15 c_54(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , 29: isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.15 c_55(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , 30: and^#(X1, X2) -> c_50(X1, X2) 920.38/297.15 , 31: and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.15 , 32: isNat^#(X) -> c_24(X) 920.38/297.15 , 33: isNat^#(n__length(V1)) -> 920.38/297.15 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.15 , 34: isNat^#(n__s(V1)) -> 920.38/297.15 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.15 , 35: isNatKind^#(X) -> c_57(X) 920.38/297.15 , 36: isNatKind^#(n__length(V1)) -> 920.38/297.15 c_59(isNatIListKind^#(activate(V1))) 920.38/297.15 , 37: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.15 , 38: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.15 , 39: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.15 , 40: U41^#(tt(), V1, V2) -> 920.38/297.15 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , 41: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.15 , 42: isNatIList^#(V) -> 920.38/297.15 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.15 , 43: isNatIList^#(n__cons(V1, V2)) -> 920.38/297.15 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , 44: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.15 , 45: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.15 , 46: U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.15 , 47: U81^#(tt()) -> c_47(nil^#()) 920.38/297.15 , 48: U91^#(tt(), IL, M, N) -> 920.38/297.15 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) 920.38/297.15 , 49: zeros^#() -> c_2() 920.38/297.15 , 50: 0^#() -> c_4() 920.38/297.15 , 51: U12^#(tt()) -> c_6() 920.38/297.15 , 52: isNatList^#(n__nil()) -> c_9() 920.38/297.15 , 53: isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.15 , 54: isNatIListKind^#(n__nil()) -> c_56() 920.38/297.15 , 55: nil^#() -> c_48() 920.38/297.15 , 56: isNat^#(n__0()) -> c_25() 920.38/297.15 , 57: isNatKind^#(n__0()) -> c_58() 920.38/297.15 , 58: U22^#(tt()) -> c_23() 920.38/297.15 , 59: U32^#(tt()) -> c_29() 920.38/297.15 , 60: U43^#(tt()) -> c_32() 920.38/297.15 , 61: isNatIList^#(n__zeros()) -> c_34() 920.38/297.15 , 62: U53^#(tt()) -> c_38() 920.38/297.15 , 63: U63^#(tt()) -> c_41() } 920.38/297.15 920.38/297.15 We are left with following problem, upon which TcT provides the 920.38/297.15 certificate MAYBE. 920.38/297.15 920.38/297.15 Strict DPs: 920.38/297.15 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.15 , cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.15 , isNatList^#(n__take(V1, V2)) -> 920.38/297.15 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , isNatList^#(n__cons(V1, V2)) -> 920.38/297.15 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , U61^#(tt(), V1, V2) -> 920.38/297.15 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , U51^#(tt(), V1, V2) -> 920.38/297.15 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , activate^#(X) -> c_10(X) 920.38/297.15 , activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.15 , activate^#(n__take(X1, X2)) -> 920.38/297.15 c_12(take^#(activate(X1), activate(X2))) 920.38/297.15 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.15 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.15 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.15 , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.15 , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.15 , activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.15 , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.15 , take^#(X1, X2) -> c_61(X1, X2) 920.38/297.15 , take^#(0(), IL) -> 920.38/297.15 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.15 , take^#(s(M), cons(N, IL)) -> 920.38/297.15 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.15 n__isNatIListKind(activate(IL))), 920.38/297.15 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.15 activate(IL), 920.38/297.15 M, 920.38/297.15 N)) 920.38/297.15 , length^#(X) -> c_44(X) 920.38/297.15 , length^#(cons(N, L)) -> 920.38/297.15 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.15 n__isNatIListKind(activate(L))), 920.38/297.15 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.15 activate(L))) 920.38/297.15 , s^#(X) -> c_43(X) 920.38/297.15 , isNatIListKind^#(X) -> c_52(X) 920.38/297.15 , isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.15 c_54(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.15 c_55(and^#(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2)))) 920.38/297.15 , and^#(X1, X2) -> c_50(X1, X2) 920.38/297.15 , and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.15 , isNat^#(X) -> c_24(X) 920.38/297.15 , isNat^#(n__length(V1)) -> 920.38/297.15 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.15 , isNat^#(n__s(V1)) -> 920.38/297.15 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.15 , isNatKind^#(X) -> c_57(X) 920.38/297.15 , isNatKind^#(n__length(V1)) -> 920.38/297.15 c_59(isNatIListKind^#(activate(V1))) 920.38/297.15 , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.15 , U41^#(tt(), V1, V2) -> 920.38/297.15 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.15 , isNatIList^#(V) -> 920.38/297.15 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.15 , isNatIList^#(n__cons(V1, V2)) -> 920.38/297.15 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.15 n__isNatIListKind(activate(V2))), 920.38/297.15 activate(V1), 920.38/297.15 activate(V2))) 920.38/297.15 , U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.15 , U91^#(tt(), IL, M, N) -> 920.38/297.16 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.16 Strict Trs: 920.38/297.16 { zeros() -> cons(0(), n__zeros()) 920.38/297.16 , zeros() -> n__zeros() 920.38/297.16 , cons(X1, X2) -> n__cons(X1, X2) 920.38/297.16 , 0() -> n__0() 920.38/297.16 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 920.38/297.16 , U12(tt()) -> tt() 920.38/297.16 , isNatList(n__take(V1, V2)) -> 920.38/297.16 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2)) 920.38/297.16 , isNatList(n__cons(V1, V2)) -> 920.38/297.16 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2)) 920.38/297.16 , isNatList(n__nil()) -> tt() 920.38/297.16 , activate(X) -> X 920.38/297.16 , activate(n__zeros()) -> zeros() 920.38/297.16 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 920.38/297.16 , activate(n__0()) -> 0() 920.38/297.16 , activate(n__length(X)) -> length(activate(X)) 920.38/297.16 , activate(n__s(X)) -> s(activate(X)) 920.38/297.16 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 920.38/297.16 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 920.38/297.16 , activate(n__nil()) -> nil() 920.38/297.16 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 920.38/297.16 , activate(n__isNat(X)) -> isNat(X) 920.38/297.16 , activate(n__isNatKind(X)) -> isNatKind(X) 920.38/297.16 , U21(tt(), V1) -> U22(isNat(activate(V1))) 920.38/297.16 , U22(tt()) -> tt() 920.38/297.16 , isNat(X) -> n__isNat(X) 920.38/297.16 , isNat(n__0()) -> tt() 920.38/297.16 , isNat(n__length(V1)) -> 920.38/297.16 U11(isNatIListKind(activate(V1)), activate(V1)) 920.38/297.16 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 920.38/297.16 , U31(tt(), V) -> U32(isNatList(activate(V))) 920.38/297.16 , U32(tt()) -> tt() 920.38/297.16 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 920.38/297.16 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 920.38/297.16 , U43(tt()) -> tt() 920.38/297.16 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 920.38/297.16 , isNatIList(n__zeros()) -> tt() 920.38/297.16 , isNatIList(n__cons(V1, V2)) -> 920.38/297.16 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2)) 920.38/297.16 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 920.38/297.16 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 920.38/297.16 , U53(tt()) -> tt() 920.38/297.16 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 920.38/297.16 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 920.38/297.16 , U63(tt()) -> tt() 920.38/297.16 , U71(tt(), L) -> s(length(activate(L))) 920.38/297.16 , s(X) -> n__s(X) 920.38/297.16 , length(X) -> n__length(X) 920.38/297.16 , length(cons(N, L)) -> 920.38/297.16 U71(and(and(isNatList(activate(L)), 920.38/297.16 n__isNatIListKind(activate(L))), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.16 activate(L)) 920.38/297.16 , length(nil()) -> 0() 920.38/297.16 , U81(tt()) -> nil() 920.38/297.16 , nil() -> n__nil() 920.38/297.16 , U91(tt(), IL, M, N) -> 920.38/297.16 cons(activate(N), n__take(activate(M), activate(IL))) 920.38/297.16 , and(X1, X2) -> n__and(X1, X2) 920.38/297.16 , and(tt(), X) -> activate(X) 920.38/297.16 , isNatIListKind(X) -> n__isNatIListKind(X) 920.38/297.16 , isNatIListKind(n__zeros()) -> tt() 920.38/297.16 , isNatIListKind(n__take(V1, V2)) -> 920.38/297.16 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.16 , isNatIListKind(n__cons(V1, V2)) -> 920.38/297.16 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.16 , isNatIListKind(n__nil()) -> tt() 920.38/297.16 , isNatKind(X) -> n__isNatKind(X) 920.38/297.16 , isNatKind(n__0()) -> tt() 920.38/297.16 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 920.38/297.16 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 920.38/297.16 , take(X1, X2) -> n__take(X1, X2) 920.38/297.16 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 920.38/297.16 , take(s(M), cons(N, IL)) -> 920.38/297.16 U91(and(and(isNatIList(activate(IL)), 920.38/297.16 n__isNatIListKind(activate(IL))), 920.38/297.16 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.16 activate(IL), 920.38/297.16 M, 920.38/297.16 N) } 920.38/297.16 Weak DPs: 920.38/297.16 { zeros^#() -> c_2() 920.38/297.16 , 0^#() -> c_4() 920.38/297.16 , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.16 , U12^#(tt()) -> c_6() 920.38/297.16 , isNatList^#(n__nil()) -> c_9() 920.38/297.16 , activate^#(n__0()) -> c_13(0^#()) 920.38/297.16 , activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.16 , length^#(nil()) -> c_46(0^#()) 920.38/297.16 , isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.16 , isNatIListKind^#(n__nil()) -> c_56() 920.38/297.16 , nil^#() -> c_48() 920.38/297.16 , isNat^#(n__0()) -> c_25() 920.38/297.16 , isNatKind^#(n__0()) -> c_58() 920.38/297.16 , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.16 , U22^#(tt()) -> c_23() 920.38/297.16 , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.16 , U32^#(tt()) -> c_29() 920.38/297.16 , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.16 , U43^#(tt()) -> c_32() 920.38/297.16 , isNatIList^#(n__zeros()) -> c_34() 920.38/297.16 , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.16 , U53^#(tt()) -> c_38() 920.38/297.16 , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.16 , U63^#(tt()) -> c_41() 920.38/297.16 , U81^#(tt()) -> c_47(nil^#()) } 920.38/297.16 Obligation: 920.38/297.16 runtime complexity 920.38/297.16 Answer: 920.38/297.16 MAYBE 920.38/297.16 920.38/297.16 We estimate the number of application of {5,6,18,29,30,34,35} by 920.38/297.16 applications of Pre({5,6,18,29,30,34,35}) = 920.38/297.16 {2,3,4,7,9,15,17,20,22,23,26,28,31,36}. Here rules are labeled as 920.38/297.16 follows: 920.38/297.16 920.38/297.16 DPs: 920.38/297.16 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.16 , 2: cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.16 , 3: isNatList^#(n__take(V1, V2)) -> 920.38/297.16 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , 4: isNatList^#(n__cons(V1, V2)) -> 920.38/297.16 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , 5: U61^#(tt(), V1, V2) -> 920.38/297.16 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.16 , 6: U51^#(tt(), V1, V2) -> 920.38/297.16 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.16 , 7: activate^#(X) -> c_10(X) 920.38/297.16 , 8: activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.16 , 9: activate^#(n__take(X1, X2)) -> 920.38/297.16 c_12(take^#(activate(X1), activate(X2))) 920.38/297.16 , 10: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.16 , 11: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.16 , 12: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.16 , 13: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.16 , 14: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.16 , 15: activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.16 , 16: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.16 , 17: take^#(X1, X2) -> c_61(X1, X2) 920.38/297.16 , 18: take^#(0(), IL) -> 920.38/297.16 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.16 , 19: take^#(s(M), cons(N, IL)) -> 920.38/297.16 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.16 n__isNatIListKind(activate(IL))), 920.38/297.16 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.16 activate(IL), 920.38/297.16 M, 920.38/297.16 N)) 920.38/297.16 , 20: length^#(X) -> c_44(X) 920.38/297.16 , 21: length^#(cons(N, L)) -> 920.38/297.16 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.16 n__isNatIListKind(activate(L))), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.16 activate(L))) 920.38/297.16 , 22: s^#(X) -> c_43(X) 920.38/297.16 , 23: isNatIListKind^#(X) -> c_52(X) 920.38/297.16 , 24: isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.16 c_54(and^#(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2)))) 920.38/297.16 , 25: isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.16 c_55(and^#(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2)))) 920.38/297.16 , 26: and^#(X1, X2) -> c_50(X1, X2) 920.38/297.16 , 27: and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.16 , 28: isNat^#(X) -> c_24(X) 920.38/297.16 , 29: isNat^#(n__length(V1)) -> 920.38/297.16 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.16 , 30: isNat^#(n__s(V1)) -> 920.38/297.16 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.16 , 31: isNatKind^#(X) -> c_57(X) 920.38/297.16 , 32: isNatKind^#(n__length(V1)) -> 920.38/297.16 c_59(isNatIListKind^#(activate(V1))) 920.38/297.16 , 33: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.16 , 34: U41^#(tt(), V1, V2) -> 920.38/297.16 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.16 , 35: isNatIList^#(V) -> 920.38/297.16 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.16 , 36: isNatIList^#(n__cons(V1, V2)) -> 920.38/297.16 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , 37: U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.16 , 38: U91^#(tt(), IL, M, N) -> 920.38/297.16 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) 920.38/297.16 , 39: zeros^#() -> c_2() 920.38/297.16 , 40: 0^#() -> c_4() 920.38/297.16 , 41: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.16 , 42: U12^#(tt()) -> c_6() 920.38/297.16 , 43: isNatList^#(n__nil()) -> c_9() 920.38/297.16 , 44: activate^#(n__0()) -> c_13(0^#()) 920.38/297.16 , 45: activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.16 , 46: length^#(nil()) -> c_46(0^#()) 920.38/297.16 , 47: isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.16 , 48: isNatIListKind^#(n__nil()) -> c_56() 920.38/297.16 , 49: nil^#() -> c_48() 920.38/297.16 , 50: isNat^#(n__0()) -> c_25() 920.38/297.16 , 51: isNatKind^#(n__0()) -> c_58() 920.38/297.16 , 52: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.16 , 53: U22^#(tt()) -> c_23() 920.38/297.16 , 54: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.16 , 55: U32^#(tt()) -> c_29() 920.38/297.16 , 56: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.16 , 57: U43^#(tt()) -> c_32() 920.38/297.16 , 58: isNatIList^#(n__zeros()) -> c_34() 920.38/297.16 , 59: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.16 , 60: U53^#(tt()) -> c_38() 920.38/297.16 , 61: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.16 , 62: U63^#(tt()) -> c_41() 920.38/297.16 , 63: U81^#(tt()) -> c_47(nil^#()) } 920.38/297.16 920.38/297.16 We are left with following problem, upon which TcT provides the 920.38/297.16 certificate MAYBE. 920.38/297.16 920.38/297.16 Strict DPs: 920.38/297.16 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.16 , cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.16 , isNatList^#(n__take(V1, V2)) -> 920.38/297.16 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , isNatList^#(n__cons(V1, V2)) -> 920.38/297.16 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , activate^#(X) -> c_10(X) 920.38/297.16 , activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.16 , activate^#(n__take(X1, X2)) -> 920.38/297.16 c_12(take^#(activate(X1), activate(X2))) 920.38/297.16 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.16 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.16 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.16 , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.16 , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.16 , activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.16 , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.16 , take^#(X1, X2) -> c_61(X1, X2) 920.38/297.16 , take^#(s(M), cons(N, IL)) -> 920.38/297.16 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.16 n__isNatIListKind(activate(IL))), 920.38/297.16 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.16 activate(IL), 920.38/297.16 M, 920.38/297.16 N)) 920.38/297.16 , length^#(X) -> c_44(X) 920.38/297.16 , length^#(cons(N, L)) -> 920.38/297.16 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.16 n__isNatIListKind(activate(L))), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.16 activate(L))) 920.38/297.16 , s^#(X) -> c_43(X) 920.38/297.16 , isNatIListKind^#(X) -> c_52(X) 920.38/297.16 , isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.16 c_54(and^#(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2)))) 920.38/297.16 , isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.16 c_55(and^#(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2)))) 920.38/297.16 , and^#(X1, X2) -> c_50(X1, X2) 920.38/297.16 , and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.16 , isNat^#(X) -> c_24(X) 920.38/297.16 , isNatKind^#(X) -> c_57(X) 920.38/297.16 , isNatKind^#(n__length(V1)) -> 920.38/297.16 c_59(isNatIListKind^#(activate(V1))) 920.38/297.16 , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.16 , isNatIList^#(n__cons(V1, V2)) -> 920.38/297.16 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.16 , U91^#(tt(), IL, M, N) -> 920.38/297.16 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.16 Strict Trs: 920.38/297.16 { zeros() -> cons(0(), n__zeros()) 920.38/297.16 , zeros() -> n__zeros() 920.38/297.16 , cons(X1, X2) -> n__cons(X1, X2) 920.38/297.16 , 0() -> n__0() 920.38/297.16 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 920.38/297.16 , U12(tt()) -> tt() 920.38/297.16 , isNatList(n__take(V1, V2)) -> 920.38/297.16 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2)) 920.38/297.16 , isNatList(n__cons(V1, V2)) -> 920.38/297.16 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2)) 920.38/297.16 , isNatList(n__nil()) -> tt() 920.38/297.16 , activate(X) -> X 920.38/297.16 , activate(n__zeros()) -> zeros() 920.38/297.16 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 920.38/297.16 , activate(n__0()) -> 0() 920.38/297.16 , activate(n__length(X)) -> length(activate(X)) 920.38/297.16 , activate(n__s(X)) -> s(activate(X)) 920.38/297.16 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 920.38/297.16 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 920.38/297.16 , activate(n__nil()) -> nil() 920.38/297.16 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 920.38/297.16 , activate(n__isNat(X)) -> isNat(X) 920.38/297.16 , activate(n__isNatKind(X)) -> isNatKind(X) 920.38/297.16 , U21(tt(), V1) -> U22(isNat(activate(V1))) 920.38/297.16 , U22(tt()) -> tt() 920.38/297.16 , isNat(X) -> n__isNat(X) 920.38/297.16 , isNat(n__0()) -> tt() 920.38/297.16 , isNat(n__length(V1)) -> 920.38/297.16 U11(isNatIListKind(activate(V1)), activate(V1)) 920.38/297.16 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 920.38/297.16 , U31(tt(), V) -> U32(isNatList(activate(V))) 920.38/297.16 , U32(tt()) -> tt() 920.38/297.16 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 920.38/297.16 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 920.38/297.16 , U43(tt()) -> tt() 920.38/297.16 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 920.38/297.16 , isNatIList(n__zeros()) -> tt() 920.38/297.16 , isNatIList(n__cons(V1, V2)) -> 920.38/297.16 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2)) 920.38/297.16 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 920.38/297.16 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 920.38/297.16 , U53(tt()) -> tt() 920.38/297.16 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 920.38/297.16 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 920.38/297.16 , U63(tt()) -> tt() 920.38/297.16 , U71(tt(), L) -> s(length(activate(L))) 920.38/297.16 , s(X) -> n__s(X) 920.38/297.16 , length(X) -> n__length(X) 920.38/297.16 , length(cons(N, L)) -> 920.38/297.16 U71(and(and(isNatList(activate(L)), 920.38/297.16 n__isNatIListKind(activate(L))), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.16 activate(L)) 920.38/297.16 , length(nil()) -> 0() 920.38/297.16 , U81(tt()) -> nil() 920.38/297.16 , nil() -> n__nil() 920.38/297.16 , U91(tt(), IL, M, N) -> 920.38/297.16 cons(activate(N), n__take(activate(M), activate(IL))) 920.38/297.16 , and(X1, X2) -> n__and(X1, X2) 920.38/297.16 , and(tt(), X) -> activate(X) 920.38/297.16 , isNatIListKind(X) -> n__isNatIListKind(X) 920.38/297.16 , isNatIListKind(n__zeros()) -> tt() 920.38/297.16 , isNatIListKind(n__take(V1, V2)) -> 920.38/297.16 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.16 , isNatIListKind(n__cons(V1, V2)) -> 920.38/297.16 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.16 , isNatIListKind(n__nil()) -> tt() 920.38/297.16 , isNatKind(X) -> n__isNatKind(X) 920.38/297.16 , isNatKind(n__0()) -> tt() 920.38/297.16 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 920.38/297.16 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 920.38/297.16 , take(X1, X2) -> n__take(X1, X2) 920.38/297.16 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 920.38/297.16 , take(s(M), cons(N, IL)) -> 920.38/297.16 U91(and(and(isNatIList(activate(IL)), 920.38/297.16 n__isNatIListKind(activate(IL))), 920.38/297.16 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.16 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.16 activate(IL), 920.38/297.16 M, 920.38/297.16 N) } 920.38/297.16 Weak DPs: 920.38/297.16 { zeros^#() -> c_2() 920.38/297.16 , 0^#() -> c_4() 920.38/297.16 , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.16 , U12^#(tt()) -> c_6() 920.38/297.16 , isNatList^#(n__nil()) -> c_9() 920.38/297.16 , U61^#(tt(), V1, V2) -> 920.38/297.16 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.16 , U51^#(tt(), V1, V2) -> 920.38/297.16 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.16 , activate^#(n__0()) -> c_13(0^#()) 920.38/297.16 , activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.16 , take^#(0(), IL) -> 920.38/297.16 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.16 , length^#(nil()) -> c_46(0^#()) 920.38/297.16 , isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.16 , isNatIListKind^#(n__nil()) -> c_56() 920.38/297.16 , nil^#() -> c_48() 920.38/297.16 , isNat^#(n__0()) -> c_25() 920.38/297.16 , isNat^#(n__length(V1)) -> 920.38/297.16 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.16 , isNat^#(n__s(V1)) -> 920.38/297.16 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.16 , isNatKind^#(n__0()) -> c_58() 920.38/297.16 , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.16 , U22^#(tt()) -> c_23() 920.38/297.16 , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.16 , U32^#(tt()) -> c_29() 920.38/297.16 , U41^#(tt(), V1, V2) -> 920.38/297.16 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.16 , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.16 , U43^#(tt()) -> c_32() 920.38/297.16 , isNatIList^#(V) -> 920.38/297.16 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.16 , isNatIList^#(n__zeros()) -> c_34() 920.38/297.16 , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.16 , U53^#(tt()) -> c_38() 920.38/297.16 , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.16 , U63^#(tt()) -> c_41() 920.38/297.16 , U81^#(tt()) -> c_47(nil^#()) } 920.38/297.16 Obligation: 920.38/297.16 runtime complexity 920.38/297.16 Answer: 920.38/297.16 MAYBE 920.38/297.16 920.38/297.16 We estimate the number of application of {3,4,29} by applications 920.38/297.16 of Pre({3,4,29}) = {2,5,15,17,19,20,23,25,26}. Here rules are 920.38/297.16 labeled as follows: 920.38/297.16 920.38/297.16 DPs: 920.38/297.16 { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.16 , 2: cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.16 , 3: isNatList^#(n__take(V1, V2)) -> 920.38/297.16 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , 4: isNatList^#(n__cons(V1, V2)) -> 920.38/297.16 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.16 n__isNatIListKind(activate(V2))), 920.38/297.16 activate(V1), 920.38/297.16 activate(V2))) 920.38/297.16 , 5: activate^#(X) -> c_10(X) 920.38/297.16 , 6: activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.16 , 7: activate^#(n__take(X1, X2)) -> 920.38/297.16 c_12(take^#(activate(X1), activate(X2))) 920.38/297.16 , 8: activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.17 , 9: activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.17 , 10: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.17 , 11: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.17 , 12: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.17 , 13: activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.17 , 14: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.17 , 15: take^#(X1, X2) -> c_61(X1, X2) 920.38/297.17 , 16: take^#(s(M), cons(N, IL)) -> 920.38/297.17 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.17 n__isNatIListKind(activate(IL))), 920.38/297.17 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.17 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.17 activate(IL), 920.38/297.17 M, 920.38/297.17 N)) 920.38/297.17 , 17: length^#(X) -> c_44(X) 920.38/297.17 , 18: length^#(cons(N, L)) -> 920.38/297.17 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.17 n__isNatIListKind(activate(L))), 920.38/297.17 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.17 activate(L))) 920.38/297.17 , 19: s^#(X) -> c_43(X) 920.38/297.17 , 20: isNatIListKind^#(X) -> c_52(X) 920.38/297.17 , 21: isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.17 c_54(and^#(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2)))) 920.38/297.17 , 22: isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.17 c_55(and^#(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2)))) 920.38/297.17 , 23: and^#(X1, X2) -> c_50(X1, X2) 920.38/297.17 , 24: and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.17 , 25: isNat^#(X) -> c_24(X) 920.38/297.17 , 26: isNatKind^#(X) -> c_57(X) 920.38/297.17 , 27: isNatKind^#(n__length(V1)) -> 920.38/297.17 c_59(isNatIListKind^#(activate(V1))) 920.38/297.17 , 28: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.17 , 29: isNatIList^#(n__cons(V1, V2)) -> 920.38/297.17 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2))) 920.38/297.17 , 30: U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.17 , 31: U91^#(tt(), IL, M, N) -> 920.38/297.17 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) 920.38/297.17 , 32: zeros^#() -> c_2() 920.38/297.17 , 33: 0^#() -> c_4() 920.38/297.17 , 34: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.17 , 35: U12^#(tt()) -> c_6() 920.38/297.17 , 36: isNatList^#(n__nil()) -> c_9() 920.38/297.17 , 37: U61^#(tt(), V1, V2) -> 920.38/297.17 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.17 , 38: U51^#(tt(), V1, V2) -> 920.38/297.17 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.17 , 39: activate^#(n__0()) -> c_13(0^#()) 920.38/297.17 , 40: activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.17 , 41: take^#(0(), IL) -> 920.38/297.17 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.17 , 42: length^#(nil()) -> c_46(0^#()) 920.38/297.17 , 43: isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.17 , 44: isNatIListKind^#(n__nil()) -> c_56() 920.38/297.17 , 45: nil^#() -> c_48() 920.38/297.17 , 46: isNat^#(n__0()) -> c_25() 920.38/297.17 , 47: isNat^#(n__length(V1)) -> 920.38/297.17 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.17 , 48: isNat^#(n__s(V1)) -> 920.38/297.17 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.17 , 49: isNatKind^#(n__0()) -> c_58() 920.38/297.17 , 50: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.17 , 51: U22^#(tt()) -> c_23() 920.38/297.17 , 52: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.17 , 53: U32^#(tt()) -> c_29() 920.38/297.17 , 54: U41^#(tt(), V1, V2) -> 920.38/297.17 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.17 , 55: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.17 , 56: U43^#(tt()) -> c_32() 920.38/297.17 , 57: isNatIList^#(V) -> 920.38/297.17 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.17 , 58: isNatIList^#(n__zeros()) -> c_34() 920.38/297.17 , 59: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.17 , 60: U53^#(tt()) -> c_38() 920.38/297.17 , 61: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.17 , 62: U63^#(tt()) -> c_41() 920.38/297.17 , 63: U81^#(tt()) -> c_47(nil^#()) } 920.38/297.17 920.38/297.17 We are left with following problem, upon which TcT provides the 920.38/297.17 certificate MAYBE. 920.38/297.17 920.38/297.17 Strict DPs: 920.38/297.17 { zeros^#() -> c_1(cons^#(0(), n__zeros())) 920.38/297.17 , cons^#(X1, X2) -> c_3(X1, X2) 920.38/297.17 , activate^#(X) -> c_10(X) 920.38/297.17 , activate^#(n__zeros()) -> c_11(zeros^#()) 920.38/297.17 , activate^#(n__take(X1, X2)) -> 920.38/297.17 c_12(take^#(activate(X1), activate(X2))) 920.38/297.17 , activate^#(n__length(X)) -> c_14(length^#(activate(X))) 920.38/297.17 , activate^#(n__s(X)) -> c_15(s^#(activate(X))) 920.38/297.17 , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2)) 920.38/297.17 , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) 920.38/297.17 , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2)) 920.38/297.17 , activate^#(n__isNat(X)) -> c_20(isNat^#(X)) 920.38/297.17 , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X)) 920.38/297.17 , take^#(X1, X2) -> c_61(X1, X2) 920.38/297.17 , take^#(s(M), cons(N, IL)) -> 920.38/297.17 c_63(U91^#(and(and(isNatIList(activate(IL)), 920.38/297.17 n__isNatIListKind(activate(IL))), 920.38/297.17 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.17 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.17 activate(IL), 920.38/297.17 M, 920.38/297.17 N)) 920.38/297.17 , length^#(X) -> c_44(X) 920.38/297.17 , length^#(cons(N, L)) -> 920.38/297.17 c_45(U71^#(and(and(isNatList(activate(L)), 920.38/297.17 n__isNatIListKind(activate(L))), 920.38/297.17 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.17 activate(L))) 920.38/297.17 , s^#(X) -> c_43(X) 920.38/297.17 , isNatIListKind^#(X) -> c_52(X) 920.38/297.17 , isNatIListKind^#(n__take(V1, V2)) -> 920.38/297.17 c_54(and^#(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2)))) 920.38/297.17 , isNatIListKind^#(n__cons(V1, V2)) -> 920.38/297.17 c_55(and^#(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2)))) 920.38/297.17 , and^#(X1, X2) -> c_50(X1, X2) 920.38/297.17 , and^#(tt(), X) -> c_51(activate^#(X)) 920.38/297.17 , isNat^#(X) -> c_24(X) 920.38/297.17 , isNatKind^#(X) -> c_57(X) 920.38/297.17 , isNatKind^#(n__length(V1)) -> 920.38/297.17 c_59(isNatIListKind^#(activate(V1))) 920.38/297.17 , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1))) 920.38/297.17 , U71^#(tt(), L) -> c_42(s^#(length(activate(L)))) 920.38/297.17 , U91^#(tt(), IL, M, N) -> 920.38/297.17 c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) } 920.38/297.17 Strict Trs: 920.38/297.17 { zeros() -> cons(0(), n__zeros()) 920.38/297.17 , zeros() -> n__zeros() 920.38/297.17 , cons(X1, X2) -> n__cons(X1, X2) 920.38/297.17 , 0() -> n__0() 920.38/297.17 , U11(tt(), V1) -> U12(isNatList(activate(V1))) 920.38/297.17 , U12(tt()) -> tt() 920.38/297.17 , isNatList(n__take(V1, V2)) -> 920.38/297.17 U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2)) 920.38/297.17 , isNatList(n__cons(V1, V2)) -> 920.38/297.17 U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2)) 920.38/297.17 , isNatList(n__nil()) -> tt() 920.38/297.17 , activate(X) -> X 920.38/297.17 , activate(n__zeros()) -> zeros() 920.38/297.17 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 920.38/297.17 , activate(n__0()) -> 0() 920.38/297.17 , activate(n__length(X)) -> length(activate(X)) 920.38/297.17 , activate(n__s(X)) -> s(activate(X)) 920.38/297.17 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 920.38/297.17 , activate(n__isNatIListKind(X)) -> isNatIListKind(X) 920.38/297.17 , activate(n__nil()) -> nil() 920.38/297.17 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 920.38/297.17 , activate(n__isNat(X)) -> isNat(X) 920.38/297.17 , activate(n__isNatKind(X)) -> isNatKind(X) 920.38/297.17 , U21(tt(), V1) -> U22(isNat(activate(V1))) 920.38/297.17 , U22(tt()) -> tt() 920.38/297.17 , isNat(X) -> n__isNat(X) 920.38/297.17 , isNat(n__0()) -> tt() 920.38/297.17 , isNat(n__length(V1)) -> 920.38/297.17 U11(isNatIListKind(activate(V1)), activate(V1)) 920.38/297.17 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 920.38/297.17 , U31(tt(), V) -> U32(isNatList(activate(V))) 920.38/297.17 , U32(tt()) -> tt() 920.38/297.17 , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) 920.38/297.17 , U42(tt(), V2) -> U43(isNatIList(activate(V2))) 920.38/297.17 , U43(tt()) -> tt() 920.38/297.17 , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) 920.38/297.17 , isNatIList(n__zeros()) -> tt() 920.38/297.17 , isNatIList(n__cons(V1, V2)) -> 920.38/297.17 U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2)) 920.38/297.17 , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) 920.38/297.17 , U52(tt(), V2) -> U53(isNatList(activate(V2))) 920.38/297.17 , U53(tt()) -> tt() 920.38/297.17 , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) 920.38/297.17 , U62(tt(), V2) -> U63(isNatIList(activate(V2))) 920.38/297.17 , U63(tt()) -> tt() 920.38/297.17 , U71(tt(), L) -> s(length(activate(L))) 920.38/297.17 , s(X) -> n__s(X) 920.38/297.17 , length(X) -> n__length(X) 920.38/297.17 , length(cons(N, L)) -> 920.38/297.17 U71(and(and(isNatList(activate(L)), 920.38/297.17 n__isNatIListKind(activate(L))), 920.38/297.17 n__and(n__isNat(N), n__isNatKind(N))), 920.38/297.17 activate(L)) 920.38/297.17 , length(nil()) -> 0() 920.38/297.17 , U81(tt()) -> nil() 920.38/297.17 , nil() -> n__nil() 920.38/297.17 , U91(tt(), IL, M, N) -> 920.38/297.17 cons(activate(N), n__take(activate(M), activate(IL))) 920.38/297.17 , and(X1, X2) -> n__and(X1, X2) 920.38/297.17 , and(tt(), X) -> activate(X) 920.38/297.17 , isNatIListKind(X) -> n__isNatIListKind(X) 920.38/297.17 , isNatIListKind(n__zeros()) -> tt() 920.38/297.17 , isNatIListKind(n__take(V1, V2)) -> 920.38/297.17 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.17 , isNatIListKind(n__cons(V1, V2)) -> 920.38/297.17 and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) 920.38/297.17 , isNatIListKind(n__nil()) -> tt() 920.38/297.17 , isNatKind(X) -> n__isNatKind(X) 920.38/297.17 , isNatKind(n__0()) -> tt() 920.38/297.17 , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) 920.38/297.17 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 920.38/297.17 , take(X1, X2) -> n__take(X1, X2) 920.38/297.17 , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) 920.38/297.17 , take(s(M), cons(N, IL)) -> 920.38/297.17 U91(and(and(isNatIList(activate(IL)), 920.38/297.17 n__isNatIListKind(activate(IL))), 920.38/297.17 n__and(n__and(n__isNat(M), n__isNatKind(M)), 920.38/297.17 n__and(n__isNat(N), n__isNatKind(N)))), 920.38/297.17 activate(IL), 920.38/297.17 M, 920.38/297.17 N) } 920.38/297.17 Weak DPs: 920.38/297.17 { zeros^#() -> c_2() 920.38/297.17 , 0^#() -> c_4() 920.38/297.17 , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) 920.38/297.17 , U12^#(tt()) -> c_6() 920.38/297.17 , isNatList^#(n__take(V1, V2)) -> 920.38/297.17 c_7(U61^#(and(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2))) 920.38/297.17 , isNatList^#(n__cons(V1, V2)) -> 920.38/297.17 c_8(U51^#(and(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2))) 920.38/297.17 , isNatList^#(n__nil()) -> c_9() 920.38/297.17 , U61^#(tt(), V1, V2) -> 920.38/297.17 c_39(U62^#(isNat(activate(V1)), activate(V2))) 920.38/297.17 , U51^#(tt(), V1, V2) -> 920.38/297.17 c_36(U52^#(isNat(activate(V1)), activate(V2))) 920.38/297.17 , activate^#(n__0()) -> c_13(0^#()) 920.38/297.17 , activate^#(n__nil()) -> c_18(nil^#()) 920.38/297.17 , take^#(0(), IL) -> 920.38/297.17 c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) 920.38/297.17 , length^#(nil()) -> c_46(0^#()) 920.38/297.17 , isNatIListKind^#(n__zeros()) -> c_53() 920.38/297.17 , isNatIListKind^#(n__nil()) -> c_56() 920.38/297.17 , nil^#() -> c_48() 920.38/297.17 , isNat^#(n__0()) -> c_25() 920.38/297.17 , isNat^#(n__length(V1)) -> 920.38/297.17 c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) 920.38/297.17 , isNat^#(n__s(V1)) -> 920.38/297.17 c_27(U21^#(isNatKind(activate(V1)), activate(V1))) 920.38/297.17 , isNatKind^#(n__0()) -> c_58() 920.38/297.17 , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1)))) 920.38/297.17 , U22^#(tt()) -> c_23() 920.38/297.17 , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V)))) 920.38/297.17 , U32^#(tt()) -> c_29() 920.38/297.17 , U41^#(tt(), V1, V2) -> 920.38/297.17 c_30(U42^#(isNat(activate(V1)), activate(V2))) 920.38/297.17 , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2)))) 920.38/297.17 , U43^#(tt()) -> c_32() 920.38/297.17 , isNatIList^#(V) -> 920.38/297.17 c_33(U31^#(isNatIListKind(activate(V)), activate(V))) 920.38/297.17 , isNatIList^#(n__zeros()) -> c_34() 920.38/297.17 , isNatIList^#(n__cons(V1, V2)) -> 920.38/297.17 c_35(U41^#(and(isNatKind(activate(V1)), 920.38/297.17 n__isNatIListKind(activate(V2))), 920.38/297.17 activate(V1), 920.38/297.17 activate(V2))) 920.38/297.17 , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2)))) 920.38/297.17 , U53^#(tt()) -> c_38() 920.38/297.17 , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2)))) 920.38/297.17 , U63^#(tt()) -> c_41() 920.38/297.17 , U81^#(tt()) -> c_47(nil^#()) } 920.38/297.17 Obligation: 920.38/297.17 runtime complexity 920.38/297.17 Answer: 920.38/297.17 MAYBE 920.38/297.17 920.38/297.17 Empty strict component of the problem is NOT empty. 920.38/297.17 920.38/297.17 920.38/297.17 Arrrr.. 920.58/297.22 EOF