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