MAYBE 351.40/144.46 MAYBE 351.40/144.46 351.40/144.46 We are left with following problem, upon which TcT provides the 351.40/144.46 certificate MAYBE. 351.40/144.46 351.40/144.46 Strict Trs: 351.40/144.46 { minus(x, 0()) -> x 351.40/144.46 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.46 , double(0()) -> 0() 351.40/144.46 , double(s(x)) -> s(s(double(x))) 351.40/144.46 , plus(0(), y) -> y 351.40/144.46 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.46 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.46 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.46 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.46 Obligation: 351.40/144.46 innermost runtime complexity 351.40/144.46 Answer: 351.40/144.46 MAYBE 351.40/144.46 351.40/144.46 None of the processors succeeded. 351.40/144.46 351.40/144.46 Details of failed attempt(s): 351.40/144.46 ----------------------------- 351.40/144.46 1) 'empty' failed due to the following reason: 351.40/144.46 351.40/144.46 Empty strict component of the problem is NOT empty. 351.40/144.46 351.40/144.46 2) 'Best' failed due to the following reason: 351.40/144.46 351.40/144.46 None of the processors succeeded. 351.40/144.46 351.40/144.46 Details of failed attempt(s): 351.40/144.46 ----------------------------- 351.40/144.46 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 351.40/144.46 following reason: 351.40/144.46 351.40/144.46 We add the following dependency tuples: 351.40/144.46 351.40/144.46 Strict DPs: 351.40/144.46 { minus^#(x, 0()) -> c_1() 351.40/144.46 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 351.40/144.46 , double^#(0()) -> c_3() 351.40/144.46 , double^#(s(x)) -> c_4(double^#(x)) 351.40/144.46 , plus^#(0(), y) -> c_5() 351.40/144.46 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 351.40/144.46 , plus^#(s(x), y) -> 351.40/144.46 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) 351.40/144.46 , plus^#(s(plus(x, y)), z) -> 351.40/144.46 c_9(plus^#(plus(x, y), z), plus^#(x, y)) } 351.40/144.46 351.40/144.46 and mark the set of starting terms. 351.40/144.46 351.40/144.46 We are left with following problem, upon which TcT provides the 351.40/144.46 certificate MAYBE. 351.40/144.46 351.40/144.46 Strict DPs: 351.40/144.46 { minus^#(x, 0()) -> c_1() 351.40/144.46 , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 351.40/144.46 , double^#(0()) -> c_3() 351.40/144.46 , double^#(s(x)) -> c_4(double^#(x)) 351.40/144.46 , plus^#(0(), y) -> c_5() 351.40/144.46 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 351.40/144.46 , plus^#(s(x), y) -> 351.40/144.46 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) 351.40/144.46 , plus^#(s(plus(x, y)), z) -> 351.40/144.46 c_9(plus^#(plus(x, y), z), plus^#(x, y)) } 351.40/144.46 Weak Trs: 351.40/144.46 { minus(x, 0()) -> x 351.40/144.46 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.46 , double(0()) -> 0() 351.40/144.46 , double(s(x)) -> s(s(double(x))) 351.40/144.46 , plus(0(), y) -> y 351.40/144.46 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.46 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.46 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.46 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.46 Obligation: 351.40/144.46 innermost runtime complexity 351.40/144.46 Answer: 351.40/144.46 MAYBE 351.40/144.46 351.40/144.46 We estimate the number of application of {1,3,5} by applications of 351.40/144.46 Pre({1,3,5}) = {2,4,6,7,8,9}. Here rules are labeled as follows: 351.40/144.46 351.40/144.46 DPs: 351.40/144.46 { 1: minus^#(x, 0()) -> c_1() 351.40/144.46 , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 351.40/144.46 , 3: double^#(0()) -> c_3() 351.40/144.46 , 4: double^#(s(x)) -> c_4(double^#(x)) 351.40/144.46 , 5: plus^#(0(), y) -> c_5() 351.40/144.46 , 6: plus^#(s(x), y) -> c_6(plus^#(x, y)) 351.40/144.46 , 7: plus^#(s(x), y) -> 351.40/144.46 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , 8: plus^#(s(x), y) -> c_8(plus^#(x, s(y))) 351.40/144.46 , 9: plus^#(s(plus(x, y)), z) -> 351.40/144.46 c_9(plus^#(plus(x, y), z), plus^#(x, y)) } 351.40/144.46 351.40/144.46 We are left with following problem, upon which TcT provides the 351.40/144.46 certificate MAYBE. 351.40/144.46 351.40/144.46 Strict DPs: 351.40/144.46 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 351.40/144.46 , double^#(s(x)) -> c_4(double^#(x)) 351.40/144.46 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 351.40/144.46 , plus^#(s(x), y) -> 351.40/144.46 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) 351.40/144.46 , plus^#(s(plus(x, y)), z) -> 351.40/144.46 c_9(plus^#(plus(x, y), z), plus^#(x, y)) } 351.40/144.46 Weak DPs: 351.40/144.46 { minus^#(x, 0()) -> c_1() 351.40/144.46 , double^#(0()) -> c_3() 351.40/144.46 , plus^#(0(), y) -> c_5() } 351.40/144.46 Weak Trs: 351.40/144.46 { minus(x, 0()) -> x 351.40/144.46 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.46 , double(0()) -> 0() 351.40/144.46 , double(s(x)) -> s(s(double(x))) 351.40/144.46 , plus(0(), y) -> y 351.40/144.46 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.46 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.46 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.46 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.46 Obligation: 351.40/144.46 innermost runtime complexity 351.40/144.46 Answer: 351.40/144.46 MAYBE 351.40/144.46 351.40/144.46 The following weak DPs constitute a sub-graph of the DG that is 351.40/144.46 closed under successors. The DPs are removed. 351.40/144.46 351.40/144.46 { minus^#(x, 0()) -> c_1() 351.40/144.46 , double^#(0()) -> c_3() 351.40/144.46 , plus^#(0(), y) -> c_5() } 351.40/144.46 351.40/144.46 We are left with following problem, upon which TcT provides the 351.40/144.46 certificate MAYBE. 351.40/144.46 351.40/144.46 Strict DPs: 351.40/144.46 { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) 351.40/144.46 , double^#(s(x)) -> c_4(double^#(x)) 351.40/144.46 , plus^#(s(x), y) -> c_6(plus^#(x, y)) 351.40/144.46 , plus^#(s(x), y) -> 351.40/144.46 c_7(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , plus^#(s(x), y) -> c_8(plus^#(x, s(y))) 351.40/144.46 , plus^#(s(plus(x, y)), z) -> 351.40/144.46 c_9(plus^#(plus(x, y), z), plus^#(x, y)) } 351.40/144.46 Weak Trs: 351.40/144.46 { minus(x, 0()) -> x 351.40/144.46 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.46 , double(0()) -> 0() 351.40/144.46 , double(s(x)) -> s(s(double(x))) 351.40/144.46 , plus(0(), y) -> y 351.40/144.46 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.46 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.46 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.46 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.46 Obligation: 351.40/144.46 innermost runtime complexity 351.40/144.46 Answer: 351.40/144.46 MAYBE 351.40/144.46 351.40/144.46 Due to missing edges in the dependency-graph, the right-hand sides 351.40/144.46 of following rules could be simplified: 351.40/144.46 351.40/144.46 { plus^#(s(plus(x, y)), z) -> 351.40/144.46 c_9(plus^#(plus(x, y), z), plus^#(x, y)) } 351.40/144.46 351.40/144.46 We are left with following problem, upon which TcT provides the 351.40/144.46 certificate MAYBE. 351.40/144.46 351.40/144.46 Strict DPs: 351.40/144.46 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 351.40/144.46 , double^#(s(x)) -> c_2(double^#(x)) 351.40/144.46 , plus^#(s(x), y) -> c_3(plus^#(x, y)) 351.40/144.46 , plus^#(s(x), y) -> 351.40/144.46 c_4(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , plus^#(s(x), y) -> c_5(plus^#(x, s(y))) 351.40/144.46 , plus^#(s(plus(x, y)), z) -> c_6(plus^#(plus(x, y), z)) } 351.40/144.46 Weak Trs: 351.40/144.46 { minus(x, 0()) -> x 351.40/144.46 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.46 , double(0()) -> 0() 351.40/144.46 , double(s(x)) -> s(s(double(x))) 351.40/144.46 , plus(0(), y) -> y 351.40/144.46 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.46 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.46 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.46 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.46 Obligation: 351.40/144.46 innermost runtime complexity 351.40/144.46 Answer: 351.40/144.46 MAYBE 351.40/144.46 351.40/144.46 None of the processors succeeded. 351.40/144.46 351.40/144.46 Details of failed attempt(s): 351.40/144.46 ----------------------------- 351.40/144.46 1) 'empty' failed due to the following reason: 351.40/144.46 351.40/144.46 Empty strict component of the problem is NOT empty. 351.40/144.46 351.40/144.46 2) 'With Problem ...' failed due to the following reason: 351.40/144.46 351.40/144.46 We use the processor 'matrix interpretation of dimension 2' to 351.40/144.46 orient following rules strictly. 351.40/144.46 351.40/144.46 DPs: 351.40/144.46 { 1: minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 351.40/144.46 , 3: plus^#(s(x), y) -> c_3(plus^#(x, y)) 351.40/144.46 , 4: plus^#(s(x), y) -> 351.40/144.46 c_4(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.46 , 5: plus^#(s(x), y) -> c_5(plus^#(x, s(y))) 351.40/144.46 , 6: plus^#(s(plus(x, y)), z) -> c_6(plus^#(plus(x, y), z)) } 351.40/144.46 Trs: { minus(s(x), s(y)) -> minus(x, y) } 351.40/144.46 351.40/144.46 Sub-proof: 351.40/144.46 ---------- 351.40/144.46 The following argument positions are usable: 351.40/144.46 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 351.40/144.46 Uargs(c_4) = {1, 2, 3}, Uargs(c_5) = {1} 351.40/144.46 351.40/144.46 TcT has computed the following constructor-based matrix 351.40/144.46 interpretation satisfying not(EDA). 351.40/144.46 351.40/144.46 [minus](x1, x2) = [1 0] x1 + [0] 351.40/144.46 [0 1] [0] 351.40/144.46 351.40/144.46 [0] = [0] 351.40/144.46 [0] 351.40/144.46 351.40/144.46 [s](x1) = [1 5] x1 + [5] 351.40/144.46 [0 1] [1] 351.40/144.46 351.40/144.46 [double](x1) = [0] 351.40/144.46 [0] 351.40/144.46 351.40/144.46 [plus](x1, x2) = [5] 351.40/144.46 [0] 351.40/144.46 351.40/144.46 [minus^#](x1, x2) = [0 1] x1 + [0] 351.40/144.47 [0 2] [0] 351.40/144.47 351.40/144.47 [double^#](x1) = [0] 351.40/144.47 [0] 351.40/144.47 351.40/144.47 [plus^#](x1, x2) = [1 3] x1 + [0] 351.40/144.47 [0 0] [0] 351.40/144.47 351.40/144.47 [c_1](x1) = [1 0] x1 + [0] 351.40/144.47 [0 0] [2] 351.40/144.47 351.40/144.47 [c_2](x1) = [1 0] x1 + [0] 351.40/144.47 [0 0] [0] 351.40/144.47 351.40/144.47 [c_3](x1) = [1 0] x1 + [7] 351.40/144.47 [0 0] [0] 351.40/144.47 351.40/144.47 [c_4](x1, x2, x3) = [1 0] x1 + [2 1] x2 + [4 0] x3 + [7] 351.40/144.47 [0 0] [0 0] [0 0] [0] 351.40/144.47 351.40/144.47 [c_5](x1) = [1 0] x1 + [7] 351.40/144.47 [0 0] [0] 351.40/144.47 351.40/144.47 [c_6](x1) = [3] 351.40/144.47 [0] 351.40/144.47 351.40/144.47 The order satisfies the following ordering constraints: 351.40/144.47 351.40/144.47 [minus(x, 0())] = [1 0] x + [0] 351.40/144.47 [0 1] [0] 351.40/144.47 >= [1 0] x + [0] 351.40/144.47 [0 1] [0] 351.40/144.47 = [x] 351.40/144.47 351.40/144.47 [minus(s(x), s(y))] = [1 5] x + [5] 351.40/144.47 [0 1] [1] 351.40/144.47 > [1 0] x + [0] 351.40/144.47 [0 1] [0] 351.40/144.47 = [minus(x, y)] 351.40/144.47 351.40/144.47 [double(0())] = [0] 351.40/144.47 [0] 351.40/144.47 >= [0] 351.40/144.47 [0] 351.40/144.47 = [0()] 351.40/144.47 351.40/144.47 [double(s(x))] = [0] 351.40/144.47 [0] 351.40/144.47 ? [15] 351.40/144.47 [2] 351.40/144.47 = [s(s(double(x)))] 351.40/144.47 351.40/144.47 [plus(0(), y)] = [5] 351.40/144.47 [0] 351.40/144.47 ? [1 0] y + [0] 351.40/144.47 [0 1] [0] 351.40/144.47 = [y] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [5] 351.40/144.47 [0] 351.40/144.47 ? [10] 351.40/144.47 [1] 351.40/144.47 = [s(plus(x, y))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [5] 351.40/144.47 [0] 351.40/144.47 ? [10] 351.40/144.47 [1] 351.40/144.47 = [s(plus(minus(x, y), double(y)))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [5] 351.40/144.47 [0] 351.40/144.47 >= [5] 351.40/144.47 [0] 351.40/144.47 = [plus(x, s(y))] 351.40/144.47 351.40/144.47 [plus(s(plus(x, y)), z)] = [5] 351.40/144.47 [0] 351.40/144.47 ? [10] 351.40/144.47 [1] 351.40/144.47 = [s(plus(plus(x, y), z))] 351.40/144.47 351.40/144.47 [minus^#(s(x), s(y))] = [0 1] x + [1] 351.40/144.47 [0 2] [2] 351.40/144.47 > [0 1] x + [0] 351.40/144.47 [0 0] [2] 351.40/144.47 = [c_1(minus^#(x, y))] 351.40/144.47 351.40/144.47 [double^#(s(x))] = [0] 351.40/144.47 [0] 351.40/144.47 >= [0] 351.40/144.47 [0] 351.40/144.47 = [c_2(double^#(x))] 351.40/144.47 351.40/144.47 [plus^#(s(x), y)] = [1 8] x + [8] 351.40/144.47 [0 0] [0] 351.40/144.47 > [1 3] x + [7] 351.40/144.47 [0 0] [0] 351.40/144.47 = [c_3(plus^#(x, y))] 351.40/144.47 351.40/144.47 [plus^#(s(x), y)] = [1 8] x + [8] 351.40/144.47 [0 0] [0] 351.40/144.47 > [1 7] x + [7] 351.40/144.47 [0 0] [0] 351.40/144.47 = [c_4(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y))] 351.40/144.47 351.40/144.47 [plus^#(s(x), y)] = [1 8] x + [8] 351.40/144.47 [0 0] [0] 351.40/144.47 > [1 3] x + [7] 351.40/144.47 [0 0] [0] 351.40/144.47 = [c_5(plus^#(x, s(y)))] 351.40/144.47 351.40/144.47 [plus^#(s(plus(x, y)), z)] = [13] 351.40/144.47 [0] 351.40/144.47 > [3] 351.40/144.47 [0] 351.40/144.47 = [c_6(plus^#(plus(x, y), z))] 351.40/144.47 351.40/144.47 351.40/144.47 The strictly oriented rules are moved into the weak component. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict DPs: { double^#(s(x)) -> c_2(double^#(x)) } 351.40/144.47 Weak DPs: 351.40/144.47 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> c_3(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.47 , plus^#(s(x), y) -> c_5(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_6(plus^#(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 The following weak DPs constitute a sub-graph of the DG that is 351.40/144.47 closed under successors. The DPs are removed. 351.40/144.47 351.40/144.47 { minus^#(s(x), s(y)) -> c_1(minus^#(x, y)) } 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict DPs: { double^#(s(x)) -> c_2(double^#(x)) } 351.40/144.47 Weak DPs: 351.40/144.47 { plus^#(s(x), y) -> c_3(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) 351.40/144.47 , plus^#(s(x), y) -> c_5(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_6(plus^#(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 Due to missing edges in the dependency-graph, the right-hand sides 351.40/144.47 of following rules could be simplified: 351.40/144.47 351.40/144.47 { plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), minus^#(x, y), double^#(y)) } 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict DPs: { double^#(s(x)) -> c_1(double^#(x)) } 351.40/144.47 Weak DPs: 351.40/144.47 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), double^#(y)) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_5(plus^#(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 We decompose the input problem according to the dependency graph 351.40/144.47 into the upper component 351.40/144.47 351.40/144.47 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), double^#(y)) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_5(plus^#(plus(x, y), z)) } 351.40/144.47 351.40/144.47 and lower component 351.40/144.47 351.40/144.47 { double^#(s(x)) -> c_1(double^#(x)) } 351.40/144.47 351.40/144.47 Further, following extension rules are added to the lower 351.40/144.47 component. 351.40/144.47 351.40/144.47 { plus^#(s(x), y) -> double^#(y) 351.40/144.47 , plus^#(s(x), y) -> plus^#(x, y) 351.40/144.47 , plus^#(s(x), y) -> plus^#(x, s(y)) 351.40/144.47 , plus^#(s(x), y) -> plus^#(minus(x, y), double(y)) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> plus^#(plus(x, y), z) } 351.40/144.47 351.40/144.47 TcT solves the upper component with certificate YES(O(1),O(n^1)). 351.40/144.47 351.40/144.47 Sub-proof: 351.40/144.47 ---------- 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate YES(O(1),O(n^1)). 351.40/144.47 351.40/144.47 Strict DPs: 351.40/144.47 { plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), double^#(y)) } 351.40/144.47 Weak DPs: 351.40/144.47 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_5(plus^#(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 YES(O(1),O(n^1)) 351.40/144.47 351.40/144.47 We use the processor 'matrix interpretation of dimension 1' to 351.40/144.47 orient following rules strictly. 351.40/144.47 351.40/144.47 DPs: 351.40/144.47 { 1: plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), double^#(y)) 351.40/144.47 , 2: plus^#(s(x), y) -> c_2(plus^#(x, y)) } 351.40/144.47 Trs: { minus(s(x), s(y)) -> minus(x, y) } 351.40/144.47 351.40/144.47 Sub-proof: 351.40/144.47 ---------- 351.40/144.47 The following argument positions are usable: 351.40/144.47 Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1} 351.40/144.47 351.40/144.47 TcT has computed the following constructor-based matrix 351.40/144.47 interpretation satisfying not(EDA). 351.40/144.47 351.40/144.47 [minus](x1, x2) = [1] x1 + [0] 351.40/144.47 351.40/144.47 [0] = [0] 351.40/144.47 351.40/144.47 [s](x1) = [1] x1 + [1] 351.40/144.47 351.40/144.47 [double](x1) = [0] 351.40/144.47 351.40/144.47 [plus](x1, x2) = [0] 351.40/144.47 351.40/144.47 [double^#](x1) = [7] x1 + [7] 351.40/144.47 351.40/144.47 [plus^#](x1, x2) = [2] x1 + [0] 351.40/144.47 351.40/144.47 [c_2](x1) = [1] x1 + [1] 351.40/144.47 351.40/144.47 [c_3](x1) = [1] x1 + [2] 351.40/144.47 351.40/144.47 [c_4](x1, x2) = [1] x1 + [1] 351.40/144.47 351.40/144.47 [c_5](x1) = [2] 351.40/144.47 351.40/144.47 The order satisfies the following ordering constraints: 351.40/144.47 351.40/144.47 [minus(x, 0())] = [1] x + [0] 351.40/144.47 >= [1] x + [0] 351.40/144.47 = [x] 351.40/144.47 351.40/144.47 [minus(s(x), s(y))] = [1] x + [1] 351.40/144.47 > [1] x + [0] 351.40/144.47 = [minus(x, y)] 351.40/144.47 351.40/144.47 [double(0())] = [0] 351.40/144.47 >= [0] 351.40/144.47 = [0()] 351.40/144.47 351.40/144.47 [double(s(x))] = [0] 351.40/144.47 ? [2] 351.40/144.47 = [s(s(double(x)))] 351.40/144.47 351.40/144.47 [plus(0(), y)] = [0] 351.40/144.47 ? [1] y + [0] 351.40/144.47 = [y] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [0] 351.40/144.47 ? [1] 351.40/144.47 = [s(plus(x, y))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [0] 351.40/144.47 ? [1] 351.40/144.47 = [s(plus(minus(x, y), double(y)))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [0] 351.40/144.47 >= [0] 351.40/144.47 = [plus(x, s(y))] 351.40/144.47 351.40/144.47 [plus(s(plus(x, y)), z)] = [0] 351.40/144.47 ? [1] 351.40/144.47 = [s(plus(plus(x, y), z))] 351.40/144.47 351.40/144.47 [plus^#(s(x), y)] = [2] x + [2] 351.40/144.47 > [2] x + [1] 351.40/144.47 = [c_2(plus^#(x, y))] 351.40/144.47 351.40/144.47 [plus^#(s(x), y)] = [2] x + [2] 351.40/144.47 >= [2] x + [2] 351.40/144.47 = [c_3(plus^#(x, s(y)))] 351.40/144.47 351.40/144.47 [plus^#(s(x), y)] = [2] x + [2] 351.40/144.47 > [2] x + [1] 351.40/144.47 = [c_4(plus^#(minus(x, y), double(y)), double^#(y))] 351.40/144.47 351.40/144.47 [plus^#(s(plus(x, y)), z)] = [2] 351.40/144.47 >= [2] 351.40/144.47 = [c_5(plus^#(plus(x, y), z))] 351.40/144.47 351.40/144.47 351.40/144.47 The strictly oriented rules are moved into the weak component. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate YES(O(1),O(1)). 351.40/144.47 351.40/144.47 Weak DPs: 351.40/144.47 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), double^#(y)) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_5(plus^#(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 YES(O(1),O(1)) 351.40/144.47 351.40/144.47 The following weak DPs constitute a sub-graph of the DG that is 351.40/144.47 closed under successors. The DPs are removed. 351.40/144.47 351.40/144.47 { plus^#(s(x), y) -> c_2(plus^#(x, y)) 351.40/144.47 , plus^#(s(x), y) -> c_3(plus^#(x, s(y))) 351.40/144.47 , plus^#(s(x), y) -> 351.40/144.47 c_4(plus^#(minus(x, y), double(y)), double^#(y)) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> c_5(plus^#(plus(x, y), z)) } 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate YES(O(1),O(1)). 351.40/144.47 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 YES(O(1),O(1)) 351.40/144.47 351.40/144.47 No rule is usable, rules are removed from the input problem. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate YES(O(1),O(1)). 351.40/144.47 351.40/144.47 Rules: Empty 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 YES(O(1),O(1)) 351.40/144.47 351.40/144.47 Empty rules are trivially bounded 351.40/144.47 351.40/144.47 We return to the main proof. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict DPs: { double^#(s(x)) -> c_1(double^#(x)) } 351.40/144.47 Weak DPs: 351.40/144.47 { plus^#(s(x), y) -> double^#(y) 351.40/144.47 , plus^#(s(x), y) -> plus^#(x, y) 351.40/144.47 , plus^#(s(x), y) -> plus^#(x, s(y)) 351.40/144.47 , plus^#(s(x), y) -> plus^#(minus(x, y), double(y)) 351.40/144.47 , plus^#(s(plus(x, y)), z) -> plus^#(plus(x, y), z) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'empty' failed due to the following reason: 351.40/144.47 351.40/144.47 Empty strict component of the problem is NOT empty. 351.40/144.47 351.40/144.47 2) 'Fastest' failed due to the following reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'With Problem ...' failed due to the following reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'empty' failed due to the following reason: 351.40/144.47 351.40/144.47 Empty strict component of the problem is NOT empty. 351.40/144.47 351.40/144.47 2) 'Polynomial Path Order (PS)' failed due to the following reason: 351.40/144.47 351.40/144.47 The input cannot be shown compatible 351.40/144.47 351.40/144.47 351.40/144.47 2) 'Polynomial Path Order (PS)' failed due to the following reason: 351.40/144.47 351.40/144.47 The input cannot be shown compatible 351.40/144.47 351.40/144.47 3) 'Fastest (timeout of 24 seconds)' failed due to the following 351.40/144.47 reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 351.40/144.47 failed due to the following reason: 351.40/144.47 351.40/144.47 match-boundness of the problem could not be verified. 351.40/144.47 351.40/144.47 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 351.40/144.47 failed due to the following reason: 351.40/144.47 351.40/144.47 match-boundness of the problem could not be verified. 351.40/144.47 351.40/144.47 351.40/144.47 351.40/144.47 351.40/144.47 351.40/144.47 2) 'Best' failed due to the following reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 351.40/144.47 seconds)' failed due to the following reason: 351.40/144.47 351.40/144.47 The weightgap principle applies (using the following nonconstant 351.40/144.47 growth matrix-interpretation) 351.40/144.47 351.40/144.47 The following argument positions are usable: 351.40/144.47 Uargs(s) = {1}, Uargs(plus) = {1, 2} 351.40/144.47 351.40/144.47 TcT has computed the following matrix interpretation satisfying 351.40/144.47 not(EDA) and not(IDA(1)). 351.40/144.47 351.40/144.47 [minus](x1, x2) = [1] x1 + [1] 351.40/144.47 351.40/144.47 [0] = [0] 351.40/144.47 351.40/144.47 [s](x1) = [1] x1 + [0] 351.40/144.47 351.40/144.47 [double](x1) = [0] 351.40/144.47 351.40/144.47 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 351.40/144.47 351.40/144.47 The order satisfies the following ordering constraints: 351.40/144.47 351.40/144.47 [minus(x, 0())] = [1] x + [1] 351.40/144.47 > [1] x + [0] 351.40/144.47 = [x] 351.40/144.47 351.40/144.47 [minus(s(x), s(y))] = [1] x + [1] 351.40/144.47 >= [1] x + [1] 351.40/144.47 = [minus(x, y)] 351.40/144.47 351.40/144.47 [double(0())] = [0] 351.40/144.47 >= [0] 351.40/144.47 = [0()] 351.40/144.47 351.40/144.47 [double(s(x))] = [0] 351.40/144.47 >= [0] 351.40/144.47 = [s(s(double(x)))] 351.40/144.47 351.40/144.47 [plus(0(), y)] = [1] y + [0] 351.40/144.47 >= [1] y + [0] 351.40/144.47 = [y] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [0] 351.40/144.47 >= [1] x + [1] y + [0] 351.40/144.47 = [s(plus(x, y))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [0] 351.40/144.47 ? [1] x + [1] 351.40/144.47 = [s(plus(minus(x, y), double(y)))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [0] 351.40/144.47 >= [1] x + [1] y + [0] 351.40/144.47 = [plus(x, s(y))] 351.40/144.47 351.40/144.47 [plus(s(plus(x, y)), z)] = [1] x + [1] y + [1] z + [0] 351.40/144.47 >= [1] x + [1] y + [1] z + [0] 351.40/144.47 = [s(plus(plus(x, y), z))] 351.40/144.47 351.40/144.47 351.40/144.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict Trs: 351.40/144.47 { minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(0(), y) -> y 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Weak Trs: { minus(x, 0()) -> x } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 The weightgap principle applies (using the following nonconstant 351.40/144.47 growth matrix-interpretation) 351.40/144.47 351.40/144.47 The following argument positions are usable: 351.40/144.47 Uargs(s) = {1}, Uargs(plus) = {1, 2} 351.40/144.47 351.40/144.47 TcT has computed the following matrix interpretation satisfying 351.40/144.47 not(EDA) and not(IDA(1)). 351.40/144.47 351.40/144.47 [minus](x1, x2) = [1] x1 + [0] 351.40/144.47 351.40/144.47 [0] = [1] 351.40/144.47 351.40/144.47 [s](x1) = [1] x1 + [0] 351.40/144.47 351.40/144.47 [double](x1) = [0] 351.40/144.47 351.40/144.47 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 351.40/144.47 351.40/144.47 The order satisfies the following ordering constraints: 351.40/144.47 351.40/144.47 [minus(x, 0())] = [1] x + [0] 351.40/144.47 >= [1] x + [0] 351.40/144.47 = [x] 351.40/144.47 351.40/144.47 [minus(s(x), s(y))] = [1] x + [0] 351.40/144.47 >= [1] x + [0] 351.40/144.47 = [minus(x, y)] 351.40/144.47 351.40/144.47 [double(0())] = [0] 351.40/144.47 ? [1] 351.40/144.47 = [0()] 351.40/144.47 351.40/144.47 [double(s(x))] = [0] 351.40/144.47 >= [0] 351.40/144.47 = [s(s(double(x)))] 351.40/144.47 351.40/144.47 [plus(0(), y)] = [1] y + [1] 351.40/144.47 > [1] y + [0] 351.40/144.47 = [y] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [0] 351.40/144.47 >= [1] x + [1] y + [0] 351.40/144.47 = [s(plus(x, y))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [0] 351.40/144.47 >= [1] x + [0] 351.40/144.47 = [s(plus(minus(x, y), double(y)))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [0] 351.40/144.47 >= [1] x + [1] y + [0] 351.40/144.47 = [plus(x, s(y))] 351.40/144.47 351.40/144.47 [plus(s(plus(x, y)), z)] = [1] x + [1] y + [1] z + [0] 351.40/144.47 >= [1] x + [1] y + [1] z + [0] 351.40/144.47 = [s(plus(plus(x, y), z))] 351.40/144.47 351.40/144.47 351.40/144.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict Trs: 351.40/144.47 { minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , plus(0(), y) -> y } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 The weightgap principle applies (using the following nonconstant 351.40/144.47 growth matrix-interpretation) 351.40/144.47 351.40/144.47 The following argument positions are usable: 351.40/144.47 Uargs(s) = {1}, Uargs(plus) = {1, 2} 351.40/144.47 351.40/144.47 TcT has computed the following matrix interpretation satisfying 351.40/144.47 not(EDA) and not(IDA(1)). 351.40/144.47 351.40/144.47 [minus](x1, x2) = [1] x1 + [4] 351.40/144.47 351.40/144.47 [0] = [7] 351.40/144.47 351.40/144.47 [s](x1) = [1] x1 + [4] 351.40/144.47 351.40/144.47 [double](x1) = [0] 351.40/144.47 351.40/144.47 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 351.40/144.47 351.40/144.47 The order satisfies the following ordering constraints: 351.40/144.47 351.40/144.47 [minus(x, 0())] = [1] x + [4] 351.40/144.47 > [1] x + [0] 351.40/144.47 = [x] 351.40/144.47 351.40/144.47 [minus(s(x), s(y))] = [1] x + [8] 351.40/144.47 > [1] x + [4] 351.40/144.47 = [minus(x, y)] 351.40/144.47 351.40/144.47 [double(0())] = [0] 351.40/144.47 ? [7] 351.40/144.47 = [0()] 351.40/144.47 351.40/144.47 [double(s(x))] = [0] 351.40/144.47 ? [8] 351.40/144.47 = [s(s(double(x)))] 351.40/144.47 351.40/144.47 [plus(0(), y)] = [1] y + [7] 351.40/144.47 > [1] y + [0] 351.40/144.47 = [y] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [4] 351.40/144.47 >= [1] x + [1] y + [4] 351.40/144.47 = [s(plus(x, y))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [4] 351.40/144.47 ? [1] x + [8] 351.40/144.47 = [s(plus(minus(x, y), double(y)))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [4] 351.40/144.47 >= [1] x + [1] y + [4] 351.40/144.47 = [plus(x, s(y))] 351.40/144.47 351.40/144.47 [plus(s(plus(x, y)), z)] = [1] x + [1] y + [1] z + [4] 351.40/144.47 >= [1] x + [1] y + [1] z + [4] 351.40/144.47 = [s(plus(plus(x, y), z))] 351.40/144.47 351.40/144.47 351.40/144.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict Trs: 351.40/144.47 { double(0()) -> 0() 351.40/144.47 , double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , plus(0(), y) -> y } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 The weightgap principle applies (using the following nonconstant 351.40/144.47 growth matrix-interpretation) 351.40/144.47 351.40/144.47 The following argument positions are usable: 351.40/144.47 Uargs(s) = {1}, Uargs(plus) = {1, 2} 351.40/144.47 351.40/144.47 TcT has computed the following matrix interpretation satisfying 351.40/144.47 not(EDA) and not(IDA(1)). 351.40/144.47 351.40/144.47 [minus](x1, x2) = [1] x1 + [4] 351.40/144.47 351.40/144.47 [0] = [7] 351.40/144.47 351.40/144.47 [s](x1) = [1] x1 + [4] 351.40/144.47 351.40/144.47 [double](x1) = [1] x1 + [4] 351.40/144.47 351.40/144.47 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 351.40/144.47 351.40/144.47 The order satisfies the following ordering constraints: 351.40/144.47 351.40/144.47 [minus(x, 0())] = [1] x + [4] 351.40/144.47 > [1] x + [0] 351.40/144.47 = [x] 351.40/144.47 351.40/144.47 [minus(s(x), s(y))] = [1] x + [8] 351.40/144.47 > [1] x + [4] 351.40/144.47 = [minus(x, y)] 351.40/144.47 351.40/144.47 [double(0())] = [11] 351.40/144.47 > [7] 351.40/144.47 = [0()] 351.40/144.47 351.40/144.47 [double(s(x))] = [1] x + [8] 351.40/144.47 ? [1] x + [12] 351.40/144.47 = [s(s(double(x)))] 351.40/144.47 351.40/144.47 [plus(0(), y)] = [1] y + [7] 351.40/144.47 > [1] y + [0] 351.40/144.47 = [y] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [4] 351.40/144.47 >= [1] x + [1] y + [4] 351.40/144.47 = [s(plus(x, y))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [4] 351.40/144.47 ? [1] x + [1] y + [12] 351.40/144.47 = [s(plus(minus(x, y), double(y)))] 351.40/144.47 351.40/144.47 [plus(s(x), y)] = [1] x + [1] y + [4] 351.40/144.47 >= [1] x + [1] y + [4] 351.40/144.47 = [plus(x, s(y))] 351.40/144.47 351.40/144.47 [plus(s(plus(x, y)), z)] = [1] x + [1] y + [1] z + [4] 351.40/144.47 >= [1] x + [1] y + [1] z + [4] 351.40/144.47 = [s(plus(plus(x, y), z))] 351.40/144.47 351.40/144.47 351.40/144.47 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 351.40/144.47 351.40/144.47 We are left with following problem, upon which TcT provides the 351.40/144.47 certificate MAYBE. 351.40/144.47 351.40/144.47 Strict Trs: 351.40/144.47 { double(s(x)) -> s(s(double(x))) 351.40/144.47 , plus(s(x), y) -> s(plus(x, y)) 351.40/144.47 , plus(s(x), y) -> s(plus(minus(x, y), double(y))) 351.40/144.47 , plus(s(x), y) -> plus(x, s(y)) 351.40/144.47 , plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)) } 351.40/144.47 Weak Trs: 351.40/144.47 { minus(x, 0()) -> x 351.40/144.47 , minus(s(x), s(y)) -> minus(x, y) 351.40/144.47 , double(0()) -> 0() 351.40/144.47 , plus(0(), y) -> y } 351.40/144.47 Obligation: 351.40/144.47 innermost runtime complexity 351.40/144.47 Answer: 351.40/144.47 MAYBE 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'empty' failed due to the following reason: 351.40/144.47 351.40/144.47 Empty strict component of the problem is NOT empty. 351.40/144.47 351.40/144.47 2) 'With Problem ...' failed due to the following reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'empty' failed due to the following reason: 351.40/144.47 351.40/144.47 Empty strict component of the problem is NOT empty. 351.40/144.47 351.40/144.47 2) 'Fastest' failed due to the following reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'With Problem ...' failed due to the following reason: 351.40/144.47 351.40/144.47 None of the processors succeeded. 351.40/144.47 351.40/144.47 Details of failed attempt(s): 351.40/144.47 ----------------------------- 351.40/144.47 1) 'empty' failed due to the following reason: 351.40/144.47 351.40/144.47 Empty strict component of the problem is NOT empty. 351.40/144.48 351.40/144.48 2) 'With Problem ...' failed due to the following reason: 351.40/144.48 351.40/144.48 Empty strict component of the problem is NOT empty. 351.40/144.48 351.40/144.48 351.40/144.48 2) 'With Problem ...' failed due to the following reason: 351.40/144.48 351.40/144.48 None of the processors succeeded. 351.40/144.48 351.40/144.48 Details of failed attempt(s): 351.40/144.48 ----------------------------- 351.40/144.48 1) 'empty' failed due to the following reason: 351.40/144.48 351.40/144.48 Empty strict component of the problem is NOT empty. 351.40/144.48 351.40/144.48 2) 'With Problem ...' failed due to the following reason: 351.40/144.48 351.40/144.48 None of the processors succeeded. 351.40/144.48 351.40/144.48 Details of failed attempt(s): 351.40/144.48 ----------------------------- 351.40/144.48 1) 'empty' failed due to the following reason: 351.40/144.48 351.40/144.48 Empty strict component of the problem is NOT empty. 351.40/144.48 351.40/144.48 2) 'With Problem ...' failed due to the following reason: 351.40/144.48 351.40/144.48 None of the processors succeeded. 351.40/144.48 351.40/144.48 Details of failed attempt(s): 351.40/144.48 ----------------------------- 351.40/144.48 1) 'empty' failed due to the following reason: 351.40/144.48 351.40/144.48 Empty strict component of the problem is NOT empty. 351.40/144.48 351.40/144.48 2) 'With Problem ...' failed due to the following reason: 351.40/144.48 351.40/144.48 Empty strict component of the problem is NOT empty. 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 2) 'Best' failed due to the following reason: 351.40/144.48 351.40/144.48 None of the processors succeeded. 351.40/144.48 351.40/144.48 Details of failed attempt(s): 351.40/144.48 ----------------------------- 351.40/144.48 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 351.40/144.48 following reason: 351.40/144.48 351.40/144.48 The input cannot be shown compatible 351.40/144.48 351.40/144.48 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 351.40/144.48 to the following reason: 351.40/144.48 351.40/144.48 The input cannot be shown compatible 351.40/144.48 351.40/144.48 351.40/144.48 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 351.40/144.48 failed due to the following reason: 351.40/144.48 351.40/144.48 None of the processors succeeded. 351.40/144.48 351.40/144.48 Details of failed attempt(s): 351.40/144.48 ----------------------------- 351.40/144.48 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 351.40/144.48 failed due to the following reason: 351.40/144.48 351.40/144.48 match-boundness of the problem could not be verified. 351.40/144.48 351.40/144.48 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 351.40/144.48 failed due to the following reason: 351.40/144.48 351.40/144.48 match-boundness of the problem could not be verified. 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 351.40/144.48 Arrrr.. 351.40/144.48 EOF