YES(O(1),O(n^2)) 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(posrecip(Y), 2ndsneg(N, activate(Z))) 153.33/71.88 , 2ndspos(0(), Z) -> rnil() 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(negrecip(Y), 2ndspos(N, activate(Z))) 153.33/71.88 , 2ndsneg(0(), Z) -> rnil() 153.33/71.88 , pi(X) -> 2ndspos(X, from(0())) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() 153.33/71.88 , square(X) -> times(X, X) } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 We add the following dependency tuples: 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { from^#(X) -> c_1() 153.33/71.88 , from^#(X) -> c_2() 153.33/71.88 , 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , activate^#(X) -> c_6() 153.33/71.88 , activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , plus^#(0(), Y) -> c_13() 153.33/71.88 , times^#(s(X), Y) -> c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , times^#(0(), Y) -> c_15() 153.33/71.88 , square^#(X) -> c_16(times^#(X, X)) } 153.33/71.88 153.33/71.88 and mark the set of starting terms. 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { from^#(X) -> c_1() 153.33/71.88 , from^#(X) -> c_2() 153.33/71.88 , 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , activate^#(X) -> c_6() 153.33/71.88 , activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , plus^#(0(), Y) -> c_13() 153.33/71.88 , times^#(s(X), Y) -> c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , times^#(0(), Y) -> c_15() 153.33/71.88 , square^#(X) -> c_16(times^#(X, X)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(posrecip(Y), 2ndsneg(N, activate(Z))) 153.33/71.88 , 2ndspos(0(), Z) -> rnil() 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(negrecip(Y), 2ndspos(N, activate(Z))) 153.33/71.88 , 2ndsneg(0(), Z) -> rnil() 153.33/71.88 , pi(X) -> 2ndspos(X, from(0())) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() 153.33/71.88 , square(X) -> times(X, X) } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 We estimate the number of application of {1,2,5,6,10,13,15} by 153.33/71.88 applications of Pre({1,2,5,6,10,13,15}) = {3,4,7,8,9,11,12,14,16}. 153.33/71.88 Here rules are labeled as follows: 153.33/71.88 153.33/71.88 DPs: 153.33/71.88 { 1: from^#(X) -> c_1() 153.33/71.88 , 2: from^#(X) -> c_2() 153.33/71.88 , 3: 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 4: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 5: 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , 6: activate^#(X) -> c_6() 153.33/71.88 , 7: activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 8: 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 9: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 10: 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , 11: pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , 12: plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , 13: plus^#(0(), Y) -> c_13() 153.33/71.88 , 14: times^#(s(X), Y) -> 153.33/71.88 c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , 15: times^#(0(), Y) -> c_15() 153.33/71.88 , 16: square^#(X) -> c_16(times^#(X, X)) } 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , square^#(X) -> c_16(times^#(X, X)) } 153.33/71.88 Weak DPs: 153.33/71.88 { from^#(X) -> c_1() 153.33/71.88 , from^#(X) -> c_2() 153.33/71.88 , 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , activate^#(X) -> c_6() 153.33/71.88 , 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , plus^#(0(), Y) -> c_13() 153.33/71.88 , times^#(0(), Y) -> c_15() } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(posrecip(Y), 2ndsneg(N, activate(Z))) 153.33/71.88 , 2ndspos(0(), Z) -> rnil() 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(negrecip(Y), 2ndspos(N, activate(Z))) 153.33/71.88 , 2ndsneg(0(), Z) -> rnil() 153.33/71.88 , pi(X) -> 2ndspos(X, from(0())) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() 153.33/71.88 , square(X) -> times(X, X) } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 We estimate the number of application of {3} by applications of 153.33/71.88 Pre({3}) = {1,2,4,5}. Here rules are labeled as follows: 153.33/71.88 153.33/71.88 DPs: 153.33/71.88 { 1: 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 3: activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 4: 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 5: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 6: pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , 7: plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , 8: times^#(s(X), Y) -> 153.33/71.88 c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , 9: square^#(X) -> c_16(times^#(X, X)) 153.33/71.88 , 10: from^#(X) -> c_1() 153.33/71.88 , 11: from^#(X) -> c_2() 153.33/71.88 , 12: 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , 13: activate^#(X) -> c_6() 153.33/71.88 , 14: 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , 15: plus^#(0(), Y) -> c_13() 153.33/71.88 , 16: times^#(0(), Y) -> c_15() } 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , square^#(X) -> c_16(times^#(X, X)) } 153.33/71.88 Weak DPs: 153.33/71.88 { from^#(X) -> c_1() 153.33/71.88 , from^#(X) -> c_2() 153.33/71.88 , 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , activate^#(X) -> c_6() 153.33/71.88 , activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , plus^#(0(), Y) -> c_13() 153.33/71.88 , times^#(0(), Y) -> c_15() } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(posrecip(Y), 2ndsneg(N, activate(Z))) 153.33/71.88 , 2ndspos(0(), Z) -> rnil() 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(negrecip(Y), 2ndspos(N, activate(Z))) 153.33/71.88 , 2ndsneg(0(), Z) -> rnil() 153.33/71.88 , pi(X) -> 2ndspos(X, from(0())) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() 153.33/71.88 , square(X) -> times(X, X) } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 The following weak DPs constitute a sub-graph of the DG that is 153.33/71.88 closed under successors. The DPs are removed. 153.33/71.88 153.33/71.88 { from^#(X) -> c_1() 153.33/71.88 , from^#(X) -> c_2() 153.33/71.88 , 2ndspos^#(0(), Z) -> c_5() 153.33/71.88 , activate^#(X) -> c_6() 153.33/71.88 , activate^#(n__from(X)) -> c_7(from^#(X)) 153.33/71.88 , 2ndsneg^#(0(), Z) -> c_10() 153.33/71.88 , plus^#(0(), Y) -> c_13() 153.33/71.88 , times^#(0(), Y) -> c_15() } 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) 153.33/71.88 , plus^#(s(X), Y) -> c_12(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_14(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , square^#(X) -> c_16(times^#(X, X)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(posrecip(Y), 2ndsneg(N, activate(Z))) 153.33/71.88 , 2ndspos(0(), Z) -> rnil() 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(negrecip(Y), 2ndspos(N, activate(Z))) 153.33/71.88 , 2ndsneg(0(), Z) -> rnil() 153.33/71.88 , pi(X) -> 2ndspos(X, from(0())) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() 153.33/71.88 , square(X) -> times(X, X) } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 Due to missing edges in the dependency-graph, the right-hand sides 153.33/71.88 of following rules could be simplified: 153.33/71.88 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndspos^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndsneg^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_8(2ndsneg^#(s(N), cons2(X, activate(Z))), activate^#(Z)) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_9(2ndspos^#(N, activate(Z)), activate^#(Z)) 153.33/71.88 , pi^#(X) -> c_11(2ndspos^#(X, from(0())), from^#(0())) } 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) 153.33/71.88 , plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , square^#(X) -> c_8(times^#(X, X)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndspos(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(posrecip(Y), 2ndsneg(N, activate(Z))) 153.33/71.88 , 2ndspos(0(), Z) -> rnil() 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z))) 153.33/71.88 , 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 rcons(negrecip(Y), 2ndspos(N, activate(Z))) 153.33/71.88 , 2ndsneg(0(), Z) -> rnil() 153.33/71.88 , pi(X) -> 2ndspos(X, from(0())) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() 153.33/71.88 , square(X) -> times(X, X) } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 We replace rewrite rules by usable rules: 153.33/71.88 153.33/71.88 Weak Usable Rules: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) 153.33/71.88 , plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 , square^#(X) -> c_8(times^#(X, X)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 Consider the dependency graph 153.33/71.88 153.33/71.88 1: 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 -->_1 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) :2 153.33/71.88 153.33/71.88 2: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 -->_1 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) :4 153.33/71.88 -->_1 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) :3 153.33/71.88 153.33/71.88 3: 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 -->_1 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) :4 153.33/71.88 153.33/71.88 4: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 -->_1 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) :2 153.33/71.88 -->_1 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) :1 153.33/71.88 153.33/71.88 5: pi^#(X) -> c_5(2ndspos^#(X, from(0()))) 153.33/71.88 -->_1 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) :2 153.33/71.88 -->_1 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) :1 153.33/71.88 153.33/71.88 6: plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 -->_1 plus^#(s(X), Y) -> c_6(plus^#(X, Y)) :6 153.33/71.88 153.33/71.88 7: times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) 153.33/71.88 -->_2 times^#(s(X), Y) -> 153.33/71.88 c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) :7 153.33/71.88 -->_1 plus^#(s(X), Y) -> c_6(plus^#(X, Y)) :6 153.33/71.88 153.33/71.88 8: square^#(X) -> c_8(times^#(X, X)) 153.33/71.88 -->_1 times^#(s(X), Y) -> 153.33/71.88 c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) :7 153.33/71.88 153.33/71.88 153.33/71.88 Following roots of the dependency graph are removed, as the 153.33/71.88 considered set of starting terms is closed under reduction with 153.33/71.88 respect to these rules (modulo compound contexts). 153.33/71.88 153.33/71.88 { square^#(X) -> c_8(times^#(X, X)) } 153.33/71.88 153.33/71.88 153.33/71.88 We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) 153.33/71.88 , plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 Obligation: 153.33/71.88 innermost runtime complexity 153.33/71.88 Answer: 153.33/71.88 YES(O(1),O(n^2)) 153.33/71.88 153.33/71.88 We analyse the complexity of following sub-problems (R) and (S). 153.33/71.88 Problem (S) is obtained from the input problem by shifting strict 153.33/71.88 rules from (R) into the weak component: 153.33/71.88 153.33/71.88 Problem (R): 153.33/71.88 ------------ 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.88 Weak DPs: 153.33/71.88 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 StartTerms: basic terms 153.33/71.88 Strategy: innermost 153.33/71.88 153.33/71.88 Problem (S): 153.33/71.88 ------------ 153.33/71.88 Strict DPs: 153.33/71.88 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.88 Weak DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 StartTerms: basic terms 153.33/71.88 Strategy: innermost 153.33/71.88 153.33/71.88 Overall, the transformation results in the following sub-problem(s): 153.33/71.88 153.33/71.88 Generated new problems: 153.33/71.88 ----------------------- 153.33/71.88 R) Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.88 Weak DPs: 153.33/71.88 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 StartTerms: basic terms 153.33/71.88 Strategy: innermost 153.33/71.88 153.33/71.88 This problem was proven YES(O(1),O(n^1)). 153.33/71.88 153.33/71.88 S) Strict DPs: 153.33/71.88 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.88 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.88 Weak DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.88 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_4(2ndspos^#(N, activate(Z))) 153.33/71.88 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.88 Weak Trs: 153.33/71.88 { from(X) -> cons(X, n__from(s(X))) 153.33/71.88 , from(X) -> n__from(X) 153.33/71.88 , activate(X) -> X 153.33/71.88 , activate(n__from(X)) -> from(X) 153.33/71.88 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.88 , plus(0(), Y) -> Y 153.33/71.88 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.88 , times(0(), Y) -> 0() } 153.33/71.88 StartTerms: basic terms 153.33/71.88 Strategy: innermost 153.33/71.88 153.33/71.88 This problem was proven YES(O(1),O(n^2)). 153.33/71.88 153.33/71.88 153.33/71.88 Proofs for generated problems: 153.33/71.88 ------------------------------ 153.33/71.88 R) We are left with following problem, upon which TcT provides the 153.33/71.88 certificate YES(O(1),O(n^1)). 153.33/71.88 153.33/71.88 Strict DPs: 153.33/71.88 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.88 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.88 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.88 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.88 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 Weak DPs: 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) 153.33/71.89 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(n^1)) 153.33/71.89 153.33/71.89 The following weak DPs constitute a sub-graph of the DG that is 153.33/71.89 closed under successors. The DPs are removed. 153.33/71.89 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(n^1)). 153.33/71.89 153.33/71.89 Strict DPs: 153.33/71.89 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) 153.33/71.89 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(n^1)) 153.33/71.89 153.33/71.89 We replace rewrite rules by usable rules: 153.33/71.89 153.33/71.89 Weak Usable Rules: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) } 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(n^1)). 153.33/71.89 153.33/71.89 Strict DPs: 153.33/71.89 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(n^1)) 153.33/71.89 153.33/71.89 We use the processor 'matrix interpretation of dimension 1' to 153.33/71.89 orient following rules strictly. 153.33/71.89 153.33/71.89 DPs: 153.33/71.89 { 2: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 4: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) } 153.33/71.89 153.33/71.89 Sub-proof: 153.33/71.89 ---------- 153.33/71.89 The following argument positions are usable: 153.33/71.89 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 153.33/71.89 Uargs(c_4) = {1}, Uargs(c_5) = {1} 153.33/71.89 153.33/71.89 TcT has computed the following constructor-based matrix 153.33/71.89 interpretation satisfying not(EDA). 153.33/71.89 153.33/71.89 [from](x1) = [0] 153.33/71.89 153.33/71.89 [cons](x1, x2) = [1] x1 + [0] 153.33/71.89 153.33/71.89 [n__from](x1) = [0] 153.33/71.89 153.33/71.89 [s](x1) = [1] x1 + [4] 153.33/71.89 153.33/71.89 [0] = [6] 153.33/71.89 153.33/71.89 [cons2](x1, x2) = [1] x1 + [0] 153.33/71.89 153.33/71.89 [activate](x1) = [0] 153.33/71.89 153.33/71.89 [2ndspos^#](x1, x2) = [1] x1 + [0] 153.33/71.89 153.33/71.89 [2ndsneg^#](x1, x2) = [1] x1 + [0] 153.33/71.89 153.33/71.89 [pi^#](x1) = [7] x1 + [7] 153.33/71.89 153.33/71.89 [c_1](x1) = [1] x1 + [0] 153.33/71.89 153.33/71.89 [c_2](x1) = [1] x1 + [1] 153.33/71.89 153.33/71.89 [c_3](x1) = [1] x1 + [0] 153.33/71.89 153.33/71.89 [c_4](x1) = [1] x1 + [3] 153.33/71.89 153.33/71.89 [c_5](x1) = [2] x1 + [7] 153.33/71.89 153.33/71.89 The order satisfies the following ordering constraints: 153.33/71.89 153.33/71.89 [from(X)] = [0] 153.33/71.89 ? [1] X + [0] 153.33/71.89 = [cons(X, n__from(s(X)))] 153.33/71.89 153.33/71.89 [from(X)] = [0] 153.33/71.89 >= [0] 153.33/71.89 = [n__from(X)] 153.33/71.89 153.33/71.89 [activate(X)] = [0] 153.33/71.89 ? [1] X + [0] 153.33/71.89 = [X] 153.33/71.89 153.33/71.89 [activate(n__from(X))] = [0] 153.33/71.89 >= [0] 153.33/71.89 = [from(X)] 153.33/71.89 153.33/71.89 [2ndspos^#(s(N), cons(X, Z))] = [1] N + [4] 153.33/71.89 >= [1] N + [4] 153.33/71.89 = [c_1(2ndspos^#(s(N), cons2(X, activate(Z))))] 153.33/71.89 153.33/71.89 [2ndspos^#(s(N), cons2(X, cons(Y, Z)))] = [1] N + [4] 153.33/71.89 > [1] N + [1] 153.33/71.89 = [c_2(2ndsneg^#(N, activate(Z)))] 153.33/71.89 153.33/71.89 [2ndsneg^#(s(N), cons(X, Z))] = [1] N + [4] 153.33/71.89 >= [1] N + [4] 153.33/71.89 = [c_3(2ndsneg^#(s(N), cons2(X, activate(Z))))] 153.33/71.89 153.33/71.89 [2ndsneg^#(s(N), cons2(X, cons(Y, Z)))] = [1] N + [4] 153.33/71.89 > [1] N + [3] 153.33/71.89 = [c_4(2ndspos^#(N, activate(Z)))] 153.33/71.89 153.33/71.89 [pi^#(X)] = [7] X + [7] 153.33/71.89 >= [2] X + [7] 153.33/71.89 = [c_5(2ndspos^#(X, from(0())))] 153.33/71.89 153.33/71.89 153.33/71.89 We return to the main proof. Consider the set of all dependency 153.33/71.89 pairs 153.33/71.89 153.33/71.89 : 153.33/71.89 { 1: 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2: 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 3: 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 4: 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , 5: pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 153.33/71.89 Processor 'matrix interpretation of dimension 1' induces the 153.33/71.89 complexity certificate YES(?,O(n^1)) on application of dependency 153.33/71.89 pairs {2,4}. These cover all (indirect) predecessors of dependency 153.33/71.89 pairs {1,2,3,4,5}, their number of application is equally bounded. 153.33/71.89 The dependency pairs are shifted into the weak component. 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(1)). 153.33/71.89 153.33/71.89 Weak DPs: 153.33/71.89 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(1)) 153.33/71.89 153.33/71.89 The following weak DPs constitute a sub-graph of the DG that is 153.33/71.89 closed under successors. The DPs are removed. 153.33/71.89 153.33/71.89 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(1)). 153.33/71.89 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(1)) 153.33/71.89 153.33/71.89 No rule is usable, rules are removed from the input problem. 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(1)). 153.33/71.89 153.33/71.89 Rules: Empty 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(1)) 153.33/71.89 153.33/71.89 Empty rules are trivially bounded 153.33/71.89 153.33/71.89 S) We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(n^2)). 153.33/71.89 153.33/71.89 Strict DPs: 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 Weak DPs: 153.33/71.89 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) 153.33/71.89 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(n^2)) 153.33/71.89 153.33/71.89 The following weak DPs constitute a sub-graph of the DG that is 153.33/71.89 closed under successors. The DPs are removed. 153.33/71.89 153.33/71.89 { 2ndspos^#(s(N), cons(X, Z)) -> 153.33/71.89 c_1(2ndspos^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndspos^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_2(2ndsneg^#(N, activate(Z))) 153.33/71.89 , 2ndsneg^#(s(N), cons(X, Z)) -> 153.33/71.89 c_3(2ndsneg^#(s(N), cons2(X, activate(Z)))) 153.33/71.89 , 2ndsneg^#(s(N), cons2(X, cons(Y, Z))) -> 153.33/71.89 c_4(2ndspos^#(N, activate(Z))) 153.33/71.89 , pi^#(X) -> c_5(2ndspos^#(X, from(0()))) } 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(n^2)). 153.33/71.89 153.33/71.89 Strict DPs: 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 Weak Trs: 153.33/71.89 { from(X) -> cons(X, n__from(s(X))) 153.33/71.89 , from(X) -> n__from(X) 153.33/71.89 , activate(X) -> X 153.33/71.89 , activate(n__from(X)) -> from(X) 153.33/71.89 , plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(n^2)) 153.33/71.89 153.33/71.89 We replace rewrite rules by usable rules: 153.33/71.89 153.33/71.89 Weak Usable Rules: 153.33/71.89 { plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(n^2)). 153.33/71.89 153.33/71.89 Strict DPs: 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 Weak Trs: 153.33/71.89 { plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(n^2)) 153.33/71.89 153.33/71.89 We use the processor 'Small Polynomial Path Order (PS,2-bounded)' 153.33/71.89 to orient following rules strictly. 153.33/71.89 153.33/71.89 DPs: 153.33/71.89 { 1: plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , 2: times^#(s(X), Y) -> 153.33/71.89 c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 Trs: { times(0(), Y) -> 0() } 153.33/71.89 153.33/71.89 Sub-proof: 153.33/71.89 ---------- 153.33/71.89 The input was oriented with the instance of 'Small Polynomial Path 153.33/71.89 Order (PS,2-bounded)' as induced by the safe mapping 153.33/71.89 153.33/71.89 safe(s) = {1}, safe(0) = {}, safe(plus) = {}, safe(times) = {}, 153.33/71.89 safe(plus^#) = {2}, safe(times^#) = {}, safe(c_6) = {}, 153.33/71.89 safe(c_7) = {} 153.33/71.89 153.33/71.89 and precedence 153.33/71.89 153.33/71.89 times > plus, times > plus^#, times^# > plus, times^# > plus^#, 153.33/71.89 plus ~ plus^#, times ~ times^# . 153.33/71.89 153.33/71.89 Following symbols are considered recursive: 153.33/71.89 153.33/71.89 {plus, times, plus^#, times^#} 153.33/71.89 153.33/71.89 The recursion depth is 2. 153.33/71.89 153.33/71.89 Further, following argument filtering is employed: 153.33/71.89 153.33/71.89 pi(s) = [1], pi(0) = [], pi(plus) = [1], pi(times) = [1], 153.33/71.89 pi(plus^#) = [1], pi(times^#) = [1, 2], pi(c_6) = [1], 153.33/71.89 pi(c_7) = [1, 2] 153.33/71.89 153.33/71.89 Usable defined function symbols are a subset of: 153.33/71.89 153.33/71.89 {plus^#, times^#} 153.33/71.89 153.33/71.89 For your convenience, here are the satisfied ordering constraints: 153.33/71.89 153.33/71.89 pi(plus^#(s(X), Y)) = plus^#(s(; X);) 153.33/71.89 > c_6(plus^#(X;);) 153.33/71.89 = pi(c_6(plus^#(X, Y))) 153.33/71.89 153.33/71.89 pi(times^#(s(X), Y)) = times^#(s(; X), Y;) 153.33/71.89 > c_7(plus^#(Y;), times^#(X, Y;);) 153.33/71.89 = pi(c_7(plus^#(Y, times(X, Y)), times^#(X, Y))) 153.33/71.89 153.33/71.89 153.33/71.89 The strictly oriented rules are moved into the weak component. 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(1)). 153.33/71.89 153.33/71.89 Weak DPs: 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 Weak Trs: 153.33/71.89 { plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(1)) 153.33/71.89 153.33/71.89 The following weak DPs constitute a sub-graph of the DG that is 153.33/71.89 closed under successors. The DPs are removed. 153.33/71.89 153.33/71.89 { plus^#(s(X), Y) -> c_6(plus^#(X, Y)) 153.33/71.89 , times^#(s(X), Y) -> c_7(plus^#(Y, times(X, Y)), times^#(X, Y)) } 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(1)). 153.33/71.89 153.33/71.89 Weak Trs: 153.33/71.89 { plus(s(X), Y) -> s(plus(X, Y)) 153.33/71.89 , plus(0(), Y) -> Y 153.33/71.89 , times(s(X), Y) -> plus(Y, times(X, Y)) 153.33/71.89 , times(0(), Y) -> 0() } 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(1)) 153.33/71.89 153.33/71.89 No rule is usable, rules are removed from the input problem. 153.33/71.89 153.33/71.89 We are left with following problem, upon which TcT provides the 153.33/71.89 certificate YES(O(1),O(1)). 153.33/71.89 153.33/71.89 Rules: Empty 153.33/71.89 Obligation: 153.33/71.89 innermost runtime complexity 153.33/71.89 Answer: 153.33/71.89 YES(O(1),O(1)) 153.33/71.89 153.33/71.89 Empty rules are trivially bounded 153.33/71.89 153.33/71.89 153.33/71.89 Hurray, we answered YES(O(1),O(n^2)) 153.51/71.92 EOF