LMPO
YES(?,ELEMENTARY)
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,ELEMENTARY)
Proof:
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 consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,PRIMREC)
Proof:
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)
POP*
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..