YES(O(1),O(n^1)) 164.03/60.30 YES(O(1),O(n^1)) 164.03/60.30 164.03/60.30 We are left with following problem, upon which TcT provides the 164.03/60.30 certificate YES(O(1),O(n^1)). 164.03/60.30 164.03/60.30 Strict Trs: 164.03/60.30 { a(a(x1)) -> b(c(x1)) 164.03/60.30 , b(b(x1)) -> c(d(x1)) 164.03/60.30 , c(c(x1)) -> d(d(d(x1))) 164.03/60.30 , d(d(d(x1))) -> a(c(x1)) } 164.03/60.30 Obligation: 164.03/60.30 derivational complexity 164.03/60.30 Answer: 164.03/60.30 YES(O(1),O(n^1)) 164.03/60.30 164.03/60.30 We use the processor 'matrix interpretation of dimension 1' to 164.03/60.30 orient following rules strictly. 164.03/60.30 164.03/60.30 Trs: { b(b(x1)) -> c(d(x1)) } 164.03/60.30 164.03/60.30 The induced complexity on above rules (modulo remaining rules) is 164.03/60.30 YES(?,O(n^1)) . These rules are moved into the corresponding weak 164.03/60.30 component(s). 164.03/60.30 164.03/60.30 Sub-proof: 164.03/60.30 ---------- 164.03/60.30 TcT has computed the following triangular matrix interpretation. 164.03/60.30 164.03/60.30 [a](x1) = [1] x1 + [3] 164.03/60.30 164.03/60.30 [b](x1) = [1] x1 + [3] 164.03/60.30 164.03/60.30 [c](x1) = [1] x1 + [3] 164.03/60.30 164.03/60.30 [d](x1) = [1] x1 + [2] 164.03/60.30 164.03/60.30 The order satisfies the following ordering constraints: 164.03/60.30 164.03/60.30 [a(a(x1))] = [1] x1 + [6] 164.03/60.30 >= [1] x1 + [6] 164.03/60.30 = [b(c(x1))] 164.03/60.30 164.03/60.30 [b(b(x1))] = [1] x1 + [6] 164.03/60.30 > [1] x1 + [5] 164.03/60.30 = [c(d(x1))] 164.03/60.30 164.03/60.30 [c(c(x1))] = [1] x1 + [6] 164.03/60.30 >= [1] x1 + [6] 164.03/60.30 = [d(d(d(x1)))] 164.03/60.30 164.03/60.30 [d(d(d(x1)))] = [1] x1 + [6] 164.03/60.30 >= [1] x1 + [6] 164.03/60.30 = [a(c(x1))] 164.03/60.30 164.03/60.30 164.03/60.30 We return to the main proof. 164.03/60.30 164.03/60.30 We are left with following problem, upon which TcT provides the 164.03/60.30 certificate YES(O(1),O(n^1)). 164.03/60.30 164.03/60.30 Strict Trs: 164.03/60.30 { a(a(x1)) -> b(c(x1)) 164.03/60.30 , c(c(x1)) -> d(d(d(x1))) 164.03/60.30 , d(d(d(x1))) -> a(c(x1)) } 164.03/60.30 Weak Trs: { b(b(x1)) -> c(d(x1)) } 164.03/60.30 Obligation: 164.03/60.30 derivational complexity 164.03/60.30 Answer: 164.03/60.30 YES(O(1),O(n^1)) 164.03/60.30 164.03/60.30 We use the processor 'matrix interpretation of dimension 1' to 164.03/60.30 orient following rules strictly. 164.03/60.30 164.03/60.30 Trs: { d(d(d(x1))) -> a(c(x1)) } 164.03/60.30 164.03/60.30 The induced complexity on above rules (modulo remaining rules) is 164.03/60.30 YES(?,O(n^1)) . These rules are moved into the corresponding weak 164.03/60.30 component(s). 164.03/60.30 164.03/60.30 Sub-proof: 164.03/60.30 ---------- 164.03/60.30 TcT has computed the following triangular matrix interpretation. 164.03/60.30 164.03/60.30 [a](x1) = [1] x1 + [34] 164.03/60.30 164.03/60.30 [b](x1) = [1] x1 + [32] 164.03/60.30 164.03/60.30 [c](x1) = [1] x1 + [36] 164.03/60.30 164.03/60.30 [d](x1) = [1] x1 + [24] 164.03/60.30 164.03/60.30 The order satisfies the following ordering constraints: 164.03/60.30 164.03/60.30 [a(a(x1))] = [1] x1 + [68] 164.03/60.30 >= [1] x1 + [68] 164.03/60.30 = [b(c(x1))] 164.03/60.30 164.03/60.30 [b(b(x1))] = [1] x1 + [64] 164.03/60.30 > [1] x1 + [60] 164.03/60.30 = [c(d(x1))] 164.03/60.30 164.03/60.30 [c(c(x1))] = [1] x1 + [72] 164.03/60.30 >= [1] x1 + [72] 164.03/60.30 = [d(d(d(x1)))] 164.03/60.30 164.03/60.30 [d(d(d(x1)))] = [1] x1 + [72] 164.03/60.30 > [1] x1 + [70] 164.03/60.30 = [a(c(x1))] 164.03/60.30 164.03/60.30 164.03/60.30 We return to the main proof. 164.03/60.30 164.03/60.30 We are left with following problem, upon which TcT provides the 164.03/60.30 certificate YES(O(1),O(n^1)). 164.03/60.30 164.03/60.30 Strict Trs: 164.03/60.30 { a(a(x1)) -> b(c(x1)) 164.03/60.30 , c(c(x1)) -> d(d(d(x1))) } 164.03/60.30 Weak Trs: 164.03/60.30 { b(b(x1)) -> c(d(x1)) 164.03/60.30 , d(d(d(x1))) -> a(c(x1)) } 164.03/60.30 Obligation: 164.03/60.30 derivational complexity 164.03/60.30 Answer: 164.03/60.30 YES(O(1),O(n^1)) 164.03/60.30 164.03/60.30 We use the processor 'matrix interpretation of dimension 1' to 164.03/60.30 orient following rules strictly. 164.03/60.30 164.03/60.30 Trs: { a(a(x1)) -> b(c(x1)) } 164.03/60.30 164.03/60.30 The induced complexity on above rules (modulo remaining rules) is 164.03/60.30 YES(?,O(n^1)) . These rules are moved into the corresponding weak 164.03/60.30 component(s). 164.03/60.30 164.03/60.30 Sub-proof: 164.03/60.30 ---------- 164.03/60.30 TcT has computed the following triangular matrix interpretation. 164.03/60.30 164.03/60.30 [a](x1) = [1] x1 + [9] 164.03/60.30 164.03/60.30 [b](x1) = [1] x1 + [8] 164.03/60.30 164.03/60.30 [c](x1) = [1] x1 + [9] 164.03/60.30 164.03/60.30 [d](x1) = [1] x1 + [6] 164.03/60.30 164.03/60.30 The order satisfies the following ordering constraints: 164.03/60.30 164.03/60.30 [a(a(x1))] = [1] x1 + [18] 164.03/60.30 > [1] x1 + [17] 164.03/60.30 = [b(c(x1))] 164.03/60.30 164.03/60.30 [b(b(x1))] = [1] x1 + [16] 164.03/60.30 > [1] x1 + [15] 164.03/60.30 = [c(d(x1))] 164.03/60.30 164.03/60.30 [c(c(x1))] = [1] x1 + [18] 164.03/60.30 >= [1] x1 + [18] 164.03/60.30 = [d(d(d(x1)))] 164.03/60.30 164.03/60.30 [d(d(d(x1)))] = [1] x1 + [18] 164.03/60.30 >= [1] x1 + [18] 164.03/60.30 = [a(c(x1))] 164.03/60.30 164.03/60.30 164.03/60.30 We return to the main proof. 164.03/60.30 164.03/60.30 We are left with following problem, upon which TcT provides the 164.03/60.30 certificate YES(O(1),O(n^1)). 164.03/60.30 164.03/60.30 Strict Trs: { c(c(x1)) -> d(d(d(x1))) } 164.03/60.30 Weak Trs: 164.03/60.30 { a(a(x1)) -> b(c(x1)) 164.03/60.30 , b(b(x1)) -> c(d(x1)) 164.03/60.30 , d(d(d(x1))) -> a(c(x1)) } 164.03/60.30 Obligation: 164.03/60.30 derivational complexity 164.03/60.30 Answer: 164.03/60.30 YES(O(1),O(n^1)) 164.03/60.30 164.03/60.30 We use the processor 'matrix interpretation of dimension 1' to 164.03/60.30 orient following rules strictly. 164.03/60.30 164.03/60.30 Trs: { c(c(x1)) -> d(d(d(x1))) } 164.03/60.30 164.03/60.30 The induced complexity on above rules (modulo remaining rules) is 164.03/60.30 YES(?,O(n^1)) . These rules are moved into the corresponding weak 164.03/60.30 component(s). 164.03/60.30 164.03/60.30 Sub-proof: 164.03/60.30 ---------- 164.03/60.30 TcT has computed the following triangular matrix interpretation. 164.03/60.30 164.03/60.30 [a](x1) = [1] x1 + [13] 164.03/60.30 164.03/60.30 [b](x1) = [1] x1 + [12] 164.03/60.30 164.03/60.30 [c](x1) = [1] x1 + [14] 164.03/60.30 164.03/60.30 [d](x1) = [1] x1 + [9] 164.03/60.30 164.03/60.30 The order satisfies the following ordering constraints: 164.03/60.30 164.03/60.30 [a(a(x1))] = [1] x1 + [26] 164.03/60.30 >= [1] x1 + [26] 164.03/60.30 = [b(c(x1))] 164.03/60.30 164.03/60.30 [b(b(x1))] = [1] x1 + [24] 164.03/60.30 > [1] x1 + [23] 164.03/60.30 = [c(d(x1))] 164.03/60.30 164.03/60.30 [c(c(x1))] = [1] x1 + [28] 164.03/60.30 > [1] x1 + [27] 164.03/60.30 = [d(d(d(x1)))] 164.03/60.30 164.03/60.30 [d(d(d(x1)))] = [1] x1 + [27] 164.03/60.30 >= [1] x1 + [27] 164.03/60.30 = [a(c(x1))] 164.03/60.30 164.03/60.30 164.03/60.30 We return to the main proof. 164.03/60.30 164.03/60.30 We are left with following problem, upon which TcT provides the 164.03/60.30 certificate YES(O(1),O(1)). 164.03/60.30 164.03/60.30 Weak Trs: 164.03/60.30 { a(a(x1)) -> b(c(x1)) 164.03/60.30 , b(b(x1)) -> c(d(x1)) 164.03/60.30 , c(c(x1)) -> d(d(d(x1))) 164.03/60.30 , d(d(d(x1))) -> a(c(x1)) } 164.03/60.30 Obligation: 164.03/60.30 derivational complexity 164.03/60.30 Answer: 164.03/60.30 YES(O(1),O(1)) 164.03/60.30 164.03/60.30 Empty rules are trivially bounded 164.03/60.30 164.03/60.30 Hurray, we answered YES(O(1),O(n^1)) 164.03/60.37 EOF