YES(O(1),O(n^1)) 7.15/3.41 YES(O(1),O(n^1)) 7.15/3.41 7.15/3.41 We are left with following problem, upon which TcT provides the 7.15/3.41 certificate YES(O(1),O(n^1)). 7.15/3.41 7.15/3.41 Strict Trs: 7.15/3.41 { admit(x, nil()) -> nil() 7.15/3.41 , admit(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 cond(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z))))) 7.15/3.41 , cond(true(), y) -> y } 7.15/3.41 Obligation: 7.15/3.41 innermost runtime complexity 7.15/3.41 Answer: 7.15/3.41 YES(O(1),O(n^1)) 7.15/3.41 7.15/3.41 We add the following weak dependency pairs: 7.15/3.41 7.15/3.41 Strict DPs: 7.15/3.41 { admit^#(x, nil()) -> c_1() 7.15/3.41 , admit^#(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) 7.15/3.41 , cond^#(true(), y) -> c_3() } 7.15/3.41 7.15/3.41 and mark the set of starting terms. 7.15/3.41 7.15/3.41 We are left with following problem, upon which TcT provides the 7.15/3.41 certificate YES(O(1),O(n^1)). 7.15/3.41 7.15/3.41 Strict DPs: 7.15/3.41 { admit^#(x, nil()) -> c_1() 7.15/3.41 , admit^#(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) 7.15/3.41 , cond^#(true(), y) -> c_3() } 7.15/3.41 Strict Trs: 7.15/3.41 { admit(x, nil()) -> nil() 7.15/3.41 , admit(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 cond(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z))))) 7.15/3.41 , cond(true(), y) -> y } 7.15/3.41 Obligation: 7.15/3.41 innermost runtime complexity 7.15/3.41 Answer: 7.15/3.41 YES(O(1),O(n^1)) 7.15/3.41 7.15/3.41 The weightgap principle applies (using the following constant 7.15/3.41 growth matrix-interpretation) 7.15/3.41 7.15/3.41 The following argument positions are usable: 7.15/3.41 Uargs(.) = {2}, Uargs(cond) = {2}, Uargs(c_2) = {1}, 7.15/3.41 Uargs(cond^#) = {2} 7.15/3.41 7.15/3.41 TcT has computed the following constructor-restricted matrix 7.15/3.41 interpretation. 7.15/3.41 7.15/3.41 [admit](x1, x2) = [2 0] x2 + [0] 7.15/3.41 [0 0] [0] 7.15/3.41 7.15/3.41 [nil] = [2] 7.15/3.41 [0] 7.15/3.41 7.15/3.41 [.](x1, x2) = [0 2] x1 + [1 0] x2 + [0] 7.15/3.41 [0 0] [0 0] [0] 7.15/3.41 7.15/3.41 [w] = [0] 7.15/3.41 [1] 7.15/3.41 7.15/3.41 [cond](x1, x2) = [1 0] x2 + [1] 7.15/3.41 [0 2] [0] 7.15/3.41 7.15/3.41 [=](x1, x2) = [0] 7.15/3.41 [1] 7.15/3.41 7.15/3.41 [sum](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0] 7.15/3.41 [0 0] [0 0] [0 0] [0] 7.15/3.41 7.15/3.41 [carry](x1, x2, x3) = [0] 7.15/3.41 [0] 7.15/3.41 7.15/3.41 [true] = [0] 7.15/3.41 [0] 7.15/3.41 7.15/3.41 [admit^#](x1, x2) = [1 2] x1 + [2 0] x2 + [2] 7.15/3.41 [2 1] [0 0] [2] 7.15/3.41 7.15/3.41 [c_1] = [1] 7.15/3.41 [1] 7.15/3.41 7.15/3.41 [c_2](x1) = [1 0] x1 + [1] 7.15/3.41 [0 1] [2] 7.15/3.41 7.15/3.41 [cond^#](x1, x2) = [0 2] x1 + [1 0] x2 + [2] 7.15/3.41 [0 0] [0 0] [2] 7.15/3.41 7.15/3.41 [c_3] = [1] 7.15/3.41 [1] 7.15/3.41 7.15/3.41 The order satisfies the following ordering constraints: 7.15/3.41 7.15/3.41 [admit(x, nil())] = [4] 7.15/3.41 [0] 7.15/3.41 > [2] 7.15/3.41 [0] 7.15/3.41 = [nil()] 7.15/3.41 7.15/3.41 [admit(x, .(u, .(v, .(w(), z))))] = [0 4] u + [0 4] v + [2 0] z + [4] 7.15/3.41 [0 0] [0 0] [0 0] [0] 7.15/3.41 > [0 2] u + [0 2] v + [2 0] z + [3] 7.15/3.41 [0 0] [0 0] [0 0] [0] 7.15/3.41 = [cond(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))] 7.15/3.41 7.15/3.41 [cond(true(), y)] = [1 0] y + [1] 7.15/3.41 [0 2] [0] 7.15/3.41 > [1 0] y + [0] 7.15/3.41 [0 1] [0] 7.15/3.41 = [y] 7.15/3.41 7.15/3.41 [admit^#(x, nil())] = [1 2] x + [6] 7.15/3.41 [2 1] [2] 7.15/3.41 > [1] 7.15/3.41 [1] 7.15/3.41 = [c_1()] 7.15/3.41 7.15/3.41 [admit^#(x, .(u, .(v, .(w(), z))))] = [1 2] x + [0 4] u + [0 4] v + [2 0] z + [6] 7.15/3.41 [2 1] [0 0] [0 0] [0 0] [2] 7.15/3.41 ? [0 2] u + [0 2] v + [2 0] z + [7] 7.15/3.41 [0 0] [0 0] [0 0] [4] 7.15/3.41 = [c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z))))))] 7.15/3.41 7.15/3.41 [cond^#(true(), y)] = [1 0] y + [2] 7.15/3.41 [0 0] [2] 7.15/3.41 > [1] 7.15/3.41 [1] 7.15/3.41 = [c_3()] 7.15/3.41 7.15/3.41 7.15/3.41 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 7.15/3.41 7.15/3.41 We are left with following problem, upon which TcT provides the 7.15/3.41 certificate YES(O(1),O(1)). 7.15/3.41 7.15/3.41 Strict DPs: 7.15/3.41 { admit^#(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) } 7.15/3.41 Weak DPs: 7.15/3.41 { admit^#(x, nil()) -> c_1() 7.15/3.41 , cond^#(true(), y) -> c_3() } 7.15/3.41 Weak Trs: 7.15/3.41 { admit(x, nil()) -> nil() 7.15/3.41 , admit(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 cond(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z))))) 7.15/3.41 , cond(true(), y) -> y } 7.15/3.41 Obligation: 7.15/3.41 innermost runtime complexity 7.15/3.41 Answer: 7.15/3.41 YES(O(1),O(1)) 7.15/3.41 7.15/3.41 We estimate the number of application of {1} by applications of 7.15/3.41 Pre({1}) = {}. Here rules are labeled as follows: 7.15/3.41 7.15/3.41 DPs: 7.15/3.41 { 1: admit^#(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) 7.15/3.41 , 2: admit^#(x, nil()) -> c_1() 7.15/3.41 , 3: cond^#(true(), y) -> c_3() } 7.15/3.41 7.15/3.41 We are left with following problem, upon which TcT provides the 7.15/3.41 certificate YES(O(1),O(1)). 7.15/3.41 7.15/3.41 Weak DPs: 7.15/3.41 { admit^#(x, nil()) -> c_1() 7.15/3.41 , admit^#(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) 7.15/3.41 , cond^#(true(), y) -> c_3() } 7.15/3.41 Weak Trs: 7.15/3.41 { admit(x, nil()) -> nil() 7.15/3.41 , admit(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 cond(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z))))) 7.15/3.41 , cond(true(), y) -> y } 7.15/3.41 Obligation: 7.15/3.41 innermost runtime complexity 7.15/3.41 Answer: 7.15/3.41 YES(O(1),O(1)) 7.15/3.41 7.15/3.41 The following weak DPs constitute a sub-graph of the DG that is 7.15/3.41 closed under successors. The DPs are removed. 7.15/3.41 7.15/3.41 { admit^#(x, nil()) -> c_1() 7.15/3.41 , admit^#(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 c_2(cond^#(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z)))))) 7.15/3.41 , cond^#(true(), y) -> c_3() } 7.15/3.41 7.15/3.41 We are left with following problem, upon which TcT provides the 7.15/3.41 certificate YES(O(1),O(1)). 7.15/3.41 7.15/3.41 Weak Trs: 7.15/3.41 { admit(x, nil()) -> nil() 7.15/3.41 , admit(x, .(u, .(v, .(w(), z)))) -> 7.15/3.41 cond(=(sum(x, u, v), w()), 7.15/3.41 .(u, .(v, .(w(), admit(carry(x, u, v), z))))) 7.15/3.41 , cond(true(), y) -> y } 7.15/3.41 Obligation: 7.15/3.41 innermost runtime complexity 7.15/3.41 Answer: 7.15/3.41 YES(O(1),O(1)) 7.15/3.41 7.15/3.41 No rule is usable, rules are removed from the input problem. 7.15/3.41 7.15/3.41 We are left with following problem, upon which TcT provides the 7.15/3.41 certificate YES(O(1),O(1)). 7.15/3.41 7.15/3.41 Rules: Empty 7.15/3.41 Obligation: 7.15/3.41 innermost runtime complexity 7.15/3.41 Answer: 7.15/3.41 YES(O(1),O(1)) 7.15/3.41 7.15/3.41 Empty rules are trivially bounded 7.15/3.41 7.15/3.41 Hurray, we answered YES(O(1),O(n^1)) 7.15/3.42 EOF