YES(O(1),O(n^2))
157.43/60.06 YES(O(1),O(n^2))
157.43/60.06
157.43/60.06 We are left with following problem, upon which TcT provides the
157.43/60.06 certificate YES(O(1),O(n^2)).
157.43/60.06
157.43/60.06 Strict Trs:
157.43/60.06 { i(i(x)) -> x
157.43/60.06 , i(0()) -> 0()
157.43/60.06 , i(+(x, y)) -> +(i(x), i(y))
157.43/60.06 , +(x, i(x)) -> 0()
157.43/60.06 , +(x, 0()) -> x
157.43/60.06 , +(x, +(y, z)) -> +(+(x, y), z)
157.43/60.06 , +(i(x), x) -> 0()
157.43/60.06 , +(0(), y) -> y
157.43/60.06 , +(+(x, y), i(y)) -> x
157.43/60.06 , +(+(x, i(y)), y) -> x }
157.43/60.06 Obligation:
157.43/60.06 derivational complexity
157.43/60.06 Answer:
157.43/60.06 YES(O(1),O(n^2))
157.43/60.06
157.43/60.06 We use the processor 'matrix interpretation of dimension 1' to
157.43/60.06 orient following rules strictly.
157.43/60.06
157.43/60.06 Trs:
157.43/60.06 { +(x, i(x)) -> 0()
157.43/60.06 , +(x, 0()) -> x
157.43/60.06 , +(i(x), x) -> 0()
157.43/60.06 , +(0(), y) -> y
157.43/60.06 , +(+(x, y), i(y)) -> x
157.43/60.06 , +(+(x, i(y)), y) -> x }
157.43/60.06
157.43/60.06 The induced complexity on above rules (modulo remaining rules) is
157.43/60.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak
157.43/60.06 component(s).
157.43/60.06
157.43/60.06 Sub-proof:
157.43/60.06 ----------
157.43/60.06 TcT has computed the following triangular matrix interpretation.
157.43/60.06
157.43/60.06 [i](x1) = [1] x1 + [0]
157.43/60.06
157.43/60.06 [0] = [0]
157.43/60.06
157.43/60.06 [+](x1, x2) = [1] x1 + [1] x2 + [1]
157.43/60.06
157.43/60.06 The order satisfies the following ordering constraints:
157.43/60.06
157.43/60.06 [i(i(x))] = [1] x + [0]
157.43/60.06 >= [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [i(0())] = [0]
157.43/60.06 >= [0]
157.43/60.06 = [0()]
157.43/60.06
157.43/60.06 [i(+(x, y))] = [1] y + [1] x + [1]
157.43/60.06 >= [1] y + [1] x + [1]
157.43/60.06 = [+(i(x), i(y))]
157.43/60.06
157.43/60.06 [+(x, i(x))] = [2] x + [1]
157.43/60.06 > [0]
157.43/60.06 = [0()]
157.43/60.06
157.43/60.06 [+(x, 0())] = [1] x + [1]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [+(x, +(y, z))] = [1] y + [1] x + [1] z + [2]
157.43/60.06 >= [1] y + [1] x + [1] z + [2]
157.43/60.06 = [+(+(x, y), z)]
157.43/60.06
157.43/60.06 [+(i(x), x)] = [2] x + [1]
157.43/60.06 > [0]
157.43/60.06 = [0()]
157.43/60.06
157.43/60.06 [+(0(), y)] = [1] y + [1]
157.43/60.06 > [1] y + [0]
157.43/60.06 = [y]
157.43/60.06
157.43/60.06 [+(+(x, y), i(y))] = [2] y + [1] x + [2]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [+(+(x, i(y)), y)] = [2] y + [1] x + [2]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06
157.43/60.06 We return to the main proof.
157.43/60.06
157.43/60.06 We are left with following problem, upon which TcT provides the
157.43/60.06 certificate YES(O(1),O(n^2)).
157.43/60.06
157.43/60.06 Strict Trs:
157.43/60.06 { i(i(x)) -> x
157.43/60.06 , i(0()) -> 0()
157.43/60.06 , i(+(x, y)) -> +(i(x), i(y))
157.43/60.06 , +(x, +(y, z)) -> +(+(x, y), z) }
157.43/60.06 Weak Trs:
157.43/60.06 { +(x, i(x)) -> 0()
157.43/60.06 , +(x, 0()) -> x
157.43/60.06 , +(i(x), x) -> 0()
157.43/60.06 , +(0(), y) -> y
157.43/60.06 , +(+(x, y), i(y)) -> x
157.43/60.06 , +(+(x, i(y)), y) -> x }
157.43/60.06 Obligation:
157.43/60.06 derivational complexity
157.43/60.06 Answer:
157.43/60.06 YES(O(1),O(n^2))
157.43/60.06
157.43/60.06 The weightgap principle applies (using the following nonconstant
157.43/60.06 growth matrix-interpretation)
157.43/60.06
157.43/60.06 TcT has computed the following triangular matrix interpretation.
157.43/60.06 Note that the diagonal of the component-wise maxima of
157.43/60.06 interpretation-entries contains no more than 1 non-zero entries.
157.43/60.06
157.43/60.06 [i](x1) = [1] x1 + [1]
157.43/60.06
157.43/60.06 [0] = [1]
157.43/60.06
157.43/60.06 [+](x1, x2) = [1] x1 + [1] x2 + [0]
157.43/60.06
157.43/60.06 The order satisfies the following ordering constraints:
157.43/60.06
157.43/60.06 [i(i(x))] = [1] x + [2]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [i(0())] = [2]
157.43/60.06 > [1]
157.43/60.06 = [0()]
157.43/60.06
157.43/60.06 [i(+(x, y))] = [1] y + [1] x + [1]
157.43/60.06 ? [1] y + [1] x + [2]
157.43/60.06 = [+(i(x), i(y))]
157.43/60.06
157.43/60.06 [+(x, i(x))] = [2] x + [1]
157.43/60.06 >= [1]
157.43/60.06 = [0()]
157.43/60.06
157.43/60.06 [+(x, 0())] = [1] x + [1]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [+(x, +(y, z))] = [1] y + [1] x + [1] z + [0]
157.43/60.06 >= [1] y + [1] x + [1] z + [0]
157.43/60.06 = [+(+(x, y), z)]
157.43/60.06
157.43/60.06 [+(i(x), x)] = [2] x + [1]
157.43/60.06 >= [1]
157.43/60.06 = [0()]
157.43/60.06
157.43/60.06 [+(0(), y)] = [1] y + [1]
157.43/60.06 > [1] y + [0]
157.43/60.06 = [y]
157.43/60.06
157.43/60.06 [+(+(x, y), i(y))] = [2] y + [1] x + [1]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [+(+(x, i(y)), y)] = [2] y + [1] x + [1]
157.43/60.06 > [1] x + [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06
157.43/60.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
157.43/60.06
157.43/60.06 We are left with following problem, upon which TcT provides the
157.43/60.06 certificate YES(O(1),O(n^2)).
157.43/60.06
157.43/60.06 Strict Trs:
157.43/60.06 { i(+(x, y)) -> +(i(x), i(y))
157.43/60.06 , +(x, +(y, z)) -> +(+(x, y), z) }
157.43/60.06 Weak Trs:
157.43/60.06 { i(i(x)) -> x
157.43/60.06 , i(0()) -> 0()
157.43/60.06 , +(x, i(x)) -> 0()
157.43/60.06 , +(x, 0()) -> x
157.43/60.06 , +(i(x), x) -> 0()
157.43/60.06 , +(0(), y) -> y
157.43/60.06 , +(+(x, y), i(y)) -> x
157.43/60.06 , +(+(x, i(y)), y) -> x }
157.43/60.06 Obligation:
157.43/60.06 derivational complexity
157.43/60.06 Answer:
157.43/60.06 YES(O(1),O(n^2))
157.43/60.06
157.43/60.06 We use the processor 'matrix interpretation of dimension 2' to
157.43/60.06 orient following rules strictly.
157.43/60.06
157.43/60.06 Trs: { +(x, +(y, z)) -> +(+(x, y), z) }
157.43/60.06
157.43/60.06 The induced complexity on above rules (modulo remaining rules) is
157.43/60.06 YES(?,O(n^2)) . These rules are moved into the corresponding weak
157.43/60.06 component(s).
157.43/60.06
157.43/60.06 Sub-proof:
157.43/60.06 ----------
157.43/60.06 TcT has computed the following triangular matrix interpretation.
157.43/60.06
157.43/60.06 [i](x1) = [1 0] x1 + [0]
157.43/60.06 [0 1] [0]
157.43/60.06
157.43/60.06 [0] = [0]
157.43/60.06 [0]
157.43/60.06
157.43/60.06 [+](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
157.43/60.06 [0 1] [0 1] [1]
157.43/60.06
157.43/60.06 The order satisfies the following ordering constraints:
157.43/60.06
157.43/60.06 [i(i(x))] = [1 0] x + [0]
157.43/60.06 [0 1] [0]
157.43/60.06 >= [1 0] x + [0]
157.43/60.06 [0 1] [0]
157.43/60.06 = [x]
157.43/60.06
157.43/60.06 [i(0())] = [0]
157.43/60.07 [0]
157.43/60.07 >= [0]
157.43/60.07 [0]
157.43/60.07 = [0()]
157.43/60.07
157.43/60.07 [i(+(x, y))] = [1 1] y + [1 0] x + [0]
157.43/60.07 [0 1] [0 1] [1]
157.43/60.07 >= [1 1] y + [1 0] x + [0]
157.43/60.07 [0 1] [0 1] [1]
157.43/60.07 = [+(i(x), i(y))]
157.43/60.07
157.43/60.07 [+(x, i(x))] = [2 1] x + [0]
157.43/60.07 [0 2] [1]
157.43/60.07 >= [0]
157.43/60.07 [0]
157.43/60.07 = [0()]
157.43/60.07
157.43/60.07 [+(x, 0())] = [1 0] x + [0]
157.43/60.07 [0 1] [1]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07 [+(x, +(y, z))] = [1 1] y + [1 0] x + [1 2] z + [1]
157.43/60.07 [0 1] [0 1] [0 1] [2]
157.43/60.07 > [1 1] y + [1 0] x + [1 1] z + [0]
157.43/60.07 [0 1] [0 1] [0 1] [2]
157.43/60.07 = [+(+(x, y), z)]
157.43/60.07
157.43/60.07 [+(i(x), x)] = [2 1] x + [0]
157.43/60.07 [0 2] [1]
157.43/60.07 >= [0]
157.43/60.07 [0]
157.43/60.07 = [0()]
157.43/60.07
157.43/60.07 [+(0(), y)] = [1 1] y + [0]
157.43/60.07 [0 1] [1]
157.43/60.07 >= [1 0] y + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [y]
157.43/60.07
157.43/60.07 [+(+(x, y), i(y))] = [2 2] y + [1 0] x + [0]
157.43/60.07 [0 2] [0 1] [2]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07 [+(+(x, i(y)), y)] = [2 2] y + [1 0] x + [0]
157.43/60.07 [0 2] [0 1] [2]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07
157.43/60.07 We return to the main proof.
157.43/60.07
157.43/60.07 We are left with following problem, upon which TcT provides the
157.43/60.07 certificate YES(O(1),O(n^2)).
157.43/60.07
157.43/60.07 Strict Trs: { i(+(x, y)) -> +(i(x), i(y)) }
157.43/60.07 Weak Trs:
157.43/60.07 { i(i(x)) -> x
157.43/60.07 , i(0()) -> 0()
157.43/60.07 , +(x, i(x)) -> 0()
157.43/60.07 , +(x, 0()) -> x
157.43/60.07 , +(x, +(y, z)) -> +(+(x, y), z)
157.43/60.07 , +(i(x), x) -> 0()
157.43/60.07 , +(0(), y) -> y
157.43/60.07 , +(+(x, y), i(y)) -> x
157.43/60.07 , +(+(x, i(y)), y) -> x }
157.43/60.07 Obligation:
157.43/60.07 derivational complexity
157.43/60.07 Answer:
157.43/60.07 YES(O(1),O(n^2))
157.43/60.07
157.43/60.07 We use the processor 'matrix interpretation of dimension 2' to
157.43/60.07 orient following rules strictly.
157.43/60.07
157.43/60.07 Trs: { i(+(x, y)) -> +(i(x), i(y)) }
157.43/60.07
157.43/60.07 The induced complexity on above rules (modulo remaining rules) is
157.43/60.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak
157.43/60.07 component(s).
157.43/60.07
157.43/60.07 Sub-proof:
157.43/60.07 ----------
157.43/60.07 TcT has computed the following triangular matrix interpretation.
157.43/60.07
157.43/60.07 [i](x1) = [1 1] x1 + [0]
157.43/60.07 [0 1] [0]
157.43/60.07
157.43/60.07 [0] = [0]
157.43/60.07 [0]
157.43/60.07
157.43/60.07 [+](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
157.43/60.07 [0 1] [0 1] [1]
157.43/60.07
157.43/60.07 The order satisfies the following ordering constraints:
157.43/60.07
157.43/60.07 [i(i(x))] = [1 2] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07 [i(0())] = [0]
157.43/60.07 [0]
157.43/60.07 >= [0]
157.43/60.07 [0]
157.43/60.07 = [0()]
157.43/60.07
157.43/60.07 [i(+(x, y))] = [1 1] y + [1 1] x + [1]
157.43/60.07 [0 1] [0 1] [1]
157.43/60.07 > [1 1] y + [1 1] x + [0]
157.43/60.07 [0 1] [0 1] [1]
157.43/60.07 = [+(i(x), i(y))]
157.43/60.07
157.43/60.07 [+(x, i(x))] = [2 1] x + [0]
157.43/60.07 [0 2] [1]
157.43/60.07 >= [0]
157.43/60.07 [0]
157.43/60.07 = [0()]
157.43/60.07
157.43/60.07 [+(x, 0())] = [1 0] x + [0]
157.43/60.07 [0 1] [1]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07 [+(x, +(y, z))] = [1 0] y + [1 0] x + [1 0] z + [0]
157.43/60.07 [0 1] [0 1] [0 1] [2]
157.43/60.07 >= [1 0] y + [1 0] x + [1 0] z + [0]
157.43/60.07 [0 1] [0 1] [0 1] [2]
157.43/60.07 = [+(+(x, y), z)]
157.43/60.07
157.43/60.07 [+(i(x), x)] = [2 1] x + [0]
157.43/60.07 [0 2] [1]
157.43/60.07 >= [0]
157.43/60.07 [0]
157.43/60.07 = [0()]
157.43/60.07
157.43/60.07 [+(0(), y)] = [1 0] y + [0]
157.43/60.07 [0 1] [1]
157.43/60.07 >= [1 0] y + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [y]
157.43/60.07
157.43/60.07 [+(+(x, y), i(y))] = [2 1] y + [1 0] x + [0]
157.43/60.07 [0 2] [0 1] [2]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07 [+(+(x, i(y)), y)] = [2 1] y + [1 0] x + [0]
157.43/60.07 [0 2] [0 1] [2]
157.43/60.07 >= [1 0] x + [0]
157.43/60.07 [0 1] [0]
157.43/60.07 = [x]
157.43/60.07
157.43/60.07
157.43/60.07 We return to the main proof.
157.43/60.07
157.43/60.07 We are left with following problem, upon which TcT provides the
157.43/60.07 certificate YES(O(1),O(1)).
157.43/60.07
157.43/60.07 Weak Trs:
157.43/60.07 { i(i(x)) -> x
157.43/60.07 , i(0()) -> 0()
157.43/60.07 , i(+(x, y)) -> +(i(x), i(y))
157.43/60.07 , +(x, i(x)) -> 0()
157.43/60.07 , +(x, 0()) -> x
157.43/60.07 , +(x, +(y, z)) -> +(+(x, y), z)
157.43/60.07 , +(i(x), x) -> 0()
157.43/60.07 , +(0(), y) -> y
157.43/60.07 , +(+(x, y), i(y)) -> x
157.43/60.07 , +(+(x, i(y)), y) -> x }
157.43/60.07 Obligation:
157.43/60.07 derivational complexity
157.43/60.07 Answer:
157.43/60.07 YES(O(1),O(1))
157.43/60.07
157.43/60.07 Empty rules are trivially bounded
157.43/60.07
157.43/60.07 Hurray, we answered YES(O(1),O(n^2))
157.43/60.08 EOF