YES(O(1),O(n^1)) 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , plus(N, s(M)) -> U41(isNat(M), M, N) 13.17/3.96 , plus(N, 0()) -> U31(isNat(N), N) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 Arguments of following rules are not normal-forms: 13.17/3.96 13.17/3.96 { plus(N, s(M)) -> U41(isNat(M), M, N) 13.17/3.96 , plus(N, 0()) -> U31(isNat(N), N) } 13.17/3.96 13.17/3.96 All above mentioned rules can be savely removed. 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We add the following dependency tuples: 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , U12^#(tt()) -> c_2() 13.17/3.96 , isNat^#(n__0()) -> c_3() 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , activate^#(X) -> c_6() 13.17/3.96 , activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , U21^#(tt()) -> c_10() 13.17/3.96 , 0^#() -> c_16() 13.17/3.96 , plus^#(X1, X2) -> c_15() 13.17/3.96 , s^#(X) -> c_14() 13.17/3.96 , U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 13.17/3.96 and mark the set of starting terms. 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , U12^#(tt()) -> c_2() 13.17/3.96 , isNat^#(n__0()) -> c_3() 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , activate^#(X) -> c_6() 13.17/3.96 , activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , U21^#(tt()) -> c_10() 13.17/3.96 , 0^#() -> c_16() 13.17/3.96 , plus^#(X1, X2) -> c_15() 13.17/3.96 , s^#(X) -> c_14() 13.17/3.96 , U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We estimate the number of application of {2,3,6,10,11,12,13} by 13.17/3.96 applications of Pre({2,3,6,10,11,12,13}) = {1,4,5,7,8,9,14,15,16}. 13.17/3.96 Here rules are labeled as follows: 13.17/3.96 13.17/3.96 DPs: 13.17/3.96 { 1: U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , 2: U12^#(tt()) -> c_2() 13.17/3.96 , 3: isNat^#(n__0()) -> c_3() 13.17/3.96 , 4: isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , 5: isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , 6: activate^#(X) -> c_6() 13.17/3.96 , 7: activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , 8: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , 9: activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , 10: U21^#(tt()) -> c_10() 13.17/3.96 , 11: 0^#() -> c_16() 13.17/3.96 , 12: plus^#(X1, X2) -> c_15() 13.17/3.96 , 13: s^#(X) -> c_14() 13.17/3.96 , 14: U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , 15: U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , 16: U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 Weak DPs: 13.17/3.96 { U12^#(tt()) -> c_2() 13.17/3.96 , isNat^#(n__0()) -> c_3() 13.17/3.96 , activate^#(X) -> c_6() 13.17/3.96 , U21^#(tt()) -> c_10() 13.17/3.96 , 0^#() -> c_16() 13.17/3.96 , plus^#(X1, X2) -> c_15() 13.17/3.96 , s^#(X) -> c_14() } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We estimate the number of application of {4,5,6} by applications of 13.17/3.96 Pre({4,5,6}) = {1,2,3,7,8,9}. Here rules are labeled as follows: 13.17/3.96 13.17/3.96 DPs: 13.17/3.96 { 1: U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , 2: isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , 3: isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , 4: activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , 5: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , 6: activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , 7: U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , 8: U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , 9: U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) 13.17/3.96 , 10: U12^#(tt()) -> c_2() 13.17/3.96 , 11: isNat^#(n__0()) -> c_3() 13.17/3.96 , 12: activate^#(X) -> c_6() 13.17/3.96 , 13: U21^#(tt()) -> c_10() 13.17/3.96 , 14: 0^#() -> c_16() 13.17/3.96 , 15: plus^#(X1, X2) -> c_15() 13.17/3.96 , 16: s^#(X) -> c_14() } 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 Weak DPs: 13.17/3.96 { U12^#(tt()) -> c_2() 13.17/3.96 , isNat^#(n__0()) -> c_3() 13.17/3.96 , activate^#(X) -> c_6() 13.17/3.96 , activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , U21^#(tt()) -> c_10() 13.17/3.96 , 0^#() -> c_16() 13.17/3.96 , plus^#(X1, X2) -> c_15() 13.17/3.96 , s^#(X) -> c_14() } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We estimate the number of application of {4,6} by applications of 13.17/3.96 Pre({4,6}) = {5}. Here rules are labeled as follows: 13.17/3.96 13.17/3.96 DPs: 13.17/3.96 { 1: U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , 2: isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , 3: isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , 4: U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , 5: U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) 13.17/3.96 , 6: U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) 13.17/3.96 , 7: U12^#(tt()) -> c_2() 13.17/3.96 , 8: isNat^#(n__0()) -> c_3() 13.17/3.96 , 9: activate^#(X) -> c_6() 13.17/3.96 , 10: activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , 11: activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , 12: activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , 13: U21^#(tt()) -> c_10() 13.17/3.96 , 14: 0^#() -> c_16() 13.17/3.96 , 15: plus^#(X1, X2) -> c_15() 13.17/3.96 , 16: s^#(X) -> c_14() } 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) } 13.17/3.96 Weak DPs: 13.17/3.96 { U12^#(tt()) -> c_2() 13.17/3.96 , isNat^#(n__0()) -> c_3() 13.17/3.96 , activate^#(X) -> c_6() 13.17/3.96 , activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , U21^#(tt()) -> c_10() 13.17/3.96 , 0^#() -> c_16() 13.17/3.96 , plus^#(X1, X2) -> c_15() 13.17/3.96 , s^#(X) -> c_14() 13.17/3.96 , U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 The following weak DPs constitute a sub-graph of the DG that is 13.17/3.96 closed under successors. The DPs are removed. 13.17/3.96 13.17/3.96 { U12^#(tt()) -> c_2() 13.17/3.96 , isNat^#(n__0()) -> c_3() 13.17/3.96 , activate^#(X) -> c_6() 13.17/3.96 , activate^#(n__0()) -> c_7(0^#()) 13.17/3.96 , activate^#(n__plus(X1, X2)) -> c_8(plus^#(X1, X2)) 13.17/3.96 , activate^#(n__s(X)) -> c_9(s^#(X)) 13.17/3.96 , U21^#(tt()) -> c_10() 13.17/3.96 , 0^#() -> c_16() 13.17/3.96 , plus^#(X1, X2) -> c_15() 13.17/3.96 , s^#(X) -> c_14() 13.17/3.96 , U31^#(tt(), N) -> c_11(activate^#(N)) 13.17/3.96 , U42^#(tt(), M, N) -> 13.17/3.96 c_13(s^#(plus(activate(N), activate(M))), 13.17/3.96 plus^#(activate(N), activate(M)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M)) } 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 Due to missing edges in the dependency-graph, the right-hand sides 13.17/3.96 of following rules could be simplified: 13.17/3.96 13.17/3.96 { U11^#(tt(), V2) -> 13.17/3.96 c_1(U12^#(isNat(activate(V2))), 13.17/3.96 isNat^#(activate(V2)), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_4(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1), 13.17/3.96 activate^#(V2)) 13.17/3.96 , isNat^#(n__s(V1)) -> 13.17/3.96 c_5(U21^#(isNat(activate(V1))), 13.17/3.96 isNat^#(activate(V1)), 13.17/3.96 activate^#(V1)) 13.17/3.96 , U41^#(tt(), M, N) -> 13.17/3.96 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 13.17/3.96 isNat^#(activate(N)), 13.17/3.96 activate^#(N), 13.17/3.96 activate^#(M), 13.17/3.96 activate^#(N)) } 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1))) 13.17/3.96 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.96 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , U31(tt(), N) -> activate(N) 13.17/3.96 , U41(tt(), M, N) -> 13.17/3.96 U42(isNat(activate(N)), activate(M), activate(N)) 13.17/3.96 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We replace rewrite rules by usable rules: 13.17/3.96 13.17/3.96 Weak Usable Rules: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 13.17/3.96 We are left with following problem, upon which TcT provides the 13.17/3.96 certificate YES(O(1),O(n^1)). 13.17/3.96 13.17/3.96 Strict DPs: 13.17/3.96 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.96 , isNat^#(n__plus(V1, V2)) -> 13.17/3.96 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.96 isNat^#(activate(V1))) 13.17/3.96 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.96 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.96 Weak Trs: 13.17/3.96 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.96 , U12(tt()) -> tt() 13.17/3.96 , isNat(n__0()) -> tt() 13.17/3.96 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.96 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.96 , activate(X) -> X 13.17/3.96 , activate(n__0()) -> 0() 13.17/3.96 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.96 , activate(n__s(X)) -> s(X) 13.17/3.96 , U21(tt()) -> tt() 13.17/3.96 , s(X) -> n__s(X) 13.17/3.96 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.96 , 0() -> n__0() } 13.17/3.96 Obligation: 13.17/3.96 innermost runtime complexity 13.17/3.96 Answer: 13.17/3.96 YES(O(1),O(n^1)) 13.17/3.96 13.17/3.96 We use the processor 'matrix interpretation of dimension 1' to 13.17/3.96 orient following rules strictly. 13.17/3.96 13.17/3.96 DPs: 13.17/3.96 { 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.96 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.96 13.17/3.96 Sub-proof: 13.17/3.96 ---------- 13.17/3.96 The following argument positions are usable: 13.17/3.96 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 13.17/3.96 Uargs(c_4) = {1} 13.17/3.96 13.17/3.96 TcT has computed the following constructor-based matrix 13.17/3.96 interpretation satisfying not(EDA). 13.17/3.96 13.17/3.96 [U11](x1, x2) = [0] 13.17/3.96 13.17/3.96 [tt] = [0] 13.17/3.96 13.17/3.96 [U12](x1) = [0] 13.17/3.96 13.17/3.96 [isNat](x1) = [0] 13.17/3.96 13.17/3.96 [activate](x1) = [1] x1 + [0] 13.17/3.96 13.17/3.96 [U21](x1) = [0] 13.17/3.96 13.17/3.96 [s](x1) = [1] x1 + [2] 13.17/3.96 13.17/3.96 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 13.17/3.96 13.17/3.96 [n__0] = [0] 13.17/3.96 13.17/3.96 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 13.17/3.96 13.17/3.96 [n__s](x1) = [1] x1 + [2] 13.17/3.96 13.17/3.96 [0] = [0] 13.17/3.96 13.17/3.96 [U11^#](x1, x2) = [2] x2 + [0] 13.17/3.96 13.17/3.96 [isNat^#](x1) = [2] x1 + [0] 13.17/3.96 13.17/3.96 [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 13.17/3.96 13.17/3.96 [c_1](x1) = [1] x1 + [0] 13.17/3.96 13.17/3.96 [c_2](x1, x2) = [1] x1 + [1] x2 + [0] 13.17/3.96 13.17/3.96 [c_3](x1) = [1] x1 + [1] 13.17/3.96 13.17/3.96 [c_4](x1) = [1] x1 + [3] 13.17/3.96 13.17/3.96 The order satisfies the following ordering constraints: 13.17/3.96 13.17/3.96 [U11(tt(), V2)] = [0] 13.17/3.96 >= [0] 13.17/3.96 = [U12(isNat(activate(V2)))] 13.17/3.96 13.17/3.96 [U12(tt())] = [0] 13.17/3.96 >= [0] 13.17/3.96 = [tt()] 13.17/3.96 13.17/3.96 [isNat(n__0())] = [0] 13.17/3.96 >= [0] 13.17/3.96 = [tt()] 13.17/3.96 13.17/3.96 [isNat(n__plus(V1, V2))] = [0] 13.17/3.96 >= [0] 13.17/3.96 = [U11(isNat(activate(V1)), activate(V2))] 13.17/3.96 13.17/3.96 [isNat(n__s(V1))] = [0] 13.17/3.96 >= [0] 13.17/3.96 = [U21(isNat(activate(V1)))] 13.17/3.96 13.17/3.96 [activate(X)] = [1] X + [0] 13.17/3.97 >= [1] X + [0] 13.17/3.97 = [X] 13.17/3.97 13.17/3.97 [activate(n__0())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [0()] 13.17/3.97 13.17/3.97 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 13.17/3.97 >= [1] X1 + [1] X2 + [0] 13.17/3.97 = [plus(X1, X2)] 13.17/3.97 13.17/3.97 [activate(n__s(X))] = [1] X + [2] 13.17/3.97 >= [1] X + [2] 13.17/3.97 = [s(X)] 13.17/3.97 13.17/3.97 [U21(tt())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [s(X)] = [1] X + [2] 13.17/3.97 >= [1] X + [2] 13.17/3.97 = [n__s(X)] 13.17/3.97 13.17/3.97 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 13.17/3.97 >= [1] X1 + [1] X2 + [0] 13.17/3.97 = [n__plus(X1, X2)] 13.17/3.97 13.17/3.97 [0()] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [n__0()] 13.17/3.97 13.17/3.97 [U11^#(tt(), V2)] = [2] V2 + [0] 13.17/3.97 >= [2] V2 + [0] 13.17/3.97 = [c_1(isNat^#(activate(V2)))] 13.17/3.97 13.17/3.97 [isNat^#(n__plus(V1, V2))] = [2] V2 + [2] V1 + [0] 13.17/3.97 >= [2] V2 + [2] V1 + [0] 13.17/3.97 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1)))] 13.17/3.97 13.17/3.97 [isNat^#(n__s(V1))] = [2] V1 + [4] 13.17/3.97 > [2] V1 + [1] 13.17/3.97 = [c_3(isNat^#(activate(V1)))] 13.17/3.97 13.17/3.97 [U41^#(tt(), M, N)] = [7] N + [7] M + [7] 13.17/3.97 > [2] N + [3] 13.17/3.97 = [c_4(isNat^#(activate(N)))] 13.17/3.97 13.17/3.97 13.17/3.97 The strictly oriented rules are moved into the weak component. 13.17/3.97 13.17/3.97 We are left with following problem, upon which TcT provides the 13.17/3.97 certificate YES(O(1),O(n^1)). 13.17/3.97 13.17/3.97 Strict DPs: 13.17/3.97 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) } 13.17/3.97 Weak DPs: 13.17/3.97 { isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.97 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 Weak Trs: 13.17/3.97 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.97 , U12(tt()) -> tt() 13.17/3.97 , isNat(n__0()) -> tt() 13.17/3.97 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.97 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.97 , activate(X) -> X 13.17/3.97 , activate(n__0()) -> 0() 13.17/3.97 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.97 , activate(n__s(X)) -> s(X) 13.17/3.97 , U21(tt()) -> tt() 13.17/3.97 , s(X) -> n__s(X) 13.17/3.97 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.97 , 0() -> n__0() } 13.17/3.97 Obligation: 13.17/3.97 innermost runtime complexity 13.17/3.97 Answer: 13.17/3.97 YES(O(1),O(n^1)) 13.17/3.97 13.17/3.97 We use the processor 'matrix interpretation of dimension 1' to 13.17/3.97 orient following rules strictly. 13.17/3.97 13.17/3.97 DPs: 13.17/3.97 { 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) } 13.17/3.97 13.17/3.97 Sub-proof: 13.17/3.97 ---------- 13.17/3.97 The following argument positions are usable: 13.17/3.97 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 13.17/3.97 Uargs(c_4) = {1} 13.17/3.97 13.17/3.97 TcT has computed the following constructor-based matrix 13.17/3.97 interpretation satisfying not(EDA). 13.17/3.97 13.17/3.97 [U11](x1, x2) = [0] 13.17/3.97 13.17/3.97 [tt] = [0] 13.17/3.97 13.17/3.97 [U12](x1) = [0] 13.17/3.97 13.17/3.97 [isNat](x1) = [0] 13.17/3.97 13.17/3.97 [activate](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [U21](x1) = [0] 13.17/3.97 13.17/3.97 [s](x1) = [1] x1 + [3] 13.17/3.97 13.17/3.97 [plus](x1, x2) = [1] x1 + [1] x2 + [4] 13.17/3.97 13.17/3.97 [n__0] = [0] 13.17/3.97 13.17/3.97 [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] 13.17/3.97 13.17/3.97 [n__s](x1) = [1] x1 + [3] 13.17/3.97 13.17/3.97 [0] = [0] 13.17/3.97 13.17/3.97 [U11^#](x1, x2) = [1] x2 + [4] 13.17/3.97 13.17/3.97 [isNat^#](x1) = [1] x1 + [1] 13.17/3.97 13.17/3.97 [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 13.17/3.97 13.17/3.97 [c_1](x1) = [1] x1 + [1] 13.17/3.97 13.17/3.97 [c_2](x1, x2) = [1] x1 + [1] x2 + [0] 13.17/3.97 13.17/3.97 [c_3](x1) = [1] x1 + [1] 13.17/3.97 13.17/3.97 [c_4](x1) = [4] x1 + [3] 13.17/3.97 13.17/3.97 The order satisfies the following ordering constraints: 13.17/3.97 13.17/3.97 [U11(tt(), V2)] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [U12(isNat(activate(V2)))] 13.17/3.97 13.17/3.97 [U12(tt())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [isNat(n__0())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [isNat(n__plus(V1, V2))] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [U11(isNat(activate(V1)), activate(V2))] 13.17/3.97 13.17/3.97 [isNat(n__s(V1))] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [U21(isNat(activate(V1)))] 13.17/3.97 13.17/3.97 [activate(X)] = [1] X + [0] 13.17/3.97 >= [1] X + [0] 13.17/3.97 = [X] 13.17/3.97 13.17/3.97 [activate(n__0())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [0()] 13.17/3.97 13.17/3.97 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4] 13.17/3.97 >= [1] X1 + [1] X2 + [4] 13.17/3.97 = [plus(X1, X2)] 13.17/3.97 13.17/3.97 [activate(n__s(X))] = [1] X + [3] 13.17/3.97 >= [1] X + [3] 13.17/3.97 = [s(X)] 13.17/3.97 13.17/3.97 [U21(tt())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [s(X)] = [1] X + [3] 13.17/3.97 >= [1] X + [3] 13.17/3.97 = [n__s(X)] 13.17/3.97 13.17/3.97 [plus(X1, X2)] = [1] X1 + [1] X2 + [4] 13.17/3.97 >= [1] X1 + [1] X2 + [4] 13.17/3.97 = [n__plus(X1, X2)] 13.17/3.97 13.17/3.97 [0()] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [n__0()] 13.17/3.97 13.17/3.97 [U11^#(tt(), V2)] = [1] V2 + [4] 13.17/3.97 > [1] V2 + [2] 13.17/3.97 = [c_1(isNat^#(activate(V2)))] 13.17/3.97 13.17/3.97 [isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [5] 13.17/3.97 >= [1] V2 + [1] V1 + [5] 13.17/3.97 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1)))] 13.17/3.97 13.17/3.97 [isNat^#(n__s(V1))] = [1] V1 + [4] 13.17/3.97 > [1] V1 + [2] 13.17/3.97 = [c_3(isNat^#(activate(V1)))] 13.17/3.97 13.17/3.97 [U41^#(tt(), M, N)] = [7] N + [7] M + [7] 13.17/3.97 >= [4] N + [7] 13.17/3.97 = [c_4(isNat^#(activate(N)))] 13.17/3.97 13.17/3.97 13.17/3.97 We return to the main proof. Consider the set of all dependency 13.17/3.97 pairs 13.17/3.97 13.17/3.97 : 13.17/3.97 { 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , 2: isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) 13.17/3.97 , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.97 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 13.17/3.97 Processor 'matrix interpretation of dimension 1' induces the 13.17/3.97 complexity certificate YES(?,O(n^1)) on application of dependency 13.17/3.97 pairs {1,3}. These cover all (indirect) predecessors of dependency 13.17/3.97 pairs {1,3,4}, their number of application is equally bounded. The 13.17/3.97 dependency pairs are shifted into the weak component. 13.17/3.97 13.17/3.97 We are left with following problem, upon which TcT provides the 13.17/3.97 certificate YES(O(1),O(n^1)). 13.17/3.97 13.17/3.97 Strict DPs: 13.17/3.97 { isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) } 13.17/3.97 Weak DPs: 13.17/3.97 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.97 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 Weak Trs: 13.17/3.97 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.97 , U12(tt()) -> tt() 13.17/3.97 , isNat(n__0()) -> tt() 13.17/3.97 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.97 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.97 , activate(X) -> X 13.17/3.97 , activate(n__0()) -> 0() 13.17/3.97 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.97 , activate(n__s(X)) -> s(X) 13.17/3.97 , U21(tt()) -> tt() 13.17/3.97 , s(X) -> n__s(X) 13.17/3.97 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.97 , 0() -> n__0() } 13.17/3.97 Obligation: 13.17/3.97 innermost runtime complexity 13.17/3.97 Answer: 13.17/3.97 YES(O(1),O(n^1)) 13.17/3.97 13.17/3.97 We use the processor 'matrix interpretation of dimension 1' to 13.17/3.97 orient following rules strictly. 13.17/3.97 13.17/3.97 DPs: 13.17/3.97 { 1: isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) 13.17/3.97 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 13.17/3.97 Sub-proof: 13.17/3.97 ---------- 13.17/3.97 The following argument positions are usable: 13.17/3.97 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 13.17/3.97 Uargs(c_4) = {1} 13.17/3.97 13.17/3.97 TcT has computed the following constructor-based matrix 13.17/3.97 interpretation satisfying not(EDA). 13.17/3.97 13.17/3.97 [U11](x1, x2) = [0] 13.17/3.97 13.17/3.97 [tt] = [0] 13.17/3.97 13.17/3.97 [U12](x1) = [0] 13.17/3.97 13.17/3.97 [isNat](x1) = [0] 13.17/3.97 13.17/3.97 [activate](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [U21](x1) = [0] 13.17/3.97 13.17/3.97 [s](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [plus](x1, x2) = [1] x1 + [1] x2 + [1] 13.17/3.97 13.17/3.97 [n__0] = [0] 13.17/3.97 13.17/3.97 [n__plus](x1, x2) = [1] x1 + [1] x2 + [1] 13.17/3.97 13.17/3.97 [n__s](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [0] = [0] 13.17/3.97 13.17/3.97 [U11^#](x1, x2) = [1] x2 + [0] 13.17/3.97 13.17/3.97 [isNat^#](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 13.17/3.97 13.17/3.97 [c_1](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [c_2](x1, x2) = [1] x1 + [1] x2 + [0] 13.17/3.97 13.17/3.97 [c_3](x1) = [1] x1 + [0] 13.17/3.97 13.17/3.97 [c_4](x1) = [4] x1 + [3] 13.17/3.97 13.17/3.97 The order satisfies the following ordering constraints: 13.17/3.97 13.17/3.97 [U11(tt(), V2)] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [U12(isNat(activate(V2)))] 13.17/3.97 13.17/3.97 [U12(tt())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [isNat(n__0())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [isNat(n__plus(V1, V2))] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [U11(isNat(activate(V1)), activate(V2))] 13.17/3.97 13.17/3.97 [isNat(n__s(V1))] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [U21(isNat(activate(V1)))] 13.17/3.97 13.17/3.97 [activate(X)] = [1] X + [0] 13.17/3.97 >= [1] X + [0] 13.17/3.97 = [X] 13.17/3.97 13.17/3.97 [activate(n__0())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [0()] 13.17/3.97 13.17/3.97 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [1] 13.17/3.97 >= [1] X1 + [1] X2 + [1] 13.17/3.97 = [plus(X1, X2)] 13.17/3.97 13.17/3.97 [activate(n__s(X))] = [1] X + [0] 13.17/3.97 >= [1] X + [0] 13.17/3.97 = [s(X)] 13.17/3.97 13.17/3.97 [U21(tt())] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [tt()] 13.17/3.97 13.17/3.97 [s(X)] = [1] X + [0] 13.17/3.97 >= [1] X + [0] 13.17/3.97 = [n__s(X)] 13.17/3.97 13.17/3.97 [plus(X1, X2)] = [1] X1 + [1] X2 + [1] 13.17/3.97 >= [1] X1 + [1] X2 + [1] 13.17/3.97 = [n__plus(X1, X2)] 13.17/3.97 13.17/3.97 [0()] = [0] 13.17/3.97 >= [0] 13.17/3.97 = [n__0()] 13.17/3.97 13.17/3.97 [U11^#(tt(), V2)] = [1] V2 + [0] 13.17/3.97 >= [1] V2 + [0] 13.17/3.97 = [c_1(isNat^#(activate(V2)))] 13.17/3.97 13.17/3.97 [isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [1] 13.17/3.97 > [1] V2 + [1] V1 + [0] 13.17/3.97 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1)))] 13.17/3.97 13.17/3.97 [isNat^#(n__s(V1))] = [1] V1 + [0] 13.17/3.97 >= [1] V1 + [0] 13.17/3.97 = [c_3(isNat^#(activate(V1)))] 13.17/3.97 13.17/3.97 [U41^#(tt(), M, N)] = [7] N + [7] M + [7] 13.17/3.97 > [4] N + [3] 13.17/3.97 = [c_4(isNat^#(activate(N)))] 13.17/3.97 13.17/3.97 13.17/3.97 We return to the main proof. Consider the set of all dependency 13.17/3.97 pairs 13.17/3.97 13.17/3.97 : 13.17/3.97 { 1: isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) 13.17/3.97 , 2: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.97 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 13.17/3.97 Processor 'matrix interpretation of dimension 1' induces the 13.17/3.97 complexity certificate YES(?,O(n^1)) on application of dependency 13.17/3.97 pairs {1,4}. These cover all (indirect) predecessors of dependency 13.17/3.97 pairs {1,2,4}, their number of application is equally bounded. The 13.17/3.97 dependency pairs are shifted into the weak component. 13.17/3.97 13.17/3.97 We are left with following problem, upon which TcT provides the 13.17/3.97 certificate YES(O(1),O(1)). 13.17/3.97 13.17/3.97 Weak DPs: 13.17/3.97 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) 13.17/3.97 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.97 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 Weak Trs: 13.17/3.97 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.97 , U12(tt()) -> tt() 13.17/3.97 , isNat(n__0()) -> tt() 13.17/3.97 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.97 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.97 , activate(X) -> X 13.17/3.97 , activate(n__0()) -> 0() 13.17/3.97 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.97 , activate(n__s(X)) -> s(X) 13.17/3.97 , U21(tt()) -> tt() 13.17/3.97 , s(X) -> n__s(X) 13.17/3.97 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.97 , 0() -> n__0() } 13.17/3.97 Obligation: 13.17/3.97 innermost runtime complexity 13.17/3.97 Answer: 13.17/3.97 YES(O(1),O(1)) 13.17/3.97 13.17/3.97 The following weak DPs constitute a sub-graph of the DG that is 13.17/3.97 closed under successors. The DPs are removed. 13.17/3.97 13.17/3.97 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 13.17/3.97 , isNat^#(n__plus(V1, V2)) -> 13.17/3.97 c_2(U11^#(isNat(activate(V1)), activate(V2)), 13.17/3.97 isNat^#(activate(V1))) 13.17/3.97 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 13.17/3.97 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 13.17/3.97 13.17/3.97 We are left with following problem, upon which TcT provides the 13.17/3.97 certificate YES(O(1),O(1)). 13.17/3.97 13.17/3.97 Weak Trs: 13.17/3.97 { U11(tt(), V2) -> U12(isNat(activate(V2))) 13.17/3.97 , U12(tt()) -> tt() 13.17/3.97 , isNat(n__0()) -> tt() 13.17/3.97 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 13.17/3.97 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 13.17/3.97 , activate(X) -> X 13.17/3.97 , activate(n__0()) -> 0() 13.17/3.97 , activate(n__plus(X1, X2)) -> plus(X1, X2) 13.17/3.97 , activate(n__s(X)) -> s(X) 13.17/3.97 , U21(tt()) -> tt() 13.17/3.97 , s(X) -> n__s(X) 13.17/3.97 , plus(X1, X2) -> n__plus(X1, X2) 13.17/3.97 , 0() -> n__0() } 13.17/3.97 Obligation: 13.17/3.97 innermost runtime complexity 13.17/3.97 Answer: 13.17/3.97 YES(O(1),O(1)) 13.17/3.97 13.17/3.97 No rule is usable, rules are removed from the input problem. 13.17/3.97 13.17/3.97 We are left with following problem, upon which TcT provides the 13.17/3.97 certificate YES(O(1),O(1)). 13.17/3.97 13.17/3.97 Rules: Empty 13.17/3.97 Obligation: 13.17/3.97 innermost runtime complexity 13.17/3.97 Answer: 13.17/3.97 YES(O(1),O(1)) 13.17/3.97 13.17/3.97 Empty rules are trivially bounded 13.17/3.97 13.17/3.97 Hurray, we answered YES(O(1),O(n^1)) 13.17/3.98 EOF