MAYBE 203.15/82.94 MAYBE 203.15/82.94 203.15/82.94 We are left with following problem, upon which TcT provides the 203.15/82.94 certificate MAYBE. 203.15/82.94 203.15/82.94 Strict Trs: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , quot(0(), s(y)) -> 0() 203.15/82.94 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 Obligation: 203.15/82.94 innermost runtime complexity 203.15/82.94 Answer: 203.15/82.94 MAYBE 203.15/82.94 203.15/82.94 None of the processors succeeded. 203.15/82.94 203.15/82.94 Details of failed attempt(s): 203.15/82.94 ----------------------------- 203.15/82.94 1) 'empty' failed due to the following reason: 203.15/82.94 203.15/82.94 Empty strict component of the problem is NOT empty. 203.15/82.94 203.15/82.94 2) 'Best' failed due to the following reason: 203.15/82.94 203.15/82.94 None of the processors succeeded. 203.15/82.94 203.15/82.94 Details of failed attempt(s): 203.15/82.94 ----------------------------- 203.15/82.94 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 203.15/82.94 following reason: 203.15/82.94 203.15/82.94 We add the following dependency tuples: 203.15/82.94 203.15/82.94 Strict DPs: 203.15/82.94 { minus^#(x, 0()) -> c_1() 203.15/82.94 , minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , plus^#(0(), y) -> c_6() 203.15/82.94 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 203.15/82.94 , quot^#(0(), s(y)) -> c_4() 203.15/82.94 , quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 203.15/82.94 and mark the set of starting terms. 203.15/82.94 203.15/82.94 We are left with following problem, upon which TcT provides the 203.15/82.94 certificate MAYBE. 203.15/82.94 203.15/82.94 Strict DPs: 203.15/82.94 { minus^#(x, 0()) -> c_1() 203.15/82.94 , minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , plus^#(0(), y) -> c_6() 203.15/82.94 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 203.15/82.94 , quot^#(0(), s(y)) -> c_4() 203.15/82.94 , quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 Weak Trs: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , quot(0(), s(y)) -> 0() 203.15/82.94 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 Obligation: 203.15/82.94 innermost runtime complexity 203.15/82.94 Answer: 203.15/82.94 MAYBE 203.15/82.94 203.15/82.94 We estimate the number of application of {1,4,6} by applications of 203.15/82.94 Pre({1,4,6}) = {2,3,5,7}. Here rules are labeled as follows: 203.15/82.94 203.15/82.94 DPs: 203.15/82.94 { 1: minus^#(x, 0()) -> c_1() 203.15/82.94 , 2: minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , 3: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , 4: plus^#(0(), y) -> c_6() 203.15/82.94 , 5: plus^#(s(x), y) -> c_7(plus^#(x, y)) 203.15/82.94 , 6: quot^#(0(), s(y)) -> c_4() 203.15/82.94 , 7: quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 203.15/82.94 We are left with following problem, upon which TcT provides the 203.15/82.94 certificate MAYBE. 203.15/82.94 203.15/82.94 Strict DPs: 203.15/82.94 { minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 203.15/82.94 , quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 Weak DPs: 203.15/82.94 { minus^#(x, 0()) -> c_1() 203.15/82.94 , plus^#(0(), y) -> c_6() 203.15/82.94 , quot^#(0(), s(y)) -> c_4() } 203.15/82.94 Weak Trs: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , quot(0(), s(y)) -> 0() 203.15/82.94 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 Obligation: 203.15/82.94 innermost runtime complexity 203.15/82.94 Answer: 203.15/82.94 MAYBE 203.15/82.94 203.15/82.94 The following weak DPs constitute a sub-graph of the DG that is 203.15/82.94 closed under successors. The DPs are removed. 203.15/82.94 203.15/82.94 { minus^#(x, 0()) -> c_1() 203.15/82.94 , plus^#(0(), y) -> c_6() 203.15/82.94 , quot^#(0(), s(y)) -> c_4() } 203.15/82.94 203.15/82.94 We are left with following problem, upon which TcT provides the 203.15/82.94 certificate MAYBE. 203.15/82.94 203.15/82.94 Strict DPs: 203.15/82.94 { minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 203.15/82.94 , quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 Weak Trs: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , quot(0(), s(y)) -> 0() 203.15/82.94 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 Obligation: 203.15/82.94 innermost runtime complexity 203.15/82.94 Answer: 203.15/82.94 MAYBE 203.15/82.94 203.15/82.94 We replace rewrite rules by usable rules: 203.15/82.94 203.15/82.94 Weak Usable Rules: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 203.15/82.94 We are left with following problem, upon which TcT provides the 203.15/82.94 certificate MAYBE. 203.15/82.94 203.15/82.94 Strict DPs: 203.15/82.94 { minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , plus^#(s(x), y) -> c_7(plus^#(x, y)) 203.15/82.94 , quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 Weak Trs: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 Obligation: 203.15/82.94 innermost runtime complexity 203.15/82.94 Answer: 203.15/82.94 MAYBE 203.15/82.94 203.15/82.94 None of the processors succeeded. 203.15/82.94 203.15/82.94 Details of failed attempt(s): 203.15/82.94 ----------------------------- 203.15/82.94 1) 'empty' failed due to the following reason: 203.15/82.94 203.15/82.94 Empty strict component of the problem is NOT empty. 203.15/82.94 203.15/82.94 2) 'With Problem ...' failed due to the following reason: 203.15/82.94 203.15/82.94 We decompose the input problem according to the dependency graph 203.15/82.94 into the upper component 203.15/82.94 203.15/82.94 { quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 203.15/82.94 and lower component 203.15/82.94 203.15/82.94 { minus^#(minus(x, y), z) -> 203.15/82.94 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.94 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.94 , plus^#(s(x), y) -> c_7(plus^#(x, y)) } 203.15/82.94 203.15/82.94 Further, following extension rules are added to the lower 203.15/82.94 component. 203.15/82.94 203.15/82.94 { quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.94 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.94 203.15/82.94 TcT solves the upper component with certificate YES(O(1),O(n^1)). 203.15/82.94 203.15/82.94 Sub-proof: 203.15/82.94 ---------- 203.15/82.94 We are left with following problem, upon which TcT provides the 203.15/82.94 certificate YES(O(1),O(n^1)). 203.15/82.94 203.15/82.94 Strict DPs: 203.15/82.94 { quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 Weak Trs: 203.15/82.94 { minus(x, 0()) -> x 203.15/82.94 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.94 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.94 , plus(0(), y) -> y 203.15/82.94 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.94 Obligation: 203.15/82.94 innermost runtime complexity 203.15/82.94 Answer: 203.15/82.94 YES(O(1),O(n^1)) 203.15/82.94 203.15/82.94 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 203.15/82.94 to orient following rules strictly. 203.15/82.94 203.15/82.94 DPs: 203.15/82.94 { 1: quot^#(s(x), s(y)) -> 203.15/82.94 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.94 Trs: { minus(s(x), s(y)) -> minus(x, y) } 203.15/82.94 203.15/82.94 Sub-proof: 203.15/82.94 ---------- 203.15/82.94 The input was oriented with the instance of 'Small Polynomial Path 203.15/82.94 Order (PS,1-bounded)' as induced by the safe mapping 203.15/82.95 203.15/82.95 safe(minus) = {1, 2}, safe(0) = {}, safe(s) = {1}, 203.15/82.95 safe(plus) = {1}, safe(minus^#) = {}, safe(quot^#) = {2}, 203.15/82.95 safe(c_5) = {} 203.15/82.95 203.15/82.95 and precedence 203.15/82.95 203.15/82.95 empty . 203.15/82.95 203.15/82.95 Following symbols are considered recursive: 203.15/82.95 203.15/82.95 {plus, quot^#} 203.15/82.95 203.15/82.95 The recursion depth is 1. 203.15/82.95 203.15/82.95 Further, following argument filtering is employed: 203.15/82.95 203.15/82.95 pi(minus) = 1, pi(0) = [], pi(s) = [1], pi(plus) = 2, 203.15/82.95 pi(minus^#) = [], pi(quot^#) = [1], pi(c_5) = [1, 2] 203.15/82.95 203.15/82.95 Usable defined function symbols are a subset of: 203.15/82.95 203.15/82.95 {minus, minus^#, quot^#} 203.15/82.95 203.15/82.95 For your convenience, here are the satisfied ordering constraints: 203.15/82.95 203.15/82.95 pi(quot^#(s(x), s(y))) = quot^#(s(; x);) 203.15/82.95 > c_5(quot^#(x;), minus^#();) 203.15/82.95 = pi(c_5(quot^#(minus(x, y), s(y)), minus^#(x, y))) 203.15/82.95 203.15/82.95 pi(minus(x, 0())) = x 203.15/82.95 >= x 203.15/82.95 = pi(x) 203.15/82.95 203.15/82.95 pi(minus(minus(x, y), z)) = x 203.15/82.95 >= x 203.15/82.95 = pi(minus(x, plus(y, z))) 203.15/82.95 203.15/82.95 pi(minus(s(x), s(y))) = s(; x) 203.15/82.95 > x 203.15/82.95 = pi(minus(x, y)) 203.15/82.95 203.15/82.95 203.15/82.95 The strictly oriented rules are moved into the weak component. 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(1)). 203.15/82.95 203.15/82.95 Weak DPs: 203.15/82.95 { quot^#(s(x), s(y)) -> 203.15/82.95 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(1)) 203.15/82.95 203.15/82.95 The following weak DPs constitute a sub-graph of the DG that is 203.15/82.95 closed under successors. The DPs are removed. 203.15/82.95 203.15/82.95 { quot^#(s(x), s(y)) -> 203.15/82.95 c_5(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(1)). 203.15/82.95 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(1)) 203.15/82.95 203.15/82.95 No rule is usable, rules are removed from the input problem. 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(1)). 203.15/82.95 203.15/82.95 Rules: Empty 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(1)) 203.15/82.95 203.15/82.95 Empty rules are trivially bounded 203.15/82.95 203.15/82.95 We return to the main proof. 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate MAYBE. 203.15/82.95 203.15/82.95 Strict DPs: 203.15/82.95 { minus^#(minus(x, y), z) -> 203.15/82.95 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.95 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.95 , plus^#(s(x), y) -> c_7(plus^#(x, y)) } 203.15/82.95 Weak DPs: 203.15/82.95 { quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 MAYBE 203.15/82.95 203.15/82.95 We decompose the input problem according to the dependency graph 203.15/82.95 into the upper component 203.15/82.95 203.15/82.95 { minus^#(minus(x, y), z) -> 203.15/82.95 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.95 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.95 , quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 203.15/82.95 and lower component 203.15/82.95 203.15/82.95 { plus^#(s(x), y) -> c_7(plus^#(x, y)) } 203.15/82.95 203.15/82.95 Further, following extension rules are added to the lower 203.15/82.95 component. 203.15/82.95 203.15/82.95 { minus^#(minus(x, y), z) -> minus^#(x, plus(y, z)) 203.15/82.95 , minus^#(minus(x, y), z) -> plus^#(y, z) 203.15/82.95 , minus^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 203.15/82.95 TcT solves the upper component with certificate YES(O(1),O(n^1)). 203.15/82.95 203.15/82.95 Sub-proof: 203.15/82.95 ---------- 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(n^1)). 203.15/82.95 203.15/82.95 Strict DPs: 203.15/82.95 { minus^#(minus(x, y), z) -> 203.15/82.95 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.95 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) } 203.15/82.95 Weak DPs: 203.15/82.95 { quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(n^1)) 203.15/82.95 203.15/82.95 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 203.15/82.95 to orient following rules strictly. 203.15/82.95 203.15/82.95 DPs: 203.15/82.95 { 1: minus^#(minus(x, y), z) -> 203.15/82.95 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.95 , 2: minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.95 , 3: quot^#(s(x), s(y)) -> minus^#(x, y) } 203.15/82.95 Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y } 203.15/82.95 203.15/82.95 Sub-proof: 203.15/82.95 ---------- 203.15/82.95 The input was oriented with the instance of 'Small Polynomial Path 203.15/82.95 Order (PS,1-bounded)' as induced by the safe mapping 203.15/82.95 203.15/82.95 safe(minus) = {1, 2}, safe(0) = {}, safe(s) = {1}, 203.15/82.95 safe(plus) = {2}, safe(minus^#) = {2}, safe(c_2) = {}, 203.15/82.95 safe(plus^#) = {}, safe(c_3) = {}, safe(quot^#) = {} 203.15/82.95 203.15/82.95 and precedence 203.15/82.95 203.15/82.95 quot^# > plus, quot^# > minus^#, plus ~ minus^# . 203.15/82.95 203.15/82.95 Following symbols are considered recursive: 203.15/82.95 203.15/82.95 {minus^#} 203.15/82.95 203.15/82.95 The recursion depth is 1. 203.15/82.95 203.15/82.95 Further, following argument filtering is employed: 203.15/82.95 203.15/82.95 pi(minus) = [1], pi(0) = [], pi(s) = [1], pi(plus) = [1, 2], 203.15/82.95 pi(minus^#) = [1], pi(c_2) = [1, 2], pi(plus^#) = [], 203.15/82.95 pi(c_3) = [1], pi(quot^#) = [1] 203.15/82.95 203.15/82.95 Usable defined function symbols are a subset of: 203.15/82.95 203.15/82.95 {minus, minus^#, plus^#, quot^#} 203.15/82.95 203.15/82.95 For your convenience, here are the satisfied ordering constraints: 203.15/82.95 203.15/82.95 pi(minus^#(minus(x, y), z)) = minus^#(minus(; x);) 203.15/82.95 > c_2(minus^#(x;), plus^#();) 203.15/82.95 = pi(c_2(minus^#(x, plus(y, z)), plus^#(y, z))) 203.15/82.95 203.15/82.95 pi(minus^#(s(x), s(y))) = minus^#(s(; x);) 203.15/82.95 > c_3(minus^#(x;);) 203.15/82.95 = pi(c_3(minus^#(x, y))) 203.15/82.95 203.15/82.95 pi(quot^#(s(x), s(y))) = quot^#(s(; x);) 203.15/82.95 > minus^#(x;) 203.15/82.95 = pi(minus^#(x, y)) 203.15/82.95 203.15/82.95 pi(quot^#(s(x), s(y))) = quot^#(s(; x);) 203.15/82.95 >= quot^#(minus(; x);) 203.15/82.95 = pi(quot^#(minus(x, y), s(y))) 203.15/82.95 203.15/82.95 pi(minus(x, 0())) = minus(; x) 203.15/82.95 > x 203.15/82.95 = pi(x) 203.15/82.95 203.15/82.95 pi(minus(minus(x, y), z)) = minus(; minus(; x)) 203.15/82.95 > minus(; x) 203.15/82.95 = pi(minus(x, plus(y, z))) 203.15/82.95 203.15/82.95 pi(minus(s(x), s(y))) = minus(; s(; x)) 203.15/82.95 > minus(; x) 203.15/82.95 = pi(minus(x, y)) 203.15/82.95 203.15/82.95 203.15/82.95 The strictly oriented rules are moved into the weak component. 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(1)). 203.15/82.95 203.15/82.95 Weak DPs: 203.15/82.95 { minus^#(minus(x, y), z) -> 203.15/82.95 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.95 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.95 , quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(1)) 203.15/82.95 203.15/82.95 The following weak DPs constitute a sub-graph of the DG that is 203.15/82.95 closed under successors. The DPs are removed. 203.15/82.95 203.15/82.95 { minus^#(minus(x, y), z) -> 203.15/82.95 c_2(minus^#(x, plus(y, z)), plus^#(y, z)) 203.15/82.95 , minus^#(s(x), s(y)) -> c_3(minus^#(x, y)) 203.15/82.95 , quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(1)). 203.15/82.95 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(1)) 203.15/82.95 203.15/82.95 No rule is usable, rules are removed from the input problem. 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate YES(O(1),O(1)). 203.15/82.95 203.15/82.95 Rules: Empty 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 YES(O(1),O(1)) 203.15/82.95 203.15/82.95 Empty rules are trivially bounded 203.15/82.95 203.15/82.95 We return to the main proof. 203.15/82.95 203.15/82.95 We are left with following problem, upon which TcT provides the 203.15/82.95 certificate MAYBE. 203.15/82.95 203.15/82.95 Strict DPs: { plus^#(s(x), y) -> c_7(plus^#(x, y)) } 203.15/82.95 Weak DPs: 203.15/82.95 { minus^#(minus(x, y), z) -> minus^#(x, plus(y, z)) 203.15/82.95 , minus^#(minus(x, y), z) -> plus^#(y, z) 203.15/82.95 , minus^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> minus^#(x, y) 203.15/82.95 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) } 203.15/82.95 Weak Trs: 203.15/82.95 { minus(x, 0()) -> x 203.15/82.95 , minus(minus(x, y), z) -> minus(x, plus(y, z)) 203.15/82.95 , minus(s(x), s(y)) -> minus(x, y) 203.15/82.95 , plus(0(), y) -> y 203.15/82.95 , plus(s(x), y) -> s(plus(x, y)) } 203.15/82.95 Obligation: 203.15/82.95 innermost runtime complexity 203.15/82.95 Answer: 203.15/82.95 MAYBE 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'Fastest' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'Polynomial Path Order (PS)' failed due to the following reason: 203.15/82.95 203.15/82.95 The input cannot be shown compatible 203.15/82.95 203.15/82.95 203.15/82.95 2) 'Polynomial Path Order (PS)' failed due to the following reason: 203.15/82.95 203.15/82.95 The input cannot be shown compatible 203.15/82.95 203.15/82.95 3) 'Fastest (timeout of 24 seconds)' failed due to the following 203.15/82.95 reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 203.15/82.95 failed due to the following reason: 203.15/82.95 203.15/82.95 match-boundness of the problem could not be verified. 203.15/82.95 203.15/82.95 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 203.15/82.95 failed due to the following reason: 203.15/82.95 203.15/82.95 match-boundness of the problem could not be verified. 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 2) 'Best' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 203.15/82.95 seconds)' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'Fastest' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 203.15/82.95 2) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'empty' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 2) 'With Problem ...' failed due to the following reason: 203.15/82.95 203.15/82.95 Empty strict component of the problem is NOT empty. 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 2) 'Best' failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 203.15/82.95 to the following reason: 203.15/82.95 203.15/82.95 The input cannot be shown compatible 203.15/82.95 203.15/82.95 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 203.15/82.95 following reason: 203.15/82.95 203.15/82.95 The input cannot be shown compatible 203.15/82.95 203.15/82.95 203.15/82.95 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 203.15/82.95 failed due to the following reason: 203.15/82.95 203.15/82.95 None of the processors succeeded. 203.15/82.95 203.15/82.95 Details of failed attempt(s): 203.15/82.95 ----------------------------- 203.15/82.95 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 203.15/82.95 failed due to the following reason: 203.15/82.95 203.15/82.95 match-boundness of the problem could not be verified. 203.15/82.95 203.15/82.95 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 203.15/82.95 failed due to the following reason: 203.15/82.95 203.15/82.95 match-boundness of the problem could not be verified. 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 203.15/82.95 Arrrr.. 203.28/83.04 EOF