interpretations
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The following argument positions are usable:
Uargs(app) = {}, Uargs(cons) = {2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[app](x1, x2) = [2] x1 + [1]
[nil] = [0]
[cons](x1, x2) = [1] x2 + [2]
This order satisfies following ordering constraints
[app(nil(), xs)] = [1]
> [0]
= [nil()]
[app(cons(x, xs), ys)] = [2] xs + [5]
> [2] xs + [3]
= [cons(x, app(xs, ys))]
Hurray, we answered YES(?,O(n^1))
lmpo
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys)) }
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(app) = {}, safe(nil) = {}, safe(cons) = {1, 2}
and precedence
empty .
Following symbols are considered recursive:
{app}
The recursion depth is 1.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ app(nil(), xs;) -> nil()
, app(cons(; x, xs), ys;) -> cons(; x, app(xs, ys;)) }
Weak Trs :
Hurray, we answered YES(?,ELEMENTARY)
mpo
YES(?,PRIMREC)
We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,PRIMREC)
The input was oriented with the instance of'multiset path orders'
as induced by the precedence
app > cons .
Hurray, we answered YES(?,PRIMREC)
popstar
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys)) }
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(app) = {}, safe(nil) = {}, safe(cons) = {1, 2}
and precedence
empty .
Following symbols are considered recursive:
{app}
The recursion depth is 1.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ app(nil(), xs;) -> nil()
, app(cons(; x, xs), ys;) -> cons(; x, app(xs, ys;)) }
Weak Trs :
Hurray, we answered YES(?,POLY)
popstar-ps
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ app(nil(), xs) -> nil()
, app(cons(x, xs), ys) -> cons(x, app(xs, ys)) }
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(app) = {}, safe(nil) = {}, safe(cons) = {1, 2}
and precedence
empty .
Following symbols are considered recursive:
{app}
The recursion depth is 1.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ app(nil(), xs;) -> nil()
, app(cons(; x, xs), ys;) -> cons(; x, app(xs, ys;)) }
Weak Trs :
Hurray, we answered YES(?,POLY)