interpretations
Execution Time (secs) | - |
Answer | YES(?,O(n^3)) |
Input | AG01 3.6a |
YES(?,O(n^3))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).
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:
innermost runtime complexity
Answer:
YES(?,O(n^3))
The following argument positions are usable:
Uargs(le) = {}, Uargs(s) = {}, Uargs(minus) = {}, Uargs(gcd) = {1},
Uargs(if_gcd) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[0 0 0] [0 0 1] [2]
[le](x1, x2) = [0 0 0] x1 + [0 1 0] x2 + [0]
[1 0 0] [1 0 0] [0]
[0]
[0] = [0]
[3]
[1]
[true] = [0]
[0]
[1 3 1] [1]
[s](x1) = [0 1 0] x1 + [0]
[0 1 1] [1]
[1]
[false] = [0]
[0]
[1 0 0] [1]
[minus](x1, x2) = [0 2 0] x1 + [0]
[0 0 1] [0]
[3 3 3] [3 3 2] [2]
[gcd](x1, x2) = [2 2 3] x1 + [2 1 2] x2 + [2]
[1 2 3] [1 2 2] [1]
[1 1 0] [3 3 2] [3 3 2] [0]
[if_gcd](x1, x2, x3) = [0 0 0] x1 + [2 2 2] x2 + [2 1 2] x3 + [2]
[0 1 0] [1 1 3] [1 2 2] [1]
This order satisfies following ordering constraints
[le(0(), y)] = [0 0 1] [2]
[0 1 0] y + [0]
[1 0 0] [0]
> [1]
[0]
[0]
= [true()]
[le(s(x), 0())] = [0 0 0] [5]
[0 0 0] x + [0]
[1 3 1] [1]
> [1]
[0]
[0]
= [false()]
[le(s(x), s(y))] = [0 1 1] [0 0 0] [3]
[0 1 0] y + [0 0 0] x + [0]
[1 3 1] [1 3 1] [2]
> [0 0 1] [0 0 0] [2]
[0 1 0] y + [0 0 0] x + [0]
[1 0 0] [1 0 0] [0]
= [le(x, y)]
[minus(x, 0())] = [1 0 0] [1]
[0 2 0] x + [0]
[0 0 1] [0]
> [1 0 0] [0]
[0 1 0] x + [0]
[0 0 1] [0]
= [x]
[minus(s(x), s(y))] = [1 3 1] [2]
[0 2 0] x + [0]
[0 1 1] [1]
> [1 0 0] [1]
[0 2 0] x + [0]
[0 0 1] [0]
= [minus(x, y)]
[gcd(0(), y)] = [3 3 2] [11]
[2 1 2] y + [11]
[1 2 2] [10]
> [1 0 0] [0]
[0 1 0] y + [0]
[0 0 1] [0]
= [y]
[gcd(s(x), 0())] = [3 15 6] [14]
[2 11 5] x + [13]
[1 8 4] [11]
> [1 3 1] [1]
[0 1 0] x + [0]
[0 1 1] [1]
= [s(x)]
[gcd(s(x), s(y))] = [3 14 5] [3 15 6] [13]
[2 9 4] y + [2 11 5] x + [11]
[1 7 3] [1 8 4] [8]
> [3 14 5] [3 15 6] [12]
[2 9 4] y + [2 10 4] x + [10]
[1 7 3] [1 8 4] [8]
= [if_gcd(le(y, x), s(x), s(y))]
[if_gcd(true(), s(x), s(y))] = [3 14 5] [3 14 5] [11]
[2 9 4] y + [2 10 4] x + [10]
[1 7 3] [1 7 4] [8]
> [3 14 5] [3 6 3] [10]
[2 9 4] y + [2 4 3] x + [8]
[1 7 3] [1 4 3] [5]
= [gcd(minus(x, y), s(y))]
[if_gcd(false(), s(x), s(y))] = [3 14 5] [3 14 5] [11]
[2 9 4] y + [2 10 4] x + [10]
[1 7 3] [1 7 4] [8]
> [3 6 3] [3 14 5] [10]
[2 4 3] y + [2 9 4] x + [8]
[1 4 3] [1 7 3] [5]
= [gcd(minus(y, x), s(x))]
Hurray, we answered YES(?,O(n^3))
lmpo
Execution Time (secs) | - |
Answer | MAYBE |
Input | AG01 3.6a |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
Execution Time (secs) | - |
Answer | MAYBE |
Input | AG01 3.6a |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
Execution Time (secs) | 0.220 |
Answer | MAYBE |
Input | AG01 3.6a |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
Execution Time (secs) | 0.215 |
Answer | MAYBE |
Input | AG01 3.6a |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..