LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ gt(s(x), 0()) -> true()
, gt(0(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)
, divides(x, y) -> div(x, y, y)
, div(0(), 0(), z) -> true()
, div(0(), s(x), z) -> false()
, div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z))
, div(s(x), s(y), z) -> div(x, y, z)
, prime(x) -> test(x, s(s(0())))
, test(x, y) -> if1(gt(x, y), x, y)
, if1(true(), x, y) -> if2(divides(x, y), x, y)
, if1(false(), x, y) -> true()
, if2(true(), x, y) -> false()
, if2(false(), x, y) -> test(x, s(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:
{ gt(s(x), 0()) -> true()
, gt(0(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)
, divides(x, y) -> div(x, y, y)
, div(0(), 0(), z) -> true()
, div(0(), s(x), z) -> false()
, div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z))
, div(s(x), s(y), z) -> div(x, y, z)
, prime(x) -> test(x, s(s(0())))
, test(x, y) -> if1(gt(x, y), x, y)
, if1(true(), x, y) -> if2(divides(x, y), x, y)
, if1(false(), x, y) -> true()
, if2(true(), x, y) -> false()
, if2(false(), x, y) -> test(x, s(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:
{ gt(s(x), 0()) -> true()
, gt(0(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)
, divides(x, y) -> div(x, y, y)
, div(0(), 0(), z) -> true()
, div(0(), s(x), z) -> false()
, div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z))
, div(s(x), s(y), z) -> div(x, y, z)
, prime(x) -> test(x, s(s(0())))
, test(x, y) -> if1(gt(x, y), x, y)
, if1(true(), x, y) -> if2(divides(x, y), x, y)
, if1(false(), x, y) -> true()
, if2(true(), x, y) -> false()
, if2(false(), x, y) -> test(x, s(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:
{ gt(s(x), 0()) -> true()
, gt(0(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)
, divides(x, y) -> div(x, y, y)
, div(0(), 0(), z) -> true()
, div(0(), s(x), z) -> false()
, div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z))
, div(s(x), s(y), z) -> div(x, y, z)
, prime(x) -> test(x, s(s(0())))
, test(x, y) -> if1(gt(x, y), x, y)
, if1(true(), x, y) -> if2(divides(x, y), x, y)
, if1(false(), x, y) -> true()
, if2(true(), x, y) -> false()
, if2(false(), x, y) -> test(x, s(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:
{ gt(s(x), 0()) -> true()
, gt(0(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)
, divides(x, y) -> div(x, y, y)
, div(0(), 0(), z) -> true()
, div(0(), s(x), z) -> false()
, div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z))
, div(s(x), s(y), z) -> div(x, y, z)
, prime(x) -> test(x, s(s(0())))
, test(x, y) -> if1(gt(x, y), x, y)
, if1(true(), x, y) -> if2(divides(x, y), x, y)
, if1(false(), x, y) -> true()
, if2(true(), x, y) -> false()
, if2(false(), x, y) -> test(x, s(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:
{ gt(s(x), 0()) -> true()
, gt(0(), y) -> false()
, gt(s(x), s(y)) -> gt(x, y)
, divides(x, y) -> div(x, y, y)
, div(0(), 0(), z) -> true()
, div(0(), s(x), z) -> false()
, div(s(x), 0(), s(z)) -> div(s(x), s(z), s(z))
, div(s(x), s(y), z) -> div(x, y, z)
, prime(x) -> test(x, s(s(0())))
, test(x, y) -> if1(gt(x, y), x, y)
, if1(true(), x, y) -> if2(divides(x, y), x, y)
, if1(false(), x, y) -> true()
, if2(true(), x, y) -> false()
, if2(false(), x, y) -> test(x, s(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..