interpretations
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ a__eq(X, Y) -> false()
, a__eq(X1, X2) -> eq(X1, X2)
, a__eq(0(), 0()) -> true()
, a__eq(s(X), s(Y)) -> a__eq(X, Y)
, a__inf(X) -> cons(X, inf(s(X)))
, a__inf(X) -> inf(X)
, a__take(X1, X2) -> take(X1, X2)
, a__take(0(), X) -> nil()
, a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
, a__length(X) -> length(X)
, a__length(cons(X, L)) -> s(length(L))
, a__length(nil()) -> 0()
, mark(0()) -> 0()
, mark(true()) -> true()
, mark(s(X)) -> s(X)
, mark(false()) -> false()
, mark(cons(X1, X2)) -> cons(X1, X2)
, mark(inf(X)) -> a__inf(mark(X))
, mark(nil()) -> nil()
, mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
, mark(length(X)) -> a__length(mark(X))
, mark(eq(X1, X2)) -> a__eq(X1, X2) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(a__eq) = {}, Uargs(s) = {}, Uargs(a__inf) = {1},
Uargs(cons) = {}, Uargs(inf) = {}, Uargs(a__take) = {1, 2},
Uargs(take) = {}, Uargs(a__length) = {1}, Uargs(length) = {},
Uargs(mark) = {}, Uargs(eq) = {}
TcT has computed following constructor-restricted polynomial
interpretation.
[a__eq](x1, x2) = 3 + 2*x1 + 2*x1*x2 + x2
[0]() = 2
[true]() = 0
[s](x1) = 1 + x1
[false]() = 0
[a__inf](x1) = 3 + x1
[cons](x1, x2) = x2
[inf](x1) = 1 + x1
[a__take](x1, x2) = 3 + x1 + x2
[nil]() = 0
[take](x1, x2) = 1 + x1 + x2
[a__length](x1) = 3 + x1
[length](x1) = 1 + x1
[mark](x1) = 1 + 3*x1 + 2*x1^2
[eq](x1, x2) = 1 + x1 + x2
This order satisfies following ordering constraints
[a__eq(X, Y)] = 3 + 2*X + 2*X*Y + Y
>
= [false()]
[a__eq(X1, X2)] = 3 + 2*X1 + 2*X1*X2 + X2
> 1 + X1 + X2
= [eq(X1, X2)]
[a__eq(0(), 0())] = 17
>
= [true()]
[a__eq(s(X), s(Y))] = 8 + 4*X + 3*Y + 2*X*Y
> 3 + 2*X + 2*X*Y + Y
= [a__eq(X, Y)]
[a__inf(X)] = 3 + X
> 2 + X
= [cons(X, inf(s(X)))]
[a__inf(X)] = 3 + X
> 1 + X
= [inf(X)]
[a__take(X1, X2)] = 3 + X1 + X2
> 1 + X1 + X2
= [take(X1, X2)]
[a__take(0(), X)] = 5 + X
>
= [nil()]
[a__take(s(X), cons(Y, L))] = 4 + X + L
> 1 + X + L
= [cons(Y, take(X, L))]
[a__length(X)] = 3 + X
> 1 + X
= [length(X)]
[a__length(cons(X, L))] = 3 + L
> 2 + L
= [s(length(L))]
[a__length(nil())] = 3
> 2
= [0()]
[mark(0())] = 15
> 2
= [0()]
[mark(true())] = 1
>
= [true()]
[mark(s(X))] = 6 + 7*X + 2*X^2
> 1 + X
= [s(X)]
[mark(false())] = 1
>
= [false()]
[mark(cons(X1, X2))] = 1 + 3*X2 + 2*X2^2
> X2
= [cons(X1, X2)]
[mark(inf(X))] = 6 + 7*X + 2*X^2
> 4 + 3*X + 2*X^2
= [a__inf(mark(X))]
[mark(nil())] = 1
>
= [nil()]
[mark(take(X1, X2))] = 6 + 7*X1 + 7*X2 + 2*X1^2 + 2*X1*X2 + 2*X2*X1 + 2*X2^2
> 5 + 3*X1 + 2*X1^2 + 3*X2 + 2*X2^2
= [a__take(mark(X1), mark(X2))]
[mark(length(X))] = 6 + 7*X + 2*X^2
> 4 + 3*X + 2*X^2
= [a__length(mark(X))]
[mark(eq(X1, X2))] = 6 + 7*X1 + 7*X2 + 2*X1^2 + 2*X1*X2 + 2*X2*X1 + 2*X2^2
> 3 + 2*X1 + 2*X1*X2 + X2
= [a__eq(X1, X2)]
Hurray, we answered YES(?,O(n^2))
lmpo
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ a__eq(0(), 0()) -> true()
, a__eq(s(X), s(Y)) -> a__eq(X, Y)
, a__eq(X, Y) -> false()
, a__inf(X) -> cons(X, inf(s(X)))
, a__take(0(), X) -> nil()
, a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
, a__length(nil()) -> 0()
, a__length(cons(X, L)) -> s(length(L))
, mark(eq(X1, X2)) -> a__eq(X1, X2)
, mark(inf(X)) -> a__inf(mark(X))
, mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
, mark(length(X)) -> a__length(mark(X))
, mark(0()) -> 0()
, mark(true()) -> true()
, mark(s(X)) -> s(X)
, mark(false()) -> false()
, mark(cons(X1, X2)) -> cons(X1, X2)
, mark(nil()) -> nil()
, a__eq(X1, X2) -> eq(X1, X2)
, a__inf(X) -> inf(X)
, a__take(X1, X2) -> take(X1, X2)
, a__length(X) -> length(X) }
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(a__eq) = {}, safe(0) = {}, safe(true) = {}, safe(s) = {1},
safe(false) = {}, safe(a__inf) = {1}, safe(cons) = {1, 2},
safe(inf) = {1}, safe(a__take) = {1, 2}, safe(nil) = {},
safe(take) = {1, 2}, safe(a__length) = {1}, safe(length) = {1},
safe(mark) = {}, safe(eq) = {1, 2}
and precedence
mark > a__eq, mark > a__inf, mark > a__take, mark > a__length .
Following symbols are considered recursive:
{a__eq, a__inf, a__take, a__length, mark}
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:
{ a__eq(0(), 0();) -> true()
, a__eq(s(; X), s(; Y);) -> a__eq(X, Y;)
, a__eq(X, Y;) -> false()
, a__inf(; X) -> cons(; X, inf(; s(; X)))
, a__take(; 0(), X) -> nil()
, a__take(; s(; X), cons(; Y, L)) -> cons(; Y, take(; X, L))
, a__length(; nil()) -> 0()
, a__length(; cons(; X, L)) -> s(; length(; L))
, mark(eq(; X1, X2);) -> a__eq(X1, X2;)
, mark(inf(; X);) -> a__inf(; mark(X;))
, mark(take(; X1, X2);) -> a__take(; mark(X1;), mark(X2;))
, mark(length(; X);) -> a__length(; mark(X;))
, mark(0();) -> 0()
, mark(true();) -> true()
, mark(s(; X);) -> s(; X)
, mark(false();) -> false()
, mark(cons(; X1, X2);) -> cons(; X1, X2)
, mark(nil();) -> nil()
, a__eq(X1, X2;) -> eq(; X1, X2)
, a__inf(; X) -> inf(; X)
, a__take(; X1, X2) -> take(; X1, X2)
, a__length(; X) -> length(; X) }
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:
{ a__eq(0(), 0()) -> true()
, a__eq(s(X), s(Y)) -> a__eq(X, Y)
, a__eq(X, Y) -> false()
, a__inf(X) -> cons(X, inf(s(X)))
, a__take(0(), X) -> nil()
, a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
, a__length(nil()) -> 0()
, a__length(cons(X, L)) -> s(length(L))
, mark(eq(X1, X2)) -> a__eq(X1, X2)
, mark(inf(X)) -> a__inf(mark(X))
, mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
, mark(length(X)) -> a__length(mark(X))
, mark(0()) -> 0()
, mark(true()) -> true()
, mark(s(X)) -> s(X)
, mark(false()) -> false()
, mark(cons(X1, X2)) -> cons(X1, X2)
, mark(nil()) -> nil()
, a__eq(X1, X2) -> eq(X1, X2)
, a__inf(X) -> inf(X)
, a__take(X1, X2) -> take(X1, X2)
, a__length(X) -> length(X) }
Obligation:
innermost runtime complexity
Answer:
YES(?,PRIMREC)
The input was oriented with the instance of'multiset path orders'
as induced by the precedence
a__eq > false, a__eq > eq, 0 > true, a__inf > s, a__inf > cons,
a__inf > inf, a__take > cons, a__take > take, a__length > s,
a__length > length, mark > a__eq, mark > a__inf, mark > a__take,
mark > a__length, 0 ~ nil .
Hurray, we answered YES(?,PRIMREC)
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ a__eq(0(), 0()) -> true()
, a__eq(s(X), s(Y)) -> a__eq(X, Y)
, a__eq(X, Y) -> false()
, a__inf(X) -> cons(X, inf(s(X)))
, a__take(0(), X) -> nil()
, a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
, a__length(nil()) -> 0()
, a__length(cons(X, L)) -> s(length(L))
, mark(eq(X1, X2)) -> a__eq(X1, X2)
, mark(inf(X)) -> a__inf(mark(X))
, mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
, mark(length(X)) -> a__length(mark(X))
, mark(0()) -> 0()
, mark(true()) -> true()
, mark(s(X)) -> s(X)
, mark(false()) -> false()
, mark(cons(X1, X2)) -> cons(X1, X2)
, mark(nil()) -> nil()
, a__eq(X1, X2) -> eq(X1, X2)
, a__inf(X) -> inf(X)
, a__take(X1, X2) -> take(X1, X2)
, a__length(X) -> length(X) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ a__eq(0(), 0()) -> true()
, a__eq(s(X), s(Y)) -> a__eq(X, Y)
, a__eq(X, Y) -> false()
, a__inf(X) -> cons(X, inf(s(X)))
, a__take(0(), X) -> nil()
, a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
, a__length(nil()) -> 0()
, a__length(cons(X, L)) -> s(length(L))
, mark(eq(X1, X2)) -> a__eq(X1, X2)
, mark(inf(X)) -> a__inf(mark(X))
, mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
, mark(length(X)) -> a__length(mark(X))
, mark(0()) -> 0()
, mark(true()) -> true()
, mark(s(X)) -> s(X)
, mark(false()) -> false()
, mark(cons(X1, X2)) -> cons(X1, X2)
, mark(nil()) -> nil()
, a__eq(X1, X2) -> eq(X1, X2)
, a__inf(X) -> inf(X)
, a__take(X1, X2) -> take(X1, X2)
, a__length(X) -> length(X) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..