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