LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ a__g(X) -> a__h(X)
, a__c() -> d()
, a__h(d()) -> a__g(c())
, mark(g(X)) -> a__g(X)
, mark(h(X)) -> a__h(X)
, mark(c()) -> a__c()
, mark(d()) -> d()
, a__g(X) -> g(X)
, a__h(X) -> h(X)
, a__c() -> c()}
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:
{ a__g(X) -> a__h(X)
, a__c() -> d()
, a__h(d()) -> a__g(c())
, mark(g(X)) -> a__g(X)
, mark(h(X)) -> a__h(X)
, mark(c()) -> a__c()
, mark(d()) -> d()
, a__g(X) -> g(X)
, a__h(X) -> h(X)
, a__c() -> c()}
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__g > a__h, a__g > g, a__h > h, a__c > d, a__c > c, d > a__g,
d > c, mark > a__g, mark > a__h, a__c ~ mark .
Hurray, we answered YES(?,PRIMREC)
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ a__g(X) -> a__h(X)
, a__c() -> d()
, a__h(d()) -> a__g(c())
, mark(g(X)) -> a__g(X)
, mark(h(X)) -> a__h(X)
, mark(c()) -> a__c()
, mark(d()) -> d()
, a__g(X) -> g(X)
, a__h(X) -> h(X)
, a__c() -> c()}
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__g(X) -> a__h(X)
, a__c() -> d()
, a__h(d()) -> a__g(c())
, mark(g(X)) -> a__g(X)
, mark(h(X)) -> a__h(X)
, mark(c()) -> a__c()
, mark(d()) -> d()
, a__g(X) -> g(X)
, a__h(X) -> h(X)
, a__c() -> c()}
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__g(X) -> a__h(X)
, a__c() -> d()
, a__h(d()) -> a__g(c())
, mark(g(X)) -> a__g(X)
, mark(h(X)) -> a__h(X)
, mark(c()) -> a__c()
, mark(d()) -> d()
, a__g(X) -> g(X)
, a__h(X) -> h(X)
, a__c() -> c()}
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__g(X) -> a__h(X)
, a__c() -> d()
, a__h(d()) -> a__g(c())
, mark(g(X)) -> a__g(X)
, mark(h(X)) -> a__h(X)
, mark(c()) -> a__c()
, mark(d()) -> d()
, a__g(X) -> g(X)
, a__h(X) -> h(X)
, a__c() -> c()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..