LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, lt(0(), s(y)) -> true()
, lt(x, 0()) -> false()
, lt(s(x), s(y)) -> lt(x, y)
, fib(x) -> fibiter(x, 0(), 0(), s(0()))
, fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
, if(false(), b, c, x, y) -> x
, if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, lt(0(), s(y)) -> true()
, lt(x, 0()) -> false()
, lt(s(x), s(y)) -> lt(x, y)
, fib(x) -> fibiter(x, 0(), 0(), s(0()))
, fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
, if(false(), b, c, x, y) -> x
, if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, lt(0(), s(y)) -> true()
, lt(x, 0()) -> false()
, lt(s(x), s(y)) -> lt(x, y)
, fib(x) -> fibiter(x, 0(), 0(), s(0()))
, fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
, if(false(), b, c, x, y) -> x
, if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
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:
{ plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, lt(0(), s(y)) -> true()
, lt(x, 0()) -> false()
, lt(s(x), s(y)) -> lt(x, y)
, fib(x) -> fibiter(x, 0(), 0(), s(0()))
, fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
, if(false(), b, c, x, y) -> x
, if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
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:
{ plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, lt(0(), s(y)) -> true()
, lt(x, 0()) -> false()
, lt(s(x), s(y)) -> lt(x, y)
, fib(x) -> fibiter(x, 0(), 0(), s(0()))
, fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
, if(false(), b, c, x, y) -> x
, if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
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:
{ plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, lt(0(), s(y)) -> true()
, lt(x, 0()) -> false()
, lt(s(x), s(y)) -> lt(x, y)
, fib(x) -> fibiter(x, 0(), 0(), s(0()))
, fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)
, if(false(), b, c, x, y) -> x
, if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..