YES(O(1),O(n^4)) 687.50/196.58 YES(O(1),O(n^4)) 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^4)). 687.50/196.58 687.50/196.58 Strict Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 687.50/196.58 , log(s(0())) -> 0() 687.50/196.58 , log(s(s(x))) -> s(log(s(quot(x, s(s(0())))))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^4)) 687.50/196.58 687.50/196.58 We add the following dependency tuples: 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { le^#(0(), y) -> c_1() 687.50/196.58 , le^#(s(x), 0()) -> c_2() 687.50/196.58 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(0(), y) -> c_4() 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(true(), s(x), y) -> c_6() 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(0(), s(y)) -> c_8() 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , log^#(s(0())) -> c_10() 687.50/196.58 , log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 687.50/196.58 and mark the set of starting terms. 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^4)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { le^#(0(), y) -> c_1() 687.50/196.58 , le^#(s(x), 0()) -> c_2() 687.50/196.58 , le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(0(), y) -> c_4() 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(true(), s(x), y) -> c_6() 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(0(), s(y)) -> c_8() 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , log^#(s(0())) -> c_10() 687.50/196.58 , log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 687.50/196.58 , log(s(0())) -> 0() 687.50/196.58 , log(s(s(x))) -> s(log(s(quot(x, s(s(0())))))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^4)) 687.50/196.58 687.50/196.58 We estimate the number of application of {1,2,4,6,8,10} by 687.50/196.58 applications of Pre({1,2,4,6,8,10}) = {3,5,7,9,11}. Here rules are 687.50/196.58 labeled as follows: 687.50/196.58 687.50/196.58 DPs: 687.50/196.58 { 1: le^#(0(), y) -> c_1() 687.50/196.58 , 2: le^#(s(x), 0()) -> c_2() 687.50/196.58 , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , 4: minus^#(0(), y) -> c_4() 687.50/196.58 , 5: minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , 6: if_minus^#(true(), s(x), y) -> c_6() 687.50/196.58 , 7: if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , 8: quot^#(0(), s(y)) -> c_8() 687.50/196.58 , 9: quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , 10: log^#(s(0())) -> c_10() 687.50/196.58 , 11: log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^4)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Weak DPs: 687.50/196.58 { le^#(0(), y) -> c_1() 687.50/196.58 , le^#(s(x), 0()) -> c_2() 687.50/196.58 , minus^#(0(), y) -> c_4() 687.50/196.58 , if_minus^#(true(), s(x), y) -> c_6() 687.50/196.58 , quot^#(0(), s(y)) -> c_8() 687.50/196.58 , log^#(s(0())) -> c_10() } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 687.50/196.58 , log(s(0())) -> 0() 687.50/196.58 , log(s(s(x))) -> s(log(s(quot(x, s(s(0())))))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^4)) 687.50/196.58 687.50/196.58 The following weak DPs constitute a sub-graph of the DG that is 687.50/196.58 closed under successors. The DPs are removed. 687.50/196.58 687.50/196.58 { le^#(0(), y) -> c_1() 687.50/196.58 , le^#(s(x), 0()) -> c_2() 687.50/196.58 , minus^#(0(), y) -> c_4() 687.50/196.58 , if_minus^#(true(), s(x), y) -> c_6() 687.50/196.58 , quot^#(0(), s(y)) -> c_8() 687.50/196.58 , log^#(s(0())) -> c_10() } 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^4)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 687.50/196.58 , log(s(0())) -> 0() 687.50/196.58 , log(s(s(x))) -> s(log(s(quot(x, s(s(0())))))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^4)) 687.50/196.58 687.50/196.58 We replace rewrite rules by usable rules: 687.50/196.58 687.50/196.58 Weak Usable Rules: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^4)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^4)) 687.50/196.58 687.50/196.58 We decompose the input problem according to the dependency graph 687.50/196.58 into the upper component 687.50/196.58 687.50/196.58 { log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 687.50/196.58 and lower component 687.50/196.58 687.50/196.58 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 687.50/196.58 687.50/196.58 Further, following extension rules are added to the lower 687.50/196.58 component. 687.50/196.58 687.50/196.58 { log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.58 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.58 687.50/196.58 TcT solves the upper component with certificate YES(O(1),O(n^1)). 687.50/196.58 687.50/196.58 Sub-proof: 687.50/196.58 ---------- 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^1)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^1)) 687.50/196.58 687.50/196.58 We use the processor 'matrix interpretation of dimension 1' to 687.50/196.58 orient following rules strictly. 687.50/196.58 687.50/196.58 DPs: 687.50/196.58 { 1: log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Trs: { if_minus(true(), s(x), y) -> 0() } 687.50/196.58 687.50/196.58 Sub-proof: 687.50/196.58 ---------- 687.50/196.58 The following argument positions are usable: 687.50/196.58 Uargs(c_11) = {1} 687.50/196.58 687.50/196.58 TcT has computed the following constructor-based matrix 687.50/196.58 interpretation satisfying not(EDA). 687.50/196.58 687.50/196.58 [le](x1, x2) = [0] 687.50/196.58 687.50/196.58 [0] = [0] 687.50/196.58 687.50/196.58 [true] = [0] 687.50/196.58 687.50/196.58 [s](x1) = [1] x1 + [1] 687.50/196.58 687.50/196.58 [false] = [0] 687.50/196.58 687.50/196.58 [minus](x1, x2) = [1] x1 + [0] 687.50/196.58 687.50/196.58 [if_minus](x1, x2, x3) = [1] x2 + [0] 687.50/196.58 687.50/196.58 [quot](x1, x2) = [1] x1 + [0] 687.50/196.58 687.50/196.58 [quot^#](x1, x2) = [7] x1 + [7] 687.50/196.58 687.50/196.58 [log^#](x1) = [1] x1 + [0] 687.50/196.58 687.50/196.58 [c_11](x1, x2) = [1] x1 + [0] 687.50/196.58 687.50/196.58 The order satisfies the following ordering constraints: 687.50/196.58 687.50/196.58 [le(0(), y)] = [0] 687.50/196.58 >= [0] 687.50/196.58 = [true()] 687.50/196.58 687.50/196.58 [le(s(x), 0())] = [0] 687.50/196.58 >= [0] 687.50/196.58 = [false()] 687.50/196.58 687.50/196.58 [le(s(x), s(y))] = [0] 687.50/196.58 >= [0] 687.50/196.58 = [le(x, y)] 687.50/196.58 687.50/196.58 [minus(0(), y)] = [0] 687.50/196.58 >= [0] 687.50/196.58 = [0()] 687.50/196.58 687.50/196.58 [minus(s(x), y)] = [1] x + [1] 687.50/196.58 >= [1] x + [1] 687.50/196.58 = [if_minus(le(s(x), y), s(x), y)] 687.50/196.58 687.50/196.58 [if_minus(true(), s(x), y)] = [1] x + [1] 687.50/196.58 > [0] 687.50/196.58 = [0()] 687.50/196.58 687.50/196.58 [if_minus(false(), s(x), y)] = [1] x + [1] 687.50/196.58 >= [1] x + [1] 687.50/196.58 = [s(minus(x, y))] 687.50/196.58 687.50/196.58 [quot(0(), s(y))] = [0] 687.50/196.58 >= [0] 687.50/196.58 = [0()] 687.50/196.58 687.50/196.58 [quot(s(x), s(y))] = [1] x + [1] 687.50/196.58 >= [1] x + [1] 687.50/196.58 = [s(quot(minus(x, y), s(y)))] 687.50/196.58 687.50/196.58 [log^#(s(s(x)))] = [1] x + [2] 687.50/196.58 > [1] x + [1] 687.50/196.58 = [c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0()))))] 687.50/196.58 687.50/196.58 687.50/196.58 The strictly oriented rules are moved into the weak component. 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(1)). 687.50/196.58 687.50/196.58 Weak DPs: 687.50/196.58 { log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(1)) 687.50/196.58 687.50/196.58 The following weak DPs constitute a sub-graph of the DG that is 687.50/196.58 closed under successors. The DPs are removed. 687.50/196.58 687.50/196.58 { log^#(s(s(x))) -> 687.50/196.58 c_11(log^#(s(quot(x, s(s(0()))))), quot^#(x, s(s(0())))) } 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(1)). 687.50/196.58 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(1)) 687.50/196.58 687.50/196.58 No rule is usable, rules are removed from the input problem. 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(1)). 687.50/196.58 687.50/196.58 Rules: Empty 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(1)) 687.50/196.58 687.50/196.58 Empty rules are trivially bounded 687.50/196.58 687.50/196.58 We return to the main proof. 687.50/196.58 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^3)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.58 , quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 687.50/196.58 Weak DPs: 687.50/196.58 { log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.58 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.58 , minus(0(), y) -> 0() 687.50/196.58 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.58 , if_minus(true(), s(x), y) -> 0() 687.50/196.58 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.58 , quot(0(), s(y)) -> 0() 687.50/196.58 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.58 Obligation: 687.50/196.58 innermost runtime complexity 687.50/196.58 Answer: 687.50/196.58 YES(O(1),O(n^3)) 687.50/196.58 687.50/196.58 We decompose the input problem according to the dependency graph 687.50/196.58 into the upper component 687.50/196.58 687.50/196.58 { quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.58 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.58 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.58 687.50/196.58 and lower component 687.50/196.58 687.50/196.58 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.58 , minus^#(s(x), y) -> 687.50/196.58 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.58 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) } 687.50/196.58 687.50/196.58 Further, following extension rules are added to the lower 687.50/196.58 component. 687.50/196.58 687.50/196.58 { quot^#(s(x), s(y)) -> minus^#(x, y) 687.50/196.58 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 687.50/196.58 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.58 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.58 687.50/196.58 TcT solves the upper component with certificate YES(O(1),O(n^1)). 687.50/196.58 687.50/196.58 Sub-proof: 687.50/196.58 ---------- 687.50/196.58 We are left with following problem, upon which TcT provides the 687.50/196.58 certificate YES(O(1),O(n^1)). 687.50/196.58 687.50/196.58 Strict DPs: 687.50/196.58 { quot^#(s(x), s(y)) -> 687.50/196.58 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) } 687.50/196.58 Weak DPs: 687.50/196.58 { log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.58 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.58 Weak Trs: 687.50/196.58 { le(0(), y) -> true() 687.50/196.58 , le(s(x), 0()) -> false() 687.50/196.58 , le(s(x), s(y)) -> le(x, y) 687.50/196.59 , minus(0(), y) -> 0() 687.50/196.59 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.59 , if_minus(true(), s(x), y) -> 0() 687.50/196.59 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.59 , quot(0(), s(y)) -> 0() 687.50/196.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(n^1)) 687.50/196.59 687.50/196.59 We use the processor 'matrix interpretation of dimension 1' to 687.50/196.59 orient following rules strictly. 687.50/196.59 687.50/196.59 DPs: 687.50/196.59 { 1: quot^#(s(x), s(y)) -> 687.50/196.59 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.59 , 2: log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , 3: log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 Trs: { if_minus(true(), s(x), y) -> 0() } 687.50/196.59 687.50/196.59 Sub-proof: 687.50/196.59 ---------- 687.50/196.59 The following argument positions are usable: 687.50/196.59 Uargs(c_9) = {1} 687.50/196.59 687.50/196.59 TcT has computed the following constructor-based matrix 687.50/196.59 interpretation satisfying not(EDA). 687.50/196.59 687.50/196.59 [le](x1, x2) = [0] 687.50/196.59 687.50/196.59 [0] = [0] 687.50/196.59 687.50/196.59 [true] = [0] 687.50/196.59 687.50/196.59 [s](x1) = [1] x1 + [1] 687.50/196.59 687.50/196.59 [false] = [0] 687.50/196.59 687.50/196.59 [minus](x1, x2) = [1] x1 + [0] 687.50/196.59 687.50/196.59 [if_minus](x1, x2, x3) = [1] x2 + [0] 687.50/196.59 687.50/196.59 [quot](x1, x2) = [1] x1 + [0] 687.50/196.59 687.50/196.59 [minus^#](x1, x2) = [7] x1 + [7] x2 + [7] 687.50/196.59 687.50/196.59 [quot^#](x1, x2) = [4] x1 + [0] 687.50/196.59 687.50/196.59 [c_9](x1, x2) = [1] x1 + [1] 687.50/196.59 687.50/196.59 [log^#](x1) = [4] x1 + [0] 687.50/196.59 687.50/196.59 The order satisfies the following ordering constraints: 687.50/196.59 687.50/196.59 [le(0(), y)] = [0] 687.50/196.59 >= [0] 687.50/196.59 = [true()] 687.50/196.59 687.50/196.59 [le(s(x), 0())] = [0] 687.50/196.59 >= [0] 687.50/196.59 = [false()] 687.50/196.59 687.50/196.59 [le(s(x), s(y))] = [0] 687.50/196.59 >= [0] 687.50/196.59 = [le(x, y)] 687.50/196.59 687.50/196.59 [minus(0(), y)] = [0] 687.50/196.59 >= [0] 687.50/196.59 = [0()] 687.50/196.59 687.50/196.59 [minus(s(x), y)] = [1] x + [1] 687.50/196.59 >= [1] x + [1] 687.50/196.59 = [if_minus(le(s(x), y), s(x), y)] 687.50/196.59 687.50/196.59 [if_minus(true(), s(x), y)] = [1] x + [1] 687.50/196.59 > [0] 687.50/196.59 = [0()] 687.50/196.59 687.50/196.59 [if_minus(false(), s(x), y)] = [1] x + [1] 687.50/196.59 >= [1] x + [1] 687.50/196.59 = [s(minus(x, y))] 687.50/196.59 687.50/196.59 [quot(0(), s(y))] = [0] 687.50/196.59 >= [0] 687.50/196.59 = [0()] 687.50/196.59 687.50/196.59 [quot(s(x), s(y))] = [1] x + [1] 687.50/196.59 >= [1] x + [1] 687.50/196.59 = [s(quot(minus(x, y), s(y)))] 687.50/196.59 687.50/196.59 [quot^#(s(x), s(y))] = [4] x + [4] 687.50/196.59 > [4] x + [1] 687.50/196.59 = [c_9(quot^#(minus(x, y), s(y)), minus^#(x, y))] 687.50/196.59 687.50/196.59 [log^#(s(s(x)))] = [4] x + [8] 687.50/196.59 > [4] x + [0] 687.50/196.59 = [quot^#(x, s(s(0())))] 687.50/196.59 687.50/196.59 [log^#(s(s(x)))] = [4] x + [8] 687.50/196.59 > [4] x + [4] 687.50/196.59 = [log^#(s(quot(x, s(s(0())))))] 687.50/196.59 687.50/196.59 687.50/196.59 The strictly oriented rules are moved into the weak component. 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(1)). 687.50/196.59 687.50/196.59 Weak DPs: 687.50/196.59 { quot^#(s(x), s(y)) -> 687.50/196.59 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.59 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 Weak Trs: 687.50/196.59 { le(0(), y) -> true() 687.50/196.59 , le(s(x), 0()) -> false() 687.50/196.59 , le(s(x), s(y)) -> le(x, y) 687.50/196.59 , minus(0(), y) -> 0() 687.50/196.59 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.59 , if_minus(true(), s(x), y) -> 0() 687.50/196.59 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.59 , quot(0(), s(y)) -> 0() 687.50/196.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(1)) 687.50/196.59 687.50/196.59 The following weak DPs constitute a sub-graph of the DG that is 687.50/196.59 closed under successors. The DPs are removed. 687.50/196.59 687.50/196.59 { quot^#(s(x), s(y)) -> 687.50/196.59 c_9(quot^#(minus(x, y), s(y)), minus^#(x, y)) 687.50/196.59 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(1)). 687.50/196.59 687.50/196.59 Weak Trs: 687.50/196.59 { le(0(), y) -> true() 687.50/196.59 , le(s(x), 0()) -> false() 687.50/196.59 , le(s(x), s(y)) -> le(x, y) 687.50/196.59 , minus(0(), y) -> 0() 687.50/196.59 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.59 , if_minus(true(), s(x), y) -> 0() 687.50/196.59 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.59 , quot(0(), s(y)) -> 0() 687.50/196.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(1)) 687.50/196.59 687.50/196.59 No rule is usable, rules are removed from the input problem. 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(1)). 687.50/196.59 687.50/196.59 Rules: Empty 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(1)) 687.50/196.59 687.50/196.59 Empty rules are trivially bounded 687.50/196.59 687.50/196.59 We return to the main proof. 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(n^2)). 687.50/196.59 687.50/196.59 Strict DPs: 687.50/196.59 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.59 , minus^#(s(x), y) -> 687.50/196.59 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.59 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) } 687.50/196.59 Weak DPs: 687.50/196.59 { quot^#(s(x), s(y)) -> minus^#(x, y) 687.50/196.59 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 687.50/196.59 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 Weak Trs: 687.50/196.59 { le(0(), y) -> true() 687.50/196.59 , le(s(x), 0()) -> false() 687.50/196.59 , le(s(x), s(y)) -> le(x, y) 687.50/196.59 , minus(0(), y) -> 0() 687.50/196.59 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.59 , if_minus(true(), s(x), y) -> 0() 687.50/196.59 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.59 , quot(0(), s(y)) -> 0() 687.50/196.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(n^2)) 687.50/196.59 687.50/196.59 We use the processor 'matrix interpretation of dimension 2' to 687.50/196.59 orient following rules strictly. 687.50/196.59 687.50/196.59 DPs: 687.50/196.59 { 1: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.59 , 2: minus^#(s(x), y) -> 687.50/196.59 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.59 , 4: quot^#(s(x), s(y)) -> minus^#(x, y) 687.50/196.59 , 7: log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 687.50/196.59 Sub-proof: 687.50/196.59 ---------- 687.50/196.59 The following argument positions are usable: 687.50/196.59 Uargs(c_3) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_7) = {1} 687.50/196.59 687.50/196.59 TcT has computed the following constructor-based matrix 687.50/196.59 interpretation satisfying not(EDA). 687.50/196.59 687.50/196.59 [le](x1, x2) = [0] 687.50/196.59 [0] 687.50/196.59 687.50/196.59 [0] = [0] 687.50/196.59 [0] 687.50/196.59 687.50/196.59 [true] = [0] 687.50/196.59 [0] 687.50/196.59 687.50/196.59 [s](x1) = [1 1] x1 + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 687.50/196.59 [false] = [0] 687.50/196.59 [0] 687.50/196.59 687.50/196.59 [minus](x1, x2) = [1 0] x1 + [0] 687.50/196.59 [0 1] [0] 687.50/196.59 687.50/196.59 [if_minus](x1, x2, x3) = [1 0] x2 + [0] 687.50/196.59 [0 1] [0] 687.50/196.59 687.50/196.59 [quot](x1, x2) = [1 0] x1 + [0] 687.50/196.59 [0 1] [0] 687.50/196.59 687.50/196.59 [le^#](x1, x2) = [0 1] x1 + [0 0] x2 + [0] 687.50/196.59 [0 1] [7 1] [0] 687.50/196.59 687.50/196.59 [c_3](x1) = [1 0] x1 + [1] 687.50/196.59 [0 0] [3] 687.50/196.59 687.50/196.59 [minus^#](x1, x2) = [1 2] x1 + [4] 687.50/196.59 [0 0] [0] 687.50/196.59 687.50/196.59 [c_5](x1, x2) = [1 0] x1 + [1 0] x2 + [3] 687.50/196.59 [0 0] [0 0] [0] 687.50/196.59 687.50/196.59 [if_minus^#](x1, x2, x3) = [1 1] x2 + [0 0] x3 + [0] 687.50/196.59 [0 0] [4 0] [0] 687.50/196.59 687.50/196.59 [c_7](x1) = [1 0] x1 + [0] 687.50/196.59 [0 0] [0] 687.50/196.59 687.50/196.59 [quot^#](x1, x2) = [2 0] x1 + [0 1] x2 + [4] 687.50/196.59 [0 0] [0 0] [0] 687.50/196.59 687.50/196.59 [log^#](x1) = [2 0] x1 + [4] 687.50/196.59 [0 0] [0] 687.50/196.59 687.50/196.59 The order satisfies the following ordering constraints: 687.50/196.59 687.50/196.59 [le(0(), y)] = [0] 687.50/196.59 [0] 687.50/196.59 >= [0] 687.50/196.59 [0] 687.50/196.59 = [true()] 687.50/196.59 687.50/196.59 [le(s(x), 0())] = [0] 687.50/196.59 [0] 687.50/196.59 >= [0] 687.50/196.59 [0] 687.50/196.59 = [false()] 687.50/196.59 687.50/196.59 [le(s(x), s(y))] = [0] 687.50/196.59 [0] 687.50/196.59 >= [0] 687.50/196.59 [0] 687.50/196.59 = [le(x, y)] 687.50/196.59 687.50/196.59 [minus(0(), y)] = [0] 687.50/196.59 [0] 687.50/196.59 >= [0] 687.50/196.59 [0] 687.50/196.59 = [0()] 687.50/196.59 687.50/196.59 [minus(s(x), y)] = [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 >= [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 = [if_minus(le(s(x), y), s(x), y)] 687.50/196.59 687.50/196.59 [if_minus(true(), s(x), y)] = [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 >= [0] 687.50/196.59 [0] 687.50/196.59 = [0()] 687.50/196.59 687.50/196.59 [if_minus(false(), s(x), y)] = [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 >= [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 = [s(minus(x, y))] 687.50/196.59 687.50/196.59 [quot(0(), s(y))] = [0] 687.50/196.59 [0] 687.50/196.59 >= [0] 687.50/196.59 [0] 687.50/196.59 = [0()] 687.50/196.59 687.50/196.59 [quot(s(x), s(y))] = [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 >= [1 1] x + [0] 687.50/196.59 [0 1] [4] 687.50/196.59 = [s(quot(minus(x, y), s(y)))] 687.50/196.59 687.50/196.59 [le^#(s(x), s(y))] = [0 0] y + [0 1] x + [4] 687.50/196.59 [7 8] [0 1] [8] 687.50/196.59 > [0 1] x + [1] 687.50/196.59 [0 0] [3] 687.50/196.59 = [c_3(le^#(x, y))] 687.50/196.59 687.50/196.59 [minus^#(s(x), y)] = [1 3] x + [12] 687.50/196.59 [0 0] [0] 687.50/196.59 > [1 3] x + [11] 687.50/196.59 [0 0] [0] 687.50/196.59 = [c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y))] 687.50/196.59 687.50/196.59 [if_minus^#(false(), s(x), y)] = [0 0] y + [1 2] x + [4] 687.50/196.59 [4 0] [0 0] [0] 687.50/196.59 >= [1 2] x + [4] 687.50/196.59 [0 0] [0] 687.50/196.59 = [c_7(minus^#(x, y))] 687.50/196.59 687.50/196.59 [quot^#(s(x), s(y))] = [0 1] y + [2 2] x + [8] 687.50/196.59 [0 0] [0 0] [0] 687.50/196.59 > [1 2] x + [4] 687.50/196.59 [0 0] [0] 687.50/196.59 = [minus^#(x, y)] 687.50/196.59 687.50/196.59 [quot^#(s(x), s(y))] = [0 1] y + [2 2] x + [8] 687.50/196.59 [0 0] [0 0] [0] 687.50/196.59 >= [0 1] y + [2 0] x + [8] 687.50/196.59 [0 0] [0 0] [0] 687.50/196.59 = [quot^#(minus(x, y), s(y))] 687.50/196.59 687.50/196.59 [log^#(s(s(x)))] = [2 4] x + [12] 687.50/196.59 [0 0] [0] 687.50/196.59 >= [2 0] x + [12] 687.50/196.59 [0 0] [0] 687.50/196.59 = [quot^#(x, s(s(0())))] 687.50/196.59 687.50/196.59 [log^#(s(s(x)))] = [2 4] x + [12] 687.50/196.59 [0 0] [0] 687.50/196.59 > [2 2] x + [4] 687.50/196.59 [0 0] [0] 687.50/196.59 = [log^#(s(quot(x, s(s(0())))))] 687.50/196.59 687.50/196.59 687.50/196.59 We return to the main proof. Consider the set of all dependency 687.50/196.59 pairs 687.50/196.59 687.50/196.59 : 687.50/196.59 { 1: le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.59 , 2: minus^#(s(x), y) -> 687.50/196.59 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.59 , 3: if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.59 , 4: quot^#(s(x), s(y)) -> minus^#(x, y) 687.50/196.59 , 5: quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 687.50/196.59 , 6: log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , 7: log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 687.50/196.59 Processor 'matrix interpretation of dimension 2' induces the 687.50/196.59 complexity certificate YES(?,O(n^2)) on application of dependency 687.50/196.59 pairs {1,2,4,7}. These cover all (indirect) predecessors of 687.50/196.59 dependency pairs {1,2,3,4,6,7}, their number of application is 687.50/196.59 equally bounded. The dependency pairs are shifted into the weak 687.50/196.59 component. 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(1)). 687.50/196.59 687.50/196.59 Weak DPs: 687.50/196.59 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.59 , minus^#(s(x), y) -> 687.50/196.59 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.59 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.59 , quot^#(s(x), s(y)) -> minus^#(x, y) 687.50/196.59 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 687.50/196.59 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 Weak Trs: 687.50/196.59 { le(0(), y) -> true() 687.50/196.59 , le(s(x), 0()) -> false() 687.50/196.59 , le(s(x), s(y)) -> le(x, y) 687.50/196.59 , minus(0(), y) -> 0() 687.50/196.59 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.59 , if_minus(true(), s(x), y) -> 0() 687.50/196.59 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.59 , quot(0(), s(y)) -> 0() 687.50/196.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(1)) 687.50/196.59 687.50/196.59 The following weak DPs constitute a sub-graph of the DG that is 687.50/196.59 closed under successors. The DPs are removed. 687.50/196.59 687.50/196.59 { le^#(s(x), s(y)) -> c_3(le^#(x, y)) 687.50/196.59 , minus^#(s(x), y) -> 687.50/196.59 c_5(if_minus^#(le(s(x), y), s(x), y), le^#(s(x), y)) 687.50/196.59 , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y)) 687.50/196.59 , quot^#(s(x), s(y)) -> minus^#(x, y) 687.50/196.59 , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) 687.50/196.59 , log^#(s(s(x))) -> quot^#(x, s(s(0()))) 687.50/196.59 , log^#(s(s(x))) -> log^#(s(quot(x, s(s(0()))))) } 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(1)). 687.50/196.59 687.50/196.59 Weak Trs: 687.50/196.59 { le(0(), y) -> true() 687.50/196.59 , le(s(x), 0()) -> false() 687.50/196.59 , le(s(x), s(y)) -> le(x, y) 687.50/196.59 , minus(0(), y) -> 0() 687.50/196.59 , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y) 687.50/196.59 , if_minus(true(), s(x), y) -> 0() 687.50/196.59 , if_minus(false(), s(x), y) -> s(minus(x, y)) 687.50/196.59 , quot(0(), s(y)) -> 0() 687.50/196.59 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) } 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(1)) 687.50/196.59 687.50/196.59 No rule is usable, rules are removed from the input problem. 687.50/196.59 687.50/196.59 We are left with following problem, upon which TcT provides the 687.50/196.59 certificate YES(O(1),O(1)). 687.50/196.59 687.50/196.59 Rules: Empty 687.50/196.59 Obligation: 687.50/196.59 innermost runtime complexity 687.50/196.59 Answer: 687.50/196.59 YES(O(1),O(1)) 687.50/196.59 687.50/196.59 Empty rules are trivially bounded 687.50/196.59 687.50/196.59 Hurray, we answered YES(O(1),O(n^4)) 687.80/196.64 EOF