YES(O(1),O(n^2)) 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , plus(N, s(M)) -> U41(isNat(M), M, N) 233.16/70.53 , plus(N, 0()) -> U31(isNat(N), N) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 Arguments of following rules are not normal-forms: 233.16/70.53 233.16/70.53 { plus(N, s(M)) -> U41(isNat(M), M, N) 233.16/70.53 , plus(N, 0()) -> U31(isNat(N), N) } 233.16/70.53 233.16/70.53 All above mentioned rules can be savely removed. 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 We add the following dependency tuples: 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , U12^#(tt()) -> c_2() 233.16/70.53 , isNat^#(n__0()) -> c_3() 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , activate^#(X) -> c_6() 233.16/70.53 , activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , U21^#(tt()) -> c_10() 233.16/70.53 , 0^#() -> c_16() 233.16/70.53 , plus^#(X1, X2) -> c_15() 233.16/70.53 , s^#(X) -> c_14() 233.16/70.53 , U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 233.16/70.53 and mark the set of starting terms. 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , U12^#(tt()) -> c_2() 233.16/70.53 , isNat^#(n__0()) -> c_3() 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , activate^#(X) -> c_6() 233.16/70.53 , activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , U21^#(tt()) -> c_10() 233.16/70.53 , 0^#() -> c_16() 233.16/70.53 , plus^#(X1, X2) -> c_15() 233.16/70.53 , s^#(X) -> c_14() 233.16/70.53 , U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 We estimate the number of application of {2,3,6,10,11,12,13} by 233.16/70.53 applications of Pre({2,3,6,10,11,12,13}) = {1,4,5,7,8,9,14,15,16}. 233.16/70.53 Here rules are labeled as follows: 233.16/70.53 233.16/70.53 DPs: 233.16/70.53 { 1: U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , 2: U12^#(tt()) -> c_2() 233.16/70.53 , 3: isNat^#(n__0()) -> c_3() 233.16/70.53 , 4: isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , 5: isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , 6: activate^#(X) -> c_6() 233.16/70.53 , 7: activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , 8: activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , 9: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , 10: U21^#(tt()) -> c_10() 233.16/70.53 , 11: 0^#() -> c_16() 233.16/70.53 , 12: plus^#(X1, X2) -> c_15() 233.16/70.53 , 13: s^#(X) -> c_14() 233.16/70.53 , 14: U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , 15: U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , 16: U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 Weak DPs: 233.16/70.53 { U12^#(tt()) -> c_2() 233.16/70.53 , isNat^#(n__0()) -> c_3() 233.16/70.53 , activate^#(X) -> c_6() 233.16/70.53 , U21^#(tt()) -> c_10() 233.16/70.53 , 0^#() -> c_16() 233.16/70.53 , plus^#(X1, X2) -> c_15() 233.16/70.53 , s^#(X) -> c_14() } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 We estimate the number of application of {4} by applications of 233.16/70.53 Pre({4}) = {1,2,3,5,6,7,8,9}. Here rules are labeled as follows: 233.16/70.53 233.16/70.53 DPs: 233.16/70.53 { 1: U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , 2: isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , 3: isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , 4: activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , 5: activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , 6: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , 7: U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , 8: U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , 9: U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) 233.16/70.53 , 10: U12^#(tt()) -> c_2() 233.16/70.53 , 11: isNat^#(n__0()) -> c_3() 233.16/70.53 , 12: activate^#(X) -> c_6() 233.16/70.53 , 13: U21^#(tt()) -> c_10() 233.16/70.53 , 14: 0^#() -> c_16() 233.16/70.53 , 15: plus^#(X1, X2) -> c_15() 233.16/70.53 , 16: s^#(X) -> c_14() } 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 Weak DPs: 233.16/70.53 { U12^#(tt()) -> c_2() 233.16/70.53 , isNat^#(n__0()) -> c_3() 233.16/70.53 , activate^#(X) -> c_6() 233.16/70.53 , activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , U21^#(tt()) -> c_10() 233.16/70.53 , 0^#() -> c_16() 233.16/70.53 , plus^#(X1, X2) -> c_15() 233.16/70.53 , s^#(X) -> c_14() } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 The following weak DPs constitute a sub-graph of the DG that is 233.16/70.53 closed under successors. The DPs are removed. 233.16/70.53 233.16/70.53 { U12^#(tt()) -> c_2() 233.16/70.53 , isNat^#(n__0()) -> c_3() 233.16/70.53 , activate^#(X) -> c_6() 233.16/70.53 , activate^#(n__0()) -> c_7(0^#()) 233.16/70.53 , U21^#(tt()) -> c_10() 233.16/70.53 , 0^#() -> c_16() 233.16/70.53 , plus^#(X1, X2) -> c_15() 233.16/70.53 , s^#(X) -> c_14() } 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_4(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , U31^#(tt(), N) -> c_11(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_12(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 Due to missing edges in the dependency-graph, the right-hand sides 233.16/70.53 of following rules could be simplified: 233.16/70.53 233.16/70.53 { U11^#(tt(), V2) -> 233.16/70.53 c_1(U12^#(isNat(activate(V2))), 233.16/70.53 isNat^#(activate(V2)), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> 233.16/70.53 c_5(U21^#(isNat(activate(V1))), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1)) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_8(plus^#(activate(X1), activate(X2)), 233.16/70.53 activate^#(X1), 233.16/70.53 activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X)) 233.16/70.53 , U42^#(tt(), M, N) -> 233.16/70.53 c_13(s^#(plus(activate(N), activate(M))), 233.16/70.53 plus^#(activate(N), activate(M)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M)) } 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.53 , U31^#(tt(), N) -> c_6(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , U31(tt(), N) -> activate(N) 233.16/70.53 , U41(tt(), M, N) -> 233.16/70.53 U42(isNat(activate(N)), activate(M), activate(N)) 233.16/70.53 , U42(tt(), M, N) -> s(plus(activate(N), activate(M))) 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 We replace rewrite rules by usable rules: 233.16/70.53 233.16/70.53 Weak Usable Rules: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.53 , U31^#(tt(), N) -> c_6(activate^#(N)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 Consider the dependency graph 233.16/70.53 233.16/70.53 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.53 -->_2 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_2 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_1 isNat^#(n__s(V1)) -> 233.16/70.53 c_3(isNat^#(activate(V1)), activate^#(V1)) :3 233.16/70.53 -->_1 isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) :2 233.16/70.53 233.16/70.53 2: isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 -->_4 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_3 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_4 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_3 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_2 isNat^#(n__s(V1)) -> 233.16/70.53 c_3(isNat^#(activate(V1)), activate^#(V1)) :3 233.16/70.53 -->_2 isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) :2 233.16/70.53 -->_1 U11^#(tt(), V2) -> 233.16/70.53 c_1(isNat^#(activate(V2)), activate^#(V2)) :1 233.16/70.53 233.16/70.53 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.53 -->_2 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_2 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_1 isNat^#(n__s(V1)) -> 233.16/70.53 c_3(isNat^#(activate(V1)), activate^#(V1)) :3 233.16/70.53 -->_1 isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) :2 233.16/70.53 233.16/70.53 4: activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) 233.16/70.53 -->_2 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_1 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_2 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_1 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 233.16/70.53 5: activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.53 -->_1 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_1 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 233.16/70.53 6: U31^#(tt(), N) -> c_6(activate^#(N)) 233.16/70.53 -->_1 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_1 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 233.16/70.53 7: U41^#(tt(), M, N) -> 233.16/70.53 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 -->_1 U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) :8 233.16/70.53 -->_5 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_4 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_3 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_5 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_4 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_3 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_2 isNat^#(n__s(V1)) -> 233.16/70.53 c_3(isNat^#(activate(V1)), activate^#(V1)) :3 233.16/70.53 -->_2 isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) :2 233.16/70.53 233.16/70.53 8: U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) 233.16/70.53 -->_2 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_1 activate^#(n__s(X)) -> c_5(activate^#(X)) :5 233.16/70.53 -->_2 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 -->_1 activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) :4 233.16/70.53 233.16/70.53 233.16/70.53 Following roots of the dependency graph are removed, as the 233.16/70.53 considered set of starting terms is closed under reduction with 233.16/70.53 respect to these rules (modulo compound contexts). 233.16/70.53 233.16/70.53 { U31^#(tt(), N) -> c_6(activate^#(N)) } 233.16/70.53 233.16/70.53 233.16/70.53 We are left with following problem, upon which TcT provides the 233.16/70.53 certificate YES(O(1),O(n^2)). 233.16/70.53 233.16/70.53 Strict DPs: 233.16/70.53 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.53 , isNat^#(n__plus(V1, V2)) -> 233.16/70.53 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.53 isNat^#(activate(V1)), 233.16/70.53 activate^#(V1), 233.16/70.53 activate^#(V2)) 233.16/70.53 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.53 , activate^#(n__plus(X1, X2)) -> 233.16/70.53 c_4(activate^#(X1), activate^#(X2)) 233.16/70.53 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.53 , U41^#(tt(), M, N) -> 233.16/70.53 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.53 isNat^#(activate(N)), 233.16/70.53 activate^#(N), 233.16/70.53 activate^#(M), 233.16/70.53 activate^#(N)) 233.16/70.53 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.53 Weak Trs: 233.16/70.53 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.53 , U12(tt()) -> tt() 233.16/70.53 , isNat(n__0()) -> tt() 233.16/70.53 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.53 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.53 , activate(X) -> X 233.16/70.53 , activate(n__0()) -> 0() 233.16/70.53 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.53 , activate(n__s(X)) -> s(activate(X)) 233.16/70.53 , U21(tt()) -> tt() 233.16/70.53 , s(X) -> n__s(X) 233.16/70.53 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.53 , 0() -> n__0() } 233.16/70.53 Obligation: 233.16/70.53 innermost runtime complexity 233.16/70.53 Answer: 233.16/70.53 YES(O(1),O(n^2)) 233.16/70.53 233.16/70.53 We analyse the complexity of following sub-problems (R) and (S). 233.16/70.53 Problem (S) is obtained from the input problem by shifting strict 233.16/70.53 rules from (R) into the weak component: 233.16/70.53 233.16/70.53 Problem (R): 233.16/70.54 ------------ 233.16/70.54 Strict DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 Problem (S): 233.16/70.54 ------------ 233.16/70.54 Strict DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.54 Weak DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 Overall, the transformation results in the following sub-problem(s): 233.16/70.54 233.16/70.54 Generated new problems: 233.16/70.54 ----------------------- 233.16/70.54 R) Strict DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 This problem was proven YES(O(1),O(n^2)). 233.16/70.54 233.16/70.54 S) Strict DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.54 Weak DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 This problem was proven YES(O(1),O(n^1)). 233.16/70.54 233.16/70.54 233.16/70.54 Proofs for generated problems: 233.16/70.54 ------------------------------ 233.16/70.54 R) We are left with following problem, upon which TcT provides the 233.16/70.54 certificate YES(O(1),O(n^2)). 233.16/70.54 233.16/70.54 Strict DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 Obligation: 233.16/70.54 innermost runtime complexity 233.16/70.54 Answer: 233.16/70.54 YES(O(1),O(n^2)) 233.16/70.54 233.16/70.54 We analyse the complexity of following sub-problems (R) and (S). 233.16/70.54 Problem (S) is obtained from the input problem by shifting strict 233.16/70.54 rules from (R) into the weak component: 233.16/70.54 233.16/70.54 Problem (R): 233.16/70.54 ------------ 233.16/70.54 Strict DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 Problem (S): 233.16/70.54 ------------ 233.16/70.54 Strict DPs: 233.16/70.54 { U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.54 , activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 Overall, the transformation results in the following sub-problem(s): 233.16/70.54 233.16/70.54 Generated new problems: 233.16/70.54 ----------------------- 233.16/70.54 R) Strict DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 This problem was proven YES(O(1),O(n^2)). 233.16/70.54 233.16/70.54 S) Strict DPs: 233.16/70.54 { U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.54 , activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 StartTerms: basic terms 233.16/70.54 Strategy: innermost 233.16/70.54 233.16/70.54 This problem was proven YES(O(1),O(1)). 233.16/70.54 233.16/70.54 233.16/70.54 Proofs for generated problems: 233.16/70.54 ------------------------------ 233.16/70.54 R) We are left with following problem, upon which TcT provides the 233.16/70.54 certificate YES(O(1),O(n^2)). 233.16/70.54 233.16/70.54 Strict DPs: 233.16/70.54 { activate^#(n__plus(X1, X2)) -> 233.16/70.54 c_4(activate^#(X1), activate^#(X2)) 233.16/70.54 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) } 233.16/70.54 Weak DPs: 233.16/70.54 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.54 , isNat^#(n__plus(V1, V2)) -> 233.16/70.54 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2)) 233.16/70.54 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.54 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.54 Weak Trs: 233.16/70.54 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.54 , U12(tt()) -> tt() 233.16/70.54 , isNat(n__0()) -> tt() 233.16/70.54 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.54 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.54 , activate(X) -> X 233.16/70.54 , activate(n__0()) -> 0() 233.16/70.54 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.54 , activate(n__s(X)) -> s(activate(X)) 233.16/70.54 , U21(tt()) -> tt() 233.16/70.54 , s(X) -> n__s(X) 233.16/70.54 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.54 , 0() -> n__0() } 233.16/70.54 Obligation: 233.16/70.54 innermost runtime complexity 233.16/70.54 Answer: 233.16/70.54 YES(O(1),O(n^2)) 233.16/70.54 233.16/70.54 We use the processor 'matrix interpretation of dimension 2' to 233.16/70.54 orient following rules strictly. 233.16/70.54 233.16/70.54 DPs: 233.16/70.54 { 2: activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.54 , 3: U41^#(tt(), M, N) -> 233.16/70.54 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.54 isNat^#(activate(N)), 233.16/70.54 activate^#(N), 233.16/70.54 activate^#(M), 233.16/70.54 activate^#(N)) } 233.16/70.54 233.16/70.54 Sub-proof: 233.16/70.54 ---------- 233.16/70.54 The following argument positions are usable: 233.16/70.54 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2, 3, 4}, 233.16/70.54 Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, 233.16/70.54 Uargs(c_7) = {1, 2, 3, 4, 5}, Uargs(c_8) = {1, 2} 233.16/70.54 233.16/70.54 TcT has computed the following constructor-based matrix 233.16/70.54 interpretation satisfying not(EDA). 233.16/70.54 233.16/70.54 [U11](x1, x2) = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [tt] = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [U12](x1) = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [isNat](x1) = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [activate](x1) = [1 0] x1 + [0] 233.16/70.54 [0 1] [0] 233.16/70.54 233.16/70.54 [U21](x1) = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [s](x1) = [1 4] x1 + [0] 233.16/70.54 [0 1] [1] 233.16/70.54 233.16/70.54 [plus](x1, x2) = [1 1] x1 + [1 4] x2 + [0] 233.16/70.54 [0 1] [0 1] [0] 233.16/70.54 233.16/70.54 [n__0] = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [n__plus](x1, x2) = [1 1] x1 + [1 4] x2 + [0] 233.16/70.54 [0 1] [0 1] [0] 233.16/70.54 233.16/70.54 [n__s](x1) = [1 4] x1 + [0] 233.16/70.54 [0 1] [1] 233.16/70.54 233.16/70.54 [0] = [0] 233.16/70.54 [0] 233.16/70.54 233.16/70.54 [U11^#](x1, x2) = [2 1] x2 + [0] 233.16/70.54 [4 0] [4] 233.16/70.54 233.16/70.54 [isNat^#](x1) = [2 0] x1 + [0] 233.16/70.54 [0 0] [4] 233.16/70.54 233.16/70.54 [activate^#](x1) = [0 1] x1 + [0] 233.16/70.54 [0 4] [0] 233.16/70.54 233.16/70.54 [U41^#](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 233.16/70.54 [7 5] [7 7] [7 7] [7] 233.16/70.54 233.16/70.54 [U42^#](x1, x2, x3) = [0 1] x2 + [0 1] x3 + [0] 233.16/70.54 [0 4] [4 4] [4] 233.16/70.54 233.16/70.54 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 233.16/70.54 [0 0] [0 0] [3] 233.16/70.54 233.16/70.54 [c_2](x1, x2, x3, x4) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 233.16/70.54 0] x4 + [0] 233.16/70.54 [0 0] [0 0] [0 0] [0 233.16/70.54 0] [3] 233.16/70.54 233.16/70.54 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 233.16/70.54 [0 0] [0 0] [3] 233.16/70.54 233.16/70.54 [c_4](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 233.16/70.54 [0 0] [0 0] [0] 233.16/70.54 233.16/70.54 [c_5](x1) = [1 0] x1 + [0] 233.16/70.54 [0 0] [3] 233.16/70.54 233.16/70.54 [c_7](x1, x2, x3, x4, x5) = [2 0] x1 + [1 0] x2 + [1 0] x3 + [1 233.16/70.54 0] x4 + [4 0] x5 + [3] 233.16/70.54 [0 0] [0 0] [0 0] [0 233.16/70.54 0] [0 0] [3] 233.16/70.54 233.16/70.54 [c_8](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 233.16/70.54 [0 0] [0 0] [3] 233.16/70.54 233.16/70.54 The order satisfies the following ordering constraints: 233.16/70.54 233.16/70.54 [U11(tt(), V2)] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [U12(isNat(activate(V2)))] 233.16/70.54 233.16/70.54 [U12(tt())] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [tt()] 233.16/70.54 233.16/70.54 [isNat(n__0())] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [tt()] 233.16/70.54 233.16/70.54 [isNat(n__plus(V1, V2))] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [U11(isNat(activate(V1)), activate(V2))] 233.16/70.54 233.16/70.54 [isNat(n__s(V1))] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [U21(isNat(activate(V1)))] 233.16/70.54 233.16/70.54 [activate(X)] = [1 0] X + [0] 233.16/70.54 [0 1] [0] 233.16/70.54 >= [1 0] X + [0] 233.16/70.54 [0 1] [0] 233.16/70.54 = [X] 233.16/70.54 233.16/70.54 [activate(n__0())] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [0()] 233.16/70.54 233.16/70.54 [activate(n__plus(X1, X2))] = [1 1] X1 + [1 4] X2 + [0] 233.16/70.54 [0 1] [0 1] [0] 233.16/70.54 >= [1 1] X1 + [1 4] X2 + [0] 233.16/70.54 [0 1] [0 1] [0] 233.16/70.54 = [plus(activate(X1), activate(X2))] 233.16/70.54 233.16/70.54 [activate(n__s(X))] = [1 4] X + [0] 233.16/70.54 [0 1] [1] 233.16/70.54 >= [1 4] X + [0] 233.16/70.54 [0 1] [1] 233.16/70.54 = [s(activate(X))] 233.16/70.54 233.16/70.54 [U21(tt())] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [tt()] 233.16/70.54 233.16/70.54 [s(X)] = [1 4] X + [0] 233.16/70.54 [0 1] [1] 233.16/70.54 >= [1 4] X + [0] 233.16/70.54 [0 1] [1] 233.16/70.54 = [n__s(X)] 233.16/70.54 233.16/70.54 [plus(X1, X2)] = [1 1] X1 + [1 4] X2 + [0] 233.16/70.54 [0 1] [0 1] [0] 233.16/70.54 >= [1 1] X1 + [1 4] X2 + [0] 233.16/70.54 [0 1] [0 1] [0] 233.16/70.54 = [n__plus(X1, X2)] 233.16/70.54 233.16/70.54 [0()] = [0] 233.16/70.54 [0] 233.16/70.54 >= [0] 233.16/70.54 [0] 233.16/70.54 = [n__0()] 233.16/70.54 233.16/70.54 [U11^#(tt(), V2)] = [2 1] V2 + [0] 233.16/70.54 [4 0] [4] 233.16/70.54 >= [2 1] V2 + [0] 233.16/70.54 [0 0] [3] 233.16/70.54 = [c_1(isNat^#(activate(V2)), activate^#(V2))] 233.16/70.54 233.16/70.54 [isNat^#(n__plus(V1, V2))] = [2 8] V2 + [2 2] V1 + [0] 233.16/70.54 [0 0] [0 0] [4] 233.16/70.54 >= [2 2] V2 + [2 1] V1 + [0] 233.16/70.54 [0 0] [0 0] [3] 233.16/70.54 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.54 isNat^#(activate(V1)), 233.16/70.54 activate^#(V1), 233.16/70.54 activate^#(V2))] 233.16/70.54 233.16/70.54 [isNat^#(n__s(V1))] = [2 8] V1 + [0] 233.16/70.54 [0 0] [4] 233.16/70.54 >= [2 1] V1 + [0] 233.16/70.55 [0 0] [3] 233.16/70.55 = [c_3(isNat^#(activate(V1)), activate^#(V1))] 233.16/70.55 233.16/70.55 [activate^#(n__plus(X1, X2))] = [0 1] X1 + [0 1] X2 + [0] 233.16/70.55 [0 4] [0 4] [0] 233.16/70.55 >= [0 1] X1 + [0 1] X2 + [0] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 = [c_4(activate^#(X1), activate^#(X2))] 233.16/70.55 233.16/70.55 [activate^#(n__s(X))] = [0 1] X + [1] 233.16/70.55 [0 4] [4] 233.16/70.55 > [0 1] X + [0] 233.16/70.55 [0 0] [3] 233.16/70.55 = [c_5(activate^#(X))] 233.16/70.55 233.16/70.55 [U41^#(tt(), M, N)] = [7 7] N + [7 7] M + [7] 233.16/70.55 [7 7] [7 7] [7] 233.16/70.55 > [2 7] N + [0 3] M + [3] 233.16/70.55 [0 0] [0 0] [3] 233.16/70.55 = [c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N))] 233.16/70.55 233.16/70.55 [U42^#(tt(), M, N)] = [0 1] N + [0 1] M + [0] 233.16/70.55 [4 4] [0 4] [4] 233.16/70.55 >= [0 1] N + [0 1] M + [0] 233.16/70.55 [0 0] [0 0] [3] 233.16/70.55 = [c_8(activate^#(N), activate^#(M))] 233.16/70.55 233.16/70.55 233.16/70.55 We return to the main proof. Consider the set of all dependency 233.16/70.55 pairs 233.16/70.55 233.16/70.55 : 233.16/70.55 { 1: activate^#(n__plus(X1, X2)) -> 233.16/70.55 c_4(activate^#(X1), activate^#(X2)) 233.16/70.55 , 2: activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.55 , 3: U41^#(tt(), M, N) -> 233.16/70.55 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N)) 233.16/70.55 , 4: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.55 , 5: isNat^#(n__plus(V1, V2)) -> 233.16/70.55 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2)) 233.16/70.55 , 6: isNat^#(n__s(V1)) -> 233.16/70.55 c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.55 , 7: U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.55 233.16/70.55 Processor 'matrix interpretation of dimension 2' induces the 233.16/70.55 complexity certificate YES(?,O(n^2)) on application of dependency 233.16/70.55 pairs {2,3}. These cover all (indirect) predecessors of dependency 233.16/70.55 pairs {2,3,7}, their number of application is equally bounded. The 233.16/70.55 dependency pairs are shifted into the weak component. 233.16/70.55 233.16/70.55 We are left with following problem, upon which TcT provides the 233.16/70.55 certificate YES(O(1),O(n^2)). 233.16/70.55 233.16/70.55 Strict DPs: 233.16/70.55 { activate^#(n__plus(X1, X2)) -> 233.16/70.55 c_4(activate^#(X1), activate^#(X2)) } 233.16/70.55 Weak DPs: 233.16/70.55 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.55 , isNat^#(n__plus(V1, V2)) -> 233.16/70.55 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2)) 233.16/70.55 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.55 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.55 , U41^#(tt(), M, N) -> 233.16/70.55 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N)) 233.16/70.55 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.55 Weak Trs: 233.16/70.55 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.55 , U12(tt()) -> tt() 233.16/70.55 , isNat(n__0()) -> tt() 233.16/70.55 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.55 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.55 , activate(X) -> X 233.16/70.55 , activate(n__0()) -> 0() 233.16/70.55 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.55 , activate(n__s(X)) -> s(activate(X)) 233.16/70.55 , U21(tt()) -> tt() 233.16/70.55 , s(X) -> n__s(X) 233.16/70.55 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.55 , 0() -> n__0() } 233.16/70.55 Obligation: 233.16/70.55 innermost runtime complexity 233.16/70.55 Answer: 233.16/70.55 YES(O(1),O(n^2)) 233.16/70.55 233.16/70.55 We use the processor 'matrix interpretation of dimension 2' to 233.16/70.55 orient following rules strictly. 233.16/70.55 233.16/70.55 DPs: 233.16/70.55 { 1: activate^#(n__plus(X1, X2)) -> 233.16/70.55 c_4(activate^#(X1), activate^#(X2)) 233.16/70.55 , 6: U41^#(tt(), M, N) -> 233.16/70.55 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N)) } 233.16/70.55 Trs: 233.16/70.55 { isNat(n__0()) -> tt() 233.16/70.55 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.55 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) } 233.16/70.55 233.16/70.55 Sub-proof: 233.16/70.55 ---------- 233.16/70.55 The following argument positions are usable: 233.16/70.55 Uargs(c_1) = {1, 2}, Uargs(c_2) = {1, 2, 3, 4}, 233.16/70.55 Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, 233.16/70.55 Uargs(c_7) = {1, 2, 3, 4, 5}, Uargs(c_8) = {1, 2} 233.16/70.55 233.16/70.55 TcT has computed the following constructor-based matrix 233.16/70.55 interpretation satisfying not(EDA). 233.16/70.55 233.16/70.55 [U11](x1, x2) = [0] 233.16/70.55 [0] 233.16/70.55 233.16/70.55 [tt] = [0] 233.16/70.55 [0] 233.16/70.55 233.16/70.55 [U12](x1) = [0] 233.16/70.55 [0] 233.16/70.55 233.16/70.55 [isNat](x1) = [0 0] x1 + [4] 233.16/70.55 [0 1] [0] 233.16/70.55 233.16/70.55 [activate](x1) = [1 0] x1 + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 233.16/70.55 [U21](x1) = [0] 233.16/70.55 [0] 233.16/70.55 233.16/70.55 [s](x1) = [1 4] x1 + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 233.16/70.55 [plus](x1, x2) = [1 4] x1 + [1 2] x2 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 233.16/70.55 [n__0] = [0] 233.16/70.55 [4] 233.16/70.55 233.16/70.55 [n__plus](x1, x2) = [1 4] x1 + [1 2] x2 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 233.16/70.55 [n__s](x1) = [1 4] x1 + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 233.16/70.55 [0] = [0] 233.16/70.55 [4] 233.16/70.55 233.16/70.55 [U11^#](x1, x2) = [0 0] x1 + [1 1] x2 + [0] 233.16/70.55 [0 2] [0 0] [0] 233.16/70.55 233.16/70.55 [isNat^#](x1) = [1 0] x1 + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 233.16/70.55 [activate^#](x1) = [0 1] x1 + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 233.16/70.55 [U41^#](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 233.16/70.55 [7 5] [7 7] [7 7] [7] 233.16/70.55 233.16/70.55 [U42^#](x1, x2, x3) = [0 1] x2 + [4 4] x3 + [0] 233.16/70.55 [4 0] [0 0] [0] 233.16/70.55 233.16/70.55 [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 233.16/70.55 [c_2](x1, x2, x3, x4) = [1 1] x1 + [1 1] x2 + [1 0] x3 + [1 233.16/70.55 0] x4 + [0] 233.16/70.55 [0 0] [0 0] [0 0] [0 233.16/70.55 0] [3] 233.16/70.55 233.16/70.55 [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 233.16/70.55 [c_4](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 233.16/70.55 [c_5](x1) = [1 0] x1 + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 233.16/70.55 [c_7](x1, x2, x3, x4, x5) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 233.16/70.55 0] x4 + [2 0] x5 + [3] 233.16/70.55 [0 0] [0 0] [0 0] [0 233.16/70.55 0] [0 0] [3] 233.16/70.55 233.16/70.55 [c_8](x1, x2) = [2 0] x1 + [1 0] x2 + [0] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 233.16/70.55 The order satisfies the following ordering constraints: 233.16/70.55 233.16/70.55 [U11(tt(), V2)] = [0] 233.16/70.55 [0] 233.16/70.55 >= [0] 233.16/70.55 [0] 233.16/70.55 = [U12(isNat(activate(V2)))] 233.16/70.55 233.16/70.55 [U12(tt())] = [0] 233.16/70.55 [0] 233.16/70.55 >= [0] 233.16/70.55 [0] 233.16/70.55 = [tt()] 233.16/70.55 233.16/70.55 [isNat(n__0())] = [4] 233.16/70.55 [4] 233.16/70.55 > [0] 233.16/70.55 [0] 233.16/70.55 = [tt()] 233.16/70.55 233.16/70.55 [isNat(n__plus(V1, V2))] = [0 0] V2 + [0 0] V1 + [4] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 > [0] 233.16/70.55 [0] 233.16/70.55 = [U11(isNat(activate(V1)), activate(V2))] 233.16/70.55 233.16/70.55 [isNat(n__s(V1))] = [0 0] V1 + [4] 233.16/70.55 [0 1] [0] 233.16/70.55 > [0] 233.16/70.55 [0] 233.16/70.55 = [U21(isNat(activate(V1)))] 233.16/70.55 233.16/70.55 [activate(X)] = [1 0] X + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 >= [1 0] X + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 = [X] 233.16/70.55 233.16/70.55 [activate(n__0())] = [0] 233.16/70.55 [4] 233.16/70.55 >= [0] 233.16/70.55 [4] 233.16/70.55 = [0()] 233.16/70.55 233.16/70.55 [activate(n__plus(X1, X2))] = [1 4] X1 + [1 2] X2 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 >= [1 4] X1 + [1 2] X2 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 = [plus(activate(X1), activate(X2))] 233.16/70.55 233.16/70.55 [activate(n__s(X))] = [1 4] X + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 >= [1 4] X + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 = [s(activate(X))] 233.16/70.55 233.16/70.55 [U21(tt())] = [0] 233.16/70.55 [0] 233.16/70.55 >= [0] 233.16/70.55 [0] 233.16/70.55 = [tt()] 233.16/70.55 233.16/70.55 [s(X)] = [1 4] X + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 >= [1 4] X + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 = [n__s(X)] 233.16/70.55 233.16/70.55 [plus(X1, X2)] = [1 4] X1 + [1 2] X2 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 >= [1 4] X1 + [1 2] X2 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 = [n__plus(X1, X2)] 233.16/70.55 233.16/70.55 [0()] = [0] 233.16/70.55 [4] 233.16/70.55 >= [0] 233.16/70.55 [4] 233.16/70.55 = [n__0()] 233.16/70.55 233.16/70.55 [U11^#(tt(), V2)] = [1 1] V2 + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 >= [1 1] V2 + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 = [c_1(isNat^#(activate(V2)), activate^#(V2))] 233.16/70.55 233.16/70.55 [isNat^#(n__plus(V1, V2))] = [1 2] V2 + [1 4] V1 + [0] 233.16/70.55 [0 1] [0 1] [4] 233.16/70.55 >= [1 2] V2 + [1 4] V1 + [0] 233.16/70.55 [0 0] [0 0] [3] 233.16/70.55 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2))] 233.16/70.55 233.16/70.55 [isNat^#(n__s(V1))] = [1 4] V1 + [0] 233.16/70.55 [0 1] [0] 233.16/70.55 >= [1 1] V1 + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 = [c_3(isNat^#(activate(V1)), activate^#(V1))] 233.16/70.55 233.16/70.55 [activate^#(n__plus(X1, X2))] = [0 1] X1 + [0 1] X2 + [4] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 > [0 1] X1 + [0 1] X2 + [1] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 = [c_4(activate^#(X1), activate^#(X2))] 233.16/70.55 233.16/70.55 [activate^#(n__s(X))] = [0 1] X + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 >= [0 1] X + [0] 233.16/70.55 [0 0] [0] 233.16/70.55 = [c_5(activate^#(X))] 233.16/70.55 233.16/70.55 [U41^#(tt(), M, N)] = [7 7] N + [7 7] M + [7] 233.16/70.55 [7 7] [7 7] [7] 233.16/70.55 > [5 7] N + [0 2] M + [3] 233.16/70.55 [0 0] [0 0] [3] 233.16/70.55 = [c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N))] 233.16/70.55 233.16/70.55 [U42^#(tt(), M, N)] = [4 4] N + [0 1] M + [0] 233.16/70.55 [0 0] [4 0] [0] 233.16/70.55 >= [0 2] N + [0 1] M + [0] 233.16/70.55 [0 0] [0 0] [0] 233.16/70.55 = [c_8(activate^#(N), activate^#(M))] 233.16/70.55 233.16/70.55 233.16/70.55 We return to the main proof. Consider the set of all dependency 233.16/70.55 pairs 233.16/70.55 233.16/70.55 : 233.16/70.55 { 1: activate^#(n__plus(X1, X2)) -> 233.16/70.55 c_4(activate^#(X1), activate^#(X2)) 233.16/70.55 , 2: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.55 , 3: isNat^#(n__plus(V1, V2)) -> 233.16/70.55 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2)) 233.16/70.55 , 4: isNat^#(n__s(V1)) -> 233.16/70.55 c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.55 , 5: activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.55 , 6: U41^#(tt(), M, N) -> 233.16/70.55 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N)) 233.16/70.55 , 7: U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.55 233.16/70.55 Processor 'matrix interpretation of dimension 2' induces the 233.16/70.55 complexity certificate YES(?,O(n^2)) on application of dependency 233.16/70.55 pairs {1,6}. These cover all (indirect) predecessors of dependency 233.16/70.55 pairs {1,6,7}, their number of application is equally bounded. The 233.16/70.55 dependency pairs are shifted into the weak component. 233.16/70.55 233.16/70.55 We are left with following problem, upon which TcT provides the 233.16/70.55 certificate YES(O(1),O(1)). 233.16/70.55 233.16/70.55 Weak DPs: 233.16/70.55 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.55 , isNat^#(n__plus(V1, V2)) -> 233.16/70.55 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2)) 233.16/70.55 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.55 , activate^#(n__plus(X1, X2)) -> 233.16/70.55 c_4(activate^#(X1), activate^#(X2)) 233.16/70.55 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.55 , U41^#(tt(), M, N) -> 233.16/70.55 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N)) 233.16/70.55 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.55 Weak Trs: 233.16/70.55 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.55 , U12(tt()) -> tt() 233.16/70.55 , isNat(n__0()) -> tt() 233.16/70.55 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.55 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.55 , activate(X) -> X 233.16/70.55 , activate(n__0()) -> 0() 233.16/70.55 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.55 , activate(n__s(X)) -> s(activate(X)) 233.16/70.55 , U21(tt()) -> tt() 233.16/70.55 , s(X) -> n__s(X) 233.16/70.55 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.55 , 0() -> n__0() } 233.16/70.55 Obligation: 233.16/70.55 innermost runtime complexity 233.16/70.55 Answer: 233.16/70.55 YES(O(1),O(1)) 233.16/70.55 233.16/70.55 The following weak DPs constitute a sub-graph of the DG that is 233.16/70.55 closed under successors. The DPs are removed. 233.16/70.55 233.16/70.55 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.55 , isNat^#(n__plus(V1, V2)) -> 233.16/70.55 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2)) 233.16/70.55 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.55 , activate^#(n__plus(X1, X2)) -> 233.16/70.55 c_4(activate^#(X1), activate^#(X2)) 233.16/70.55 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.55 , U41^#(tt(), M, N) -> 233.16/70.55 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.55 isNat^#(activate(N)), 233.16/70.55 activate^#(N), 233.16/70.55 activate^#(M), 233.16/70.55 activate^#(N)) 233.16/70.55 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.55 233.16/70.55 We are left with following problem, upon which TcT provides the 233.16/70.55 certificate YES(O(1),O(1)). 233.16/70.55 233.16/70.55 Weak Trs: 233.16/70.55 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.55 , U12(tt()) -> tt() 233.16/70.55 , isNat(n__0()) -> tt() 233.16/70.55 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.55 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.55 , activate(X) -> X 233.16/70.55 , activate(n__0()) -> 0() 233.16/70.55 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.55 , activate(n__s(X)) -> s(activate(X)) 233.16/70.55 , U21(tt()) -> tt() 233.16/70.55 , s(X) -> n__s(X) 233.16/70.55 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.55 , 0() -> n__0() } 233.16/70.55 Obligation: 233.16/70.55 innermost runtime complexity 233.16/70.55 Answer: 233.16/70.55 YES(O(1),O(1)) 233.16/70.55 233.16/70.55 No rule is usable, rules are removed from the input problem. 233.16/70.55 233.16/70.55 We are left with following problem, upon which TcT provides the 233.16/70.55 certificate YES(O(1),O(1)). 233.16/70.55 233.16/70.55 Rules: Empty 233.16/70.55 Obligation: 233.16/70.55 innermost runtime complexity 233.16/70.55 Answer: 233.16/70.55 YES(O(1),O(1)) 233.16/70.55 233.16/70.55 Empty rules are trivially bounded 233.16/70.55 233.16/70.55 S) We are left with following problem, upon which TcT provides the 233.16/70.55 certificate YES(O(1),O(1)). 233.16/70.55 233.16/70.55 Strict DPs: 233.16/70.55 { U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.55 Weak DPs: 233.16/70.55 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.55 , isNat^#(n__plus(V1, V2)) -> 233.16/70.55 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.55 isNat^#(activate(V1)), 233.16/70.55 activate^#(V1), 233.16/70.55 activate^#(V2)) 233.16/70.55 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.56 , activate^#(n__plus(X1, X2)) -> 233.16/70.56 c_4(activate^#(X1), activate^#(X2)) 233.16/70.56 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.56 , U41^#(tt(), M, N) -> 233.16/70.56 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.56 isNat^#(activate(N)), 233.16/70.56 activate^#(N), 233.16/70.56 activate^#(M), 233.16/70.56 activate^#(N)) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 The following weak DPs constitute a sub-graph of the DG that is 233.16/70.56 closed under successors. The DPs are removed. 233.16/70.56 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1)), 233.16/70.56 activate^#(V1), 233.16/70.56 activate^#(V2)) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.56 , activate^#(n__plus(X1, X2)) -> 233.16/70.56 c_4(activate^#(X1), activate^#(X2)) 233.16/70.56 , activate^#(n__s(X)) -> c_5(activate^#(X)) } 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Strict DPs: 233.16/70.56 { U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.56 Weak DPs: 233.16/70.56 { U41^#(tt(), M, N) -> 233.16/70.56 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.56 isNat^#(activate(N)), 233.16/70.56 activate^#(N), 233.16/70.56 activate^#(M), 233.16/70.56 activate^#(N)) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 Due to missing edges in the dependency-graph, the right-hand sides 233.16/70.56 of following rules could be simplified: 233.16/70.56 233.16/70.56 { U41^#(tt(), M, N) -> 233.16/70.56 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.56 isNat^#(activate(N)), 233.16/70.56 activate^#(N), 233.16/70.56 activate^#(M), 233.16/70.56 activate^#(N)) 233.16/70.56 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Strict DPs: { U42^#(tt(), M, N) -> c_1() } 233.16/70.56 Weak DPs: 233.16/70.56 { U41^#(tt(), M, N) -> 233.16/70.56 c_2(U42^#(isNat(activate(N)), activate(M), activate(N))) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 The dependency graph contains no loops, we remove all dependency 233.16/70.56 pairs. 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 No rule is usable, rules are removed from the input problem. 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Rules: Empty 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 Empty rules are trivially bounded 233.16/70.56 233.16/70.56 233.16/70.56 S) We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(n^1)). 233.16/70.56 233.16/70.56 Strict DPs: 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1)), 233.16/70.56 activate^#(V1), 233.16/70.56 activate^#(V2)) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.56 Weak DPs: 233.16/70.56 { activate^#(n__plus(X1, X2)) -> 233.16/70.56 c_4(activate^#(X1), activate^#(X2)) 233.16/70.56 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.56 , U41^#(tt(), M, N) -> 233.16/70.56 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.56 isNat^#(activate(N)), 233.16/70.56 activate^#(N), 233.16/70.56 activate^#(M), 233.16/70.56 activate^#(N)) 233.16/70.56 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(n^1)) 233.16/70.56 233.16/70.56 The following weak DPs constitute a sub-graph of the DG that is 233.16/70.56 closed under successors. The DPs are removed. 233.16/70.56 233.16/70.56 { activate^#(n__plus(X1, X2)) -> 233.16/70.56 c_4(activate^#(X1), activate^#(X2)) 233.16/70.56 , activate^#(n__s(X)) -> c_5(activate^#(X)) 233.16/70.56 , U42^#(tt(), M, N) -> c_8(activate^#(N), activate^#(M)) } 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(n^1)). 233.16/70.56 233.16/70.56 Strict DPs: 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1)), 233.16/70.56 activate^#(V1), 233.16/70.56 activate^#(V2)) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) } 233.16/70.56 Weak DPs: 233.16/70.56 { U41^#(tt(), M, N) -> 233.16/70.56 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.56 isNat^#(activate(N)), 233.16/70.56 activate^#(N), 233.16/70.56 activate^#(M), 233.16/70.56 activate^#(N)) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(n^1)) 233.16/70.56 233.16/70.56 Due to missing edges in the dependency-graph, the right-hand sides 233.16/70.56 of following rules could be simplified: 233.16/70.56 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2)), activate^#(V2)) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1)), 233.16/70.56 activate^#(V1), 233.16/70.56 activate^#(V2)) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1)), activate^#(V1)) 233.16/70.56 , U41^#(tt(), M, N) -> 233.16/70.56 c_7(U42^#(isNat(activate(N)), activate(M), activate(N)), 233.16/70.56 isNat^#(activate(N)), 233.16/70.56 activate^#(N), 233.16/70.56 activate^#(M), 233.16/70.56 activate^#(N)) } 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(n^1)). 233.16/70.56 233.16/70.56 Strict DPs: 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1))) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) } 233.16/70.56 Weak DPs: { U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(n^1)) 233.16/70.56 233.16/70.56 We use the processor 'matrix interpretation of dimension 1' to 233.16/70.56 orient following rules strictly. 233.16/70.56 233.16/70.56 DPs: 233.16/70.56 { 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 233.16/70.56 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 233.16/70.56 Sub-proof: 233.16/70.56 ---------- 233.16/70.56 The following argument positions are usable: 233.16/70.56 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 233.16/70.56 Uargs(c_4) = {1} 233.16/70.56 233.16/70.56 TcT has computed the following constructor-based matrix 233.16/70.56 interpretation satisfying not(EDA). 233.16/70.56 233.16/70.56 [U11](x1, x2) = [0] 233.16/70.56 233.16/70.56 [tt] = [0] 233.16/70.56 233.16/70.56 [U12](x1) = [0] 233.16/70.56 233.16/70.56 [isNat](x1) = [0] 233.16/70.56 233.16/70.56 [activate](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [U21](x1) = [0] 233.16/70.56 233.16/70.56 [s](x1) = [1] x1 + [2] 233.16/70.56 233.16/70.56 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 233.16/70.56 233.16/70.56 [n__0] = [0] 233.16/70.56 233.16/70.56 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 233.16/70.56 233.16/70.56 [n__s](x1) = [1] x1 + [2] 233.16/70.56 233.16/70.56 [0] = [0] 233.16/70.56 233.16/70.56 [U11^#](x1, x2) = [2] x2 + [0] 233.16/70.56 233.16/70.56 [isNat^#](x1) = [2] x1 + [0] 233.16/70.56 233.16/70.56 [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 233.16/70.56 233.16/70.56 [c_1](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [c_2](x1, x2) = [1] x1 + [1] x2 + [0] 233.16/70.56 233.16/70.56 [c_3](x1) = [1] x1 + [1] 233.16/70.56 233.16/70.56 [c_4](x1) = [2] x1 + [3] 233.16/70.56 233.16/70.56 The order satisfies the following ordering constraints: 233.16/70.56 233.16/70.56 [U11(tt(), V2)] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [U12(isNat(activate(V2)))] 233.16/70.56 233.16/70.56 [U12(tt())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [tt()] 233.16/70.56 233.16/70.56 [isNat(n__0())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [tt()] 233.16/70.56 233.16/70.56 [isNat(n__plus(V1, V2))] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [U11(isNat(activate(V1)), activate(V2))] 233.16/70.56 233.16/70.56 [isNat(n__s(V1))] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [U21(isNat(activate(V1)))] 233.16/70.56 233.16/70.56 [activate(X)] = [1] X + [0] 233.16/70.56 >= [1] X + [0] 233.16/70.56 = [X] 233.16/70.56 233.16/70.56 [activate(n__0())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [0()] 233.16/70.56 233.16/70.56 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 233.16/70.56 >= [1] X1 + [1] X2 + [0] 233.16/70.56 = [plus(activate(X1), activate(X2))] 233.16/70.56 233.16/70.56 [activate(n__s(X))] = [1] X + [2] 233.16/70.56 >= [1] X + [2] 233.16/70.56 = [s(activate(X))] 233.16/70.56 233.16/70.56 [U21(tt())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [tt()] 233.16/70.56 233.16/70.56 [s(X)] = [1] X + [2] 233.16/70.56 >= [1] X + [2] 233.16/70.56 = [n__s(X)] 233.16/70.56 233.16/70.56 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 233.16/70.56 >= [1] X1 + [1] X2 + [0] 233.16/70.56 = [n__plus(X1, X2)] 233.16/70.56 233.16/70.56 [0()] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [n__0()] 233.16/70.56 233.16/70.56 [U11^#(tt(), V2)] = [2] V2 + [0] 233.16/70.56 >= [2] V2 + [0] 233.16/70.56 = [c_1(isNat^#(activate(V2)))] 233.16/70.56 233.16/70.56 [isNat^#(n__plus(V1, V2))] = [2] V2 + [2] V1 + [0] 233.16/70.56 >= [2] V2 + [2] V1 + [0] 233.16/70.56 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1)))] 233.16/70.56 233.16/70.56 [isNat^#(n__s(V1))] = [2] V1 + [4] 233.16/70.56 > [2] V1 + [1] 233.16/70.56 = [c_3(isNat^#(activate(V1)))] 233.16/70.56 233.16/70.56 [U41^#(tt(), M, N)] = [7] N + [7] M + [7] 233.16/70.56 > [4] N + [3] 233.16/70.56 = [c_4(isNat^#(activate(N)))] 233.16/70.56 233.16/70.56 233.16/70.56 The strictly oriented rules are moved into the weak component. 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(n^1)). 233.16/70.56 233.16/70.56 Strict DPs: 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1))) } 233.16/70.56 Weak DPs: 233.16/70.56 { isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 233.16/70.56 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(n^1)) 233.16/70.56 233.16/70.56 We use the processor 'matrix interpretation of dimension 1' to 233.16/70.56 orient following rules strictly. 233.16/70.56 233.16/70.56 DPs: 233.16/70.56 { 2: isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1))) 233.16/70.56 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 233.16/70.56 Sub-proof: 233.16/70.56 ---------- 233.16/70.56 The following argument positions are usable: 233.16/70.56 Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, 233.16/70.56 Uargs(c_4) = {1} 233.16/70.56 233.16/70.56 TcT has computed the following constructor-based matrix 233.16/70.56 interpretation satisfying not(EDA). 233.16/70.56 233.16/70.56 [U11](x1, x2) = [0] 233.16/70.56 233.16/70.56 [tt] = [0] 233.16/70.56 233.16/70.56 [U12](x1) = [0] 233.16/70.56 233.16/70.56 [isNat](x1) = [0] 233.16/70.56 233.16/70.56 [activate](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [U21](x1) = [0] 233.16/70.56 233.16/70.56 [s](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [plus](x1, x2) = [1] x1 + [1] x2 + [2] 233.16/70.56 233.16/70.56 [n__0] = [0] 233.16/70.56 233.16/70.56 [n__plus](x1, x2) = [1] x1 + [1] x2 + [2] 233.16/70.56 233.16/70.56 [n__s](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [0] = [0] 233.16/70.56 233.16/70.56 [U11^#](x1, x2) = [1] x2 + [0] 233.16/70.56 233.16/70.56 [isNat^#](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 233.16/70.56 233.16/70.56 [c_1](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [c_2](x1, x2) = [1] x1 + [1] x2 + [1] 233.16/70.56 233.16/70.56 [c_3](x1) = [1] x1 + [0] 233.16/70.56 233.16/70.56 [c_4](x1) = [1] x1 + [3] 233.16/70.56 233.16/70.56 The order satisfies the following ordering constraints: 233.16/70.56 233.16/70.56 [U11(tt(), V2)] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [U12(isNat(activate(V2)))] 233.16/70.56 233.16/70.56 [U12(tt())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [tt()] 233.16/70.56 233.16/70.56 [isNat(n__0())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [tt()] 233.16/70.56 233.16/70.56 [isNat(n__plus(V1, V2))] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [U11(isNat(activate(V1)), activate(V2))] 233.16/70.56 233.16/70.56 [isNat(n__s(V1))] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [U21(isNat(activate(V1)))] 233.16/70.56 233.16/70.56 [activate(X)] = [1] X + [0] 233.16/70.56 >= [1] X + [0] 233.16/70.56 = [X] 233.16/70.56 233.16/70.56 [activate(n__0())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [0()] 233.16/70.56 233.16/70.56 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [2] 233.16/70.56 >= [1] X1 + [1] X2 + [2] 233.16/70.56 = [plus(activate(X1), activate(X2))] 233.16/70.56 233.16/70.56 [activate(n__s(X))] = [1] X + [0] 233.16/70.56 >= [1] X + [0] 233.16/70.56 = [s(activate(X))] 233.16/70.56 233.16/70.56 [U21(tt())] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [tt()] 233.16/70.56 233.16/70.56 [s(X)] = [1] X + [0] 233.16/70.56 >= [1] X + [0] 233.16/70.56 = [n__s(X)] 233.16/70.56 233.16/70.56 [plus(X1, X2)] = [1] X1 + [1] X2 + [2] 233.16/70.56 >= [1] X1 + [1] X2 + [2] 233.16/70.56 = [n__plus(X1, X2)] 233.16/70.56 233.16/70.56 [0()] = [0] 233.16/70.56 >= [0] 233.16/70.56 = [n__0()] 233.16/70.56 233.16/70.56 [U11^#(tt(), V2)] = [1] V2 + [0] 233.16/70.56 >= [1] V2 + [0] 233.16/70.56 = [c_1(isNat^#(activate(V2)))] 233.16/70.56 233.16/70.56 [isNat^#(n__plus(V1, V2))] = [1] V2 + [1] V1 + [2] 233.16/70.56 > [1] V2 + [1] V1 + [1] 233.16/70.56 = [c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1)))] 233.16/70.56 233.16/70.56 [isNat^#(n__s(V1))] = [1] V1 + [0] 233.16/70.56 >= [1] V1 + [0] 233.16/70.56 = [c_3(isNat^#(activate(V1)))] 233.16/70.56 233.16/70.56 [U41^#(tt(), M, N)] = [7] N + [7] M + [7] 233.16/70.56 > [1] N + [3] 233.16/70.56 = [c_4(isNat^#(activate(N)))] 233.16/70.56 233.16/70.56 233.16/70.56 We return to the main proof. Consider the set of all dependency 233.16/70.56 pairs 233.16/70.56 233.16/70.56 : 233.16/70.56 { 1: U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 233.16/70.56 , 2: isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1))) 233.16/70.56 , 3: isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 233.16/70.56 , 4: U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 233.16/70.56 Processor 'matrix interpretation of dimension 1' induces the 233.16/70.56 complexity certificate YES(?,O(n^1)) on application of dependency 233.16/70.56 pairs {2,4}. These cover all (indirect) predecessors of dependency 233.16/70.56 pairs {1,2,4}, their number of application is equally bounded. The 233.16/70.56 dependency pairs are shifted into the weak component. 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Weak DPs: 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1))) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 233.16/70.56 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 The following weak DPs constitute a sub-graph of the DG that is 233.16/70.56 closed under successors. The DPs are removed. 233.16/70.56 233.16/70.56 { U11^#(tt(), V2) -> c_1(isNat^#(activate(V2))) 233.16/70.56 , isNat^#(n__plus(V1, V2)) -> 233.16/70.56 c_2(U11^#(isNat(activate(V1)), activate(V2)), 233.16/70.56 isNat^#(activate(V1))) 233.16/70.56 , isNat^#(n__s(V1)) -> c_3(isNat^#(activate(V1))) 233.16/70.56 , U41^#(tt(), M, N) -> c_4(isNat^#(activate(N))) } 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Weak Trs: 233.16/70.56 { U11(tt(), V2) -> U12(isNat(activate(V2))) 233.16/70.56 , U12(tt()) -> tt() 233.16/70.56 , isNat(n__0()) -> tt() 233.16/70.56 , isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2)) 233.16/70.56 , isNat(n__s(V1)) -> U21(isNat(activate(V1))) 233.16/70.56 , activate(X) -> X 233.16/70.56 , activate(n__0()) -> 0() 233.16/70.56 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 233.16/70.56 , activate(n__s(X)) -> s(activate(X)) 233.16/70.56 , U21(tt()) -> tt() 233.16/70.56 , s(X) -> n__s(X) 233.16/70.56 , plus(X1, X2) -> n__plus(X1, X2) 233.16/70.56 , 0() -> n__0() } 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 No rule is usable, rules are removed from the input problem. 233.16/70.56 233.16/70.56 We are left with following problem, upon which TcT provides the 233.16/70.56 certificate YES(O(1),O(1)). 233.16/70.56 233.16/70.56 Rules: Empty 233.16/70.56 Obligation: 233.16/70.56 innermost runtime complexity 233.16/70.56 Answer: 233.16/70.56 YES(O(1),O(1)) 233.16/70.56 233.16/70.56 Empty rules are trivially bounded 233.16/70.56 233.16/70.56 233.16/70.56 Hurray, we answered YES(O(1),O(n^2)) 233.36/70.62 EOF