YES(O(1),O(n^2)) 169.64/60.03 YES(O(1),O(n^2)) 169.64/60.03 169.64/60.03 We are left with following problem, upon which TcT provides the 169.64/60.03 certificate YES(O(1),O(n^2)). 169.64/60.03 169.64/60.03 Strict Trs: 169.64/60.03 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 169.64/60.03 , average(s(x), y) -> average(x, s(y)) 169.64/60.03 , average(0(), s(s(0()))) -> s(0()) 169.64/60.03 , average(0(), s(0())) -> 0() 169.64/60.03 , average(0(), 0()) -> 0() } 169.64/60.03 Obligation: 169.64/60.03 derivational complexity 169.64/60.03 Answer: 169.64/60.03 YES(O(1),O(n^2)) 169.64/60.03 169.64/60.03 We use the processor 'matrix interpretation of dimension 1' to 169.64/60.03 orient following rules strictly. 169.64/60.03 169.64/60.03 Trs: 169.64/60.03 { average(0(), s(s(0()))) -> s(0()) 169.64/60.03 , average(0(), s(0())) -> 0() 169.64/60.03 , average(0(), 0()) -> 0() } 169.64/60.03 169.64/60.03 The induced complexity on above rules (modulo remaining rules) is 169.64/60.03 YES(?,O(n^1)) . These rules are moved into the corresponding weak 169.64/60.03 component(s). 169.64/60.03 169.64/60.03 Sub-proof: 169.64/60.03 ---------- 169.64/60.03 TcT has computed the following triangular matrix interpretation. 169.64/60.03 169.64/60.03 [average](x1, x2) = [1] x1 + [1] x2 + [1] 169.64/60.03 169.64/60.03 [s](x1) = [1] x1 + [0] 169.64/60.03 169.64/60.03 [0] = [0] 169.64/60.03 169.64/60.03 The order satisfies the following ordering constraints: 169.64/60.03 169.64/60.03 [average(x, s(s(s(y))))] = [1] x + [1] y + [1] 169.64/60.03 >= [1] x + [1] y + [1] 169.64/60.03 = [s(average(s(x), y))] 169.64/60.03 169.64/60.03 [average(s(x), y)] = [1] x + [1] y + [1] 169.64/60.03 >= [1] x + [1] y + [1] 169.64/60.03 = [average(x, s(y))] 169.64/60.03 169.64/60.03 [average(0(), s(s(0())))] = [1] 169.64/60.03 > [0] 169.64/60.03 = [s(0())] 169.64/60.03 169.64/60.03 [average(0(), s(0()))] = [1] 169.64/60.03 > [0] 169.64/60.03 = [0()] 169.64/60.03 169.64/60.03 [average(0(), 0())] = [1] 169.64/60.03 > [0] 169.64/60.03 = [0()] 169.64/60.03 169.64/60.03 169.64/60.03 We return to the main proof. 169.64/60.03 169.64/60.03 We are left with following problem, upon which TcT provides the 169.64/60.03 certificate YES(O(1),O(n^2)). 169.64/60.03 169.64/60.03 Strict Trs: 169.64/60.03 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 169.64/60.03 , average(s(x), y) -> average(x, s(y)) } 169.64/60.03 Weak Trs: 169.64/60.03 { average(0(), s(s(0()))) -> s(0()) 169.64/60.03 , average(0(), s(0())) -> 0() 169.64/60.03 , average(0(), 0()) -> 0() } 169.64/60.03 Obligation: 169.64/60.03 derivational complexity 169.64/60.03 Answer: 169.64/60.03 YES(O(1),O(n^2)) 169.64/60.03 169.64/60.03 We use the processor 'matrix interpretation of dimension 1' to 169.64/60.03 orient following rules strictly. 169.64/60.03 169.64/60.03 Trs: { average(x, s(s(s(y)))) -> s(average(s(x), y)) } 169.64/60.03 169.64/60.03 The induced complexity on above rules (modulo remaining rules) is 169.64/60.03 YES(?,O(n^1)) . These rules are moved into the corresponding weak 169.64/60.03 component(s). 169.64/60.03 169.64/60.03 Sub-proof: 169.64/60.03 ---------- 169.64/60.03 TcT has computed the following triangular matrix interpretation. 169.64/60.03 169.64/60.03 [average](x1, x2) = [1] x1 + [1] x2 + [1] 169.64/60.03 169.64/60.03 [s](x1) = [1] x1 + [2] 169.64/60.03 169.64/60.03 [0] = [0] 169.64/60.03 169.64/60.03 The order satisfies the following ordering constraints: 169.64/60.03 169.64/60.03 [average(x, s(s(s(y))))] = [1] x + [1] y + [7] 169.64/60.03 > [1] x + [1] y + [5] 169.64/60.03 = [s(average(s(x), y))] 169.64/60.03 169.64/60.03 [average(s(x), y)] = [1] x + [1] y + [3] 169.64/60.03 >= [1] x + [1] y + [3] 169.64/60.03 = [average(x, s(y))] 169.64/60.03 169.64/60.03 [average(0(), s(s(0())))] = [5] 169.64/60.03 > [2] 169.64/60.03 = [s(0())] 169.64/60.03 169.64/60.03 [average(0(), s(0()))] = [3] 169.64/60.03 > [0] 169.64/60.03 = [0()] 169.64/60.03 169.64/60.03 [average(0(), 0())] = [1] 169.64/60.03 > [0] 169.64/60.03 = [0()] 169.64/60.03 169.64/60.03 169.64/60.03 We return to the main proof. 169.64/60.03 169.64/60.03 We are left with following problem, upon which TcT provides the 169.64/60.03 certificate YES(O(1),O(n^2)). 169.64/60.03 169.64/60.03 Strict Trs: { average(s(x), y) -> average(x, s(y)) } 169.64/60.03 Weak Trs: 169.64/60.03 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 169.64/60.03 , average(0(), s(s(0()))) -> s(0()) 169.64/60.03 , average(0(), s(0())) -> 0() 169.64/60.03 , average(0(), 0()) -> 0() } 169.64/60.03 Obligation: 169.64/60.03 derivational complexity 169.64/60.03 Answer: 169.64/60.03 YES(O(1),O(n^2)) 169.64/60.03 169.64/60.03 We use the processor 'matrix interpretation of dimension 2' to 169.64/60.03 orient following rules strictly. 169.64/60.03 169.64/60.03 Trs: { average(s(x), y) -> average(x, s(y)) } 169.64/60.03 169.64/60.03 The induced complexity on above rules (modulo remaining rules) is 169.64/60.03 YES(?,O(n^2)) . These rules are moved into the corresponding weak 169.64/60.03 component(s). 169.64/60.03 169.64/60.03 Sub-proof: 169.64/60.03 ---------- 169.64/60.03 TcT has computed the following triangular matrix interpretation. 169.64/60.03 169.64/60.03 [average](x1, x2) = [1 2] x1 + [1 1] x2 + [2] 169.64/60.03 [0 1] [0 1] [0] 169.64/60.03 169.64/60.03 [s](x1) = [1 0] x1 + [0] 169.64/60.03 [0 1] [1] 169.64/60.03 169.64/60.03 [0] = [0] 169.64/60.03 [1] 169.64/60.03 169.64/60.03 The order satisfies the following ordering constraints: 169.64/60.03 169.64/60.03 [average(x, s(s(s(y))))] = [1 2] x + [1 1] y + [5] 169.64/60.03 [0 1] [0 1] [3] 169.64/60.03 > [1 2] x + [1 1] y + [4] 169.64/60.03 [0 1] [0 1] [2] 169.64/60.03 = [s(average(s(x), y))] 169.64/60.03 169.64/60.03 [average(s(x), y)] = [1 2] x + [1 1] y + [4] 169.64/60.03 [0 1] [0 1] [1] 169.64/60.03 > [1 2] x + [1 1] y + [3] 169.64/60.03 [0 1] [0 1] [1] 169.64/60.03 = [average(x, s(y))] 169.64/60.03 169.64/60.03 [average(0(), s(s(0())))] = [7] 169.64/60.03 [4] 169.64/60.03 > [0] 169.64/60.03 [2] 169.64/60.03 = [s(0())] 169.64/60.03 169.64/60.03 [average(0(), s(0()))] = [6] 169.64/60.03 [3] 169.64/60.03 > [0] 169.64/60.03 [1] 169.64/60.03 = [0()] 169.64/60.03 169.64/60.03 [average(0(), 0())] = [5] 169.64/60.03 [2] 169.64/60.03 > [0] 169.64/60.03 [1] 169.64/60.03 = [0()] 169.64/60.03 169.64/60.03 169.64/60.03 We return to the main proof. 169.64/60.03 169.64/60.03 We are left with following problem, upon which TcT provides the 169.64/60.03 certificate YES(O(1),O(1)). 169.64/60.03 169.64/60.03 Weak Trs: 169.64/60.03 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 169.64/60.03 , average(s(x), y) -> average(x, s(y)) 169.64/60.03 , average(0(), s(s(0()))) -> s(0()) 169.64/60.03 , average(0(), s(0())) -> 0() 169.64/60.03 , average(0(), 0()) -> 0() } 169.64/60.03 Obligation: 169.64/60.03 derivational complexity 169.64/60.03 Answer: 169.64/60.03 YES(O(1),O(1)) 169.64/60.03 169.64/60.03 Empty rules are trivially bounded 169.64/60.03 169.64/60.03 Hurray, we answered YES(O(1),O(n^2)) 169.64/60.05 EOF