interpretations
Execution Time (secs) | - |
Answer | YES(?,O(n^2)) |
Input | SK90 2.18 |
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ sum(0()) -> 0()
, sum(s(x)) -> +(sum(x), s(x))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(sum) = {}, Uargs(s) = {1}, Uargs(+) = {1}
TcT has computed following constructor-restricted polynomial
interpretation.
[sum](x1) = 2 + 3*x1 + x1^2
[0]() = 0
[s](x1) = 1 + x1
[+](x1, x2) = 1 + x1 + 2*x2
This order satisfies following ordering constraints
[sum(0())] = 2
>
= [0()]
[sum(s(x))] = 6 + 5*x + x^2
> 5 + 5*x + x^2
= [+(sum(x), s(x))]
[+(x, 0())] = 1 + x
> x
= [x]
[+(x, s(y))] = 3 + x + 2*y
> 2 + x + 2*y
= [s(+(x, y))]
Hurray, we answered YES(?,O(n^2))
lmpo
Execution Time (secs) | - |
Answer | YES(?,ELEMENTARY) |
Input | SK90 2.18 |
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ sum(0()) -> 0()
, sum(s(x)) -> +(sum(x), s(x))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(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(sum) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1}
and precedence
sum > + .
Following symbols are considered recursive:
{sum, +}
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:
{ sum(0();) -> 0()
, sum(s(; x);) -> +(s(; x); sum(x;))
, +(0(); x) -> x
, +(s(; y); x) -> s(; +(y; x)) }
Weak Trs :
Hurray, we answered YES(?,ELEMENTARY)
mpo
Execution Time (secs) | - |
Answer | YES(?,PRIMREC) |
Input | SK90 2.18 |
YES(?,PRIMREC)
We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).
Strict Trs:
{ sum(0()) -> 0()
, sum(s(x)) -> +(sum(x), s(x))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(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
sum > +, + > s .
Hurray, we answered YES(?,PRIMREC)
popstar
Execution Time (secs) | 0.116 |
Answer | YES(?,POLY) |
Input | SK90 2.18 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ sum(0()) -> 0()
, sum(s(x)) -> +(sum(x), s(x))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(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(sum) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1}
and precedence
sum > + .
Following symbols are considered recursive:
{sum, +}
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:
{ sum(0();) -> 0()
, sum(s(; x);) -> +(s(; x); sum(x;))
, +(0(); x) -> x
, +(s(; y); x) -> s(; +(y; x)) }
Weak Trs :
Hurray, we answered YES(?,POLY)
popstar-ps
Execution Time (secs) | 0.129 |
Answer | YES(?,POLY) |
Input | SK90 2.18 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ sum(0()) -> 0()
, sum(s(x)) -> +(sum(x), s(x))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(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(sum) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1}
and precedence
sum > + .
Following symbols are considered recursive:
{sum, +}
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:
{ sum(0();) -> 0()
, sum(s(; x);) -> +(s(; x); sum(x;))
, +(0(); x) -> x
, +(s(; y); x) -> s(; +(y; x)) }
Weak Trs :
Hurray, we answered YES(?,POLY)