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