LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, 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:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, 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:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, 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:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..