YES(O(1),O(n^4)) 735.26/297.11 YES(O(1),O(n^4)) 735.26/297.11 735.26/297.11 We are left with following problem, upon which TcT provides the 735.26/297.11 certificate YES(O(1),O(n^4)). 735.26/297.11 735.26/297.11 Strict Trs: 735.26/297.11 { 1(2(1(x1))) -> 2(0(2(x1))) 735.26/297.11 , 1(2(0(x1))) -> 2(0(1(x1))) 735.26/297.11 , 1(2(R(x1))) -> 2(0(1(R(x1)))) 735.26/297.11 , 0(2(1(x1))) -> 1(0(2(x1))) 735.26/297.11 , 0(2(0(x1))) -> 1(0(1(x1))) 735.26/297.11 , 0(2(R(x1))) -> 1(0(1(R(x1)))) 735.26/297.11 , L(2(1(x1))) -> L(1(0(2(x1)))) 735.26/297.11 , L(2(0(x1))) -> L(1(0(1(x1)))) } 735.26/297.11 Obligation: 735.26/297.11 derivational complexity 735.26/297.11 Answer: 735.26/297.11 YES(O(1),O(n^4)) 735.26/297.11 735.26/297.11 We use the processor 'matrix interpretation of dimension 2' to 735.26/297.11 orient following rules strictly. 735.26/297.11 735.26/297.11 Trs: 735.26/297.11 { 1(2(R(x1))) -> 2(0(1(R(x1)))) 735.26/297.11 , 0(2(R(x1))) -> 1(0(1(R(x1)))) 735.26/297.11 , L(2(1(x1))) -> L(1(0(2(x1)))) 735.26/297.11 , L(2(0(x1))) -> L(1(0(1(x1)))) } 735.26/297.11 735.26/297.11 The induced complexity on above rules (modulo remaining rules) is 735.26/297.11 YES(?,O(n^1)) . These rules are removed from the problem. Note that 735.26/297.11 none of the weakly oriented rules is size-increasing. The overall 735.26/297.11 complexity is obtained by composition . 735.26/297.11 735.26/297.11 Sub-proof: 735.26/297.11 ---------- 735.26/297.11 TcT has computed the following triangular matrix interpretation. 735.26/297.11 735.26/297.11 [1](x1) = [1 0] x1 + [0] 735.26/297.11 [0 1] [0] 735.26/297.11 735.26/297.11 [2](x1) = [1 1] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 735.26/297.11 [0](x1) = [1 0] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 735.26/297.11 [L](x1) = [1 1] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 735.26/297.11 [R](x1) = [1 0] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 735.26/297.11 The order satisfies the following ordering constraints: 735.26/297.11 735.26/297.11 [1(2(1(x1)))] = [1 1] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 >= [1 1] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 = [2(0(2(x1)))] 735.26/297.11 735.26/297.11 [1(2(0(x1)))] = [1 0] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 >= [1 0] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 = [2(0(1(x1)))] 735.26/297.11 735.26/297.11 [1(2(R(x1)))] = [1 0] x1 + [1] 735.26/297.11 [0 0] [1] 735.26/297.11 > [1 0] x1 + [0] 735.26/297.11 [0 0] [1] 735.26/297.11 = [2(0(1(R(x1))))] 735.26/297.11 735.26/297.11 [0(2(1(x1)))] = [1 1] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 >= [1 1] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 = [1(0(2(x1)))] 735.26/297.11 735.26/297.11 [0(2(0(x1)))] = [1 0] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 >= [1 0] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 = [1(0(1(x1)))] 735.26/297.11 735.26/297.11 [0(2(R(x1)))] = [1 0] x1 + [1] 735.26/297.11 [0 0] [0] 735.26/297.11 > [1 0] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 = [1(0(1(R(x1))))] 735.26/297.11 735.26/297.11 [L(2(1(x1)))] = [1 1] x1 + [1] 735.26/297.11 [0 0] [0] 735.26/297.11 > [1 1] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 = [L(1(0(2(x1))))] 735.26/297.11 735.26/297.11 [L(2(0(x1)))] = [1 0] x1 + [1] 735.26/297.11 [0 0] [0] 735.26/297.11 > [1 0] x1 + [0] 735.26/297.11 [0 0] [0] 735.26/297.11 = [L(1(0(1(x1))))] 735.26/297.11 735.26/297.11 735.26/297.11 We return to the main proof. 735.26/297.11 735.26/297.11 We are left with following problem, upon which TcT provides the 735.26/297.11 certificate YES(O(1),O(n^3)). 735.26/297.11 735.26/297.11 Strict Trs: 735.26/297.11 { 1(2(1(x1))) -> 2(0(2(x1))) 735.26/297.11 , 1(2(0(x1))) -> 2(0(1(x1))) 735.26/297.11 , 0(2(1(x1))) -> 1(0(2(x1))) 735.26/297.11 , 0(2(0(x1))) -> 1(0(1(x1))) } 735.26/297.11 Obligation: 735.26/297.11 derivational complexity 735.26/297.11 Answer: 735.26/297.11 YES(O(1),O(n^3)) 735.26/297.11 735.26/297.11 We use the processor 'matrix interpretation of dimension 3' to 735.26/297.11 orient following rules strictly. 735.26/297.11 735.26/297.11 Trs: 735.26/297.11 { 1(2(1(x1))) -> 2(0(2(x1))) 735.26/297.11 , 1(2(0(x1))) -> 2(0(1(x1))) 735.26/297.11 , 0(2(1(x1))) -> 1(0(2(x1))) 735.26/297.11 , 0(2(0(x1))) -> 1(0(1(x1))) } 735.26/297.11 735.26/297.11 The induced complexity on above rules (modulo remaining rules) is 735.26/297.11 YES(?,O(n^3)) . These rules are removed from the problem. Note that 735.26/297.11 no rule is size-increasing. The overall complexity is obtained by 735.26/297.11 multiplication . 735.26/297.11 735.26/297.11 Sub-proof: 735.26/297.11 ---------- 735.26/297.11 TcT has computed the following triangular matrix interpretation. 735.26/297.11 735.26/297.11 [1 1 0] [0] 735.26/297.11 [1](x1) = [0 1 1] x1 + [0] 735.26/297.11 [0 0 1] [1] 735.26/297.11 735.26/297.11 [1 0 0] [0] 735.26/297.11 [2](x1) = [0 1 1] x1 + [0] 735.26/297.11 [0 0 1] [0] 735.26/297.11 735.26/297.11 [1 2 0] [0] 735.26/297.11 [0](x1) = [0 1 1] x1 + [0] 735.26/297.11 [0 0 1] [2] 735.26/297.11 735.26/297.11 The order satisfies the following ordering constraints: 735.26/297.11 735.26/297.11 [1(2(1(x1)))] = [1 2 2] [1] 735.26/297.11 [0 1 3] x1 + [2] 735.26/297.11 [0 0 1] [2] 735.26/297.11 > [1 2 2] [0] 735.26/297.11 [0 1 3] x1 + [2] 735.26/297.11 [0 0 1] [2] 735.26/297.11 = [2(0(2(x1)))] 735.26/297.11 735.26/297.11 [1(2(0(x1)))] = [1 3 2] [2] 735.26/297.11 [0 1 3] x1 + [4] 735.26/297.11 [0 0 1] [3] 735.26/297.11 > [1 3 2] [0] 735.26/297.11 [0 1 3] x1 + [4] 735.26/297.11 [0 0 1] [3] 735.26/297.11 = [2(0(1(x1)))] 735.26/297.11 735.26/297.11 [0(2(1(x1)))] = [1 3 4] [2] 735.26/297.11 [0 1 3] x1 + [2] 735.26/297.11 [0 0 1] [3] 735.26/297.11 > [1 3 4] [0] 735.26/297.11 [0 1 3] x1 + [2] 735.26/297.11 [0 0 1] [3] 735.26/297.11 = [1(0(2(x1)))] 735.26/297.11 735.26/297.11 [0(2(0(x1)))] = [1 4 4] [4] 735.26/297.11 [0 1 3] x1 + [4] 735.26/297.11 [0 0 1] [4] 735.26/297.11 > [1 4 4] [1] 735.26/297.11 [0 1 3] x1 + [4] 735.26/297.11 [0 0 1] [4] 735.26/297.11 = [1(0(1(x1)))] 735.26/297.11 735.26/297.11 735.26/297.11 We return to the main proof. 735.26/297.11 735.26/297.11 We are left with following problem, upon which TcT provides the 735.26/297.11 certificate YES(O(1),O(1)). 735.26/297.11 735.26/297.11 Rules: Empty 735.26/297.11 Obligation: 735.26/297.11 derivational complexity 735.26/297.11 Answer: 735.26/297.11 YES(O(1),O(1)) 735.26/297.11 735.26/297.11 Empty rules are trivially bounded 735.26/297.11 735.26/297.11 Hurray, we answered YES(O(1),O(n^4)) 735.26/297.14 EOF