YES(O(1),O(n^3)) 867.31/217.54 YES(O(1),O(n^3)) 867.31/217.54 867.31/217.54 We are left with following problem, upon which TcT provides the 867.31/217.54 certificate YES(O(1),O(n^3)). 867.31/217.54 867.31/217.54 Strict Trs: 867.31/217.54 { half(0()) -> 0() 867.31/217.54 , half(s(0())) -> 0() 867.31/217.54 , half(s(s(x))) -> s(half(x)) 867.31/217.54 , s(log(0())) -> s(0()) 867.31/217.54 , log(s(x)) -> s(log(half(s(x)))) } 867.31/217.54 Obligation: 867.31/217.54 derivational complexity 867.31/217.54 Answer: 867.31/217.54 YES(O(1),O(n^3)) 867.31/217.54 867.31/217.54 The weightgap principle applies (using the following nonconstant 867.31/217.54 growth matrix-interpretation) 867.31/217.54 867.31/217.54 TcT has computed the following triangular matrix interpretation. 867.31/217.54 Note that the diagonal of the component-wise maxima of 867.31/217.54 interpretation-entries contains no more than 1 non-zero entries. 867.31/217.54 867.31/217.54 [half](x1) = [1] x1 + [1] 867.31/217.54 867.31/217.54 [0] = [0] 867.31/217.54 867.31/217.54 [s](x1) = [1] x1 + [0] 867.31/217.54 867.31/217.54 [log](x1) = [1] x1 + [0] 867.31/217.54 867.31/217.54 The order satisfies the following ordering constraints: 867.31/217.54 867.31/217.54 [half(0())] = [1] 867.31/217.54 > [0] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(0()))] = [1] 867.31/217.54 > [0] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(s(x)))] = [1] x + [1] 867.31/217.54 >= [1] x + [1] 867.31/217.54 = [s(half(x))] 867.31/217.54 867.31/217.54 [s(log(0()))] = [0] 867.31/217.54 >= [0] 867.31/217.54 = [s(0())] 867.31/217.54 867.31/217.54 [log(s(x))] = [1] x + [0] 867.31/217.54 ? [1] x + [1] 867.31/217.54 = [s(log(half(s(x))))] 867.31/217.54 867.31/217.54 867.31/217.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 867.31/217.54 867.31/217.54 We are left with following problem, upon which TcT provides the 867.31/217.54 certificate YES(O(1),O(n^3)). 867.31/217.54 867.31/217.54 Strict Trs: 867.31/217.54 { half(s(s(x))) -> s(half(x)) 867.31/217.54 , s(log(0())) -> s(0()) 867.31/217.54 , log(s(x)) -> s(log(half(s(x)))) } 867.31/217.54 Weak Trs: 867.31/217.54 { half(0()) -> 0() 867.31/217.54 , half(s(0())) -> 0() } 867.31/217.54 Obligation: 867.31/217.54 derivational complexity 867.31/217.54 Answer: 867.31/217.54 YES(O(1),O(n^3)) 867.31/217.54 867.31/217.54 We use the processor 'matrix interpretation of dimension 1' to 867.31/217.54 orient following rules strictly. 867.31/217.54 867.31/217.54 Trs: { s(log(0())) -> s(0()) } 867.31/217.54 867.31/217.54 The induced complexity on above rules (modulo remaining rules) is 867.31/217.54 YES(?,O(n^1)) . These rules are moved into the corresponding weak 867.31/217.54 component(s). 867.31/217.54 867.31/217.54 Sub-proof: 867.31/217.54 ---------- 867.31/217.54 TcT has computed the following triangular matrix interpretation. 867.31/217.54 867.31/217.54 [half](x1) = [1] x1 + [0] 867.31/217.54 867.31/217.54 [0] = [0] 867.31/217.54 867.31/217.54 [s](x1) = [1] x1 + [0] 867.31/217.54 867.31/217.54 [log](x1) = [1] x1 + [1] 867.31/217.54 867.31/217.54 The order satisfies the following ordering constraints: 867.31/217.54 867.31/217.54 [half(0())] = [0] 867.31/217.54 >= [0] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(0()))] = [0] 867.31/217.54 >= [0] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(s(x)))] = [1] x + [0] 867.31/217.54 >= [1] x + [0] 867.31/217.54 = [s(half(x))] 867.31/217.54 867.31/217.54 [s(log(0()))] = [1] 867.31/217.54 > [0] 867.31/217.54 = [s(0())] 867.31/217.54 867.31/217.54 [log(s(x))] = [1] x + [1] 867.31/217.54 >= [1] x + [1] 867.31/217.54 = [s(log(half(s(x))))] 867.31/217.54 867.31/217.54 867.31/217.54 We return to the main proof. 867.31/217.54 867.31/217.54 We are left with following problem, upon which TcT provides the 867.31/217.54 certificate YES(O(1),O(n^3)). 867.31/217.54 867.31/217.54 Strict Trs: 867.31/217.54 { half(s(s(x))) -> s(half(x)) 867.31/217.54 , log(s(x)) -> s(log(half(s(x)))) } 867.31/217.54 Weak Trs: 867.31/217.54 { half(0()) -> 0() 867.31/217.54 , half(s(0())) -> 0() 867.31/217.54 , s(log(0())) -> s(0()) } 867.31/217.54 Obligation: 867.31/217.54 derivational complexity 867.31/217.54 Answer: 867.31/217.54 YES(O(1),O(n^3)) 867.31/217.54 867.31/217.54 The weightgap principle applies (using the following nonconstant 867.31/217.54 growth matrix-interpretation) 867.31/217.54 867.31/217.54 TcT has computed the following triangular matrix interpretation. 867.31/217.54 Note that the diagonal of the component-wise maxima of 867.31/217.54 interpretation-entries contains no more than 1 non-zero entries. 867.31/217.54 867.31/217.54 [half](x1) = [1] x1 + [0] 867.31/217.54 867.31/217.54 [0] = [2] 867.31/217.54 867.31/217.54 [s](x1) = [1] x1 + [2] 867.31/217.54 867.31/217.54 [log](x1) = [1] x1 + [0] 867.31/217.54 867.31/217.54 The order satisfies the following ordering constraints: 867.31/217.54 867.31/217.54 [half(0())] = [2] 867.31/217.54 >= [2] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(0()))] = [4] 867.31/217.54 > [2] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(s(x)))] = [1] x + [4] 867.31/217.54 > [1] x + [2] 867.31/217.54 = [s(half(x))] 867.31/217.54 867.31/217.54 [s(log(0()))] = [4] 867.31/217.54 >= [4] 867.31/217.54 = [s(0())] 867.31/217.54 867.31/217.54 [log(s(x))] = [1] x + [2] 867.31/217.54 ? [1] x + [4] 867.31/217.54 = [s(log(half(s(x))))] 867.31/217.54 867.31/217.54 867.31/217.54 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 867.31/217.54 867.31/217.54 We are left with following problem, upon which TcT provides the 867.31/217.54 certificate YES(O(1),O(n^3)). 867.31/217.54 867.31/217.54 Strict Trs: { log(s(x)) -> s(log(half(s(x)))) } 867.31/217.54 Weak Trs: 867.31/217.54 { half(0()) -> 0() 867.31/217.54 , half(s(0())) -> 0() 867.31/217.54 , half(s(s(x))) -> s(half(x)) 867.31/217.54 , s(log(0())) -> s(0()) } 867.31/217.54 Obligation: 867.31/217.54 derivational complexity 867.31/217.54 Answer: 867.31/217.54 YES(O(1),O(n^3)) 867.31/217.54 867.31/217.54 We use the processor 'matrix interpretation of dimension 3' to 867.31/217.54 orient following rules strictly. 867.31/217.54 867.31/217.54 Trs: { log(s(x)) -> s(log(half(s(x)))) } 867.31/217.54 867.31/217.54 The induced complexity on above rules (modulo remaining rules) is 867.31/217.54 YES(?,O(n^3)) . These rules are removed from the problem. Note that 867.31/217.54 none of the weakly oriented rules is size-increasing. The overall 867.31/217.54 complexity is obtained by composition . 867.31/217.54 867.31/217.54 Sub-proof: 867.31/217.54 ---------- 867.31/217.54 TcT has computed the following matrix interpretation satisfying 867.31/217.54 not(EDA). 867.31/217.54 867.31/217.54 [1 0 0] [2] 867.31/217.54 [half](x1) = [0 0 1] x1 + [0] 867.31/217.54 [0 0 1] [0] 867.31/217.54 867.31/217.54 [0] 867.31/217.54 [0] = [2] 867.31/217.54 [2] 867.31/217.54 867.31/217.54 [1 0 0] [1] 867.31/217.54 [s](x1) = [0 0 1] x1 + [4] 867.31/217.54 [0 0 1] [2] 867.31/217.54 867.31/217.54 [1 2 0] [0] 867.31/217.54 [log](x1) = [0 1 0] x1 + [4] 867.31/217.54 [0 1 0] [2] 867.31/217.54 867.31/217.54 The order satisfies the following ordering constraints: 867.31/217.54 867.31/217.54 [half(0())] = [2] 867.31/217.54 [2] 867.31/217.54 [2] 867.31/217.54 > [0] 867.31/217.54 [2] 867.31/217.54 [2] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(0()))] = [3] 867.31/217.54 [4] 867.31/217.54 [4] 867.31/217.54 > [0] 867.31/217.54 [2] 867.31/217.54 [2] 867.31/217.54 = [0()] 867.31/217.54 867.31/217.54 [half(s(s(x)))] = [1 0 0] [4] 867.31/217.54 [0 0 1] x + [4] 867.31/217.54 [0 0 1] [4] 867.31/217.54 > [1 0 0] [3] 867.31/217.54 [0 0 1] x + [4] 867.31/217.54 [0 0 1] [2] 867.31/217.54 = [s(half(x))] 867.31/217.54 867.31/217.54 [s(log(0()))] = [5] 867.31/217.54 [8] 867.31/217.54 [6] 867.31/217.54 > [1] 867.31/217.54 [6] 867.31/217.55 [4] 867.31/217.55 = [s(0())] 867.31/217.55 867.31/217.55 [log(s(x))] = [1 0 2] [9] 867.31/217.55 [0 0 1] x + [8] 867.31/217.55 [0 0 1] [6] 867.31/217.55 > [1 0 2] [8] 867.31/217.55 [0 0 1] x + [8] 867.31/217.55 [0 0 1] [6] 867.31/217.55 = [s(log(half(s(x))))] 867.31/217.55 867.31/217.55 867.31/217.55 We return to the main proof. 867.31/217.55 867.31/217.55 We are left with following problem, upon which TcT provides the 867.31/217.55 certificate YES(O(1),O(1)). 867.31/217.55 867.31/217.55 Weak Trs: 867.31/217.55 { half(0()) -> 0() 867.31/217.55 , half(s(0())) -> 0() 867.31/217.55 , half(s(s(x))) -> s(half(x)) 867.31/217.55 , s(log(0())) -> s(0()) } 867.31/217.55 Obligation: 867.31/217.55 derivational complexity 867.31/217.55 Answer: 867.31/217.55 YES(O(1),O(1)) 867.31/217.55 867.31/217.55 Empty rules are trivially bounded 867.31/217.55 867.31/217.55 Hurray, we answered YES(O(1),O(n^3)) 867.31/217.58 EOF