We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ minus(s(x), s(y)) -> minus(x, y)
, mod(s(x), 0()) -> 0()
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(mod) = {1}, Uargs(if_mod) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[le](x1, x2) = [0]
[0] = [0]
[true] = [0]
[s](x1) = [1] x1 + [1]
[false] = [0]
[minus](x1, x2) = [1] x1 + [0]
[mod](x1, x2) = [1] x1 + [0]
[if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [0]
The order satisfies the following ordering constraints:
[le(0(), y)] = [0]
>= [0]
= [true()]
[le(s(x), 0())] = [0]
>= [0]
= [false()]
[le(s(x), s(y))] = [0]
>= [0]
= [le(x, y)]
[minus(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[minus(s(x), s(y))] = [1] x + [1]
> [1] x + [0]
= [minus(x, y)]
[mod(0(), y)] = [0]
>= [0]
= [0()]
[mod(s(x), 0())] = [1] x + [1]
> [0]
= [0()]
[mod(s(x), s(y))] = [1] x + [1]
>= [1] x + [1]
= [if_mod(le(y, x), s(x), s(y))]
[if_mod(true(), s(x), s(y))] = [1] x + [1]
> [1] x + [0]
= [mod(minus(x, y), s(y))]
[if_mod(false(), s(x), s(y))] = [1] x + [1]
>= [1] x + [1]
= [s(x)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(x, 0()) -> x
, mod(0(), y) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(false(), s(x), s(y)) -> s(x) }
Weak Trs:
{ minus(s(x), s(y)) -> minus(x, y)
, mod(s(x), 0()) -> 0()
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y)) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ le(s(x), 0()) -> false()
, minus(x, 0()) -> x
, mod(0(), y) -> 0()
, if_mod(false(), s(x), s(y)) -> s(x) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(mod) = {1}, Uargs(if_mod) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[le](x1, x2) = [1]
[0] = [1]
[true] = [1]
[s](x1) = [1] x1 + [2]
[false] = [0]
[minus](x1, x2) = [1] x1 + [2]
[mod](x1, x2) = [1] x1 + [4] x2 + [2]
[if_mod](x1, x2, x3) = [2] x1 + [1] x2 + [4] x3 + [0]
The order satisfies the following ordering constraints:
[le(0(), y)] = [1]
>= [1]
= [true()]
[le(s(x), 0())] = [1]
> [0]
= [false()]
[le(s(x), s(y))] = [1]
>= [1]
= [le(x, y)]
[minus(x, 0())] = [1] x + [2]
> [1] x + [0]
= [x]
[minus(s(x), s(y))] = [1] x + [4]
> [1] x + [2]
= [minus(x, y)]
[mod(0(), y)] = [4] y + [3]
> [1]
= [0()]
[mod(s(x), 0())] = [1] x + [8]
> [1]
= [0()]
[mod(s(x), s(y))] = [4] y + [1] x + [12]
>= [4] y + [1] x + [12]
= [if_mod(le(y, x), s(x), s(y))]
[if_mod(true(), s(x), s(y))] = [4] y + [1] x + [12]
>= [4] y + [1] x + [12]
= [mod(minus(x, y), s(y))]
[if_mod(false(), s(x), s(y))] = [4] y + [1] x + [10]
> [1] x + [2]
= [s(x)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), s(y)) -> le(x, y)
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) }
Weak Trs:
{ le(s(x), 0()) -> false()
, minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(mod) = {1}, Uargs(if_mod) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[le](x1, x2) = [0]
[0] = [0]
[true] = [0]
[s](x1) = [1] x1 + [7]
[false] = [0]
[minus](x1, x2) = [1] x1 + [0]
[mod](x1, x2) = [1] x1 + [1]
[if_mod](x1, x2, x3) = [2] x1 + [1] x2 + [0]
The order satisfies the following ordering constraints:
[le(0(), y)] = [0]
>= [0]
= [true()]
[le(s(x), 0())] = [0]
>= [0]
= [false()]
[le(s(x), s(y))] = [0]
>= [0]
= [le(x, y)]
[minus(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[minus(s(x), s(y))] = [1] x + [7]
> [1] x + [0]
= [minus(x, y)]
[mod(0(), y)] = [1]
> [0]
= [0()]
[mod(s(x), 0())] = [1] x + [8]
> [0]
= [0()]
[mod(s(x), s(y))] = [1] x + [8]
> [1] x + [7]
= [if_mod(le(y, x), s(x), s(y))]
[if_mod(true(), s(x), s(y))] = [1] x + [7]
> [1] x + [1]
= [mod(minus(x, y), s(y))]
[if_mod(false(), s(x), s(y))] = [1] x + [7]
>= [1] x + [7]
= [s(x)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), s(y)) -> le(x, y) }
Weak Trs:
{ le(s(x), 0()) -> false()
, minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { le(0(), y) -> true() }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(mod) = {1}, Uargs(if_mod) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[le](x1, x2) = [1]
[0] = [4]
[true] = [0]
[s](x1) = [1] x1 + [2]
[false] = [0]
[minus](x1, x2) = [1] x1 + [0]
[mod](x1, x2) = [1] x1 + [7]
[if_mod](x1, x2, x3) = [1] x1 + [1] x2 + [6]
The order satisfies the following ordering constraints:
[le(0(), y)] = [1]
> [0]
= [true()]
[le(s(x), 0())] = [1]
> [0]
= [false()]
[le(s(x), s(y))] = [1]
>= [1]
= [le(x, y)]
[minus(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[minus(s(x), s(y))] = [1] x + [2]
> [1] x + [0]
= [minus(x, y)]
[mod(0(), y)] = [11]
> [4]
= [0()]
[mod(s(x), 0())] = [1] x + [9]
> [4]
= [0()]
[mod(s(x), s(y))] = [1] x + [9]
>= [1] x + [9]
= [if_mod(le(y, x), s(x), s(y))]
[if_mod(true(), s(x), s(y))] = [1] x + [8]
> [1] x + [7]
= [mod(minus(x, y), s(y))]
[if_mod(false(), s(x), s(y))] = [1] x + [8]
> [1] x + [2]
= [s(x)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs: { le(s(x), s(y)) -> le(x, y) }
Weak Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs: { le(s(x), s(y)) -> le(x, y) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(mod) = {1}, Uargs(if_mod) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[le](x1, x2) = x2
[0]() = 0
[true]() = 0
[s](x1) = 1 + x1
[false]() = 0
[minus](x1, x2) = x1
[mod](x1, x2) = 3*x1 + x1^2
[if_mod](x1, x2, x3) = x1 + x2 + x2^2
This order satisfies the following ordering constraints.
[le(0(), y)] = y
>=
= [true()]
[le(s(x), 0())] =
>=
= [false()]
[le(s(x), s(y))] = 1 + y
> y
= [le(x, y)]
[minus(x, 0())] = x
>= x
= [x]
[minus(s(x), s(y))] = 1 + x
> x
= [minus(x, y)]
[mod(0(), y)] =
>=
= [0()]
[mod(s(x), 0())] = 4 + 5*x + x^2
>
= [0()]
[mod(s(x), s(y))] = 4 + 5*x + x^2
> 4*x + 2 + x^2
= [if_mod(le(y, x), s(x), s(y))]
[if_mod(true(), s(x), s(y))] = 2 + 3*x + x^2
> 3*x + x^2
= [mod(minus(x, y), s(y))]
[if_mod(false(), s(x), s(y))] = 2 + 3*x + x^2
> 1 + x
= [s(x)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))