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