YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , plus(N, s(M)) -> U61(isNat(M), M, N) , plus(N, 0()) -> U51(isNat(N), N) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Arguments of following rules are not normal-forms: { plus(N, s(M)) -> U61(isNat(M), M, N) , plus(N, 0()) -> U51(isNat(N), N) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add the following dependency tuples: Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__0()) -> c_3() , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , activate^#(n__s(X)) -> c_9(s^#(X)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U41^#(tt()) -> c_22() , 0^#() -> c_31() , plus^#(X1, X2) -> c_30() , s^#(X) -> c_29() , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__0()) -> c_13() , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U16^#(tt()) -> c_16() , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U23^#(tt()) -> c_19() , U32^#(tt()) -> c_21() , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U52^#(tt(), N) -> c_24(activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__0()) -> c_3() , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , activate^#(n__s(X)) -> c_9(s^#(X)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U41^#(tt()) -> c_22() , 0^#() -> c_31() , plus^#(X1, X2) -> c_30() , s^#(X) -> c_29() , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__0()) -> c_13() , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U16^#(tt()) -> c_16() , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U23^#(tt()) -> c_19() , U32^#(tt()) -> c_21() , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U52^#(tt(), N) -> c_24(activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {3,6,12,13,14,15,18,21,24,25} by applications of Pre({3,6,12,13,14,15,18,21,24,25}) = {1,2,4,5,7,8,9,10,11,16,17,19,20,22,23,26,27,28,29,30,31}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , 3: isNatKind^#(n__0()) -> c_3() , 4: isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , 5: isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , 6: activate^#(X) -> c_6() , 7: activate^#(n__0()) -> c_7(0^#()) , 8: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , 9: activate^#(n__s(X)) -> c_9(s^#(X)) , 10: U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , 11: U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , 12: U41^#(tt()) -> c_22() , 13: 0^#() -> c_31() , 14: plus^#(X1, X2) -> c_30() , 15: s^#(X) -> c_29() , 16: U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , 17: U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , 18: isNat^#(n__0()) -> c_13() , 19: isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , 20: isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , 21: U16^#(tt()) -> c_16() , 22: U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , 23: U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , 24: U23^#(tt()) -> c_19() , 25: U32^#(tt()) -> c_21() , 26: U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , 27: U52^#(tt(), N) -> c_24(activate^#(N)) , 28: U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , 29: U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , 30: U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , 31: U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , activate^#(n__s(X)) -> c_9(s^#(X)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U52^#(tt(), N) -> c_24(activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } Weak DPs: { isNatKind^#(n__0()) -> c_3() , activate^#(X) -> c_6() , U41^#(tt()) -> c_22() , 0^#() -> c_31() , plus^#(X1, X2) -> c_30() , s^#(X) -> c_29() , isNat^#(n__0()) -> c_13() , U16^#(tt()) -> c_16() , U23^#(tt()) -> c_19() , U32^#(tt()) -> c_21() } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {5,6,7} by applications of Pre({5,6,7}) = {1,2,3,4,8,9,10,11,12,13,14,15,16,17,18,19,20,21}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , 3: isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , 5: activate^#(n__0()) -> c_7(0^#()) , 6: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , 7: activate^#(n__s(X)) -> c_9(s^#(X)) , 8: U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , 9: U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , 10: U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , 11: U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , 12: isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , 13: isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , 14: U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , 15: U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , 16: U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , 17: U52^#(tt(), N) -> c_24(activate^#(N)) , 18: U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , 19: U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , 20: U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , 21: U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) , 22: isNatKind^#(n__0()) -> c_3() , 23: activate^#(X) -> c_6() , 24: U41^#(tt()) -> c_22() , 25: 0^#() -> c_31() , 26: plus^#(X1, X2) -> c_30() , 27: s^#(X) -> c_29() , 28: isNat^#(n__0()) -> c_13() , 29: U16^#(tt()) -> c_16() , 30: U23^#(tt()) -> c_19() , 31: U32^#(tt()) -> c_21() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U52^#(tt(), N) -> c_24(activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } Weak DPs: { isNatKind^#(n__0()) -> c_3() , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , activate^#(n__s(X)) -> c_9(s^#(X)) , U41^#(tt()) -> c_22() , 0^#() -> c_31() , plus^#(X1, X2) -> c_30() , s^#(X) -> c_29() , isNat^#(n__0()) -> c_13() , U16^#(tt()) -> c_16() , U23^#(tt()) -> c_19() , U32^#(tt()) -> c_21() } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {14,18} by applications of Pre({14,18}) = {13,17}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , 3: isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , 5: U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , 6: U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , 7: U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , 8: U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , 9: isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , 10: isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , 11: U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , 12: U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , 13: U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , 14: U52^#(tt(), N) -> c_24(activate^#(N)) , 15: U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , 16: U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , 17: U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , 18: U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) , 19: isNatKind^#(n__0()) -> c_3() , 20: activate^#(X) -> c_6() , 21: activate^#(n__0()) -> c_7(0^#()) , 22: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , 23: activate^#(n__s(X)) -> c_9(s^#(X)) , 24: U41^#(tt()) -> c_22() , 25: 0^#() -> c_31() , 26: plus^#(X1, X2) -> c_30() , 27: s^#(X) -> c_29() , 28: isNat^#(n__0()) -> c_13() , 29: U16^#(tt()) -> c_16() , 30: U23^#(tt()) -> c_19() , 31: U32^#(tt()) -> c_21() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) } Weak DPs: { isNatKind^#(n__0()) -> c_3() , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , activate^#(n__s(X)) -> c_9(s^#(X)) , U41^#(tt()) -> c_22() , 0^#() -> c_31() , plus^#(X1, X2) -> c_30() , s^#(X) -> c_29() , isNat^#(n__0()) -> c_13() , U16^#(tt()) -> c_16() , U23^#(tt()) -> c_19() , U32^#(tt()) -> c_21() , U52^#(tt(), N) -> c_24(activate^#(N)) , U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { isNatKind^#(n__0()) -> c_3() , activate^#(X) -> c_6() , activate^#(n__0()) -> c_7(0^#()) , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) , activate^#(n__s(X)) -> c_9(s^#(X)) , U41^#(tt()) -> c_22() , 0^#() -> c_31() , plus^#(X1, X2) -> c_30() , s^#(X) -> c_29() , isNat^#(n__0()) -> c_13() , U16^#(tt()) -> c_16() , U23^#(tt()) -> c_19() , U32^#(tt()) -> c_21() , U52^#(tt(), N) -> c_24(activate^#(N)) , U64^#(tt(), M, N) -> c_28(s^#(plus(activate(N), activate(M))), plus^#(activate(N), activate(M)), activate^#(N), activate^#(M)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_4(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNatKind^#(n__s(V1)) -> c_5(U41^#(isNatKind(activate(V1))), isNatKind^#(activate(V1)), activate^#(V1)) , U13^#(tt(), V1, V2) -> c_10(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2)), activate^#(V2), activate^#(V1), activate^#(V2)) , U31^#(tt(), V2) -> c_20(U32^#(isNatKind(activate(V2))), isNatKind^#(activate(V2)), activate^#(V2)) , U14^#(tt(), V1, V2) -> c_11(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)), activate^#(V1), activate^#(V2)) , U15^#(tt(), V2) -> c_12(U16^#(isNat(activate(V2))), isNat^#(activate(V2)), activate^#(V2)) , isNat^#(n__plus(V1, V2)) -> c_14(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1), activate^#(V2)) , isNat^#(n__s(V1)) -> c_15(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U21^#(tt(), V1) -> c_17(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1)), activate^#(V1), activate^#(V1)) , U22^#(tt(), V1) -> c_18(U23^#(isNat(activate(V1))), isNat^#(activate(V1)), activate^#(V1)) , U51^#(tt(), N) -> c_23(U52^#(isNatKind(activate(N)), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(N)) , U61^#(tt(), M, N) -> c_25(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M)), activate^#(M), activate^#(M), activate^#(N)) , U62^#(tt(), M, N) -> c_26(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) , U63^#(tt(), M, N) -> c_27(U64^#(isNatKind(activate(N)), activate(M), activate(N)), isNatKind^#(activate(N)), activate^#(N), activate^#(M), activate^#(N)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) , U52(tt(), N) -> activate(N) , U61(tt(), M, N) -> U62(isNatKind(activate(M)), activate(M), activate(N)) , U62(tt(), M, N) -> U63(isNat(activate(N)), activate(M), activate(N)) , U63(tt(), M, N) -> U64(isNatKind(activate(N)), activate(M), activate(N)) , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } StartTerms: basic terms Defined Symbols: U11^# U12^# isNatKind^# activate^# U13^# U31^# U41^# 0^# plus^# s^# U14^# U15^# isNat^# U16^# U21^# U22^# U23^# U32^# U51^# U52^# U61^# U62^# U63^# U64^# Constructors: tt n__0 n__plus n__s Strategy: innermost Problem (S): ------------ Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } StartTerms: basic terms Defined Symbols: U11^# U12^# isNatKind^# activate^# U13^# U31^# U41^# 0^# plus^# s^# U14^# U15^# isNat^# U16^# U21^# U22^# U23^# U32^# U51^# U52^# U61^# U62^# U63^# U64^# Constructors: tt n__0 n__plus n__s Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } StartTerms: basic terms Defined Symbols: U11^# U12^# isNatKind^# activate^# U13^# U31^# U41^# 0^# plus^# s^# U14^# U15^# isNat^# U16^# U21^# U22^# U23^# U32^# U51^# U52^# U61^# U62^# U63^# U64^# Constructors: tt n__0 n__plus n__s Strategy: innermost This problem was proven YES(O(1),O(n^2)). S) Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } StartTerms: basic terms Defined Symbols: U11^# U12^# isNatKind^# activate^# U13^# U31^# U41^# 0^# plus^# s^# U14^# U15^# isNat^# U16^# U21^# U22^# U23^# U32^# U51^# U52^# U61^# U62^# U63^# U64^# Constructors: tt n__0 n__plus n__s Strategy: innermost This problem was proven YES(O(1),O(n^1)). Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } and lower component { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) } Further, following extension rules are added to the lower component. { U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , U15^#(tt(), V2) -> isNat^#(activate(V2)) , isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , U22^#(tt(), V1) -> isNat^#(activate(V1)) , U51^#(tt(), N) -> isNatKind^#(activate(N)) , U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , U62^#(tt(), M, N) -> isNat^#(activate(N)) , U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {6,7} by applications of Pre({6,7}) = {5}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 3: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 4: isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 5: isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 6: U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 7: U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , 8: U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , 9: U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) , 10: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 11: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 12: U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , 13: U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {2}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 3: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 4: isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 5: isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 6: U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , 7: U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) , 8: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 9: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 10: U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 11: U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , 12: U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , 13: U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {2} by applications of Pre({2}) = {1}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 3: isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 4: isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 5: U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , 6: U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) , 7: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 8: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 9: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 10: U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 11: U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , 12: U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , 13: U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {1} by applications of Pre({1}) = {2}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 2: isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 3: isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 4: U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , 5: U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) , 6: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 7: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 8: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 9: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 10: U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 11: U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , 12: U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , 13: U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {}. Here rules are labeled as follows: DPs: { 1: isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 2: isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 3: U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , 4: U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) , 5: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 6: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 7: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 8: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 9: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 10: U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 11: U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , 12: U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , 13: U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) , U63^#(tt(), M, N) -> c_3() } Weak DPs: { U11^#(tt(), V1, V2) -> c_4(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_5(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_6(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_9(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_10(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_11(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_12(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 11: U61^#(tt(), M, N) -> c_11(U62^#(isNatKind(activate(M)), activate(M), activate(N))) } Trs: { isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U16(tt()) -> tt() , s(X) -> n__s(X) , 0() -> n__0() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1, 2}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1}, Uargs(c_12) = {1, 2} TcT has computed the following constructor-restricted matrix interpretation. Note that the diagonal of the component-wise maxima of interpretation-entries (of constructors) contains no more than 0 non-zero entries. [U11](x1, x2, x3) = [4] [tt] = [0] [U12](x1, x2, x3) = [4] [isNatKind](x1) = [4] [activate](x1) = [1] x1 + [4] [U13](x1, x2, x3) = [4] [U14](x1, x2, x3) = [4] [U15](x1, x2) = [4] [isNat](x1) = [4] x1 + [0] [U16](x1) = [4] [U21](x1, x2) = [0] [U22](x1, x2) = [0] [U23](x1) = [0] [U31](x1, x2) = [0] [U32](x1) = [0] [U41](x1) = [0] [U51](x1, x2) = [0] [U52](x1, x2) = [0] [U61](x1, x2, x3) = [0] [U62](x1, x2, x3) = [0] [U63](x1, x2, x3) = [0] [U64](x1, x2, x3) = [0] [s](x1) = [1] [plus](x1, x2) = [1] [n__0] = [0] [n__plus](x1, x2) = [1] [n__s](x1) = [0] [0] = [1] [U11^#](x1, x2, x3) = [0] [c_1](x1, x2, x3, x4, x5) = [0] [U12^#](x1, x2, x3) = [0] [isNatKind^#](x1) = [0] [activate^#](x1) = [0] [c_2](x1, x2, x3, x4, x5) = [0] [U13^#](x1, x2, x3) = [0] [c_3] = [0] [c_4](x1, x2, x3, x4) = [0] [U31^#](x1, x2) = [0] [c_5](x1, x2, x3) = [0] [U41^#](x1) = [0] [c_6] = [0] [c_7](x1) = [0] [0^#] = [0] [c_8](x1) = [0] [plus^#](x1, x2) = [0] [c_9](x1) = [0] [s^#](x1) = [0] [c_10](x1, x2, x3, x4, x5) = [0] [U14^#](x1, x2, x3) = [0] [c_11](x1, x2, x3, x4) = [0] [U15^#](x1, x2) = [0] [isNat^#](x1) = [0] [c_12](x1, x2, x3) = [0] [U16^#](x1) = [0] [c_13] = [0] [c_14](x1, x2, x3, x4, x5) = [0] [c_15](x1, x2, x3, x4) = [0] [U21^#](x1, x2) = [0] [c_16] = [0] [c_17](x1, x2, x3, x4) = [0] [U22^#](x1, x2) = [0] [c_18](x1, x2, x3) = [0] [U23^#](x1) = [0] [c_19] = [0] [c_20](x1, x2, x3) = [0] [U32^#](x1) = [0] [c_21] = [0] [c_22] = [0] [U51^#](x1, x2) = [0] [c_23](x1, x2, x3, x4) = [0] [U52^#](x1, x2) = [0] [c_24](x1) = [0] [U61^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] [c_25](x1, x2, x3, x4, x5) = [0] [U62^#](x1, x2, x3) = [0] [c_26](x1, x2, x3, x4, x5) = [0] [U63^#](x1, x2, x3) = [0] [c_27](x1, x2, x3, x4, x5) = [0] [U64^#](x1, x2, x3) = [0] [c_28](x1, x2, x3, x4) = [0] [c_29] = [0] [c_30] = [0] [c_31] = [0] [c] = [0] [c_1](x1, x2) = [0] [c_2](x1, x2) = [0] [c_3](x1, x2) = [0] [c_4](x1) = [0] [c_5](x1, x2) = [0] [c_6](x1) = [0] [c_7](x1, x2) = [0] [c_8](x1) = [0] [c_9](x1, x2) = [0] [c_10](x1, x2) = [0] [c_11](x1, x2) = [0] [c_12](x1) = [0] [c_13](x1) = [0] [c_14](x1, x2) = [0] [c_15](x1, x2) = [0] [c_16](x1) = [0] [c] = [0] [c_1](x1) = [2] x1 + [0] [c_2](x1) = [2] x1 + [0] [c_3] = [0] [c_4](x1) = [2] x1 + [0] [c_5](x1) = [4] x1 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1, x2) = [4] x1 + [2] x2 + [0] [c_8](x1) = [4] x1 + [0] [c_9](x1) = [1] x1 + [0] [c_10](x1) = [2] x1 + [0] [c_11](x1) = [2] x1 + [3] [c_12](x1, x2) = [4] x1 + [4] x2 + [0] The following symbols are considered usable {U11, U12, isNatKind, activate, U13, U14, U15, isNat, U16, U21, U22, U23, U31, U32, U41, s, plus, 0, U11^#, U12^#, U13^#, U14^#, U15^#, isNat^#, U21^#, U22^#, U61^#, U62^#, U63^#} The order satisfies the following ordering constraints: [U11(tt(), V1, V2)] = [4] >= [4] = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] [U12(tt(), V1, V2)] = [4] >= [4] = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind(n__0())] = [4] > [0] = [tt()] [isNatKind(n__plus(V1, V2))] = [4] > [0] = [U31(isNatKind(activate(V1)), activate(V2))] [isNatKind(n__s(V1))] = [4] > [0] = [U41(isNatKind(activate(V1)))] [activate(X)] = [1] X + [4] > [1] X + [0] = [X] [activate(n__0())] = [4] > [1] = [0()] [activate(n__plus(X1, X2))] = [5] > [1] = [plus(X1, X2)] [activate(n__s(X))] = [4] > [1] = [s(X)] [U13(tt(), V1, V2)] = [4] >= [4] = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] [U14(tt(), V1, V2)] = [4] >= [4] = [U15(isNat(activate(V1)), activate(V2))] [U15(tt(), V2)] = [4] >= [4] = [U16(isNat(activate(V2)))] [isNat(n__0())] = [0] >= [0] = [tt()] [isNat(n__plus(V1, V2))] = [4] >= [4] = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat(n__s(V1))] = [0] >= [0] = [U21(isNatKind(activate(V1)), activate(V1))] [U16(tt())] = [4] > [0] = [tt()] [U21(tt(), V1)] = [0] >= [0] = [U22(isNatKind(activate(V1)), activate(V1))] [U22(tt(), V1)] = [0] >= [0] = [U23(isNat(activate(V1)))] [U23(tt())] = [0] >= [0] = [tt()] [U31(tt(), V2)] = [0] >= [0] = [U32(isNatKind(activate(V2)))] [U32(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [tt()] [s(X)] = [1] > [0] = [n__s(X)] [plus(X1, X2)] = [1] >= [1] = [n__plus(X1, X2)] [0()] = [1] > [0] = [n__0()] [U11^#(tt(), V1, V2)] = [0] >= [0] = [c_4(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)))] [U12^#(tt(), V1, V2)] = [0] >= [0] = [c_5(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)))] [U13^#(tt(), V1, V2)] = [0] >= [0] = [c_6(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)))] [U14^#(tt(), V1, V2)] = [0] >= [0] = [c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)))] [U15^#(tt(), V2)] = [0] >= [0] = [c_8(isNat^#(activate(V2)))] [isNat^#(n__plus(V1, V2))] = [0] >= [0] = [c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)))] [isNat^#(n__s(V1))] = [0] >= [0] = [c_2(U21^#(isNatKind(activate(V1)), activate(V1)))] [U21^#(tt(), V1)] = [0] >= [0] = [c_9(U22^#(isNatKind(activate(V1)), activate(V1)))] [U22^#(tt(), V1)] = [0] >= [0] = [c_10(isNat^#(activate(V1)))] [U61^#(tt(), M, N)] = [7] N + [7] M + [7] > [3] = [c_11(U62^#(isNatKind(activate(M)), activate(M), activate(N)))] [U62^#(tt(), M, N)] = [0] >= [0] = [c_12(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N)))] [U63^#(tt(), M, N)] = [0] >= [0] = [c_3()] We return to the main proof. Consider the set of all dependency pairs : { 1: isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 2: isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) , 3: U63^#(tt(), M, N) -> c_3() , 4: U11^#(tt(), V1, V2) -> c_4(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 5: U12^#(tt(), V1, V2) -> c_5(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 6: U13^#(tt(), V1, V2) -> c_6(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 7: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 8: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 9: U21^#(tt(), V1) -> c_9(U22^#(isNatKind(activate(V1)), activate(V1))) , 10: U22^#(tt(), V1) -> c_10(isNat^#(activate(V1))) , 11: U61^#(tt(), M, N) -> c_11(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , 12: U62^#(tt(), M, N) -> c_12(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(1)) on application of dependency pairs {11}. These cover all (indirect) predecessors of dependency pairs {3,11,12}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_4(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_5(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_6(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_9(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_10(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_11(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_12(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_3() } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { U63^#(tt(), M, N) -> c_3() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_4(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_5(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_6(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_9(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_10(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_11(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_12(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U62^#(tt(), M, N) -> c_12(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) } Weak DPs: { U11^#(tt(), V1, V2) -> c_3(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_4(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_6(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_7(isNat^#(activate(V2))) , U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 2: isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) , 10: U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) } Trs: { isNatKind(n__0()) -> tt() , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U32(tt()) -> tt() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [U11](x1, x2, x3) = [1] x1 + [4] x3 + [4] [tt] = [0] [U12](x1, x2, x3) = [4] [isNatKind](x1) = [4] [activate](x1) = [1] x1 + [0] [U13](x1, x2, x3) = [4] [U14](x1, x2, x3) = [4] [U15](x1, x2) = [4] [isNat](x1) = [6] x1 + [0] [U16](x1) = [0] [U21](x1, x2) = [0] [U22](x1, x2) = [0] [U23](x1) = [0] [U31](x1, x2) = [4] [U32](x1) = [4] [U41](x1) = [0] [U51](x1, x2) = [7] x1 + [7] x2 + [0] [U52](x1, x2) = [7] x1 + [7] x2 + [0] [U61](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U62](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U63](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U64](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [s](x1) = [1] x1 + [2] [plus](x1, x2) = [1] x1 + [1] x2 + [2] [n__0] = [0] [n__plus](x1, x2) = [1] x1 + [1] x2 + [2] [n__s](x1) = [1] x1 + [2] [0] = [0] [U11^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [c_1](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U12^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [isNatKind^#](x1) = [7] x1 + [0] [activate^#](x1) = [7] x1 + [0] [c_2](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U13^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [c_3] = [0] [c_4](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U31^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_5](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U41^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [0^#] = [0] [c_8](x1) = [7] x1 + [0] [plus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1) = [7] x1 + [0] [s^#](x1) = [7] x1 + [0] [c_10](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U14^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [c_11](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U15^#](x1, x2) = [4] x2 + [0] [isNat^#](x1) = [4] x1 + [0] [c_12](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U16^#](x1) = [7] x1 + [0] [c_13] = [0] [c_14](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [c_15](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U21^#](x1, x2) = [4] x2 + [0] [c_16] = [0] [c_17](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U22^#](x1, x2) = [4] x2 + [0] [c_18](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U23^#](x1) = [7] x1 + [0] [c_19] = [0] [c_20](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U32^#](x1) = [7] x1 + [0] [c_21] = [0] [c_22] = [0] [U51^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_23](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U52^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_24](x1) = [7] x1 + [0] [U61^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] [c_25](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U62^#](x1, x2, x3) = [4] x3 + [0] [c_26](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U63^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_27](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U64^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_28](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_29] = [0] [c_30] = [0] [c_31] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [c_3](x1, x2) = [7] x1 + [7] x2 + [0] [c_4](x1) = [7] x1 + [0] [c_5](x1, x2) = [7] x1 + [7] x2 + [0] [c_6](x1) = [7] x1 + [0] [c_7](x1, x2) = [7] x1 + [7] x2 + [0] [c_8](x1) = [7] x1 + [0] [c_9](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1) = [7] x1 + [0] [c_14](x1, x2) = [7] x1 + [7] x2 + [0] [c_15](x1, x2) = [7] x1 + [7] x2 + [0] [c_16](x1) = [7] x1 + [0] [c] = [0] [c_1](x1) = [7] x1 + [0] [c_2](x1) = [7] x1 + [0] [c_3] = [0] [c_4](x1) = [7] x1 + [0] [c_5](x1) = [7] x1 + [0] [c_6](x1) = [7] x1 + [0] [c_7](x1, x2) = [7] x1 + [7] x2 + [0] [c_8](x1) = [7] x1 + [0] [c_9](x1) = [7] x1 + [0] [c_10](x1) = [7] x1 + [0] [c_11](x1) = [7] x1 + [0] [c_12](x1, x2) = [7] x1 + [7] x2 + [0] [c] = [0] [c_1](x1) = [1] x1 + [3] [c_2](x1) = [1] x1 + [1] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] [c_5](x1) = [1] x1 + [0] [c_6](x1, x2) = [1] x1 + [1] x2 + [0] [c_7](x1) = [1] x1 + [0] [c_8](x1) = [1] x1 + [0] [c_9](x1) = [1] x1 + [0] [c_10](x1) = [1] x1 + [3] [c_11](x1) = [1] x1 + [0] The following symbols are considered usable {U11, U12, isNatKind, activate, U13, U14, U15, isNat, U16, U21, U22, U23, U31, U32, U41, s, plus, 0, U11^#, U12^#, U13^#, U14^#, U15^#, isNat^#, U21^#, U22^#, U61^#, U62^#} The order satisfies the following ordering constraints: [U11(tt(), V1, V2)] = [4] V2 + [4] >= [4] = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] [U12(tt(), V1, V2)] = [4] >= [4] = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind(n__0())] = [4] > [0] = [tt()] [isNatKind(n__plus(V1, V2))] = [4] >= [4] = [U31(isNatKind(activate(V1)), activate(V2))] [isNatKind(n__s(V1))] = [4] > [0] = [U41(isNatKind(activate(V1)))] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__0())] = [0] >= [0] = [0()] [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = [plus(X1, X2)] [activate(n__s(X))] = [1] X + [2] >= [1] X + [2] = [s(X)] [U13(tt(), V1, V2)] = [4] >= [4] = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] [U14(tt(), V1, V2)] = [4] >= [4] = [U15(isNat(activate(V1)), activate(V2))] [U15(tt(), V2)] = [4] > [0] = [U16(isNat(activate(V2)))] [isNat(n__0())] = [0] >= [0] = [tt()] [isNat(n__plus(V1, V2))] = [6] V1 + [6] V2 + [12] > [4] V2 + [8] = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat(n__s(V1))] = [6] V1 + [12] > [0] = [U21(isNatKind(activate(V1)), activate(V1))] [U16(tt())] = [0] >= [0] = [tt()] [U21(tt(), V1)] = [0] >= [0] = [U22(isNatKind(activate(V1)), activate(V1))] [U22(tt(), V1)] = [0] >= [0] = [U23(isNat(activate(V1)))] [U23(tt())] = [0] >= [0] = [tt()] [U31(tt(), V2)] = [4] >= [4] = [U32(isNatKind(activate(V2)))] [U32(tt())] = [4] > [0] = [tt()] [U41(tt())] = [0] >= [0] = [tt()] [s(X)] = [1] X + [2] >= [1] X + [2] = [n__s(X)] [plus(X1, X2)] = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = [n__plus(X1, X2)] [0()] = [0] >= [0] = [n__0()] [U11^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [4] V2 + [0] = [c_3(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)))] [U12^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [4] V2 + [0] = [c_4(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)))] [U13^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [4] V2 + [0] = [c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)))] [U14^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [4] V2 + [0] = [c_6(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)))] [U15^#(tt(), V2)] = [4] V2 + [0] >= [4] V2 + [0] = [c_7(isNat^#(activate(V2)))] [isNat^#(n__plus(V1, V2))] = [4] V1 + [4] V2 + [8] > [4] V1 + [4] V2 + [3] = [c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)))] [isNat^#(n__s(V1))] = [4] V1 + [8] > [4] V1 + [1] = [c_2(U21^#(isNatKind(activate(V1)), activate(V1)))] [U21^#(tt(), V1)] = [4] V1 + [0] >= [4] V1 + [0] = [c_8(U22^#(isNatKind(activate(V1)), activate(V1)))] [U22^#(tt(), V1)] = [4] V1 + [0] >= [4] V1 + [0] = [c_9(isNat^#(activate(V1)))] [U61^#(tt(), M, N)] = [7] N + [7] M + [7] > [4] N + [3] = [c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N)))] [U62^#(tt(), M, N)] = [4] N + [0] >= [4] N + [0] = [c_11(isNat^#(activate(N)))] We return to the main proof. Consider the set of all dependency pairs : { 1: isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 2: isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) , 3: U11^#(tt(), V1, V2) -> c_3(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 4: U12^#(tt(), V1, V2) -> c_4(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 5: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 6: U14^#(tt(), V1, V2) -> c_6(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 7: U15^#(tt(), V2) -> c_7(isNat^#(activate(V2))) , 8: U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , 9: U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , 10: U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , 11: U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,2,10}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7,8,9,10,11}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { U11^#(tt(), V1, V2) -> c_3(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_4(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_6(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_7(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { U11^#(tt(), V1, V2) -> c_3(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_4(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_6(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_7(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_1(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_2(U21^#(isNatKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) } Weak DPs: { U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , U15^#(tt(), V2) -> isNat^#(activate(V2)) , isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , U22^#(tt(), V1) -> isNat^#(activate(V1)) , U51^#(tt(), N) -> isNatKind^#(activate(N)) , U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , U62^#(tt(), M, N) -> isNat^#(activate(N)) , U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , 4: U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , 5: U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , 14: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , 20: U51^#(tt(), N) -> isNatKind^#(activate(N)) , 21: U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , 22: U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [U11](x1, x2, x3) = [0] [tt] = [0] [U12](x1, x2, x3) = [0] [isNatKind](x1) = [0] [activate](x1) = [1] x1 + [0] [U13](x1, x2, x3) = [0] [U14](x1, x2, x3) = [0] [U15](x1, x2) = [0] [isNat](x1) = [0] [U16](x1) = [0] [U21](x1, x2) = [0] [U22](x1, x2) = [0] [U23](x1) = [0] [U31](x1, x2) = [0] [U32](x1) = [0] [U41](x1) = [0] [U51](x1, x2) = [7] x1 + [7] x2 + [0] [U52](x1, x2) = [7] x1 + [7] x2 + [0] [U61](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U62](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U63](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U64](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [s](x1) = [1] x1 + [0] [plus](x1, x2) = [1] x1 + [1] x2 + [1] [n__0] = [0] [n__plus](x1, x2) = [1] x1 + [1] x2 + [1] [n__s](x1) = [1] x1 + [0] [0] = [0] [U11^#](x1, x2, x3) = [4] x2 + [4] x3 + [4] [c_1](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U12^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [isNatKind^#](x1) = [4] x1 + [0] [activate^#](x1) = [7] x1 + [0] [c_2](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U13^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [c_3] = [0] [c_4](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U31^#](x1, x2) = [4] x2 + [0] [c_5](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U41^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [0^#] = [0] [c_8](x1) = [7] x1 + [0] [plus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1) = [7] x1 + [0] [s^#](x1) = [7] x1 + [0] [c_10](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U14^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] [c_11](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U15^#](x1, x2) = [4] x2 + [0] [isNat^#](x1) = [4] x1 + [0] [c_12](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U16^#](x1) = [7] x1 + [0] [c_13] = [0] [c_14](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [c_15](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U21^#](x1, x2) = [4] x2 + [0] [c_16] = [0] [c_17](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U22^#](x1, x2) = [4] x2 + [0] [c_18](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U23^#](x1) = [7] x1 + [0] [c_19] = [0] [c_20](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U32^#](x1) = [7] x1 + [0] [c_21] = [0] [c_22] = [0] [U51^#](x1, x2) = [7] x1 + [7] x2 + [3] [c_23](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U52^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_24](x1) = [7] x1 + [0] [U61^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [1] [c_25](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U62^#](x1, x2, x3) = [4] x3 + [0] [c_26](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U63^#](x1, x2, x3) = [4] x3 + [0] [c_27](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U64^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_28](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_29] = [0] [c_30] = [0] [c_31] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [c_3](x1, x2) = [1] x1 + [1] x2 + [1] [c_4](x1) = [1] x1 + [0] [c_5](x1, x2) = [7] x1 + [7] x2 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1, x2) = [7] x1 + [7] x2 + [0] [c_8](x1) = [7] x1 + [0] [c_9](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1) = [7] x1 + [0] [c_14](x1, x2) = [7] x1 + [7] x2 + [0] [c_15](x1, x2) = [7] x1 + [7] x2 + [0] [c_16](x1) = [7] x1 + [0] The following symbols are considered usable {U11, U12, isNatKind, activate, U13, U14, U15, isNat, U16, U21, U22, U23, U31, U32, U41, s, plus, 0, U11^#, U12^#, isNatKind^#, U13^#, U31^#, U14^#, U15^#, isNat^#, U21^#, U22^#, U51^#, U61^#, U62^#, U63^#} The order satisfies the following ordering constraints: [U11(tt(), V1, V2)] = [0] >= [0] = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] [U12(tt(), V1, V2)] = [0] >= [0] = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind(n__0())] = [0] >= [0] = [tt()] [isNatKind(n__plus(V1, V2))] = [0] >= [0] = [U31(isNatKind(activate(V1)), activate(V2))] [isNatKind(n__s(V1))] = [0] >= [0] = [U41(isNatKind(activate(V1)))] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__0())] = [0] >= [0] = [0()] [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = [plus(X1, X2)] [activate(n__s(X))] = [1] X + [0] >= [1] X + [0] = [s(X)] [U13(tt(), V1, V2)] = [0] >= [0] = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] [U14(tt(), V1, V2)] = [0] >= [0] = [U15(isNat(activate(V1)), activate(V2))] [U15(tt(), V2)] = [0] >= [0] = [U16(isNat(activate(V2)))] [isNat(n__0())] = [0] >= [0] = [tt()] [isNat(n__plus(V1, V2))] = [0] >= [0] = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat(n__s(V1))] = [0] >= [0] = [U21(isNatKind(activate(V1)), activate(V1))] [U16(tt())] = [0] >= [0] = [tt()] [U21(tt(), V1)] = [0] >= [0] = [U22(isNatKind(activate(V1)), activate(V1))] [U22(tt(), V1)] = [0] >= [0] = [U23(isNat(activate(V1)))] [U23(tt())] = [0] >= [0] = [tt()] [U31(tt(), V2)] = [0] >= [0] = [U32(isNatKind(activate(V2)))] [U32(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [tt()] [s(X)] = [1] X + [0] >= [1] X + [0] = [n__s(X)] [plus(X1, X2)] = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = [n__plus(X1, X2)] [0()] = [0] >= [0] = [n__0()] [U11^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [4] > [4] V1 + [4] V2 + [0] = [U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))] [U11^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [4] > [4] V1 + [0] = [isNatKind^#(activate(V1))] [U12^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V2 + [0] = [isNatKind^#(activate(V2))] [U12^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [4] V2 + [0] = [U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind^#(n__plus(V1, V2))] = [4] V1 + [4] V2 + [4] > [4] V1 + [4] V2 + [1] = [c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)))] [isNatKind^#(n__s(V1))] = [4] V1 + [0] >= [4] V1 + [0] = [c_4(isNatKind^#(activate(V1)))] [U13^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V2 + [0] = [isNatKind^#(activate(V2))] [U13^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [4] V2 + [0] = [U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))] [U31^#(tt(), V2)] = [4] V2 + [0] >= [4] V2 + [0] = [c_6(isNatKind^#(activate(V2)))] [U14^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V2 + [0] = [U15^#(isNat(activate(V1)), activate(V2))] [U14^#(tt(), V1, V2)] = [4] V1 + [4] V2 + [0] >= [4] V1 + [0] = [isNat^#(activate(V1))] [U15^#(tt(), V2)] = [4] V2 + [0] >= [4] V2 + [0] = [isNat^#(activate(V2))] [isNat^#(n__plus(V1, V2))] = [4] V1 + [4] V2 + [4] >= [4] V1 + [4] V2 + [4] = [U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat^#(n__plus(V1, V2))] = [4] V1 + [4] V2 + [4] > [4] V1 + [0] = [isNatKind^#(activate(V1))] [isNat^#(n__s(V1))] = [4] V1 + [0] >= [4] V1 + [0] = [isNatKind^#(activate(V1))] [isNat^#(n__s(V1))] = [4] V1 + [0] >= [4] V1 + [0] = [U21^#(isNatKind(activate(V1)), activate(V1))] [U21^#(tt(), V1)] = [4] V1 + [0] >= [4] V1 + [0] = [isNatKind^#(activate(V1))] [U21^#(tt(), V1)] = [4] V1 + [0] >= [4] V1 + [0] = [U22^#(isNatKind(activate(V1)), activate(V1))] [U22^#(tt(), V1)] = [4] V1 + [0] >= [4] V1 + [0] = [isNat^#(activate(V1))] [U51^#(tt(), N)] = [7] N + [3] > [4] N + [0] = [isNatKind^#(activate(N))] [U61^#(tt(), M, N)] = [7] N + [7] M + [1] > [4] M + [0] = [isNatKind^#(activate(M))] [U61^#(tt(), M, N)] = [7] N + [7] M + [1] > [4] N + [0] = [U62^#(isNatKind(activate(M)), activate(M), activate(N))] [U62^#(tt(), M, N)] = [4] N + [0] >= [4] N + [0] = [isNat^#(activate(N))] [U62^#(tt(), M, N)] = [4] N + [0] >= [4] N + [0] = [U63^#(isNat(activate(N)), activate(M), activate(N))] [U63^#(tt(), M, N)] = [4] N + [0] >= [4] N + [0] = [isNatKind^#(activate(N))] We return to the main proof. Consider the set of all dependency pairs : { 1: isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , 2: isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , 3: U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , 4: U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , 5: U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , 6: U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , 7: U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , 8: U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , 9: U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , 10: U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , 11: U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , 12: U15^#(tt(), V2) -> isNat^#(activate(V2)) , 13: isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , 14: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , 15: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , 16: isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , 17: U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , 18: U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , 19: U22^#(tt(), V1) -> isNat^#(activate(V1)) , 20: U51^#(tt(), N) -> isNatKind^#(activate(N)) , 21: U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , 22: U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , 23: U62^#(tt(), M, N) -> isNat^#(activate(N)) , 24: U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , 25: U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,4,5,14,20,21,22}. These cover all (indirect) predecessors of dependency pairs {1,3,4,5,6,7,8,9,10,11,12,14,20,21,22,23,24,25}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) } Weak DPs: { U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , U15^#(tt(), V2) -> isNat^#(activate(V2)) , isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , U22^#(tt(), V1) -> isNat^#(activate(V1)) , U51^#(tt(), N) -> isNatKind^#(activate(N)) , U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , U62^#(tt(), M, N) -> isNat^#(activate(N)) , U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , 15: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , 16: isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , 20: U51^#(tt(), N) -> isNatKind^#(activate(N)) , 21: U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , 22: U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1, 2}, Uargs(c_4) = {1}, Uargs(c_6) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [U11](x1, x2, x3) = [0] [tt] = [0] [U12](x1, x2, x3) = [0] [isNatKind](x1) = [0] [activate](x1) = [1] x1 + [0] [U13](x1, x2, x3) = [0] [U14](x1, x2, x3) = [0] [U15](x1, x2) = [0] [isNat](x1) = [0] [U16](x1) = [0] [U21](x1, x2) = [0] [U22](x1, x2) = [0] [U23](x1) = [0] [U31](x1, x2) = [0] [U32](x1) = [0] [U41](x1) = [0] [U51](x1, x2) = [7] x1 + [7] x2 + [0] [U52](x1, x2) = [7] x1 + [7] x2 + [0] [U61](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U62](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U63](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U64](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [s](x1) = [1] x1 + [1] [plus](x1, x2) = [1] x1 + [1] x2 + [0] [n__0] = [0] [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] [n__s](x1) = [1] x1 + [1] [0] = [0] [U11^#](x1, x2, x3) = [2] x2 + [2] x3 + [0] [c_1](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U12^#](x1, x2, x3) = [2] x2 + [2] x3 + [0] [isNatKind^#](x1) = [2] x1 + [0] [activate^#](x1) = [7] x1 + [0] [c_2](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U13^#](x1, x2, x3) = [2] x2 + [2] x3 + [0] [c_3] = [0] [c_4](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U31^#](x1, x2) = [2] x2 + [0] [c_5](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U41^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [0^#] = [0] [c_8](x1) = [7] x1 + [0] [plus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1) = [7] x1 + [0] [s^#](x1) = [7] x1 + [0] [c_10](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U14^#](x1, x2, x3) = [2] x2 + [2] x3 + [0] [c_11](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U15^#](x1, x2) = [2] x2 + [0] [isNat^#](x1) = [2] x1 + [0] [c_12](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U16^#](x1) = [7] x1 + [0] [c_13] = [0] [c_14](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [c_15](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U21^#](x1, x2) = [2] x2 + [0] [c_16] = [0] [c_17](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U22^#](x1, x2) = [2] x2 + [0] [c_18](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U23^#](x1) = [7] x1 + [0] [c_19] = [0] [c_20](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U32^#](x1) = [7] x1 + [0] [c_21] = [0] [c_22] = [0] [U51^#](x1, x2) = [7] x1 + [7] x2 + [7] [c_23](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U52^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_24](x1) = [7] x1 + [0] [U61^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [1] [c_25](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U62^#](x1, x2, x3) = [4] x3 + [0] [c_26](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U63^#](x1, x2, x3) = [4] x3 + [0] [c_27](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U64^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_28](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_29] = [0] [c_30] = [0] [c_31] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [c_3](x1, x2) = [1] x1 + [1] x2 + [0] [c_4](x1) = [1] x1 + [1] [c_5](x1, x2) = [7] x1 + [7] x2 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1, x2) = [7] x1 + [7] x2 + [0] [c_8](x1) = [7] x1 + [0] [c_9](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1) = [7] x1 + [0] [c_14](x1, x2) = [7] x1 + [7] x2 + [0] [c_15](x1, x2) = [7] x1 + [7] x2 + [0] [c_16](x1) = [7] x1 + [0] The following symbols are considered usable {U11, U12, isNatKind, activate, U13, U14, U15, isNat, U16, U21, U22, U23, U31, U32, U41, s, plus, 0, U11^#, U12^#, isNatKind^#, U13^#, U31^#, U14^#, U15^#, isNat^#, U21^#, U22^#, U51^#, U61^#, U62^#, U63^#} The order satisfies the following ordering constraints: [U11(tt(), V1, V2)] = [0] >= [0] = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] [U12(tt(), V1, V2)] = [0] >= [0] = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind(n__0())] = [0] >= [0] = [tt()] [isNatKind(n__plus(V1, V2))] = [0] >= [0] = [U31(isNatKind(activate(V1)), activate(V2))] [isNatKind(n__s(V1))] = [0] >= [0] = [U41(isNatKind(activate(V1)))] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__0())] = [0] >= [0] = [0()] [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [plus(X1, X2)] [activate(n__s(X))] = [1] X + [1] >= [1] X + [1] = [s(X)] [U13(tt(), V1, V2)] = [0] >= [0] = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] [U14(tt(), V1, V2)] = [0] >= [0] = [U15(isNat(activate(V1)), activate(V2))] [U15(tt(), V2)] = [0] >= [0] = [U16(isNat(activate(V2)))] [isNat(n__0())] = [0] >= [0] = [tt()] [isNat(n__plus(V1, V2))] = [0] >= [0] = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat(n__s(V1))] = [0] >= [0] = [U21(isNatKind(activate(V1)), activate(V1))] [U16(tt())] = [0] >= [0] = [tt()] [U21(tt(), V1)] = [0] >= [0] = [U22(isNatKind(activate(V1)), activate(V1))] [U22(tt(), V1)] = [0] >= [0] = [U23(isNat(activate(V1)))] [U23(tt())] = [0] >= [0] = [tt()] [U31(tt(), V2)] = [0] >= [0] = [U32(isNatKind(activate(V2)))] [U32(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [tt()] [s(X)] = [1] X + [1] >= [1] X + [1] = [n__s(X)] [plus(X1, X2)] = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = [n__plus(X1, X2)] [0()] = [0] >= [0] = [n__0()] [U11^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V1 + [2] V2 + [0] = [U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))] [U11^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V1 + [0] = [isNatKind^#(activate(V1))] [U12^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V2 + [0] = [isNatKind^#(activate(V2))] [U12^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V1 + [2] V2 + [0] = [U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind^#(n__plus(V1, V2))] = [2] V1 + [2] V2 + [0] >= [2] V1 + [2] V2 + [0] = [c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1)))] [isNatKind^#(n__s(V1))] = [2] V1 + [2] > [2] V1 + [1] = [c_4(isNatKind^#(activate(V1)))] [U13^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V2 + [0] = [isNatKind^#(activate(V2))] [U13^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V1 + [2] V2 + [0] = [U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))] [U31^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [c_6(isNatKind^#(activate(V2)))] [U14^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V2 + [0] = [U15^#(isNat(activate(V1)), activate(V2))] [U14^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V1 + [0] = [isNat^#(activate(V1))] [U15^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [isNat^#(activate(V2))] [isNat^#(n__plus(V1, V2))] = [2] V1 + [2] V2 + [0] >= [2] V1 + [2] V2 + [0] = [U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat^#(n__plus(V1, V2))] = [2] V1 + [2] V2 + [0] >= [2] V1 + [0] = [isNatKind^#(activate(V1))] [isNat^#(n__s(V1))] = [2] V1 + [2] > [2] V1 + [0] = [isNatKind^#(activate(V1))] [isNat^#(n__s(V1))] = [2] V1 + [2] > [2] V1 + [0] = [U21^#(isNatKind(activate(V1)), activate(V1))] [U21^#(tt(), V1)] = [2] V1 + [0] >= [2] V1 + [0] = [isNatKind^#(activate(V1))] [U21^#(tt(), V1)] = [2] V1 + [0] >= [2] V1 + [0] = [U22^#(isNatKind(activate(V1)), activate(V1))] [U22^#(tt(), V1)] = [2] V1 + [0] >= [2] V1 + [0] = [isNat^#(activate(V1))] [U51^#(tt(), N)] = [7] N + [7] > [2] N + [0] = [isNatKind^#(activate(N))] [U61^#(tt(), M, N)] = [7] N + [7] M + [1] > [2] M + [0] = [isNatKind^#(activate(M))] [U61^#(tt(), M, N)] = [7] N + [7] M + [1] > [4] N + [0] = [U62^#(isNatKind(activate(M)), activate(M), activate(N))] [U62^#(tt(), M, N)] = [4] N + [0] >= [2] N + [0] = [isNat^#(activate(N))] [U62^#(tt(), M, N)] = [4] N + [0] >= [4] N + [0] = [U63^#(isNat(activate(N)), activate(M), activate(N))] [U63^#(tt(), M, N)] = [4] N + [0] >= [2] N + [0] = [isNatKind^#(activate(N))] We return to the main proof. Consider the set of all dependency pairs : { 1: isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , 2: U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , 3: U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , 4: U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , 5: U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , 6: isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , 7: U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , 8: U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , 9: U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , 10: U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , 11: U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , 12: U15^#(tt(), V2) -> isNat^#(activate(V2)) , 13: isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , 14: isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , 15: isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , 16: isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , 17: U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , 18: U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , 19: U22^#(tt(), V1) -> isNat^#(activate(V1)) , 20: U51^#(tt(), N) -> isNatKind^#(activate(N)) , 21: U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , 22: U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , 23: U62^#(tt(), M, N) -> isNat^#(activate(N)) , 24: U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , 25: U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,15,16,20,21,22}. These cover all (indirect) predecessors of dependency pairs {1,15,16,17,18,19,20,21,22,23,24,25}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , U15^#(tt(), V2) -> isNat^#(activate(V2)) , isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , U22^#(tt(), V1) -> isNat^#(activate(V1)) , U51^#(tt(), N) -> isNatKind^#(activate(N)) , U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , U62^#(tt(), M, N) -> isNat^#(activate(N)) , U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { U11^#(tt(), V1, V2) -> U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11^#(tt(), V1, V2) -> isNatKind^#(activate(V1)) , U12^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U12^#(tt(), V1, V2) -> U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U13^#(tt(), V1, V2) -> isNatKind^#(activate(V2)) , U13^#(tt(), V1, V2) -> U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> U15^#(isNat(activate(V1)), activate(V2)) , U14^#(tt(), V1, V2) -> isNat^#(activate(V1)) , U15^#(tt(), V2) -> isNat^#(activate(V2)) , isNat^#(n__plus(V1, V2)) -> U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat^#(n__plus(V1, V2)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> isNatKind^#(activate(V1)) , isNat^#(n__s(V1)) -> U21^#(isNatKind(activate(V1)), activate(V1)) , U21^#(tt(), V1) -> isNatKind^#(activate(V1)) , U21^#(tt(), V1) -> U22^#(isNatKind(activate(V1)), activate(V1)) , U22^#(tt(), V1) -> isNat^#(activate(V1)) , U51^#(tt(), N) -> isNatKind^#(activate(N)) , U61^#(tt(), M, N) -> isNatKind^#(activate(M)) , U61^#(tt(), M, N) -> U62^#(isNatKind(activate(M)), activate(M), activate(N)) , U62^#(tt(), M, N) -> isNat^#(activate(N)) , U62^#(tt(), M, N) -> U63^#(isNat(activate(N)), activate(M), activate(N)) , U63^#(tt(), M, N) -> isNatKind^#(activate(N)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {12} by applications of Pre({12}) = {11}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 3: U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , 4: U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 5: U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , 6: isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , 7: isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 8: U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , 9: U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , 10: U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , 11: U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) , 12: U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) , 13: isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , 14: isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , 15: U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , 16: U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak DPs: { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { isNatKind^#(n__plus(V1, V2)) -> c_3(U31^#(isNatKind(activate(V1)), activate(V2)), isNatKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_4(isNatKind^#(activate(V1))) , U31^#(tt(), V2) -> c_6(isNatKind^#(activate(V2))) , U51^#(tt(), N) -> c_13(isNatKind^#(activate(N))) , U63^#(tt(), M, N) -> c_16(isNatKind^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U14^#(tt(), V1, V2) -> c_7(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_8(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U22^#(tt(), V1) -> c_12(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , U13^#(tt(), V1, V2) -> c_5(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)), isNatKind^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_9(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)), isNatKind^#(activate(V1))) , isNat^#(n__s(V1)) -> c_10(U21^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_11(U22^#(isNatKind(activate(V1)), activate(V1)), isNatKind^#(activate(V1))) , U61^#(tt(), M, N) -> c_14(U62^#(isNatKind(activate(M)), activate(M), activate(N)), isNatKind^#(activate(M))) , U62^#(tt(), M, N) -> c_15(U63^#(isNat(activate(N)), activate(M), activate(N)), isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_3(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_4(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_5(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_6(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_7(U21^#(isNatKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 3: U13^#(tt(), V1, V2) -> c_3(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 6: isNat^#(n__plus(V1, V2)) -> c_6(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 7: isNat^#(n__s(V1)) -> c_7(U21^#(isNatKind(activate(V1)), activate(V1))) , 11: U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [U11](x1, x2, x3) = [0] [tt] = [0] [U12](x1, x2, x3) = [0] [isNatKind](x1) = [0] [activate](x1) = [1] x1 + [0] [U13](x1, x2, x3) = [0] [U14](x1, x2, x3) = [0] [U15](x1, x2) = [0] [isNat](x1) = [0] [U16](x1) = [0] [U21](x1, x2) = [0] [U22](x1, x2) = [0] [U23](x1) = [0] [U31](x1, x2) = [0] [U32](x1) = [0] [U41](x1) = [0] [U51](x1, x2) = [7] x1 + [7] x2 + [0] [U52](x1, x2) = [7] x1 + [7] x2 + [0] [U61](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U62](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U63](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U64](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [s](x1) = [1] x1 + [4] [plus](x1, x2) = [1] x1 + [1] x2 + [4] [n__0] = [0] [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] [n__s](x1) = [1] x1 + [4] [0] = [0] [U11^#](x1, x2, x3) = [2] x2 + [2] x3 + [4] [c_1](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U12^#](x1, x2, x3) = [2] x2 + [2] x3 + [4] [isNatKind^#](x1) = [7] x1 + [0] [activate^#](x1) = [7] x1 + [0] [c_2](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U13^#](x1, x2, x3) = [2] x2 + [2] x3 + [4] [c_3] = [0] [c_4](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U31^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_5](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U41^#](x1) = [7] x1 + [0] [c_6] = [0] [c_7](x1) = [7] x1 + [0] [0^#] = [0] [c_8](x1) = [7] x1 + [0] [plus^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1) = [7] x1 + [0] [s^#](x1) = [7] x1 + [0] [c_10](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U14^#](x1, x2, x3) = [2] x2 + [2] x3 + [0] [c_11](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U15^#](x1, x2) = [2] x2 + [0] [isNat^#](x1) = [2] x1 + [0] [c_12](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U16^#](x1) = [7] x1 + [0] [c_13] = [0] [c_14](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [c_15](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U21^#](x1, x2) = [2] x2 + [0] [c_16] = [0] [c_17](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U22^#](x1, x2) = [2] x2 + [0] [c_18](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U23^#](x1) = [7] x1 + [0] [c_19] = [0] [c_20](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U32^#](x1) = [7] x1 + [0] [c_21] = [0] [c_22] = [0] [U51^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_23](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U52^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_24](x1) = [7] x1 + [0] [U61^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] [c_25](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U62^#](x1, x2, x3) = [2] x3 + [4] [c_26](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U63^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_27](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U64^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_28](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_29] = [0] [c_30] = [0] [c_31] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [c_3](x1, x2) = [7] x1 + [7] x2 + [0] [c_4](x1) = [7] x1 + [0] [c_5](x1, x2) = [7] x1 + [7] x2 + [0] [c_6](x1) = [7] x1 + [0] [c_7](x1, x2) = [7] x1 + [7] x2 + [0] [c_8](x1) = [7] x1 + [0] [c_9](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1) = [7] x1 + [0] [c_14](x1, x2) = [7] x1 + [7] x2 + [0] [c_15](x1, x2) = [7] x1 + [7] x2 + [0] [c_16](x1) = [7] x1 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [1] [c_4](x1, x2) = [1] x1 + [1] x2 + [0] [c_5](x1) = [1] x1 + [0] [c_6](x1) = [1] x1 + [3] [c_7](x1) = [1] x1 + [3] [c_8](x1) = [1] x1 + [0] [c_9](x1) = [1] x1 + [0] [c_10](x1) = [1] x1 + [3] [c_11](x1) = [1] x1 + [3] The following symbols are considered usable {U11, U12, isNatKind, activate, U13, U14, U15, isNat, U16, U21, U22, U23, U31, U32, U41, s, plus, 0, U11^#, U12^#, U13^#, U14^#, U15^#, isNat^#, U21^#, U22^#, U61^#, U62^#} The order satisfies the following ordering constraints: [U11(tt(), V1, V2)] = [0] >= [0] = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] [U12(tt(), V1, V2)] = [0] >= [0] = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] [isNatKind(n__0())] = [0] >= [0] = [tt()] [isNatKind(n__plus(V1, V2))] = [0] >= [0] = [U31(isNatKind(activate(V1)), activate(V2))] [isNatKind(n__s(V1))] = [0] >= [0] = [U41(isNatKind(activate(V1)))] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__0())] = [0] >= [0] = [0()] [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = [plus(X1, X2)] [activate(n__s(X))] = [1] X + [4] >= [1] X + [4] = [s(X)] [U13(tt(), V1, V2)] = [0] >= [0] = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] [U14(tt(), V1, V2)] = [0] >= [0] = [U15(isNat(activate(V1)), activate(V2))] [U15(tt(), V2)] = [0] >= [0] = [U16(isNat(activate(V2)))] [isNat(n__0())] = [0] >= [0] = [tt()] [isNat(n__plus(V1, V2))] = [0] >= [0] = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] [isNat(n__s(V1))] = [0] >= [0] = [U21(isNatKind(activate(V1)), activate(V1))] [U16(tt())] = [0] >= [0] = [tt()] [U21(tt(), V1)] = [0] >= [0] = [U22(isNatKind(activate(V1)), activate(V1))] [U22(tt(), V1)] = [0] >= [0] = [U23(isNat(activate(V1)))] [U23(tt())] = [0] >= [0] = [tt()] [U31(tt(), V2)] = [0] >= [0] = [U32(isNatKind(activate(V2)))] [U32(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [tt()] [s(X)] = [1] X + [4] >= [1] X + [4] = [n__s(X)] [plus(X1, X2)] = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = [n__plus(X1, X2)] [0()] = [0] >= [0] = [n__0()] [U11^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [4] >= [2] V1 + [2] V2 + [4] = [c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2)))] [U12^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [4] >= [2] V1 + [2] V2 + [4] = [c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2)))] [U13^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [4] > [2] V1 + [2] V2 + [1] = [c_3(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2)))] [U14^#(tt(), V1, V2)] = [2] V1 + [2] V2 + [0] >= [2] V1 + [2] V2 + [0] = [c_4(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1)))] [U15^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [c_5(isNat^#(activate(V2)))] [isNat^#(n__plus(V1, V2))] = [2] V1 + [2] V2 + [8] > [2] V1 + [2] V2 + [7] = [c_6(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2)))] [isNat^#(n__s(V1))] = [2] V1 + [8] > [2] V1 + [3] = [c_7(U21^#(isNatKind(activate(V1)), activate(V1)))] [U21^#(tt(), V1)] = [2] V1 + [0] >= [2] V1 + [0] = [c_8(U22^#(isNatKind(activate(V1)), activate(V1)))] [U22^#(tt(), V1)] = [2] V1 + [0] >= [2] V1 + [0] = [c_9(isNat^#(activate(V1)))] [U61^#(tt(), M, N)] = [7] N + [7] M + [7] >= [2] N + [7] = [c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N)))] [U62^#(tt(), M, N)] = [2] N + [4] > [2] N + [3] = [c_11(isNat^#(activate(N)))] We return to the main proof. Consider the set of all dependency pairs : { 1: U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 2: U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 3: U13^#(tt(), V1, V2) -> c_3(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , 4: U14^#(tt(), V1, V2) -> c_4(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , 5: U15^#(tt(), V2) -> c_5(isNat^#(activate(V2))) , 6: isNat^#(n__plus(V1, V2)) -> c_6(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 7: isNat^#(n__s(V1)) -> c_7(U21^#(isNatKind(activate(V1)), activate(V1))) , 8: U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , 9: U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , 10: U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , 11: U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {3,6,7,11}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7,8,9,10,11}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_3(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_4(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_5(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_6(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_7(U21^#(isNatKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { U11^#(tt(), V1, V2) -> c_1(U12^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1, V2) -> c_2(U13^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U13^#(tt(), V1, V2) -> c_3(U14^#(isNatKind(activate(V2)), activate(V1), activate(V2))) , U14^#(tt(), V1, V2) -> c_4(U15^#(isNat(activate(V1)), activate(V2)), isNat^#(activate(V1))) , U15^#(tt(), V2) -> c_5(isNat^#(activate(V2))) , isNat^#(n__plus(V1, V2)) -> c_6(U11^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNat^#(n__s(V1)) -> c_7(U21^#(isNatKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_8(U22^#(isNatKind(activate(V1)), activate(V1))) , U22^#(tt(), V1) -> c_9(isNat^#(activate(V1))) , U61^#(tt(), M, N) -> c_10(U62^#(isNatKind(activate(M)), activate(M), activate(N))) , U62^#(tt(), M, N) -> c_11(isNat^#(activate(N))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { U11(tt(), V1, V2) -> U12(isNatKind(activate(V1)), activate(V1), activate(V2)) , U12(tt(), V1, V2) -> U13(isNatKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__plus(V1, V2)) -> U31(isNatKind(activate(V1)), activate(V2)) , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) , activate(X) -> X , activate(n__0()) -> 0() , activate(n__plus(X1, X2)) -> plus(X1, X2) , activate(n__s(X)) -> s(X) , U13(tt(), V1, V2) -> U14(isNatKind(activate(V2)), activate(V1), activate(V2)) , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) , U15(tt(), V2) -> U16(isNat(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__plus(V1, V2)) -> U11(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U16(tt()) -> tt() , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V2) -> U32(isNatKind(activate(V2))) , U32(tt()) -> tt() , U41(tt()) -> tt() , s(X) -> n__s(X) , plus(X1, X2) -> n__plus(X1, X2) , 0() -> n__0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))