LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ acka(y(), n) -> s(n)
, acka(a(m), y()) -> acka(m, s(0()))
, acka(a(m), a(n)) -> acka(m, ackb(s(m), n))
, ackb(z(), n) -> s(n)
, ackb(b(m), z()) -> ackb(m, s(0()))
, ackb(b(m), b(n)) -> acka(m, ackb(s(m), n))
, s(n) -> a(n)
, s(n) -> b(n)
, 0() -> y()
, 0() -> z()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ acka(y(), n) -> s(n)
, acka(a(m), y()) -> acka(m, s(0()))
, acka(a(m), a(n)) -> acka(m, ackb(s(m), n))
, ackb(z(), n) -> s(n)
, ackb(b(m), z()) -> ackb(m, s(0()))
, ackb(b(m), b(n)) -> acka(m, ackb(s(m), n))
, s(n) -> a(n)
, s(n) -> b(n)
, 0() -> y()
, 0() -> z()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ acka(y(), n) -> s(n)
, acka(a(m), y()) -> acka(m, s(0()))
, acka(a(m), a(n)) -> acka(m, ackb(s(m), n))
, ackb(z(), n) -> s(n)
, ackb(b(m), z()) -> ackb(m, s(0()))
, ackb(b(m), b(n)) -> acka(m, ackb(s(m), n))
, s(n) -> a(n)
, s(n) -> b(n)
, 0() -> y()
, 0() -> z()}
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:
{ acka(y(), n) -> s(n)
, acka(a(m), y()) -> acka(m, s(0()))
, acka(a(m), a(n)) -> acka(m, ackb(s(m), n))
, ackb(z(), n) -> s(n)
, ackb(b(m), z()) -> ackb(m, s(0()))
, ackb(b(m), b(n)) -> acka(m, ackb(s(m), n))
, s(n) -> a(n)
, s(n) -> b(n)
, 0() -> y()
, 0() -> z()}
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:
{ acka(y(), n) -> s(n)
, acka(a(m), y()) -> acka(m, s(0()))
, acka(a(m), a(n)) -> acka(m, ackb(s(m), n))
, ackb(z(), n) -> s(n)
, ackb(b(m), z()) -> ackb(m, s(0()))
, ackb(b(m), b(n)) -> acka(m, ackb(s(m), n))
, s(n) -> a(n)
, s(n) -> b(n)
, 0() -> y()
, 0() -> z()}
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:
{ acka(y(), n) -> s(n)
, acka(a(m), y()) -> acka(m, s(0()))
, acka(a(m), a(n)) -> acka(m, ackb(s(m), n))
, ackb(z(), n) -> s(n)
, ackb(b(m), z()) -> ackb(m, s(0()))
, ackb(b(m), b(n)) -> acka(m, ackb(s(m), n))
, s(n) -> a(n)
, s(n) -> b(n)
, 0() -> y()
, 0() -> z()}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..