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