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