YES(O(1),O(n^1)) 64.93/24.04 YES(O(1),O(n^1)) 64.93/24.04 64.93/24.04 We are left with following problem, upon which TcT provides the 64.93/24.04 certificate YES(O(1),O(n^1)). 64.93/24.04 64.93/24.04 Strict Trs: 64.93/24.04 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 64.93/24.04 , average(s(x), y) -> average(x, s(y)) 64.93/24.04 , average(0(), s(s(0()))) -> s(0()) 64.93/24.04 , average(0(), s(0())) -> 0() 64.93/24.04 , average(0(), 0()) -> 0() } 64.93/24.04 Obligation: 64.93/24.04 innermost runtime complexity 64.93/24.04 Answer: 64.93/24.04 YES(O(1),O(n^1)) 64.93/24.04 64.93/24.04 The weightgap principle applies (using the following nonconstant 64.93/24.04 growth matrix-interpretation) 64.93/24.04 64.93/24.04 The following argument positions are usable: 64.93/24.04 Uargs(s) = {1} 64.93/24.04 64.93/24.04 TcT has computed the following matrix interpretation satisfying 64.93/24.04 not(EDA) and not(IDA(1)). 64.93/24.04 64.93/24.04 [average](x1, x2) = [1] 64.93/24.04 64.93/24.04 [s](x1) = [1] x1 + [0] 64.93/24.04 64.93/24.04 [0] = [0] 64.93/24.04 64.93/24.04 The order satisfies the following ordering constraints: 64.93/24.04 64.93/24.04 [average(x, s(s(s(y))))] = [1] 64.93/24.04 >= [1] 64.93/24.04 = [s(average(s(x), y))] 64.93/24.04 64.93/24.04 [average(s(x), y)] = [1] 64.93/24.04 >= [1] 64.93/24.04 = [average(x, s(y))] 64.93/24.04 64.93/24.04 [average(0(), s(s(0())))] = [1] 64.93/24.04 > [0] 64.93/24.04 = [s(0())] 64.93/24.04 64.93/24.04 [average(0(), s(0()))] = [1] 64.93/24.04 > [0] 64.93/24.04 = [0()] 64.93/24.04 64.93/24.04 [average(0(), 0())] = [1] 64.93/24.04 > [0] 64.93/24.04 = [0()] 64.93/24.04 64.93/24.04 64.93/24.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 64.93/24.04 64.93/24.04 We are left with following problem, upon which TcT provides the 64.93/24.04 certificate YES(O(1),O(n^1)). 64.93/24.04 64.93/24.04 Strict Trs: 64.93/24.04 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 64.93/24.04 , average(s(x), y) -> average(x, s(y)) } 64.93/24.04 Weak Trs: 64.93/24.04 { average(0(), s(s(0()))) -> s(0()) 64.93/24.04 , average(0(), s(0())) -> 0() 64.93/24.04 , average(0(), 0()) -> 0() } 64.93/24.04 Obligation: 64.93/24.04 innermost runtime complexity 64.93/24.04 Answer: 64.93/24.04 YES(O(1),O(n^1)) 64.93/24.04 64.93/24.04 The weightgap principle applies (using the following nonconstant 64.93/24.04 growth matrix-interpretation) 64.93/24.04 64.93/24.04 The following argument positions are usable: 64.93/24.04 Uargs(s) = {1} 64.93/24.04 64.93/24.04 TcT has computed the following matrix interpretation satisfying 64.93/24.04 not(EDA) and not(IDA(1)). 64.93/24.04 64.93/24.04 [average](x1, x2) = [1] x1 + [1] x2 + [0] 64.93/24.04 64.93/24.04 [s](x1) = [1] x1 + [4] 64.93/24.04 64.93/24.04 [0] = [0] 64.93/24.04 64.93/24.04 The order satisfies the following ordering constraints: 64.93/24.04 64.93/24.04 [average(x, s(s(s(y))))] = [1] x + [1] y + [12] 64.93/24.04 > [1] x + [1] y + [8] 64.93/24.04 = [s(average(s(x), y))] 64.93/24.04 64.93/24.04 [average(s(x), y)] = [1] x + [1] y + [4] 64.93/24.04 >= [1] x + [1] y + [4] 64.93/24.04 = [average(x, s(y))] 64.93/24.04 64.93/24.04 [average(0(), s(s(0())))] = [8] 64.93/24.04 > [4] 64.93/24.04 = [s(0())] 64.93/24.04 64.93/24.04 [average(0(), s(0()))] = [4] 64.93/24.04 > [0] 64.93/24.04 = [0()] 64.93/24.04 64.93/24.04 [average(0(), 0())] = [0] 64.93/24.04 >= [0] 64.93/24.04 = [0()] 64.93/24.04 64.93/24.04 64.93/24.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 64.93/24.04 64.93/24.04 We are left with following problem, upon which TcT provides the 64.93/24.04 certificate YES(O(1),O(n^1)). 64.93/24.04 64.93/24.04 Strict Trs: { average(s(x), y) -> average(x, s(y)) } 64.93/24.04 Weak Trs: 64.93/24.04 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 64.93/24.04 , average(0(), s(s(0()))) -> s(0()) 64.93/24.04 , average(0(), s(0())) -> 0() 64.93/24.04 , average(0(), 0()) -> 0() } 64.93/24.04 Obligation: 64.93/24.04 innermost runtime complexity 64.93/24.04 Answer: 64.93/24.04 YES(O(1),O(n^1)) 64.93/24.04 64.93/24.04 We use the processor 'matrix interpretation of dimension 1' to 64.93/24.04 orient following rules strictly. 64.93/24.04 64.93/24.04 Trs: { average(s(x), y) -> average(x, s(y)) } 64.93/24.04 64.93/24.04 The induced complexity on above rules (modulo remaining rules) is 64.93/24.04 YES(?,O(n^1)) . These rules are moved into the corresponding weak 64.93/24.04 component(s). 64.93/24.04 64.93/24.04 Sub-proof: 64.93/24.04 ---------- 64.93/24.04 The following argument positions are usable: 64.93/24.04 Uargs(s) = {1} 64.93/24.04 64.93/24.04 TcT has computed the following constructor-based matrix 64.93/24.04 interpretation satisfying not(EDA). 64.93/24.04 64.93/24.04 [average](x1, x2) = [2] x1 + [1] x2 + [6] 64.93/24.04 64.93/24.04 [s](x1) = [1] x1 + [1] 64.93/24.04 64.93/24.04 [0] = [0] 64.93/24.04 64.93/24.04 The order satisfies the following ordering constraints: 64.93/24.04 64.93/24.04 [average(x, s(s(s(y))))] = [2] x + [1] y + [9] 64.93/24.04 >= [2] x + [1] y + [9] 64.93/24.04 = [s(average(s(x), y))] 64.93/24.04 64.93/24.04 [average(s(x), y)] = [2] x + [1] y + [8] 64.93/24.04 > [2] x + [1] y + [7] 64.93/24.04 = [average(x, s(y))] 64.93/24.04 64.93/24.04 [average(0(), s(s(0())))] = [8] 64.93/24.04 > [1] 64.93/24.04 = [s(0())] 64.93/24.04 64.93/24.04 [average(0(), s(0()))] = [7] 64.93/24.04 > [0] 64.93/24.04 = [0()] 64.93/24.04 64.93/24.04 [average(0(), 0())] = [6] 64.93/24.04 > [0] 64.93/24.04 = [0()] 64.93/24.04 64.93/24.04 64.93/24.04 We return to the main proof. 64.93/24.04 64.93/24.04 We are left with following problem, upon which TcT provides the 64.93/24.04 certificate YES(O(1),O(1)). 64.93/24.04 64.93/24.04 Weak Trs: 64.93/24.04 { average(x, s(s(s(y)))) -> s(average(s(x), y)) 64.93/24.04 , average(s(x), y) -> average(x, s(y)) 64.93/24.04 , average(0(), s(s(0()))) -> s(0()) 64.93/24.04 , average(0(), s(0())) -> 0() 64.93/24.04 , average(0(), 0()) -> 0() } 64.93/24.04 Obligation: 64.93/24.04 innermost runtime complexity 64.93/24.04 Answer: 64.93/24.04 YES(O(1),O(1)) 64.93/24.04 64.93/24.04 Empty rules are trivially bounded 64.93/24.04 64.93/24.04 Hurray, we answered YES(O(1),O(n^1)) 64.93/24.09 EOF