YES(O(1),O(n^2)) 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 We are left with following problem, upon which TcT provides the 528.74/149.28 certificate YES(O(1),O(n^2)). 528.74/149.28 528.74/149.28 Strict Trs: 528.74/149.28 { app(l, nil()) -> l 528.74/149.28 , app(nil(), k) -> k 528.74/149.28 , app(cons(x, l), k) -> cons(x, app(l, k)) 528.74/149.28 , sum(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 sum(app(l, sum(cons(x, cons(y, k))))) 528.74/149.28 , sum(cons(x, nil())) -> cons(x, nil()) 528.74/149.28 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) 528.74/149.28 , plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 Obligation: 528.74/149.28 innermost runtime complexity 528.74/149.28 Answer: 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 We add the following dependency tuples: 528.74/149.28 528.74/149.28 Strict DPs: 528.74/149.28 { app^#(l, nil()) -> c_1() 528.74/149.28 , app^#(nil(), k) -> c_2() 528.74/149.28 , app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , sum^#(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), 528.74/149.28 app^#(l, sum(cons(x, cons(y, k)))), 528.74/149.28 sum^#(cons(x, cons(y, k)))) 528.74/149.28 , sum^#(cons(x, nil())) -> c_5() 528.74/149.28 , sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , plus^#(0(), y) -> c_7() 528.74/149.28 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 528.74/149.28 and mark the set of starting terms. 528.74/149.28 528.74/149.28 We are left with following problem, upon which TcT provides the 528.74/149.28 certificate YES(O(1),O(n^2)). 528.74/149.28 528.74/149.28 Strict DPs: 528.74/149.28 { app^#(l, nil()) -> c_1() 528.74/149.28 , app^#(nil(), k) -> c_2() 528.74/149.28 , app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , sum^#(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), 528.74/149.28 app^#(l, sum(cons(x, cons(y, k)))), 528.74/149.28 sum^#(cons(x, cons(y, k)))) 528.74/149.28 , sum^#(cons(x, nil())) -> c_5() 528.74/149.28 , sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , plus^#(0(), y) -> c_7() 528.74/149.28 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 Weak Trs: 528.74/149.28 { app(l, nil()) -> l 528.74/149.28 , app(nil(), k) -> k 528.74/149.28 , app(cons(x, l), k) -> cons(x, app(l, k)) 528.74/149.28 , sum(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 sum(app(l, sum(cons(x, cons(y, k))))) 528.74/149.28 , sum(cons(x, nil())) -> cons(x, nil()) 528.74/149.28 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) 528.74/149.28 , plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 Obligation: 528.74/149.28 innermost runtime complexity 528.74/149.28 Answer: 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 Consider the dependency graph: 528.74/149.28 528.74/149.28 1: app^#(l, nil()) -> c_1() 528.74/149.28 528.74/149.28 2: app^#(nil(), k) -> c_2() 528.74/149.28 528.74/149.28 3: app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 -->_1 app^#(cons(x, l), k) -> c_3(app^#(l, k)) :3 528.74/149.28 -->_1 app^#(nil(), k) -> c_2() :2 528.74/149.28 -->_1 app^#(l, nil()) -> c_1() :1 528.74/149.28 528.74/149.28 4: sum^#(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), 528.74/149.28 app^#(l, sum(cons(x, cons(y, k)))), 528.74/149.28 sum^#(cons(x, cons(y, k)))) 528.74/149.28 -->_3 sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6 528.74/149.28 -->_1 sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6 528.74/149.28 -->_1 sum^#(cons(x, nil())) -> c_5() :5 528.74/149.28 -->_1 sum^#(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 c_4(sum^#(app(l, sum(cons(x, cons(y, k))))), 528.74/149.28 app^#(l, sum(cons(x, cons(y, k)))), 528.74/149.28 sum^#(cons(x, cons(y, k)))) :4 528.74/149.28 -->_2 app^#(l, nil()) -> c_1() :1 528.74/149.28 528.74/149.28 5: sum^#(cons(x, nil())) -> c_5() 528.74/149.28 528.74/149.28 6: sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 -->_2 plus^#(s(x), y) -> c_8(plus^#(x, y)) :8 528.74/149.28 -->_2 plus^#(0(), y) -> c_7() :7 528.74/149.28 -->_1 sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6 528.74/149.28 -->_1 sum^#(cons(x, nil())) -> c_5() :5 528.74/149.28 528.74/149.28 7: plus^#(0(), y) -> c_7() 528.74/149.28 528.74/149.28 8: plus^#(s(x), y) -> c_8(plus^#(x, y)) 528.74/149.28 -->_1 plus^#(s(x), y) -> c_8(plus^#(x, y)) :8 528.74/149.28 -->_1 plus^#(0(), y) -> c_7() :7 528.74/149.28 528.74/149.28 528.74/149.28 Only the nodes {1,2,3,5,6,8,7} are reachable from nodes 528.74/149.28 {1,2,3,5,6,7,8} that start derivation from marked basic terms. The 528.74/149.28 nodes not reachable are removed from the problem. 528.74/149.28 528.74/149.28 We are left with following problem, upon which TcT provides the 528.74/149.28 certificate YES(O(1),O(n^2)). 528.74/149.28 528.74/149.28 Strict DPs: 528.74/149.28 { app^#(l, nil()) -> c_1() 528.74/149.28 , app^#(nil(), k) -> c_2() 528.74/149.28 , app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , sum^#(cons(x, nil())) -> c_5() 528.74/149.28 , sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , plus^#(0(), y) -> c_7() 528.74/149.28 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 Weak Trs: 528.74/149.28 { app(l, nil()) -> l 528.74/149.28 , app(nil(), k) -> k 528.74/149.28 , app(cons(x, l), k) -> cons(x, app(l, k)) 528.74/149.28 , sum(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 sum(app(l, sum(cons(x, cons(y, k))))) 528.74/149.28 , sum(cons(x, nil())) -> cons(x, nil()) 528.74/149.28 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) 528.74/149.28 , plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 Obligation: 528.74/149.28 innermost runtime complexity 528.74/149.28 Answer: 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 We estimate the number of application of {1,2,4,6} by applications 528.74/149.28 of Pre({1,2,4,6}) = {3,5,7}. Here rules are labeled as follows: 528.74/149.28 528.74/149.28 DPs: 528.74/149.28 { 1: app^#(l, nil()) -> c_1() 528.74/149.28 , 2: app^#(nil(), k) -> c_2() 528.74/149.28 , 3: app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , 4: sum^#(cons(x, nil())) -> c_5() 528.74/149.28 , 5: sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , 6: plus^#(0(), y) -> c_7() 528.74/149.28 , 7: plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 528.74/149.28 We are left with following problem, upon which TcT provides the 528.74/149.28 certificate YES(O(1),O(n^2)). 528.74/149.28 528.74/149.28 Strict DPs: 528.74/149.28 { app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 Weak DPs: 528.74/149.28 { app^#(l, nil()) -> c_1() 528.74/149.28 , app^#(nil(), k) -> c_2() 528.74/149.28 , sum^#(cons(x, nil())) -> c_5() 528.74/149.28 , plus^#(0(), y) -> c_7() } 528.74/149.28 Weak Trs: 528.74/149.28 { app(l, nil()) -> l 528.74/149.28 , app(nil(), k) -> k 528.74/149.28 , app(cons(x, l), k) -> cons(x, app(l, k)) 528.74/149.28 , sum(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 sum(app(l, sum(cons(x, cons(y, k))))) 528.74/149.28 , sum(cons(x, nil())) -> cons(x, nil()) 528.74/149.28 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) 528.74/149.28 , plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 Obligation: 528.74/149.28 innermost runtime complexity 528.74/149.28 Answer: 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 The following weak DPs constitute a sub-graph of the DG that is 528.74/149.28 closed under successors. The DPs are removed. 528.74/149.28 528.74/149.28 { app^#(l, nil()) -> c_1() 528.74/149.28 , app^#(nil(), k) -> c_2() 528.74/149.28 , sum^#(cons(x, nil())) -> c_5() 528.74/149.28 , plus^#(0(), y) -> c_7() } 528.74/149.28 528.74/149.28 We are left with following problem, upon which TcT provides the 528.74/149.28 certificate YES(O(1),O(n^2)). 528.74/149.28 528.74/149.28 Strict DPs: 528.74/149.28 { app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 Weak Trs: 528.74/149.28 { app(l, nil()) -> l 528.74/149.28 , app(nil(), k) -> k 528.74/149.28 , app(cons(x, l), k) -> cons(x, app(l, k)) 528.74/149.28 , sum(app(l, cons(x, cons(y, k)))) -> 528.74/149.28 sum(app(l, sum(cons(x, cons(y, k))))) 528.74/149.28 , sum(cons(x, nil())) -> cons(x, nil()) 528.74/149.28 , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l)) 528.74/149.28 , plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 Obligation: 528.74/149.28 innermost runtime complexity 528.74/149.28 Answer: 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 We replace rewrite rules by usable rules: 528.74/149.28 528.74/149.28 Weak Usable Rules: 528.74/149.28 { plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 528.74/149.28 We are left with following problem, upon which TcT provides the 528.74/149.28 certificate YES(O(1),O(n^2)). 528.74/149.28 528.74/149.28 Strict DPs: 528.74/149.28 { app^#(cons(x, l), k) -> c_3(app^#(l, k)) 528.74/149.28 , sum^#(cons(x, cons(y, l))) -> 528.74/149.28 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.28 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.28 Weak Trs: 528.74/149.28 { plus(0(), y) -> y 528.74/149.28 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.28 Obligation: 528.74/149.28 innermost runtime complexity 528.74/149.28 Answer: 528.74/149.28 YES(O(1),O(n^2)) 528.74/149.28 528.74/149.28 We use the processor 'matrix interpretation of dimension 1' to 528.74/149.28 orient following rules strictly. 528.74/149.28 528.74/149.28 DPs: 528.74/149.28 { 1: app^#(cons(x, l), k) -> c_3(app^#(l, k)) } 528.74/149.28 528.74/149.28 Sub-proof: 528.74/149.28 ---------- 528.74/149.28 The following argument positions are usable: 528.74/149.28 Uargs(c_3) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_8) = {1} 528.74/149.28 528.74/149.28 TcT has computed the following constructor-based matrix 528.74/149.28 interpretation satisfying not(EDA). 528.74/149.28 528.74/149.28 [cons](x1, x2) = [1] x2 + [4] 528.74/149.28 528.74/149.28 [plus](x1, x2) = [0] 528.74/149.28 528.74/149.28 [0] = [7] 528.74/149.28 528.74/149.28 [s](x1) = [0] 528.74/149.28 528.74/149.28 [app^#](x1, x2) = [1] x1 + [7] x2 + [0] 528.74/149.28 528.74/149.29 [c_3](x1) = [1] x1 + [1] 528.74/149.29 528.74/149.29 [sum^#](x1) = [0] 528.74/149.29 528.74/149.29 [c_6](x1, x2) = [2] x1 + [1] x2 + [0] 528.74/149.29 528.74/149.29 [plus^#](x1, x2) = [0] 528.74/149.29 528.74/149.29 [c_8](x1) = [2] x1 + [0] 528.74/149.29 528.74/149.29 The order satisfies the following ordering constraints: 528.74/149.29 528.74/149.29 [plus(0(), y)] = [0] 528.74/149.29 ? [1] y + [0] 528.74/149.29 = [y] 528.74/149.29 528.74/149.29 [plus(s(x), y)] = [0] 528.74/149.29 >= [0] 528.74/149.29 = [s(plus(x, y))] 528.74/149.29 528.74/149.29 [app^#(cons(x, l), k)] = [7] k + [1] l + [4] 528.74/149.29 > [7] k + [1] l + [1] 528.74/149.29 = [c_3(app^#(l, k))] 528.74/149.29 528.74/149.29 [sum^#(cons(x, cons(y, l)))] = [0] 528.74/149.29 >= [0] 528.74/149.29 = [c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))] 528.74/149.29 528.74/149.29 [plus^#(s(x), y)] = [0] 528.74/149.29 >= [0] 528.74/149.29 = [c_8(plus^#(x, y))] 528.74/149.29 528.74/149.29 528.74/149.29 The strictly oriented rules are moved into the weak component. 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(n^2)). 528.74/149.29 528.74/149.29 Strict DPs: 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.29 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 Weak DPs: { app^#(cons(x, l), k) -> c_3(app^#(l, k)) } 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(n^2)) 528.74/149.29 528.74/149.29 The following weak DPs constitute a sub-graph of the DG that is 528.74/149.29 closed under successors. The DPs are removed. 528.74/149.29 528.74/149.29 { app^#(cons(x, l), k) -> c_3(app^#(l, k)) } 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(n^2)). 528.74/149.29 528.74/149.29 Strict DPs: 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) 528.74/149.29 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(n^2)) 528.74/149.29 528.74/149.29 We decompose the input problem according to the dependency graph 528.74/149.29 into the upper component 528.74/149.29 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 528.74/149.29 528.74/149.29 and lower component 528.74/149.29 528.74/149.29 { plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 528.74/149.29 Further, following extension rules are added to the lower 528.74/149.29 component. 528.74/149.29 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) 528.74/149.29 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) } 528.74/149.29 528.74/149.29 TcT solves the upper component with certificate YES(O(1),O(n^1)). 528.74/149.29 528.74/149.29 Sub-proof: 528.74/149.29 ---------- 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(n^1)). 528.74/149.29 528.74/149.29 Strict DPs: 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(n^1)) 528.74/149.29 528.74/149.29 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 528.74/149.29 to orient following rules strictly. 528.74/149.29 528.74/149.29 DPs: 528.74/149.29 { 1: sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 528.74/149.29 Trs: { plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 528.74/149.29 Sub-proof: 528.74/149.29 ---------- 528.74/149.29 The input was oriented with the instance of 'Small Polynomial Path 528.74/149.29 Order (PS,1-bounded)' as induced by the safe mapping 528.74/149.29 528.74/149.29 safe(cons) = {1, 2}, safe(plus) = {1}, safe(0) = {}, safe(s) = {1}, 528.74/149.29 safe(sum^#) = {}, safe(c_6) = {}, safe(plus^#) = {} 528.74/149.29 528.74/149.29 and precedence 528.74/149.29 528.74/149.29 plus ~ sum^# . 528.74/149.29 528.74/149.29 Following symbols are considered recursive: 528.74/149.29 528.74/149.29 {plus, sum^#} 528.74/149.29 528.74/149.29 The recursion depth is 1. 528.74/149.29 528.74/149.29 Further, following argument filtering is employed: 528.74/149.29 528.74/149.29 pi(cons) = [2], pi(plus) = [1], pi(0) = [], pi(s) = [], 528.74/149.29 pi(sum^#) = [1], pi(c_6) = [1, 2], pi(plus^#) = [] 528.74/149.29 528.74/149.29 Usable defined function symbols are a subset of: 528.74/149.29 528.74/149.29 {sum^#, plus^#} 528.74/149.29 528.74/149.29 For your convenience, here are the satisfied ordering constraints: 528.74/149.29 528.74/149.29 pi(sum^#(cons(x, cons(y, l)))) = sum^#(cons(; cons(; l));) 528.74/149.29 > c_6(sum^#(cons(; l);), plus^#();) 528.74/149.29 = pi(c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))) 528.74/149.29 528.74/149.29 528.74/149.29 The strictly oriented rules are moved into the weak component. 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(1)). 528.74/149.29 528.74/149.29 Weak DPs: 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(1)) 528.74/149.29 528.74/149.29 The following weak DPs constitute a sub-graph of the DG that is 528.74/149.29 closed under successors. The DPs are removed. 528.74/149.29 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> 528.74/149.29 c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) } 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(1)). 528.74/149.29 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(1)) 528.74/149.29 528.74/149.29 No rule is usable, rules are removed from the input problem. 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(1)). 528.74/149.29 528.74/149.29 Rules: Empty 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(1)) 528.74/149.29 528.74/149.29 Empty rules are trivially bounded 528.74/149.29 528.74/149.29 We return to the main proof. 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(n^1)). 528.74/149.29 528.74/149.29 Strict DPs: { plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 Weak DPs: 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) 528.74/149.29 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) } 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(n^1)) 528.74/149.29 528.74/149.29 We use the processor 'matrix interpretation of dimension 1' to 528.74/149.29 orient following rules strictly. 528.74/149.29 528.74/149.29 DPs: 528.74/149.29 { 1: plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 Trs: { plus(0(), y) -> y } 528.74/149.29 528.74/149.29 Sub-proof: 528.74/149.29 ---------- 528.74/149.29 The following argument positions are usable: 528.74/149.29 Uargs(c_8) = {1} 528.74/149.29 528.74/149.29 TcT has computed the following constructor-based matrix 528.74/149.29 interpretation satisfying not(EDA). 528.74/149.29 528.74/149.29 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 528.74/149.29 528.74/149.29 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 528.74/149.29 528.74/149.29 [0] = [1] 528.74/149.29 528.74/149.29 [s](x1) = [1] x1 + [1] 528.74/149.29 528.74/149.29 [sum^#](x1) = [4] x1 + [0] 528.74/149.29 528.74/149.29 [plus^#](x1, x2) = [4] x1 + [4] x2 + [0] 528.74/149.29 528.74/149.29 [c_8](x1) = [1] x1 + [1] 528.74/149.29 528.74/149.29 The order satisfies the following ordering constraints: 528.74/149.29 528.74/149.29 [plus(0(), y)] = [1] y + [1] 528.74/149.29 > [1] y + [0] 528.74/149.29 = [y] 528.74/149.29 528.74/149.29 [plus(s(x), y)] = [1] x + [1] y + [1] 528.74/149.29 >= [1] x + [1] y + [1] 528.74/149.29 = [s(plus(x, y))] 528.74/149.29 528.74/149.29 [sum^#(cons(x, cons(y, l)))] = [4] l + [4] x + [4] y + [0] 528.74/149.29 >= [4] l + [4] x + [4] y + [0] 528.74/149.29 = [sum^#(cons(plus(x, y), l))] 528.74/149.29 528.74/149.29 [sum^#(cons(x, cons(y, l)))] = [4] l + [4] x + [4] y + [0] 528.74/149.29 >= [4] x + [4] y + [0] 528.74/149.29 = [plus^#(x, y)] 528.74/149.29 528.74/149.29 [plus^#(s(x), y)] = [4] x + [4] y + [4] 528.74/149.29 > [4] x + [4] y + [1] 528.74/149.29 = [c_8(plus^#(x, y))] 528.74/149.29 528.74/149.29 528.74/149.29 The strictly oriented rules are moved into the weak component. 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(1)). 528.74/149.29 528.74/149.29 Weak DPs: 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) 528.74/149.29 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 528.74/149.29 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(1)) 528.74/149.29 528.74/149.29 The following weak DPs constitute a sub-graph of the DG that is 528.74/149.29 closed under successors. The DPs are removed. 528.74/149.29 528.74/149.29 { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l)) 528.74/149.29 , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) 528.74/149.29 , plus^#(s(x), y) -> c_8(plus^#(x, y)) } 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(1)). 528.74/149.29 528.74/149.29 Weak Trs: 528.74/149.29 { plus(0(), y) -> y 528.74/149.29 , plus(s(x), y) -> s(plus(x, y)) } 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(1)) 528.74/149.29 528.74/149.29 No rule is usable, rules are removed from the input problem. 528.74/149.29 528.74/149.29 We are left with following problem, upon which TcT provides the 528.74/149.29 certificate YES(O(1),O(1)). 528.74/149.29 528.74/149.29 Rules: Empty 528.74/149.29 Obligation: 528.74/149.29 innermost runtime complexity 528.74/149.29 Answer: 528.74/149.29 YES(O(1),O(1)) 528.74/149.29 528.74/149.29 Empty rules are trivially bounded 528.74/149.29 528.74/149.29 Hurray, we answered YES(O(1),O(n^2)) 529.50/149.70 EOF