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)
, gcd(0(), y) -> y
, gcd(s(x), 0()) -> s(x)
, gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
, if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), 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:
{ gcd(0(), y) -> y
, gcd(s(x), 0()) -> 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(gcd) = {1}, Uargs(if_gcd) = {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 + [0]
[false] = [0]
[minus](x1, x2) = [1] x1 + [0]
[gcd](x1, x2) = [1] x1 + [1] x2 + [1]
[if_gcd](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
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 + [0]
>= [1] x + [0]
= [minus(x, y)]
[gcd(0(), y)] = [1] y + [1]
> [1] y + [0]
= [y]
[gcd(s(x), 0())] = [1] x + [1]
> [1] x + [0]
= [s(x)]
[gcd(s(x), s(y))] = [1] y + [1] x + [1]
>= [1] y + [1] x + [1]
= [if_gcd(le(y, x), s(x), s(y))]
[if_gcd(true(), s(x), s(y))] = [1] y + [1] x + [1]
>= [1] y + [1] x + [1]
= [gcd(minus(x, y), s(y))]
[if_gcd(false(), s(x), s(y))] = [1] y + [1] x + [1]
>= [1] y + [1] x + [1]
= [gcd(minus(y, 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(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)
, gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
, if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
Weak Trs:
{ gcd(0(), y) -> y
, gcd(s(x), 0()) -> 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()
, le(s(x), 0()) -> false()
, minus(s(x), s(y)) -> minus(x, y)
, gcd(s(x), s(y)) -> if_gcd(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(gcd) = {1}, Uargs(if_gcd) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[le](x1, x2) = [1]
[0] = [0]
[true] = [0]
[s](x1) = [1] x1 + [2]
[false] = [0]
[minus](x1, x2) = [1] x1 + [0]
[gcd](x1, x2) = [2] x1 + [2] x2 + [5]
[if_gcd](x1, x2, x3) = [3] x1 + [2] x2 + [2] x3 + [1]
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)]
[gcd(0(), y)] = [2] y + [5]
> [1] y + [0]
= [y]
[gcd(s(x), 0())] = [2] x + [9]
> [1] x + [2]
= [s(x)]
[gcd(s(x), s(y))] = [2] y + [2] x + [13]
> [2] y + [2] x + [12]
= [if_gcd(le(y, x), s(x), s(y))]
[if_gcd(true(), s(x), s(y))] = [2] y + [2] x + [9]
>= [2] y + [2] x + [9]
= [gcd(minus(x, y), s(y))]
[if_gcd(false(), s(x), s(y))] = [2] y + [2] x + [9]
>= [2] y + [2] x + [9]
= [gcd(minus(y, 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(n^2)).
Strict Trs:
{ le(s(x), s(y)) -> le(x, y)
, minus(x, 0()) -> x
, if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), s(x)) }
Weak Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, minus(s(x), s(y)) -> minus(x, y)
, gcd(0(), y) -> y
, gcd(s(x), 0()) -> s(x)
, gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), 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:
{ if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), 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(gcd) = {1}, Uargs(if_gcd) = {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 + [2]
[false] = [0]
[minus](x1, x2) = [1] x1 + [0]
[gcd](x1, x2) = [1] x1 + [1] x2 + [1]
[if_gcd](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [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 + [2]
> [1] x + [0]
= [minus(x, y)]
[gcd(0(), y)] = [1] y + [1]
> [1] y + [0]
= [y]
[gcd(s(x), 0())] = [1] x + [3]
> [1] x + [2]
= [s(x)]
[gcd(s(x), s(y))] = [1] y + [1] x + [5]
> [1] y + [1] x + [4]
= [if_gcd(le(y, x), s(x), s(y))]
[if_gcd(true(), s(x), s(y))] = [1] y + [1] x + [4]
> [1] y + [1] x + [3]
= [gcd(minus(x, y), s(y))]
[if_gcd(false(), s(x), s(y))] = [1] y + [1] x + [4]
> [1] y + [1] x + [3]
= [gcd(minus(y, 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(n^2)).
Strict Trs:
{ le(s(x), s(y)) -> le(x, y)
, minus(x, 0()) -> x }
Weak Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, minus(s(x), s(y)) -> minus(x, y)
, gcd(0(), y) -> y
, gcd(s(x), 0()) -> s(x)
, gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
, if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), 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(x, 0()) -> 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(gcd) = {1}, Uargs(if_gcd) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[le](x1, x2) = [1]
[0] = [0]
[true] = [1]
[s](x1) = [1] x1 + [2]
[false] = [1]
[minus](x1, x2) = [1] x1 + [1]
[gcd](x1, x2) = [1] x1 + [1] x2 + [6]
[if_gcd](x1, x2, x3) = [5] x1 + [1] x2 + [1] x3 + [0]
The order satisfies the following ordering constraints:
[le(0(), y)] = [1]
>= [1]
= [true()]
[le(s(x), 0())] = [1]
>= [1]
= [false()]
[le(s(x), s(y))] = [1]
>= [1]
= [le(x, y)]
[minus(x, 0())] = [1] x + [1]
> [1] x + [0]
= [x]
[minus(s(x), s(y))] = [1] x + [3]
> [1] x + [1]
= [minus(x, y)]
[gcd(0(), y)] = [1] y + [6]
> [1] y + [0]
= [y]
[gcd(s(x), 0())] = [1] x + [8]
> [1] x + [2]
= [s(x)]
[gcd(s(x), s(y))] = [1] y + [1] x + [10]
> [1] y + [1] x + [9]
= [if_gcd(le(y, x), s(x), s(y))]
[if_gcd(true(), s(x), s(y))] = [1] y + [1] x + [9]
>= [1] y + [1] x + [9]
= [gcd(minus(x, y), s(y))]
[if_gcd(false(), s(x), s(y))] = [1] y + [1] x + [9]
>= [1] y + [1] x + [9]
= [gcd(minus(y, 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(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)
, gcd(0(), y) -> y
, gcd(s(x), 0()) -> s(x)
, gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
, if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), 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(gcd) = {1}, Uargs(if_gcd) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[le](x1, x2) = x1
[0]() = 0
[true]() = 0
[s](x1) = 1 + x1
[false]() = 1
[minus](x1, x2) = x1
[gcd](x1, x2) = x1 + x1*x2 + 2*x1^2 + x2 + 2*x2^2
[if_gcd](x1, x2, x3) = x1 + x2*x3 + 2*x2^2 + 2*x3^2
This order satisfies the following ordering constraints.
[le(0(), y)] =
>=
= [true()]
[le(s(x), 0())] = 1 + x
>= 1
= [false()]
[le(s(x), s(y))] = 1 + x
> x
= [le(x, y)]
[minus(x, 0())] = x
>= x
= [x]
[minus(s(x), s(y))] = 1 + x
> x
= [minus(x, y)]
[gcd(0(), y)] = y + 2*y^2
>= y
= [y]
[gcd(s(x), 0())] = 3 + 5*x + 2*x^2
> 1 + x
= [s(x)]
[gcd(s(x), s(y))] = 7 + 6*x + 6*y + x*y + 2*x^2 + 2*y^2
> 6*y + 5 + 5*x + x*y + 2*x^2 + 2*y^2
= [if_gcd(le(y, x), s(x), s(y))]
[if_gcd(true(), s(x), s(y))] = 5 + 5*y + 5*x + x*y + 2*x^2 + 2*y^2
> 2*x + x*y + 2*x^2 + 3 + 5*y + 2*y^2
= [gcd(minus(x, y), s(y))]
[if_gcd(false(), s(x), s(y))] = 6 + 5*y + 5*x + x*y + 2*x^2 + 2*y^2
> 2*y + y*x + 2*y^2 + 3 + 5*x + 2*x^2
= [gcd(minus(y, 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)
, gcd(0(), y) -> y
, gcd(s(x), 0()) -> s(x)
, gcd(s(x), s(y)) -> if_gcd(le(y, x), s(x), s(y))
, if_gcd(true(), s(x), s(y)) -> gcd(minus(x, y), s(y))
, if_gcd(false(), s(x), s(y)) -> gcd(minus(y, x), 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))