interpretations
Execution Time (secs) | - |
Answer | YES(?,O(n^2)) |
Input | SK90 2.22 |
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ exp(x, 0()) -> s(0())
, exp(x, s(y)) -> *(x, exp(x, y))
, *(0(), y) -> 0()
, *(s(x), y) -> +(y, *(x, y))
, -(x, 0()) -> x
, -(0(), y) -> 0()
, -(s(x), s(y)) -> -(x, y) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(exp) = {}, Uargs(s) = {}, Uargs(*) = {2}, Uargs(+) = {2},
Uargs(-) = {}
TcT has computed following constructor-restricted polynomial
interpretation.
[exp](x1, x2) = 2*x1 + x1*x2 + x2^2
[0]() = 3
[s](x1) = 2 + x1
[*](x1, x2) = 1 + 2*x1 + x2
[+](x1, x2) = 2 + x2
[-](x1, x2) = 2 + x1
This order satisfies following ordering constraints
[exp(x, 0())] = 5*x + 9
> 5
= [s(0())]
[exp(x, s(y))] = 4*x + x*y + 4 + 4*y + y^2
> 1 + 4*x + x*y + y^2
= [*(x, exp(x, y))]
[*(0(), y)] = 7 + y
> 3
= [0()]
[*(s(x), y)] = 5 + 2*x + y
> 3 + 2*x + y
= [+(y, *(x, y))]
[-(x, 0())] = 2 + x
> x
= [x]
[-(0(), y)] = 5
> 3
= [0()]
[-(s(x), s(y))] = 4 + x
> 2 + x
= [-(x, y)]
Hurray, we answered YES(?,O(n^2))
lmpo
Execution Time (secs) | - |
Answer | YES(?,ELEMENTARY) |
Input | SK90 2.22 |
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ exp(x, 0()) -> s(0())
, exp(x, s(y)) -> *(x, exp(x, y))
, *(0(), y) -> 0()
, *(s(x), y) -> +(y, *(x, y))
, -(0(), y) -> 0()
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y) }
Obligation:
innermost runtime complexity
Answer:
YES(?,ELEMENTARY)
The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping
safe(exp) = {}, safe(0) = {}, safe(s) = {1}, safe(*) = {2},
safe(+) = {1, 2}, safe(-) = {2}
and precedence
exp > * .
Following symbols are considered recursive:
{exp, *, -}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ exp(x, 0();) -> s(; 0())
, exp(x, s(; y);) -> *(x; exp(x, y;))
, *(0(); y) -> 0()
, *(s(; x); y) -> +(; y, *(x; y))
, -(0(); y) -> 0()
, -(x; 0()) -> x
, -(s(; x); s(; y)) -> -(x; y) }
Weak Trs :
Hurray, we answered YES(?,ELEMENTARY)
mpo
Execution Time (secs) | - |
Answer | YES(?,PRIMREC) |
Input | SK90 2.22 |
YES(?,PRIMREC)
We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).
Strict Trs:
{ exp(x, 0()) -> s(0())
, exp(x, s(y)) -> *(x, exp(x, y))
, *(0(), y) -> 0()
, *(s(x), y) -> +(y, *(x, y))
, -(0(), y) -> 0()
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y) }
Obligation:
innermost runtime complexity
Answer:
YES(?,PRIMREC)
The input was oriented with the instance of'multiset path orders'
as induced by the precedence
exp > s, exp > *, * > + .
Hurray, we answered YES(?,PRIMREC)
popstar
Execution Time (secs) | 0.285 |
Answer | YES(?,POLY) |
Input | SK90 2.22 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ exp(x, 0()) -> s(0())
, exp(x, s(y)) -> *(x, exp(x, y))
, *(0(), y) -> 0()
, *(s(x), y) -> +(y, *(x, y))
, -(0(), y) -> 0()
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order'
as induced by the safe mapping
safe(exp) = {}, safe(0) = {}, safe(s) = {1}, safe(*) = {2},
safe(+) = {1, 2}, safe(-) = {2}
and precedence
exp > * .
Following symbols are considered recursive:
{exp, *, -}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ exp(x, 0();) -> s(; 0())
, exp(x, s(; y);) -> *(x; exp(x, y;))
, *(0(); y) -> 0()
, *(s(; x); y) -> +(; y, *(x; y))
, -(0(); y) -> 0()
, -(x; 0()) -> x
, -(s(; x); s(; y)) -> -(x; y) }
Weak Trs :
Hurray, we answered YES(?,POLY)
popstar-ps
Execution Time (secs) | 0.218 |
Answer | YES(?,POLY) |
Input | SK90 2.22 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ exp(x, 0()) -> s(0())
, exp(x, s(y)) -> *(x, exp(x, y))
, *(0(), y) -> 0()
, *(s(x), y) -> +(y, *(x, y))
, -(0(), y) -> 0()
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping
safe(exp) = {}, safe(0) = {}, safe(s) = {1}, safe(*) = {2},
safe(+) = {1, 2}, safe(-) = {2}
and precedence
exp > * .
Following symbols are considered recursive:
{exp, *, -}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ exp(x, 0();) -> s(; 0())
, exp(x, s(; y);) -> *(x; exp(x, y;))
, *(0(); y) -> 0()
, *(s(; x); y) -> +(; y, *(x; y))
, -(0(); y) -> 0()
, -(x; 0()) -> x
, -(s(; x); s(; y)) -> -(x; y) }
Weak Trs :
Hurray, we answered YES(?,POLY)