LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
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:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
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:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
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:
{ sort(l) -> st(0(), l)
, st(n, l) -> cond1(member(n, l), n, l)
, cond1(true(), n, l) -> cons(n, st(s(n), l))
, cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
, cond2(true(), n, l) -> nil()
, cond2(false(), n, l) -> st(s(n), l)
, member(n, nil()) -> false()
, member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
, or(x, true()) -> true()
, or(x, false()) -> x
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)
, gt(0(), v) -> false()
, gt(s(u), 0()) -> true()
, gt(s(u), s(v)) -> gt(u, v)
, max(nil()) -> 0()
, max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
, if(true(), u, v) -> u
, if(false(), u, v) -> v}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..