LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
YES(?,PRIMREC)
We consider the following Problem:
Strict Trs:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(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
f > c, s > a, c > s .
Hurray, we answered YES(?,PRIMREC)
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(X)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..