YES(O(1),O(n^1)) 26.54/7.33 YES(O(1),O(n^1)) 26.54/7.33 26.54/7.33 We are left with following problem, upon which TcT provides the 26.54/7.33 certificate YES(O(1),O(n^1)). 26.54/7.33 26.54/7.33 Strict Trs: 26.54/7.33 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.33 , U12(tt()) -> tt() 26.54/7.33 , isNat(n__0()) -> tt() 26.54/7.33 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.33 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.33 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.33 , activate(X) -> X 26.54/7.33 , activate(n__0()) -> 0() 26.54/7.33 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.33 , activate(n__s(X)) -> s(X) 26.54/7.33 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.33 , U21(tt()) -> tt() 26.54/7.33 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.33 , U32(tt()) -> tt() 26.54/7.33 , U41(tt(), N) -> activate(N) 26.54/7.33 , U51(tt(), M, N) -> 26.54/7.33 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.33 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.33 , s(X) -> n__s(X) 26.54/7.33 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.33 , plus(N, s(M)) -> U51(isNat(M), M, N) 26.54/7.33 , plus(N, 0()) -> U41(isNat(N), N) 26.54/7.33 , U61(tt()) -> 0() 26.54/7.33 , 0() -> n__0() 26.54/7.33 , U71(tt(), M, N) -> 26.54/7.33 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.33 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.33 , x(X1, X2) -> n__x(X1, X2) 26.54/7.33 , x(N, s(M)) -> U71(isNat(M), M, N) 26.54/7.33 , x(N, 0()) -> U61(isNat(N)) } 26.54/7.33 Obligation: 26.54/7.33 innermost runtime complexity 26.54/7.33 Answer: 26.54/7.33 YES(O(1),O(n^1)) 26.54/7.33 26.54/7.33 Arguments of following rules are not normal-forms: 26.54/7.33 26.54/7.33 { plus(N, s(M)) -> U51(isNat(M), M, N) 26.54/7.33 , plus(N, 0()) -> U41(isNat(N), N) 26.54/7.33 , x(N, s(M)) -> U71(isNat(M), M, N) 26.54/7.33 , x(N, 0()) -> U61(isNat(N)) } 26.54/7.33 26.54/7.33 All above mentioned rules can be savely removed. 26.54/7.33 26.54/7.33 We are left with following problem, upon which TcT provides the 26.54/7.33 certificate YES(O(1),O(n^1)). 26.54/7.33 26.54/7.33 Strict Trs: 26.54/7.33 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.33 , U12(tt()) -> tt() 26.54/7.33 , isNat(n__0()) -> tt() 26.54/7.33 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.33 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.33 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.33 , activate(X) -> X 26.54/7.33 , activate(n__0()) -> 0() 26.54/7.33 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.33 , activate(n__s(X)) -> s(X) 26.54/7.33 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.33 , U21(tt()) -> tt() 26.54/7.33 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.33 , U32(tt()) -> tt() 26.54/7.33 , U41(tt(), N) -> activate(N) 26.54/7.33 , U51(tt(), M, N) -> 26.54/7.33 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.33 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.33 , s(X) -> n__s(X) 26.54/7.33 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.33 , U61(tt()) -> 0() 26.54/7.33 , 0() -> n__0() 26.54/7.33 , U71(tt(), M, N) -> 26.54/7.33 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.33 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.33 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.33 Obligation: 26.54/7.33 innermost runtime complexity 26.54/7.33 Answer: 26.54/7.33 YES(O(1),O(n^1)) 26.54/7.33 26.54/7.33 We add the following dependency tuples: 26.54/7.33 26.54/7.33 Strict DPs: 26.54/7.33 { U11^#(tt(), V2) -> 26.54/7.33 c_1(U12^#(isNat(activate(V2))), 26.54/7.33 isNat^#(activate(V2)), 26.54/7.33 activate^#(V2)) 26.54/7.33 , U12^#(tt()) -> c_2() 26.54/7.33 , isNat^#(n__0()) -> c_3() 26.54/7.33 , isNat^#(n__plus(V1, V2)) -> 26.54/7.33 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.33 isNat^#(activate(V1)), 26.54/7.33 activate^#(V1), 26.54/7.33 activate^#(V2)) 26.54/7.33 , isNat^#(n__s(V1)) -> 26.54/7.33 c_5(U21^#(isNat(activate(V1))), 26.54/7.33 isNat^#(activate(V1)), 26.54/7.33 activate^#(V1)) 26.54/7.33 , isNat^#(n__x(V1, V2)) -> 26.54/7.33 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.33 isNat^#(activate(V1)), 26.54/7.33 activate^#(V1), 26.54/7.33 activate^#(V2)) 26.54/7.33 , activate^#(X) -> c_7() 26.54/7.33 , activate^#(n__0()) -> c_8(0^#()) 26.54/7.33 , activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.33 , activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.33 , activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.33 , U21^#(tt()) -> c_12() 26.54/7.33 , U31^#(tt(), V2) -> 26.54/7.33 c_13(U32^#(isNat(activate(V2))), 26.54/7.33 isNat^#(activate(V2)), 26.54/7.33 activate^#(V2)) 26.54/7.33 , 0^#() -> c_21() 26.54/7.33 , plus^#(X1, X2) -> c_19() 26.54/7.33 , s^#(X) -> c_18() 26.54/7.33 , x^#(X1, X2) -> c_24() 26.54/7.33 , U32^#(tt()) -> c_14() 26.54/7.33 , U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.33 , U51^#(tt(), M, N) -> 26.54/7.33 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.33 isNat^#(activate(N)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M), 26.54/7.33 activate^#(N)) 26.54/7.33 , U52^#(tt(), M, N) -> 26.54/7.33 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.33 plus^#(activate(N), activate(M)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M)) 26.54/7.33 , U61^#(tt()) -> c_20(0^#()) 26.54/7.33 , U71^#(tt(), M, N) -> 26.54/7.33 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.33 isNat^#(activate(N)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M), 26.54/7.33 activate^#(N)) 26.54/7.33 , U72^#(tt(), M, N) -> 26.54/7.33 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.33 x^#(activate(N), activate(M)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M), 26.54/7.33 activate^#(N)) } 26.54/7.33 26.54/7.33 and mark the set of starting terms. 26.54/7.33 26.54/7.33 We are left with following problem, upon which TcT provides the 26.54/7.33 certificate YES(O(1),O(n^1)). 26.54/7.33 26.54/7.33 Strict DPs: 26.54/7.33 { U11^#(tt(), V2) -> 26.54/7.33 c_1(U12^#(isNat(activate(V2))), 26.54/7.33 isNat^#(activate(V2)), 26.54/7.33 activate^#(V2)) 26.54/7.33 , U12^#(tt()) -> c_2() 26.54/7.33 , isNat^#(n__0()) -> c_3() 26.54/7.33 , isNat^#(n__plus(V1, V2)) -> 26.54/7.33 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.33 isNat^#(activate(V1)), 26.54/7.33 activate^#(V1), 26.54/7.33 activate^#(V2)) 26.54/7.33 , isNat^#(n__s(V1)) -> 26.54/7.33 c_5(U21^#(isNat(activate(V1))), 26.54/7.33 isNat^#(activate(V1)), 26.54/7.33 activate^#(V1)) 26.54/7.33 , isNat^#(n__x(V1, V2)) -> 26.54/7.33 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.33 isNat^#(activate(V1)), 26.54/7.33 activate^#(V1), 26.54/7.33 activate^#(V2)) 26.54/7.33 , activate^#(X) -> c_7() 26.54/7.33 , activate^#(n__0()) -> c_8(0^#()) 26.54/7.33 , activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.33 , activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.33 , activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.33 , U21^#(tt()) -> c_12() 26.54/7.33 , U31^#(tt(), V2) -> 26.54/7.33 c_13(U32^#(isNat(activate(V2))), 26.54/7.33 isNat^#(activate(V2)), 26.54/7.33 activate^#(V2)) 26.54/7.33 , 0^#() -> c_21() 26.54/7.33 , plus^#(X1, X2) -> c_19() 26.54/7.33 , s^#(X) -> c_18() 26.54/7.33 , x^#(X1, X2) -> c_24() 26.54/7.33 , U32^#(tt()) -> c_14() 26.54/7.33 , U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.33 , U51^#(tt(), M, N) -> 26.54/7.33 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.33 isNat^#(activate(N)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M), 26.54/7.33 activate^#(N)) 26.54/7.33 , U52^#(tt(), M, N) -> 26.54/7.33 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.33 plus^#(activate(N), activate(M)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M)) 26.54/7.33 , U61^#(tt()) -> c_20(0^#()) 26.54/7.33 , U71^#(tt(), M, N) -> 26.54/7.33 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.33 isNat^#(activate(N)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M), 26.54/7.33 activate^#(N)) 26.54/7.33 , U72^#(tt(), M, N) -> 26.54/7.33 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.33 x^#(activate(N), activate(M)), 26.54/7.33 activate^#(N), 26.54/7.33 activate^#(M), 26.54/7.33 activate^#(N)) } 26.54/7.33 Weak Trs: 26.54/7.33 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.33 , U12(tt()) -> tt() 26.54/7.33 , isNat(n__0()) -> tt() 26.54/7.33 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.33 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.33 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.33 , activate(X) -> X 26.54/7.33 , activate(n__0()) -> 0() 26.54/7.33 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.33 , activate(n__s(X)) -> s(X) 26.54/7.33 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.33 , U21(tt()) -> tt() 26.54/7.33 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.33 , U32(tt()) -> tt() 26.54/7.33 , U41(tt(), N) -> activate(N) 26.54/7.33 , U51(tt(), M, N) -> 26.54/7.33 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.33 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.33 , s(X) -> n__s(X) 26.54/7.33 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.33 , U61(tt()) -> 0() 26.54/7.33 , 0() -> n__0() 26.54/7.33 , U71(tt(), M, N) -> 26.54/7.33 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.33 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.33 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.33 Obligation: 26.54/7.33 innermost runtime complexity 26.54/7.33 Answer: 26.54/7.33 YES(O(1),O(n^1)) 26.54/7.33 26.54/7.33 We estimate the number of application of {2,3,7,12,14,15,16,17,18} 26.54/7.33 by applications of Pre({2,3,7,12,14,15,16,17,18}) = 26.54/7.33 {1,4,5,6,8,9,10,11,13,19,20,21,22,23,24}. Here rules are labeled as 26.54/7.33 follows: 26.54/7.33 26.54/7.33 DPs: 26.54/7.33 { 1: U11^#(tt(), V2) -> 26.54/7.33 c_1(U12^#(isNat(activate(V2))), 26.54/7.33 isNat^#(activate(V2)), 26.54/7.33 activate^#(V2)) 26.54/7.33 , 2: U12^#(tt()) -> c_2() 26.54/7.34 , 3: isNat^#(n__0()) -> c_3() 26.54/7.34 , 4: isNat^#(n__plus(V1, V2)) -> 26.54/7.34 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 5: isNat^#(n__s(V1)) -> 26.54/7.34 c_5(U21^#(isNat(activate(V1))), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1)) 26.54/7.34 , 6: isNat^#(n__x(V1, V2)) -> 26.54/7.34 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 7: activate^#(X) -> c_7() 26.54/7.34 , 8: activate^#(n__0()) -> c_8(0^#()) 26.54/7.34 , 9: activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.34 , 10: activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.34 , 11: activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.34 , 12: U21^#(tt()) -> c_12() 26.54/7.34 , 13: U31^#(tt(), V2) -> 26.54/7.34 c_13(U32^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 14: 0^#() -> c_21() 26.54/7.34 , 15: plus^#(X1, X2) -> c_19() 26.54/7.34 , 16: s^#(X) -> c_18() 26.54/7.34 , 17: x^#(X1, X2) -> c_24() 26.54/7.34 , 18: U32^#(tt()) -> c_14() 26.54/7.34 , 19: U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.34 , 20: U51^#(tt(), M, N) -> 26.54/7.34 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 21: U52^#(tt(), M, N) -> 26.54/7.34 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.34 plus^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M)) 26.54/7.34 , 22: U61^#(tt()) -> c_20(0^#()) 26.54/7.34 , 23: U71^#(tt(), M, N) -> 26.54/7.34 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 24: U72^#(tt(), M, N) -> 26.54/7.34 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.34 x^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) } 26.54/7.34 26.54/7.34 We are left with following problem, upon which TcT provides the 26.54/7.34 certificate YES(O(1),O(n^1)). 26.54/7.34 26.54/7.34 Strict DPs: 26.54/7.34 { U11^#(tt(), V2) -> 26.54/7.34 c_1(U12^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , isNat^#(n__plus(V1, V2)) -> 26.54/7.34 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , isNat^#(n__s(V1)) -> 26.54/7.34 c_5(U21^#(isNat(activate(V1))), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1)) 26.54/7.34 , isNat^#(n__x(V1, V2)) -> 26.54/7.34 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , activate^#(n__0()) -> c_8(0^#()) 26.54/7.34 , activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.34 , activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.34 , activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.34 , U31^#(tt(), V2) -> 26.54/7.34 c_13(U32^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.34 , U51^#(tt(), M, N) -> 26.54/7.34 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , U52^#(tt(), M, N) -> 26.54/7.34 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.34 plus^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M)) 26.54/7.34 , U61^#(tt()) -> c_20(0^#()) 26.54/7.34 , U71^#(tt(), M, N) -> 26.54/7.34 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , U72^#(tt(), M, N) -> 26.54/7.34 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.34 x^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) } 26.54/7.34 Weak DPs: 26.54/7.34 { U12^#(tt()) -> c_2() 26.54/7.34 , isNat^#(n__0()) -> c_3() 26.54/7.34 , activate^#(X) -> c_7() 26.54/7.34 , U21^#(tt()) -> c_12() 26.54/7.34 , 0^#() -> c_21() 26.54/7.34 , plus^#(X1, X2) -> c_19() 26.54/7.34 , s^#(X) -> c_18() 26.54/7.34 , x^#(X1, X2) -> c_24() 26.54/7.34 , U32^#(tt()) -> c_14() } 26.54/7.34 Weak Trs: 26.54/7.34 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.34 , U12(tt()) -> tt() 26.54/7.34 , isNat(n__0()) -> tt() 26.54/7.34 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.34 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.34 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.34 , activate(X) -> X 26.54/7.34 , activate(n__0()) -> 0() 26.54/7.34 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.34 , activate(n__s(X)) -> s(X) 26.54/7.34 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.34 , U21(tt()) -> tt() 26.54/7.34 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.34 , U32(tt()) -> tt() 26.54/7.34 , U41(tt(), N) -> activate(N) 26.54/7.34 , U51(tt(), M, N) -> 26.54/7.34 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.34 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.34 , s(X) -> n__s(X) 26.54/7.34 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.34 , U61(tt()) -> 0() 26.54/7.34 , 0() -> n__0() 26.54/7.34 , U71(tt(), M, N) -> 26.54/7.34 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.34 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.34 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.34 Obligation: 26.54/7.34 innermost runtime complexity 26.54/7.34 Answer: 26.54/7.34 YES(O(1),O(n^1)) 26.54/7.34 26.54/7.34 We estimate the number of application of {5,6,7,8,13} by 26.54/7.34 applications of Pre({5,6,7,8,13}) = {1,2,3,4,9,10,11,12,14,15}. 26.54/7.34 Here rules are labeled as follows: 26.54/7.34 26.54/7.34 DPs: 26.54/7.34 { 1: U11^#(tt(), V2) -> 26.54/7.34 c_1(U12^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 2: isNat^#(n__plus(V1, V2)) -> 26.54/7.34 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 3: isNat^#(n__s(V1)) -> 26.54/7.34 c_5(U21^#(isNat(activate(V1))), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1)) 26.54/7.34 , 4: isNat^#(n__x(V1, V2)) -> 26.54/7.34 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 5: activate^#(n__0()) -> c_8(0^#()) 26.54/7.34 , 6: activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.34 , 7: activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.34 , 8: activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.34 , 9: U31^#(tt(), V2) -> 26.54/7.34 c_13(U32^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 10: U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.34 , 11: U51^#(tt(), M, N) -> 26.54/7.34 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 12: U52^#(tt(), M, N) -> 26.54/7.34 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.34 plus^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M)) 26.54/7.34 , 13: U61^#(tt()) -> c_20(0^#()) 26.54/7.34 , 14: U71^#(tt(), M, N) -> 26.54/7.34 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 15: U72^#(tt(), M, N) -> 26.54/7.34 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.34 x^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 16: U12^#(tt()) -> c_2() 26.54/7.34 , 17: isNat^#(n__0()) -> c_3() 26.54/7.34 , 18: activate^#(X) -> c_7() 26.54/7.34 , 19: U21^#(tt()) -> c_12() 26.54/7.34 , 20: 0^#() -> c_21() 26.54/7.34 , 21: plus^#(X1, X2) -> c_19() 26.54/7.34 , 22: s^#(X) -> c_18() 26.54/7.34 , 23: x^#(X1, X2) -> c_24() 26.54/7.34 , 24: U32^#(tt()) -> c_14() } 26.54/7.34 26.54/7.34 We are left with following problem, upon which TcT provides the 26.54/7.34 certificate YES(O(1),O(n^1)). 26.54/7.34 26.54/7.34 Strict DPs: 26.54/7.34 { U11^#(tt(), V2) -> 26.54/7.34 c_1(U12^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , isNat^#(n__plus(V1, V2)) -> 26.54/7.34 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , isNat^#(n__s(V1)) -> 26.54/7.34 c_5(U21^#(isNat(activate(V1))), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1)) 26.54/7.34 , isNat^#(n__x(V1, V2)) -> 26.54/7.34 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , U31^#(tt(), V2) -> 26.54/7.34 c_13(U32^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.34 , U51^#(tt(), M, N) -> 26.54/7.34 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , U52^#(tt(), M, N) -> 26.54/7.34 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.34 plus^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M)) 26.54/7.34 , U71^#(tt(), M, N) -> 26.54/7.34 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , U72^#(tt(), M, N) -> 26.54/7.34 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.34 x^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) } 26.54/7.34 Weak DPs: 26.54/7.34 { U12^#(tt()) -> c_2() 26.54/7.34 , isNat^#(n__0()) -> c_3() 26.54/7.34 , activate^#(X) -> c_7() 26.54/7.34 , activate^#(n__0()) -> c_8(0^#()) 26.54/7.34 , activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.34 , activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.34 , activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.34 , U21^#(tt()) -> c_12() 26.54/7.34 , 0^#() -> c_21() 26.54/7.34 , plus^#(X1, X2) -> c_19() 26.54/7.34 , s^#(X) -> c_18() 26.54/7.34 , x^#(X1, X2) -> c_24() 26.54/7.34 , U32^#(tt()) -> c_14() 26.54/7.34 , U61^#(tt()) -> c_20(0^#()) } 26.54/7.34 Weak Trs: 26.54/7.34 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.34 , U12(tt()) -> tt() 26.54/7.34 , isNat(n__0()) -> tt() 26.54/7.34 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.34 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.34 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.34 , activate(X) -> X 26.54/7.34 , activate(n__0()) -> 0() 26.54/7.34 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.34 , activate(n__s(X)) -> s(X) 26.54/7.34 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.34 , U21(tt()) -> tt() 26.54/7.34 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.34 , U32(tt()) -> tt() 26.54/7.34 , U41(tt(), N) -> activate(N) 26.54/7.34 , U51(tt(), M, N) -> 26.54/7.34 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.34 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.34 , s(X) -> n__s(X) 26.54/7.34 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.34 , U61(tt()) -> 0() 26.54/7.34 , 0() -> n__0() 26.54/7.34 , U71(tt(), M, N) -> 26.54/7.34 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.34 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.34 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.34 Obligation: 26.54/7.34 innermost runtime complexity 26.54/7.34 Answer: 26.54/7.34 YES(O(1),O(n^1)) 26.54/7.34 26.54/7.34 We estimate the number of application of {6,8,10} by applications 26.54/7.34 of Pre({6,8,10}) = {7,9}. Here rules are labeled as follows: 26.54/7.34 26.54/7.34 DPs: 26.54/7.34 { 1: U11^#(tt(), V2) -> 26.54/7.34 c_1(U12^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 2: isNat^#(n__plus(V1, V2)) -> 26.54/7.34 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 3: isNat^#(n__s(V1)) -> 26.54/7.34 c_5(U21^#(isNat(activate(V1))), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1)) 26.54/7.34 , 4: isNat^#(n__x(V1, V2)) -> 26.54/7.34 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 5: U31^#(tt(), V2) -> 26.54/7.34 c_13(U32^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , 6: U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.34 , 7: U51^#(tt(), M, N) -> 26.54/7.34 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 8: U52^#(tt(), M, N) -> 26.54/7.34 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.34 plus^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M)) 26.54/7.34 , 9: U71^#(tt(), M, N) -> 26.54/7.34 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 10: U72^#(tt(), M, N) -> 26.54/7.34 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.34 x^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , 11: U12^#(tt()) -> c_2() 26.54/7.34 , 12: isNat^#(n__0()) -> c_3() 26.54/7.34 , 13: activate^#(X) -> c_7() 26.54/7.34 , 14: activate^#(n__0()) -> c_8(0^#()) 26.54/7.34 , 15: activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.34 , 16: activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.34 , 17: activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.34 , 18: U21^#(tt()) -> c_12() 26.54/7.34 , 19: 0^#() -> c_21() 26.54/7.34 , 20: plus^#(X1, X2) -> c_19() 26.54/7.34 , 21: s^#(X) -> c_18() 26.54/7.34 , 22: x^#(X1, X2) -> c_24() 26.54/7.34 , 23: U32^#(tt()) -> c_14() 26.54/7.34 , 24: U61^#(tt()) -> c_20(0^#()) } 26.54/7.34 26.54/7.34 We are left with following problem, upon which TcT provides the 26.54/7.34 certificate YES(O(1),O(n^1)). 26.54/7.34 26.54/7.34 Strict DPs: 26.54/7.34 { U11^#(tt(), V2) -> 26.54/7.34 c_1(U12^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , isNat^#(n__plus(V1, V2)) -> 26.54/7.34 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , isNat^#(n__s(V1)) -> 26.54/7.34 c_5(U21^#(isNat(activate(V1))), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1)) 26.54/7.34 , isNat^#(n__x(V1, V2)) -> 26.54/7.34 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.34 isNat^#(activate(V1)), 26.54/7.34 activate^#(V1), 26.54/7.34 activate^#(V2)) 26.54/7.34 , U31^#(tt(), V2) -> 26.54/7.34 c_13(U32^#(isNat(activate(V2))), 26.54/7.34 isNat^#(activate(V2)), 26.54/7.34 activate^#(V2)) 26.54/7.34 , U51^#(tt(), M, N) -> 26.54/7.34 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) 26.54/7.34 , U71^#(tt(), M, N) -> 26.54/7.34 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.34 isNat^#(activate(N)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) } 26.54/7.34 Weak DPs: 26.54/7.34 { U12^#(tt()) -> c_2() 26.54/7.34 , isNat^#(n__0()) -> c_3() 26.54/7.34 , activate^#(X) -> c_7() 26.54/7.34 , activate^#(n__0()) -> c_8(0^#()) 26.54/7.34 , activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.34 , activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.34 , activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.34 , U21^#(tt()) -> c_12() 26.54/7.34 , 0^#() -> c_21() 26.54/7.34 , plus^#(X1, X2) -> c_19() 26.54/7.34 , s^#(X) -> c_18() 26.54/7.34 , x^#(X1, X2) -> c_24() 26.54/7.34 , U32^#(tt()) -> c_14() 26.54/7.34 , U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.34 , U52^#(tt(), M, N) -> 26.54/7.34 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.34 plus^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M)) 26.54/7.34 , U61^#(tt()) -> c_20(0^#()) 26.54/7.34 , U72^#(tt(), M, N) -> 26.54/7.34 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.34 x^#(activate(N), activate(M)), 26.54/7.34 activate^#(N), 26.54/7.34 activate^#(M), 26.54/7.34 activate^#(N)) } 26.54/7.34 Weak Trs: 26.54/7.34 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.34 , U12(tt()) -> tt() 26.54/7.34 , isNat(n__0()) -> tt() 26.54/7.34 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.34 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.34 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.34 , activate(X) -> X 26.54/7.34 , activate(n__0()) -> 0() 26.54/7.34 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.34 , activate(n__s(X)) -> s(X) 26.54/7.34 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.34 , U21(tt()) -> tt() 26.54/7.34 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.34 , U32(tt()) -> tt() 26.54/7.34 , U41(tt(), N) -> activate(N) 26.54/7.34 , U51(tt(), M, N) -> 26.54/7.34 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.34 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.34 , s(X) -> n__s(X) 26.54/7.34 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.34 , U61(tt()) -> 0() 26.54/7.34 , 0() -> n__0() 26.54/7.34 , U71(tt(), M, N) -> 26.54/7.34 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.34 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.34 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.34 Obligation: 26.54/7.34 innermost runtime complexity 26.54/7.34 Answer: 26.54/7.34 YES(O(1),O(n^1)) 26.54/7.34 26.54/7.34 The following weak DPs constitute a sub-graph of the DG that is 26.54/7.34 closed under successors. The DPs are removed. 26.54/7.34 26.54/7.34 { U12^#(tt()) -> c_2() 26.54/7.34 , isNat^#(n__0()) -> c_3() 26.54/7.34 , activate^#(X) -> c_7() 26.54/7.34 , activate^#(n__0()) -> c_8(0^#()) 26.54/7.35 , activate^#(n__plus(X1, X2)) -> c_9(plus^#(X1, X2)) 26.54/7.35 , activate^#(n__s(X)) -> c_10(s^#(X)) 26.54/7.35 , activate^#(n__x(X1, X2)) -> c_11(x^#(X1, X2)) 26.54/7.35 , U21^#(tt()) -> c_12() 26.54/7.35 , 0^#() -> c_21() 26.54/7.35 , plus^#(X1, X2) -> c_19() 26.54/7.35 , s^#(X) -> c_18() 26.54/7.35 , x^#(X1, X2) -> c_24() 26.54/7.35 , U32^#(tt()) -> c_14() 26.54/7.35 , U41^#(tt(), N) -> c_15(activate^#(N)) 26.54/7.35 , U52^#(tt(), M, N) -> 26.54/7.35 c_17(s^#(plus(activate(N), activate(M))), 26.54/7.35 plus^#(activate(N), activate(M)), 26.54/7.35 activate^#(N), 26.54/7.35 activate^#(M)) 26.54/7.35 , U61^#(tt()) -> c_20(0^#()) 26.54/7.35 , U72^#(tt(), M, N) -> 26.54/7.35 c_23(plus^#(x(activate(N), activate(M)), activate(N)), 26.54/7.35 x^#(activate(N), activate(M)), 26.54/7.35 activate^#(N), 26.54/7.35 activate^#(M), 26.54/7.35 activate^#(N)) } 26.54/7.35 26.54/7.35 We are left with following problem, upon which TcT provides the 26.54/7.35 certificate YES(O(1),O(n^1)). 26.54/7.35 26.54/7.35 Strict DPs: 26.54/7.35 { U11^#(tt(), V2) -> 26.54/7.35 c_1(U12^#(isNat(activate(V2))), 26.54/7.35 isNat^#(activate(V2)), 26.54/7.35 activate^#(V2)) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1)), 26.54/7.35 activate^#(V1), 26.54/7.35 activate^#(V2)) 26.54/7.35 , isNat^#(n__s(V1)) -> 26.54/7.35 c_5(U21^#(isNat(activate(V1))), 26.54/7.35 isNat^#(activate(V1)), 26.54/7.35 activate^#(V1)) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1)), 26.54/7.35 activate^#(V1), 26.54/7.35 activate^#(V2)) 26.54/7.35 , U31^#(tt(), V2) -> 26.54/7.35 c_13(U32^#(isNat(activate(V2))), 26.54/7.35 isNat^#(activate(V2)), 26.54/7.35 activate^#(V2)) 26.54/7.35 , U51^#(tt(), M, N) -> 26.54/7.35 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.35 isNat^#(activate(N)), 26.54/7.35 activate^#(N), 26.54/7.35 activate^#(M), 26.54/7.35 activate^#(N)) 26.54/7.35 , U71^#(tt(), M, N) -> 26.54/7.35 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.35 isNat^#(activate(N)), 26.54/7.35 activate^#(N), 26.54/7.35 activate^#(M), 26.54/7.35 activate^#(N)) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , U41(tt(), N) -> activate(N) 26.54/7.35 , U51(tt(), M, N) -> 26.54/7.35 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.35 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , U61(tt()) -> 0() 26.54/7.35 , 0() -> n__0() 26.54/7.35 , U71(tt(), M, N) -> 26.54/7.35 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.35 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 Obligation: 26.54/7.35 innermost runtime complexity 26.54/7.35 Answer: 26.54/7.35 YES(O(1),O(n^1)) 26.54/7.35 26.54/7.35 Due to missing edges in the dependency-graph, the right-hand sides 26.54/7.35 of following rules could be simplified: 26.54/7.35 26.54/7.35 { U11^#(tt(), V2) -> 26.54/7.35 c_1(U12^#(isNat(activate(V2))), 26.54/7.35 isNat^#(activate(V2)), 26.54/7.35 activate^#(V2)) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_4(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1)), 26.54/7.35 activate^#(V1), 26.54/7.35 activate^#(V2)) 26.54/7.35 , isNat^#(n__s(V1)) -> 26.54/7.35 c_5(U21^#(isNat(activate(V1))), 26.54/7.35 isNat^#(activate(V1)), 26.54/7.35 activate^#(V1)) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_6(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1)), 26.54/7.35 activate^#(V1), 26.54/7.35 activate^#(V2)) 26.54/7.35 , U31^#(tt(), V2) -> 26.54/7.35 c_13(U32^#(isNat(activate(V2))), 26.54/7.35 isNat^#(activate(V2)), 26.54/7.35 activate^#(V2)) 26.54/7.35 , U51^#(tt(), M, N) -> 26.54/7.35 c_16(U52^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.35 isNat^#(activate(N)), 26.54/7.35 activate^#(N), 26.54/7.35 activate^#(M), 26.54/7.35 activate^#(N)) 26.54/7.35 , U71^#(tt(), M, N) -> 26.54/7.35 c_22(U72^#(isNat(activate(N)), activate(M), activate(N)), 26.54/7.35 isNat^#(activate(N)), 26.54/7.35 activate^#(N), 26.54/7.35 activate^#(M), 26.54/7.35 activate^#(N)) } 26.54/7.35 26.54/7.35 We are left with following problem, upon which TcT provides the 26.54/7.35 certificate YES(O(1),O(n^1)). 26.54/7.35 26.54/7.35 Strict DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.35 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , U41(tt(), N) -> activate(N) 26.54/7.35 , U51(tt(), M, N) -> 26.54/7.35 U52(isNat(activate(N)), activate(M), activate(N)) 26.54/7.35 , U52(tt(), M, N) -> s(plus(activate(N), activate(M))) 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , U61(tt()) -> 0() 26.54/7.35 , 0() -> n__0() 26.54/7.35 , U71(tt(), M, N) -> 26.54/7.35 U72(isNat(activate(N)), activate(M), activate(N)) 26.54/7.35 , U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 Obligation: 26.54/7.35 innermost runtime complexity 26.54/7.35 Answer: 26.54/7.35 YES(O(1),O(n^1)) 26.54/7.35 26.54/7.35 We replace rewrite rules by usable rules: 26.54/7.35 26.54/7.35 Weak Usable Rules: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 26.54/7.35 We are left with following problem, upon which TcT provides the 26.54/7.35 certificate YES(O(1),O(n^1)). 26.54/7.35 26.54/7.35 Strict DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.35 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 Obligation: 26.54/7.35 innermost runtime complexity 26.54/7.35 Answer: 26.54/7.35 YES(O(1),O(n^1)) 26.54/7.35 26.54/7.35 We analyse the complexity of following sub-problems (R) and (S). 26.54/7.35 Problem (S) is obtained from the input problem by shifting strict 26.54/7.35 rules from (R) into the weak component: 26.54/7.35 26.54/7.35 Problem (R): 26.54/7.35 ------------ 26.54/7.35 Strict DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.35 Weak DPs: { U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 StartTerms: basic terms 26.54/7.35 Strategy: innermost 26.54/7.35 26.54/7.35 Problem (S): 26.54/7.35 ------------ 26.54/7.35 Strict DPs: { U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 StartTerms: basic terms 26.54/7.35 Strategy: innermost 26.54/7.35 26.54/7.35 Overall, the transformation results in the following sub-problem(s): 26.54/7.35 26.54/7.35 Generated new problems: 26.54/7.35 ----------------------- 26.54/7.35 R) Strict DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.35 Weak DPs: { U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 StartTerms: basic terms 26.54/7.35 Strategy: innermost 26.54/7.35 26.54/7.35 This problem was proven YES(O(1),O(n^1)). 26.54/7.35 26.54/7.35 S) Strict DPs: { U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 StartTerms: basic terms 26.54/7.35 Strategy: innermost 26.54/7.35 26.54/7.35 This problem was proven YES(O(1),O(1)). 26.54/7.35 26.54/7.35 26.54/7.35 Proofs for generated problems: 26.54/7.35 ------------------------------ 26.54/7.35 R) We are left with following problem, upon which TcT provides the 26.54/7.35 certificate YES(O(1),O(n^1)). 26.54/7.35 26.54/7.35 Strict DPs: 26.54/7.35 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.35 , isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , isNat^#(n__x(V1, V2)) -> 26.54/7.35 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.35 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.35 Weak DPs: { U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 Weak Trs: 26.54/7.35 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.35 , U12(tt()) -> tt() 26.54/7.35 , isNat(n__0()) -> tt() 26.54/7.35 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.35 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.35 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.35 , activate(X) -> X 26.54/7.35 , activate(n__0()) -> 0() 26.54/7.35 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.35 , activate(n__s(X)) -> s(X) 26.54/7.35 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.35 , U21(tt()) -> tt() 26.54/7.35 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.35 , U32(tt()) -> tt() 26.54/7.35 , s(X) -> n__s(X) 26.54/7.35 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.35 , 0() -> n__0() 26.54/7.35 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.35 Obligation: 26.54/7.35 innermost runtime complexity 26.54/7.35 Answer: 26.54/7.35 YES(O(1),O(n^1)) 26.54/7.35 26.54/7.35 We use the processor 'matrix interpretation of dimension 1' to 26.54/7.35 orient following rules strictly. 26.54/7.35 26.54/7.35 DPs: 26.54/7.35 { 2: isNat^#(n__plus(V1, V2)) -> 26.54/7.35 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.35 isNat^#(activate(V1))) 26.54/7.35 , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.35 , 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.35 , 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.35 26.54/7.35 Sub-proof: 26.54/7.35 ---------- 26.54/7.35 The following argument positions are usable: 26.54/7.35 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 26.54/7.35 Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 26.54/7.35 Uargs(c_7) = {1} 26.54/7.35 26.54/7.35 TcT has computed the following constructor-based matrix 26.54/7.35 interpretation satisfying not(EDA). 26.54/7.35 26.54/7.35 [U11](x1, x2) = [0] 26.54/7.35 26.54/7.35 [tt] = [0] 26.54/7.35 26.54/7.35 [U12](x1) = [0] 26.54/7.35 26.54/7.35 [isNat](x1) = [0] 26.54/7.35 26.54/7.35 [activate](x1) = [1] x1 + [0] 26.54/7.35 26.54/7.35 [U21](x1) = [0] 26.54/7.35 26.54/7.35 [U31](x1, x2) = [0] 26.54/7.35 26.54/7.35 [U32](x1) = [0] 26.54/7.35 26.54/7.35 [s](x1) = [1] x1 + [1] 26.54/7.35 26.54/7.35 [plus](x1, x2) = [1] x1 + [1] x2 + [1] 26.54/7.35 26.54/7.35 [0] = [0] 26.54/7.35 26.54/7.35 [x](x1, x2) = [1] x1 + [1] x2 + [0] 26.54/7.35 26.54/7.35 [n__0] = [0] 26.54/7.35 26.54/7.35 [n__plus](x1, x2) = [1] x1 + [1] x2 + [1] 26.54/7.35 26.54/7.35 [n__s](x1) = [1] x1 + [1] 26.54/7.35 26.54/7.35 [n__x](x1, x2) = [1] x1 + [1] x2 + [0] 26.54/7.35 26.54/7.35 [U11^#](x1, x2) = [4] x2 + [0] 26.54/7.35 26.54/7.35 [isNat^#](x1) = [4] x1 + [0] 26.54/7.35 26.54/7.35 [U31^#](x1, x2) = [4] x2 + [0] 26.54/7.35 26.54/7.35 [U51^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 26.54/7.35 26.54/7.35 [U71^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 26.54/7.35 26.54/7.35 [c_1](x1) = [1] x1 + [0] 26.54/7.35 26.54/7.35 [c_2](x1, x2) = [1] x1 + [1] x2 + [3] 26.54/7.35 26.54/7.35 [c_3](x1) = [1] x1 + [1] 26.54/7.35 26.54/7.35 [c_4](x1, x2) = [1] x1 + [1] x2 + [0] 26.54/7.35 26.54/7.35 [c_5](x1) = [1] x1 + [0] 26.54/7.35 26.54/7.35 [c_6](x1) = [1] x1 + [3] 26.54/7.35 26.54/7.35 [c_7](x1) = [1] x1 + [3] 26.54/7.35 26.54/7.35 The order satisfies the following ordering constraints: 26.54/7.35 26.54/7.35 [U11(tt(), V2)] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [U12(isNat(activate(V2)))] 26.54/7.35 26.54/7.35 [U12(tt())] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [tt()] 26.54/7.35 26.54/7.35 [isNat(n__0())] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [tt()] 26.54/7.35 26.54/7.35 [isNat(n__plus(V1, V2))] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [U11(isNat(activate(V1)), activate(V2))] 26.54/7.35 26.54/7.35 [isNat(n__s(V1))] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [U21(isNat(activate(V1)))] 26.54/7.35 26.54/7.35 [isNat(n__x(V1, V2))] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [U31(isNat(activate(V1)), activate(V2))] 26.54/7.35 26.54/7.35 [activate(X)] = [1] X + [0] 26.54/7.35 >= [1] X + [0] 26.54/7.35 = [X] 26.54/7.35 26.54/7.35 [activate(n__0())] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [0()] 26.54/7.35 26.54/7.35 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [1] 26.54/7.35 >= [1] X1 + [1] X2 + [1] 26.54/7.35 = [plus(X1, X2)] 26.54/7.35 26.54/7.35 [activate(n__s(X))] = [1] X + [1] 26.54/7.35 >= [1] X + [1] 26.54/7.35 = [s(X)] 26.54/7.35 26.54/7.35 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0] 26.54/7.35 >= [1] X1 + [1] X2 + [0] 26.54/7.35 = [x(X1, X2)] 26.54/7.35 26.54/7.35 [U21(tt())] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [tt()] 26.54/7.35 26.54/7.35 [U31(tt(), V2)] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [U32(isNat(activate(V2)))] 26.54/7.35 26.54/7.35 [U32(tt())] = [0] 26.54/7.35 >= [0] 26.54/7.35 = [tt()] 26.54/7.35 26.54/7.35 [s(X)] = [1] X + [1] 26.54/7.35 >= [1] X + [1] 26.54/7.35 = [n__s(X)] 26.54/7.35 26.54/7.35 [plus(X1, X2)] = [1] X1 + [1] X2 + [1] 26.54/7.35 >= [1] X1 + [1] X2 + [1] 26.54/7.35 = [n__plus(X1, X2)] 26.54/7.36 26.54/7.36 [0()] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [n__0()] 26.54/7.36 26.54/7.36 [x(X1, X2)] = [1] X1 + [1] X2 + [0] 26.54/7.36 >= [1] X1 + [1] X2 + [0] 26.54/7.36 = [n__x(X1, X2)] 26.54/7.36 26.54/7.36 [U11^#(tt(), V2)] = [4] V2 + [0] 26.54/7.36 >= [4] V2 + [0] 26.54/7.36 = [c_1(isNat^#(activate(V2)))] 26.54/7.36 26.54/7.36 [isNat^#(n__plus(V1, V2))] = [4] V2 + [4] V1 + [4] 26.54/7.36 > [4] V2 + [4] V1 + [3] 26.54/7.36 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1)))] 26.54/7.36 26.54/7.36 [isNat^#(n__s(V1))] = [4] V1 + [4] 26.54/7.36 > [4] V1 + [1] 26.54/7.36 = [c_3(isNat^#(activate(V1)))] 26.54/7.36 26.54/7.36 [isNat^#(n__x(V1, V2))] = [4] V2 + [4] V1 + [0] 26.54/7.36 >= [4] V2 + [4] V1 + [0] 26.54/7.36 = [c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1)))] 26.54/7.36 26.54/7.36 [U31^#(tt(), V2)] = [4] V2 + [0] 26.54/7.36 >= [4] V2 + [0] 26.54/7.36 = [c_5(isNat^#(activate(V2)))] 26.54/7.36 26.54/7.36 [U51^#(tt(), M, N)] = [7] N + [7] M + [7] 26.54/7.36 > [4] N + [3] 26.54/7.36 = [c_6(isNat^#(activate(N)))] 26.54/7.36 26.54/7.36 [U71^#(tt(), M, N)] = [7] N + [7] M + [7] 26.54/7.36 > [4] N + [3] 26.54/7.36 = [c_7(isNat^#(activate(N)))] 26.54/7.36 26.54/7.36 26.54/7.36 We return to the main proof. Consider the set of all dependency 26.54/7.36 pairs 26.54/7.36 26.54/7.36 : 26.54/7.36 { 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , 2: isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , 4: isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 5: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 26.54/7.36 Processor 'matrix interpretation of dimension 1' induces the 26.54/7.36 complexity certificate YES(?,O(n^1)) on application of dependency 26.54/7.36 pairs {2,3,6,7}. These cover all (indirect) predecessors of 26.54/7.36 dependency pairs {1,2,3,6,7}, their number of application is 26.54/7.36 equally bounded. The dependency pairs are shifted into the weak 26.54/7.36 component. 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(n^1)). 26.54/7.36 26.54/7.36 Strict DPs: 26.54/7.36 { isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) } 26.54/7.36 Weak DPs: 26.54/7.36 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 Weak Trs: 26.54/7.36 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.36 , U12(tt()) -> tt() 26.54/7.36 , isNat(n__0()) -> tt() 26.54/7.36 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.36 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.36 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.36 , activate(X) -> X 26.54/7.36 , activate(n__0()) -> 0() 26.54/7.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.36 , activate(n__s(X)) -> s(X) 26.54/7.36 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.36 , U21(tt()) -> tt() 26.54/7.36 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.36 , U32(tt()) -> tt() 26.54/7.36 , s(X) -> n__s(X) 26.54/7.36 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.36 , 0() -> n__0() 26.54/7.36 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(n^1)) 26.54/7.36 26.54/7.36 We use the processor 'matrix interpretation of dimension 1' to 26.54/7.36 orient following rules strictly. 26.54/7.36 26.54/7.36 DPs: 26.54/7.36 { 1: isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 26.54/7.36 Sub-proof: 26.54/7.36 ---------- 26.54/7.36 The following argument positions are usable: 26.54/7.36 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 26.54/7.36 Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 26.54/7.36 Uargs(c_7) = {1} 26.54/7.36 26.54/7.36 TcT has computed the following constructor-based matrix 26.54/7.36 interpretation satisfying not(EDA). 26.54/7.36 26.54/7.36 [U11](x1, x2) = [0] 26.54/7.36 26.54/7.36 [tt] = [0] 26.54/7.36 26.54/7.36 [U12](x1) = [0] 26.54/7.36 26.54/7.36 [isNat](x1) = [0] 26.54/7.36 26.54/7.36 [activate](x1) = [1] x1 + [0] 26.54/7.36 26.54/7.36 [U21](x1) = [0] 26.54/7.36 26.54/7.36 [U31](x1, x2) = [0] 26.54/7.36 26.54/7.36 [U32](x1) = [0] 26.54/7.36 26.54/7.36 [s](x1) = [1] x1 + [0] 26.54/7.36 26.54/7.36 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 26.54/7.36 26.54/7.36 [0] = [0] 26.54/7.36 26.54/7.36 [x](x1, x2) = [1] x1 + [1] x2 + [1] 26.54/7.36 26.54/7.36 [n__0] = [0] 26.54/7.36 26.54/7.36 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 26.54/7.36 26.54/7.36 [n__s](x1) = [1] x1 + [0] 26.54/7.36 26.54/7.36 [n__x](x1, x2) = [1] x1 + [1] x2 + [1] 26.54/7.36 26.54/7.36 [U11^#](x1, x2) = [4] x2 + [0] 26.54/7.36 26.54/7.36 [isNat^#](x1) = [4] x1 + [0] 26.54/7.36 26.54/7.36 [U31^#](x1, x2) = [4] x2 + [0] 26.54/7.36 26.54/7.36 [U51^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 26.54/7.36 26.54/7.36 [U71^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 26.54/7.36 26.54/7.36 [c_1](x1) = [1] x1 + [0] 26.54/7.36 26.54/7.36 [c_2](x1, x2) = [1] x1 + [1] x2 + [0] 26.54/7.36 26.54/7.36 [c_3](x1) = [1] x1 + [0] 26.54/7.36 26.54/7.36 [c_4](x1, x2) = [1] x1 + [1] x2 + [1] 26.54/7.36 26.54/7.36 [c_5](x1) = [1] x1 + [0] 26.54/7.36 26.54/7.36 [c_6](x1) = [1] x1 + [3] 26.54/7.36 26.54/7.36 [c_7](x1) = [1] x1 + [3] 26.54/7.36 26.54/7.36 The order satisfies the following ordering constraints: 26.54/7.36 26.54/7.36 [U11(tt(), V2)] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [U12(isNat(activate(V2)))] 26.54/7.36 26.54/7.36 [U12(tt())] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [tt()] 26.54/7.36 26.54/7.36 [isNat(n__0())] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [tt()] 26.54/7.36 26.54/7.36 [isNat(n__plus(V1, V2))] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [U11(isNat(activate(V1)), activate(V2))] 26.54/7.36 26.54/7.36 [isNat(n__s(V1))] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [U21(isNat(activate(V1)))] 26.54/7.36 26.54/7.36 [isNat(n__x(V1, V2))] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [U31(isNat(activate(V1)), activate(V2))] 26.54/7.36 26.54/7.36 [activate(X)] = [1] X + [0] 26.54/7.36 >= [1] X + [0] 26.54/7.36 = [X] 26.54/7.36 26.54/7.36 [activate(n__0())] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [0()] 26.54/7.36 26.54/7.36 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 26.54/7.36 >= [1] X1 + [1] X2 + [0] 26.54/7.36 = [plus(X1, X2)] 26.54/7.36 26.54/7.36 [activate(n__s(X))] = [1] X + [0] 26.54/7.36 >= [1] X + [0] 26.54/7.36 = [s(X)] 26.54/7.36 26.54/7.36 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [1] 26.54/7.36 >= [1] X1 + [1] X2 + [1] 26.54/7.36 = [x(X1, X2)] 26.54/7.36 26.54/7.36 [U21(tt())] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [tt()] 26.54/7.36 26.54/7.36 [U31(tt(), V2)] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [U32(isNat(activate(V2)))] 26.54/7.36 26.54/7.36 [U32(tt())] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [tt()] 26.54/7.36 26.54/7.36 [s(X)] = [1] X + [0] 26.54/7.36 >= [1] X + [0] 26.54/7.36 = [n__s(X)] 26.54/7.36 26.54/7.36 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 26.54/7.36 >= [1] X1 + [1] X2 + [0] 26.54/7.36 = [n__plus(X1, X2)] 26.54/7.36 26.54/7.36 [0()] = [0] 26.54/7.36 >= [0] 26.54/7.36 = [n__0()] 26.54/7.36 26.54/7.36 [x(X1, X2)] = [1] X1 + [1] X2 + [1] 26.54/7.36 >= [1] X1 + [1] X2 + [1] 26.54/7.36 = [n__x(X1, X2)] 26.54/7.36 26.54/7.36 [U11^#(tt(), V2)] = [4] V2 + [0] 26.54/7.36 >= [4] V2 + [0] 26.54/7.36 = [c_1(isNat^#(activate(V2)))] 26.54/7.36 26.54/7.36 [isNat^#(n__plus(V1, V2))] = [4] V2 + [4] V1 + [0] 26.54/7.36 >= [4] V2 + [4] V1 + [0] 26.54/7.36 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1)))] 26.54/7.36 26.54/7.36 [isNat^#(n__s(V1))] = [4] V1 + [0] 26.54/7.36 >= [4] V1 + [0] 26.54/7.36 = [c_3(isNat^#(activate(V1)))] 26.54/7.36 26.54/7.36 [isNat^#(n__x(V1, V2))] = [4] V2 + [4] V1 + [4] 26.54/7.36 > [4] V2 + [4] V1 + [1] 26.54/7.36 = [c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1)))] 26.54/7.36 26.54/7.36 [U31^#(tt(), V2)] = [4] V2 + [0] 26.54/7.36 >= [4] V2 + [0] 26.54/7.36 = [c_5(isNat^#(activate(V2)))] 26.54/7.36 26.54/7.36 [U51^#(tt(), M, N)] = [7] N + [7] M + [7] 26.54/7.36 > [4] N + [3] 26.54/7.36 = [c_6(isNat^#(activate(N)))] 26.54/7.36 26.54/7.36 [U71^#(tt(), M, N)] = [7] N + [7] M + [7] 26.54/7.36 > [4] N + [3] 26.54/7.36 = [c_7(isNat^#(activate(N)))] 26.54/7.36 26.54/7.36 26.54/7.36 We return to the main proof. Consider the set of all dependency 26.54/7.36 pairs 26.54/7.36 26.54/7.36 : 26.54/7.36 { 1: isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 2: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , 3: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , 4: isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 5: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , 6: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , 7: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 26.54/7.36 Processor 'matrix interpretation of dimension 1' induces the 26.54/7.36 complexity certificate YES(?,O(n^1)) on application of dependency 26.54/7.36 pairs {1,6,7}. These cover all (indirect) predecessors of 26.54/7.36 dependency pairs {1,2,6,7}, their number of application is equally 26.54/7.36 bounded. The dependency pairs are shifted into the weak component. 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Weak DPs: 26.54/7.36 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 Weak Trs: 26.54/7.36 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.36 , U12(tt()) -> tt() 26.54/7.36 , isNat(n__0()) -> tt() 26.54/7.36 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.36 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.36 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.36 , activate(X) -> X 26.54/7.36 , activate(n__0()) -> 0() 26.54/7.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.36 , activate(n__s(X)) -> s(X) 26.54/7.36 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.36 , U21(tt()) -> tt() 26.54/7.36 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.36 , U32(tt()) -> tt() 26.54/7.36 , s(X) -> n__s(X) 26.54/7.36 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.36 , 0() -> n__0() 26.54/7.36 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 The following weak DPs constitute a sub-graph of the DG that is 26.54/7.36 closed under successors. The DPs are removed. 26.54/7.36 26.54/7.36 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Weak Trs: 26.54/7.36 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.36 , U12(tt()) -> tt() 26.54/7.36 , isNat(n__0()) -> tt() 26.54/7.36 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.36 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.36 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.36 , activate(X) -> X 26.54/7.36 , activate(n__0()) -> 0() 26.54/7.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.36 , activate(n__s(X)) -> s(X) 26.54/7.36 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.36 , U21(tt()) -> tt() 26.54/7.36 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.36 , U32(tt()) -> tt() 26.54/7.36 , s(X) -> n__s(X) 26.54/7.36 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.36 , 0() -> n__0() 26.54/7.36 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 No rule is usable, rules are removed from the input problem. 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Rules: Empty 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 Empty rules are trivially bounded 26.54/7.36 26.54/7.36 S) We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Strict DPs: { U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 Weak DPs: 26.54/7.36 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.36 Weak Trs: 26.54/7.36 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.36 , U12(tt()) -> tt() 26.54/7.36 , isNat(n__0()) -> tt() 26.54/7.36 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.36 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.36 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.36 , activate(X) -> X 26.54/7.36 , activate(n__0()) -> 0() 26.54/7.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.36 , activate(n__s(X)) -> s(X) 26.54/7.36 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.36 , U21(tt()) -> tt() 26.54/7.36 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.36 , U32(tt()) -> tt() 26.54/7.36 , s(X) -> n__s(X) 26.54/7.36 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.36 , 0() -> n__0() 26.54/7.36 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 We estimate the number of application of {1} by applications of 26.54/7.36 Pre({1}) = {}. Here rules are labeled as follows: 26.54/7.36 26.54/7.36 DPs: 26.54/7.36 { 1: U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) 26.54/7.36 , 2: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , 3: isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 4: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , 5: isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , 6: U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , 7: U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) } 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Weak DPs: 26.54/7.36 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 Weak Trs: 26.54/7.36 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.36 , U12(tt()) -> tt() 26.54/7.36 , isNat(n__0()) -> tt() 26.54/7.36 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.36 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.36 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.36 , activate(X) -> X 26.54/7.36 , activate(n__0()) -> 0() 26.54/7.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.36 , activate(n__s(X)) -> s(X) 26.54/7.36 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.36 , U21(tt()) -> tt() 26.54/7.36 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.36 , U32(tt()) -> tt() 26.54/7.36 , s(X) -> n__s(X) 26.54/7.36 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.36 , 0() -> n__0() 26.54/7.36 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 The following weak DPs constitute a sub-graph of the DG that is 26.54/7.36 closed under successors. The DPs are removed. 26.54/7.36 26.54/7.36 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 26.54/7.36 , isNat^#(n__plus(V1, V2)) -> 26.54/7.36 c_2(U11^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 26.54/7.36 , isNat^#(n__x(V1, V2)) -> 26.54/7.36 c_4(U31^#(isNat(activate(V1)), activate(V2)), 26.54/7.36 isNat^#(activate(V1))) 26.54/7.36 , U31^#(tt(), V2) -> c_5(isNat^#(activate(V2))) 26.54/7.36 , U51^#(tt(), M, N) -> c_6(isNat^#(activate(N))) 26.54/7.36 , U71^#(tt(), M, N) -> c_7(isNat^#(activate(N))) } 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Weak Trs: 26.54/7.36 { U11(tt(), V2) -> U12(isNat(activate(V2))) 26.54/7.36 , U12(tt()) -> tt() 26.54/7.36 , isNat(n__0()) -> tt() 26.54/7.36 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 26.54/7.36 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 26.54/7.36 , isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2)) 26.54/7.36 , activate(X) -> X 26.54/7.36 , activate(n__0()) -> 0() 26.54/7.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 26.54/7.36 , activate(n__s(X)) -> s(X) 26.54/7.36 , activate(n__x(X1, X2)) -> x(X1, X2) 26.54/7.36 , U21(tt()) -> tt() 26.54/7.36 , U31(tt(), V2) -> U32(isNat(activate(V2))) 26.54/7.36 , U32(tt()) -> tt() 26.54/7.36 , s(X) -> n__s(X) 26.54/7.36 , plus(X1, X2) -> n__plus(X1, X2) 26.54/7.36 , 0() -> n__0() 26.54/7.36 , x(X1, X2) -> n__x(X1, X2) } 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 No rule is usable, rules are removed from the input problem. 26.54/7.36 26.54/7.36 We are left with following problem, upon which TcT provides the 26.54/7.36 certificate YES(O(1),O(1)). 26.54/7.36 26.54/7.36 Rules: Empty 26.54/7.36 Obligation: 26.54/7.36 innermost runtime complexity 26.54/7.36 Answer: 26.54/7.36 YES(O(1),O(1)) 26.54/7.36 26.54/7.36 Empty rules are trivially bounded 26.54/7.36 26.54/7.36 26.54/7.36 Hurray, we answered YES(O(1),O(n^1)) 26.54/7.37 EOF