LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ pairNs() -> cons(0(), incr(oddNs()))
, oddNs() -> incr(pairNs())
, incr(cons(X, XS)) -> cons(s(X), incr(XS))
, take(0(), XS) -> nil()
, take(s(N), cons(X, XS)) -> cons(X, take(N, XS))
, zip(nil(), XS) -> nil()
, zip(X, nil()) -> nil()
, zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS))
, tail(cons(X, XS)) -> XS
, repItems(nil()) -> nil()
, repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ pairNs() -> cons(0(), incr(oddNs()))
, oddNs() -> incr(pairNs())
, incr(cons(X, XS)) -> cons(s(X), incr(XS))
, take(0(), XS) -> nil()
, take(s(N), cons(X, XS)) -> cons(X, take(N, XS))
, zip(nil(), XS) -> nil()
, zip(X, nil()) -> nil()
, zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS))
, tail(cons(X, XS)) -> XS
, repItems(nil()) -> nil()
, repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ pairNs() -> cons(0(), incr(oddNs()))
, oddNs() -> incr(pairNs())
, incr(cons(X, XS)) -> cons(s(X), incr(XS))
, take(0(), XS) -> nil()
, take(s(N), cons(X, XS)) -> cons(X, take(N, XS))
, zip(nil(), XS) -> nil()
, zip(X, nil()) -> nil()
, zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS))
, tail(cons(X, XS)) -> XS
, repItems(nil()) -> nil()
, repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS)))}
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:
{ pairNs() -> cons(0(), incr(oddNs()))
, oddNs() -> incr(pairNs())
, incr(cons(X, XS)) -> cons(s(X), incr(XS))
, take(0(), XS) -> nil()
, take(s(N), cons(X, XS)) -> cons(X, take(N, XS))
, zip(nil(), XS) -> nil()
, zip(X, nil()) -> nil()
, zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS))
, tail(cons(X, XS)) -> XS
, repItems(nil()) -> nil()
, repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS)))}
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:
{ pairNs() -> cons(0(), incr(oddNs()))
, oddNs() -> incr(pairNs())
, incr(cons(X, XS)) -> cons(s(X), incr(XS))
, take(0(), XS) -> nil()
, take(s(N), cons(X, XS)) -> cons(X, take(N, XS))
, zip(nil(), XS) -> nil()
, zip(X, nil()) -> nil()
, zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS))
, tail(cons(X, XS)) -> XS
, repItems(nil()) -> nil()
, repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS)))}
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:
{ pairNs() -> cons(0(), incr(oddNs()))
, oddNs() -> incr(pairNs())
, incr(cons(X, XS)) -> cons(s(X), incr(XS))
, take(0(), XS) -> nil()
, take(s(N), cons(X, XS)) -> cons(X, take(N, XS))
, zip(nil(), XS) -> nil()
, zip(X, nil()) -> nil()
, zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS))
, tail(cons(X, XS)) -> XS
, repItems(nil()) -> nil()
, repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..