YES(O(1),O(n^1)) 160.11/60.02 YES(O(1),O(n^1)) 160.11/60.02 160.11/60.02 We are left with following problem, upon which TcT provides the 160.11/60.02 certificate YES(O(1),O(n^1)). 160.11/60.02 160.11/60.02 Strict Trs: 160.11/60.02 { a(a(x1)) -> b(b(b(x1))) 160.11/60.02 , b(b(x1)) -> c(c(c(x1))) 160.11/60.02 , c(c(c(c(x1)))) -> a(b(x1)) } 160.11/60.02 Obligation: 160.11/60.02 derivational complexity 160.11/60.02 Answer: 160.11/60.02 YES(O(1),O(n^1)) 160.11/60.02 160.11/60.02 We use the processor 'matrix interpretation of dimension 1' to 160.11/60.02 orient following rules strictly. 160.11/60.02 160.11/60.02 Trs: 160.11/60.02 { a(a(x1)) -> b(b(b(x1))) 160.11/60.02 , c(c(c(c(x1)))) -> a(b(x1)) } 160.11/60.02 160.11/60.02 The induced complexity on above rules (modulo remaining rules) is 160.11/60.02 YES(?,O(n^1)) . These rules are moved into the corresponding weak 160.11/60.02 component(s). 160.11/60.02 160.11/60.02 Sub-proof: 160.11/60.02 ---------- 160.11/60.02 TcT has computed the following triangular matrix interpretation. 160.11/60.02 160.11/60.02 [a](x1) = [1] x1 + [37] 160.11/60.02 160.11/60.02 [b](x1) = [1] x1 + [24] 160.11/60.02 160.11/60.02 [c](x1) = [1] x1 + [16] 160.11/60.02 160.11/60.02 The order satisfies the following ordering constraints: 160.11/60.02 160.11/60.02 [a(a(x1))] = [1] x1 + [74] 160.11/60.02 > [1] x1 + [72] 160.11/60.02 = [b(b(b(x1)))] 160.11/60.02 160.11/60.02 [b(b(x1))] = [1] x1 + [48] 160.11/60.02 >= [1] x1 + [48] 160.11/60.02 = [c(c(c(x1)))] 160.11/60.02 160.11/60.02 [c(c(c(c(x1))))] = [1] x1 + [64] 160.11/60.02 > [1] x1 + [61] 160.11/60.02 = [a(b(x1))] 160.11/60.02 160.11/60.02 160.11/60.02 We return to the main proof. 160.11/60.02 160.11/60.02 We are left with following problem, upon which TcT provides the 160.11/60.02 certificate YES(O(1),O(n^1)). 160.11/60.02 160.11/60.02 Strict Trs: { b(b(x1)) -> c(c(c(x1))) } 160.11/60.02 Weak Trs: 160.11/60.02 { a(a(x1)) -> b(b(b(x1))) 160.11/60.02 , c(c(c(c(x1)))) -> a(b(x1)) } 160.11/60.02 Obligation: 160.11/60.02 derivational complexity 160.11/60.02 Answer: 160.11/60.02 YES(O(1),O(n^1)) 160.11/60.02 160.11/60.02 We use the processor 'matrix interpretation of dimension 1' to 160.11/60.02 orient following rules strictly. 160.11/60.02 160.11/60.02 Trs: { b(b(x1)) -> c(c(c(x1))) } 160.11/60.02 160.11/60.02 The induced complexity on above rules (modulo remaining rules) is 160.11/60.02 YES(?,O(n^1)) . These rules are moved into the corresponding weak 160.11/60.02 component(s). 160.11/60.02 160.11/60.02 Sub-proof: 160.11/60.02 ---------- 160.11/60.02 TcT has computed the following triangular matrix interpretation. 160.11/60.02 160.11/60.02 [a](x1) = [1] x1 + [38] 160.11/60.02 160.11/60.02 [b](x1) = [1] x1 + [25] 160.11/60.02 160.11/60.02 [c](x1) = [1] x1 + [16] 160.11/60.02 160.11/60.02 The order satisfies the following ordering constraints: 160.11/60.02 160.11/60.02 [a(a(x1))] = [1] x1 + [76] 160.11/60.02 > [1] x1 + [75] 160.11/60.02 = [b(b(b(x1)))] 160.11/60.02 160.11/60.02 [b(b(x1))] = [1] x1 + [50] 160.11/60.02 > [1] x1 + [48] 160.11/60.02 = [c(c(c(x1)))] 160.11/60.02 160.11/60.02 [c(c(c(c(x1))))] = [1] x1 + [64] 160.11/60.02 > [1] x1 + [63] 160.11/60.02 = [a(b(x1))] 160.11/60.02 160.11/60.02 160.11/60.02 We return to the main proof. 160.11/60.02 160.11/60.02 We are left with following problem, upon which TcT provides the 160.11/60.02 certificate YES(O(1),O(1)). 160.11/60.02 160.11/60.02 Weak Trs: 160.11/60.02 { a(a(x1)) -> b(b(b(x1))) 160.11/60.02 , b(b(x1)) -> c(c(c(x1))) 160.11/60.02 , c(c(c(c(x1)))) -> a(b(x1)) } 160.11/60.02 Obligation: 160.11/60.02 derivational complexity 160.11/60.02 Answer: 160.11/60.02 YES(O(1),O(1)) 160.11/60.02 160.11/60.02 Empty rules are trivially bounded 160.11/60.02 160.11/60.02 Hurray, we answered YES(O(1),O(n^1)) 160.25/60.14 EOF