YES(O(1),O(n^1)) 7.80/4.18 YES(O(1),O(n^1)) 7.80/4.18 7.80/4.18 We are left with following problem, upon which TcT provides the 7.80/4.18 certificate YES(O(1),O(n^1)). 7.80/4.18 7.80/4.18 Strict Trs: 7.80/4.18 { f(X, X) -> c(X) 7.80/4.18 , f(X, c(X)) -> f(s(X), X) 7.80/4.18 , f(s(X), X) -> f(X, a(X)) } 7.80/4.18 Obligation: 7.80/4.18 derivational complexity 7.80/4.18 Answer: 7.80/4.18 YES(O(1),O(n^1)) 7.80/4.18 7.80/4.18 We use the processor 'matrix interpretation of dimension 1' to 7.80/4.18 orient following rules strictly. 7.80/4.18 7.80/4.18 Trs: { f(X, X) -> c(X) } 7.80/4.18 7.80/4.18 The induced complexity on above rules (modulo remaining rules) is 7.80/4.18 YES(?,O(n^1)) . These rules are moved into the corresponding weak 7.80/4.18 component(s). 7.80/4.18 7.80/4.18 Sub-proof: 7.80/4.18 ---------- 7.80/4.18 TcT has computed the following triangular matrix interpretation. 7.80/4.18 7.80/4.18 [f](x1, x2) = [1] x1 + [1] x2 + [1] 7.80/4.18 7.80/4.18 [s](x1) = [1] x1 + [0] 7.80/4.18 7.80/4.18 [a](x1) = [1] x1 + [0] 7.80/4.18 7.80/4.18 [c](x1) = [1] x1 + [0] 7.80/4.18 7.80/4.18 The order satisfies the following ordering constraints: 7.80/4.18 7.80/4.18 [f(X, X)] = [2] X + [1] 7.80/4.18 > [1] X + [0] 7.80/4.18 = [c(X)] 7.80/4.18 7.80/4.18 [f(X, c(X))] = [2] X + [1] 7.80/4.18 >= [2] X + [1] 7.80/4.18 = [f(s(X), X)] 7.80/4.18 7.80/4.18 [f(s(X), X)] = [2] X + [1] 7.80/4.18 >= [2] X + [1] 7.80/4.18 = [f(X, a(X))] 7.80/4.18 7.80/4.18 7.80/4.18 We return to the main proof. 7.80/4.18 7.80/4.18 We are left with following problem, upon which TcT provides the 7.80/4.18 certificate YES(O(1),O(n^1)). 7.80/4.18 7.80/4.18 Strict Trs: 7.80/4.18 { f(X, c(X)) -> f(s(X), X) 7.80/4.18 , f(s(X), X) -> f(X, a(X)) } 7.80/4.18 Weak Trs: { f(X, X) -> c(X) } 7.80/4.18 Obligation: 7.80/4.18 derivational complexity 7.80/4.18 Answer: 7.80/4.18 YES(O(1),O(n^1)) 7.80/4.18 7.80/4.18 We use the processor 'matrix interpretation of dimension 1' to 7.80/4.18 orient following rules strictly. 7.80/4.18 7.80/4.18 Trs: { f(s(X), X) -> f(X, a(X)) } 7.80/4.18 7.80/4.18 The induced complexity on above rules (modulo remaining rules) is 7.80/4.18 YES(?,O(n^1)) . These rules are moved into the corresponding weak 7.80/4.18 component(s). 7.80/4.18 7.80/4.18 Sub-proof: 7.80/4.18 ---------- 7.80/4.18 TcT has computed the following triangular matrix interpretation. 7.80/4.18 7.80/4.18 [f](x1, x2) = [1] x1 + [1] x2 + [2] 7.80/4.18 7.80/4.18 [s](x1) = [1] x1 + [2] 7.80/4.18 7.80/4.18 [a](x1) = [1] x1 + [0] 7.80/4.18 7.80/4.18 [c](x1) = [1] x1 + [2] 7.80/4.18 7.80/4.18 The order satisfies the following ordering constraints: 7.80/4.18 7.80/4.18 [f(X, X)] = [2] X + [2] 7.80/4.18 >= [1] X + [2] 7.80/4.18 = [c(X)] 7.80/4.18 7.80/4.18 [f(X, c(X))] = [2] X + [4] 7.80/4.18 >= [2] X + [4] 7.80/4.18 = [f(s(X), X)] 7.80/4.18 7.80/4.18 [f(s(X), X)] = [2] X + [4] 7.80/4.18 > [2] X + [2] 7.80/4.18 = [f(X, a(X))] 7.80/4.18 7.80/4.18 7.80/4.18 We return to the main proof. 7.80/4.18 7.80/4.18 We are left with following problem, upon which TcT provides the 7.80/4.18 certificate YES(O(1),O(n^1)). 7.80/4.18 7.80/4.18 Strict Trs: { f(X, c(X)) -> f(s(X), X) } 7.80/4.18 Weak Trs: 7.80/4.18 { f(X, X) -> c(X) 7.80/4.18 , f(s(X), X) -> f(X, a(X)) } 7.80/4.18 Obligation: 7.80/4.18 derivational complexity 7.80/4.18 Answer: 7.80/4.18 YES(O(1),O(n^1)) 7.80/4.18 7.80/4.18 We use the processor 'matrix interpretation of dimension 2' to 7.80/4.18 orient following rules strictly. 7.80/4.18 7.80/4.18 Trs: { f(X, c(X)) -> f(s(X), X) } 7.80/4.18 7.80/4.18 The induced complexity on above rules (modulo remaining rules) is 7.80/4.18 YES(?,O(n^1)) . These rules are moved into the corresponding weak 7.80/4.18 component(s). 7.80/4.18 7.80/4.18 Sub-proof: 7.80/4.18 ---------- 7.80/4.18 TcT has computed the following triangular matrix interpretation. 7.80/4.18 Note that the diagonal of the component-wise maxima of 7.80/4.18 interpretation-entries contains no more than 1 non-zero entries. 7.80/4.18 7.80/4.18 [f](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 7.80/4.18 [0 0] [0 0] [2] 7.80/4.18 7.80/4.18 [s](x1) = [1 0] x1 + [1] 7.80/4.18 [0 0] [2] 7.80/4.18 7.80/4.18 [a](x1) = [1 0] x1 + [0] 7.80/4.18 [0 0] [2] 7.80/4.18 7.80/4.18 [c](x1) = [1 0] x1 + [2] 7.80/4.18 [0 0] [1] 7.80/4.18 7.80/4.18 The order satisfies the following ordering constraints: 7.80/4.18 7.80/4.18 [f(X, X)] = [2 0] X + [2] 7.80/4.18 [0 0] [2] 7.80/4.18 >= [1 0] X + [2] 7.80/4.18 [0 0] [1] 7.80/4.18 = [c(X)] 7.80/4.18 7.80/4.18 [f(X, c(X))] = [2 0] X + [4] 7.80/4.18 [0 0] [2] 7.80/4.18 > [2 0] X + [3] 7.80/4.18 [0 0] [2] 7.80/4.18 = [f(s(X), X)] 7.80/4.18 7.80/4.18 [f(s(X), X)] = [2 0] X + [3] 7.80/4.18 [0 0] [2] 7.80/4.18 > [2 0] X + [2] 7.80/4.18 [0 0] [2] 7.80/4.18 = [f(X, a(X))] 7.80/4.18 7.80/4.18 7.80/4.18 We return to the main proof. 7.80/4.18 7.80/4.18 We are left with following problem, upon which TcT provides the 7.80/4.18 certificate YES(O(1),O(1)). 7.80/4.18 7.80/4.18 Weak Trs: 7.80/4.18 { f(X, X) -> c(X) 7.80/4.18 , f(X, c(X)) -> f(s(X), X) 7.80/4.18 , f(s(X), X) -> f(X, a(X)) } 7.80/4.18 Obligation: 7.80/4.18 derivational complexity 7.80/4.18 Answer: 7.80/4.18 YES(O(1),O(1)) 7.80/4.18 7.80/4.18 Empty rules are trivially bounded 7.80/4.18 7.80/4.18 Hurray, we answered YES(O(1),O(n^1)) 7.80/4.20 EOF