YES(O(1),O(n^6)) 917.68/297.08 YES(O(1),O(n^6)) 917.68/297.08 917.68/297.08 We are left with following problem, upon which TcT provides the 917.68/297.08 certificate YES(O(1),O(n^6)). 917.68/297.08 917.68/297.08 Strict Trs: 917.68/297.08 { r0(0(x1)) -> 0(r0(x1)) 917.68/297.08 , r0(1(x1)) -> 1(r0(x1)) 917.68/297.08 , r0(m(x1)) -> m(r0(x1)) 917.68/297.08 , r0(b(x1)) -> qr(0(b(x1))) 917.68/297.08 , 0(qr(x1)) -> qr(0(x1)) 917.68/297.08 , 0(ql(x1)) -> ql(0(x1)) 917.68/297.08 , 1(qr(x1)) -> qr(1(x1)) 917.68/297.08 , 1(ql(x1)) -> ql(1(x1)) 917.68/297.08 , m(qr(x1)) -> ql(m(x1)) 917.68/297.08 , r1(0(x1)) -> 0(r1(x1)) 917.68/297.08 , r1(1(x1)) -> 1(r1(x1)) 917.68/297.08 , r1(m(x1)) -> m(r1(x1)) 917.68/297.08 , r1(b(x1)) -> qr(1(b(x1))) 917.68/297.08 , b(ql(0(x1))) -> 0(b(r0(x1))) 917.68/297.08 , b(ql(1(x1))) -> 1(b(r1(x1))) } 917.68/297.08 Obligation: 917.68/297.08 derivational complexity 917.68/297.08 Answer: 917.68/297.08 YES(O(1),O(n^6)) 917.68/297.08 917.68/297.08 We use the processor 'matrix interpretation of dimension 2' to 917.68/297.08 orient following rules strictly. 917.68/297.08 917.68/297.08 Trs: 917.68/297.08 { r0(b(x1)) -> qr(0(b(x1))) 917.68/297.08 , m(qr(x1)) -> ql(m(x1)) 917.68/297.08 , r1(b(x1)) -> qr(1(b(x1))) 917.68/297.08 , b(ql(0(x1))) -> 0(b(r0(x1))) 917.68/297.08 , b(ql(1(x1))) -> 1(b(r1(x1))) } 917.68/297.08 917.68/297.08 The induced complexity on above rules (modulo remaining rules) is 917.68/297.08 YES(?,O(n^2)) . These rules are removed from the problem. Note that 917.68/297.08 none of the weakly oriented rules is size-increasing. The overall 917.68/297.08 complexity is obtained by composition . 917.68/297.08 917.68/297.08 Sub-proof: 917.68/297.08 ---------- 917.68/297.08 TcT has computed the following triangular matrix interpretation. 917.68/297.08 917.68/297.08 [r0](x1) = [1 0] x1 + [2] 917.68/297.08 [0 1] [0] 917.68/297.08 917.68/297.08 [0](x1) = [1 0] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 917.68/297.08 [1](x1) = [1 0] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 917.68/297.08 [m](x1) = [1 0] x1 + [0] 917.68/297.08 [0 0] [0] 917.68/297.08 917.68/297.08 [r1](x1) = [1 0] x1 + [2] 917.68/297.08 [0 1] [0] 917.68/297.08 917.68/297.08 [b](x1) = [1 2] x1 + [0] 917.68/297.08 [0 1] [0] 917.68/297.08 917.68/297.08 [qr](x1) = [1 0] x1 + [1] 917.68/297.08 [0 0] [0] 917.68/297.08 917.68/297.08 [ql](x1) = [1 0] x1 + [0] 917.68/297.08 [0 1] [0] 917.68/297.08 917.68/297.08 The order satisfies the following ordering constraints: 917.68/297.08 917.68/297.08 [r0(0(x1))] = [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 >= [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 = [0(r0(x1))] 917.68/297.08 917.68/297.08 [r0(1(x1))] = [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 >= [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 = [1(r0(x1))] 917.68/297.08 917.68/297.08 [r0(m(x1))] = [1 0] x1 + [2] 917.68/297.08 [0 0] [0] 917.68/297.08 >= [1 0] x1 + [2] 917.68/297.08 [0 0] [0] 917.68/297.08 = [m(r0(x1))] 917.68/297.08 917.68/297.08 [r0(b(x1))] = [1 2] x1 + [2] 917.68/297.08 [0 1] [0] 917.68/297.08 > [1 2] x1 + [1] 917.68/297.08 [0 0] [0] 917.68/297.08 = [qr(0(b(x1)))] 917.68/297.08 917.68/297.08 [0(qr(x1))] = [1 0] x1 + [1] 917.68/297.08 [0 0] [2] 917.68/297.08 >= [1 0] x1 + [1] 917.68/297.08 [0 0] [0] 917.68/297.08 = [qr(0(x1))] 917.68/297.08 917.68/297.08 [0(ql(x1))] = [1 0] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 >= [1 0] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 = [ql(0(x1))] 917.68/297.08 917.68/297.08 [1(qr(x1))] = [1 0] x1 + [1] 917.68/297.08 [0 0] [2] 917.68/297.08 >= [1 0] x1 + [1] 917.68/297.08 [0 0] [0] 917.68/297.08 = [qr(1(x1))] 917.68/297.08 917.68/297.08 [1(ql(x1))] = [1 0] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 >= [1 0] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 = [ql(1(x1))] 917.68/297.08 917.68/297.08 [m(qr(x1))] = [1 0] x1 + [1] 917.68/297.08 [0 0] [0] 917.68/297.08 > [1 0] x1 + [0] 917.68/297.08 [0 0] [0] 917.68/297.08 = [ql(m(x1))] 917.68/297.08 917.68/297.08 [r1(0(x1))] = [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 >= [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 = [0(r1(x1))] 917.68/297.08 917.68/297.08 [r1(1(x1))] = [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 >= [1 0] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 = [1(r1(x1))] 917.68/297.08 917.68/297.08 [r1(m(x1))] = [1 0] x1 + [2] 917.68/297.08 [0 0] [0] 917.68/297.08 >= [1 0] x1 + [2] 917.68/297.08 [0 0] [0] 917.68/297.08 = [m(r1(x1))] 917.68/297.08 917.68/297.08 [r1(b(x1))] = [1 2] x1 + [2] 917.68/297.08 [0 1] [0] 917.68/297.08 > [1 2] x1 + [1] 917.68/297.08 [0 0] [0] 917.68/297.08 = [qr(1(b(x1)))] 917.68/297.08 917.68/297.08 [b(ql(0(x1)))] = [1 2] x1 + [4] 917.68/297.08 [0 1] [2] 917.68/297.08 > [1 2] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 = [0(b(r0(x1)))] 917.68/297.08 917.68/297.08 [b(ql(1(x1)))] = [1 2] x1 + [4] 917.68/297.08 [0 1] [2] 917.68/297.08 > [1 2] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 = [1(b(r1(x1)))] 917.68/297.08 917.68/297.08 917.68/297.08 We return to the main proof. 917.68/297.08 917.68/297.08 We are left with following problem, upon which TcT provides the 917.68/297.08 certificate YES(?,O(n^2)). 917.68/297.08 917.68/297.08 Strict Trs: 917.68/297.08 { r0(0(x1)) -> 0(r0(x1)) 917.68/297.08 , r0(1(x1)) -> 1(r0(x1)) 917.68/297.08 , r0(m(x1)) -> m(r0(x1)) 917.68/297.08 , 0(qr(x1)) -> qr(0(x1)) 917.68/297.08 , 0(ql(x1)) -> ql(0(x1)) 917.68/297.08 , 1(qr(x1)) -> qr(1(x1)) 917.68/297.08 , 1(ql(x1)) -> ql(1(x1)) 917.68/297.08 , r1(0(x1)) -> 0(r1(x1)) 917.68/297.08 , r1(1(x1)) -> 1(r1(x1)) 917.68/297.08 , r1(m(x1)) -> m(r1(x1)) } 917.68/297.08 Obligation: 917.68/297.08 derivational complexity 917.68/297.08 Answer: 917.68/297.08 YES(?,O(n^2)) 917.68/297.08 917.68/297.08 TcT has computed the following triangular matrix interpretation. 917.68/297.08 917.68/297.08 [r0](x1) = [1 1] x1 + [0] 917.68/297.08 [0 1] [0] 917.68/297.08 917.68/297.08 [0](x1) = [1 2] x1 + [0] 917.68/297.08 [0 1] [4] 917.68/297.08 917.68/297.08 [1](x1) = [1 2] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 917.68/297.08 [m](x1) = [1 0] x1 + [2] 917.68/297.08 [0 1] [6] 917.68/297.08 917.68/297.08 [r1](x1) = [1 2] x1 + [0] 917.68/297.08 [0 1] [0] 917.68/297.08 917.68/297.08 [qr](x1) = [1 0] x1 + [6] 917.68/297.08 [0 1] [1] 917.68/297.08 917.68/297.08 [ql](x1) = [1 0] x1 + [0] 917.68/297.08 [0 1] [4] 917.68/297.08 917.68/297.08 The order satisfies the following ordering constraints: 917.68/297.08 917.68/297.08 [r0(0(x1))] = [1 3] x1 + [4] 917.68/297.08 [0 1] [4] 917.68/297.08 > [1 3] x1 + [0] 917.68/297.08 [0 1] [4] 917.68/297.08 = [0(r0(x1))] 917.68/297.08 917.68/297.08 [r0(1(x1))] = [1 3] x1 + [2] 917.68/297.08 [0 1] [2] 917.68/297.08 > [1 3] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 = [1(r0(x1))] 917.68/297.08 917.68/297.08 [r0(m(x1))] = [1 1] x1 + [8] 917.68/297.08 [0 1] [6] 917.68/297.08 > [1 1] x1 + [2] 917.68/297.08 [0 1] [6] 917.68/297.08 = [m(r0(x1))] 917.68/297.08 917.68/297.08 [0(qr(x1))] = [1 2] x1 + [8] 917.68/297.08 [0 1] [5] 917.68/297.08 > [1 2] x1 + [6] 917.68/297.08 [0 1] [5] 917.68/297.08 = [qr(0(x1))] 917.68/297.08 917.68/297.08 [0(ql(x1))] = [1 2] x1 + [8] 917.68/297.08 [0 1] [8] 917.68/297.08 > [1 2] x1 + [0] 917.68/297.08 [0 1] [8] 917.68/297.08 = [ql(0(x1))] 917.68/297.08 917.68/297.08 [1(qr(x1))] = [1 2] x1 + [8] 917.68/297.08 [0 1] [3] 917.68/297.08 > [1 2] x1 + [6] 917.68/297.08 [0 1] [3] 917.68/297.08 = [qr(1(x1))] 917.68/297.08 917.68/297.08 [1(ql(x1))] = [1 2] x1 + [8] 917.68/297.08 [0 1] [6] 917.68/297.08 > [1 2] x1 + [0] 917.68/297.08 [0 1] [6] 917.68/297.08 = [ql(1(x1))] 917.68/297.08 917.68/297.08 [r1(0(x1))] = [1 4] x1 + [8] 917.68/297.08 [0 1] [4] 917.68/297.08 > [1 4] x1 + [0] 917.68/297.08 [0 1] [4] 917.68/297.08 = [0(r1(x1))] 917.68/297.08 917.68/297.08 [r1(1(x1))] = [1 4] x1 + [4] 917.68/297.08 [0 1] [2] 917.68/297.08 > [1 4] x1 + [0] 917.68/297.08 [0 1] [2] 917.68/297.08 = [1(r1(x1))] 917.68/297.08 917.68/297.08 [r1(m(x1))] = [1 2] x1 + [14] 917.68/297.08 [0 1] [6] 917.68/297.08 > [1 2] x1 + [2] 917.68/297.08 [0 1] [6] 917.68/297.08 = [m(r1(x1))] 917.68/297.08 917.68/297.08 917.68/297.08 Hurray, we answered YES(O(1),O(n^6)) 918.01/297.15 EOF