LMPO

Execution Time (secs)	0.118
Answer	MAYBE
Input	Transformed CSR 04 ExSec4 2 DLMMU04 Z

MAYBE

We consider the following Problem:

  Strict Trs:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , fst(pair(XS, YS)) -> XS
     , snd(pair(XS, YS)) -> YS
     , splitAt(0(), XS) -> pair(nil(), XS)
     , splitAt(s(N), cons(X, XS)) ->
       u(splitAt(N, activate(XS)), N, X, activate(XS))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)	0.173
Answer	MAYBE
Input	Transformed CSR 04 ExSec4 2 DLMMU04 Z

MAYBE

We consider the following Problem:

  Strict Trs:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , fst(pair(XS, YS)) -> XS
     , snd(pair(XS, YS)) -> YS
     , splitAt(0(), XS) -> pair(nil(), XS)
     , splitAt(s(N), cons(X, XS)) ->
       u(splitAt(N, activate(XS)), N, X, activate(XS))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)	0.136
Answer	MAYBE
Input	Transformed CSR 04 ExSec4 2 DLMMU04 Z

MAYBE

We consider the following Problem:

  Strict Trs:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , fst(pair(XS, YS)) -> XS
     , snd(pair(XS, YS)) -> YS
     , splitAt(0(), XS) -> pair(nil(), XS)
     , splitAt(s(N), cons(X, XS)) ->
       u(splitAt(N, activate(XS)), N, X, activate(XS))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)	0.164
Answer	YES(?,POLY)
Input	Transformed CSR 04 ExSec4 2 DLMMU04 Z

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , fst(pair(XS, YS)) -> XS
     , snd(pair(XS, YS)) -> YS
     , splitAt(0(), XS) -> pair(nil(), XS)
     , splitAt(s(N), cons(X, XS)) ->
       u(splitAt(N, activate(XS)), N, X, activate(XS))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order (PS) as induced by the safe mapping

   safe(natsFrom) = {1}, safe(cons) = {1, 2}, safe(n__natsFrom) = {1},
   safe(s) = {1}, safe(fst) = {1}, safe(pair) = {1, 2},
   safe(snd) = {1}, safe(splitAt) = {2}, safe(0) = {}, safe(nil) = {},
   safe(u) = {1, 3, 4}, safe(activate) = {1}, safe(head) = {1},
   safe(tail) = {}, safe(sel) = {}, safe(afterNth) = {2},
   safe(take) = {}

  and precedence

   splitAt > u, splitAt > activate, u > activate, activate > natsFrom,
   sel > head, afterNth > snd, afterNth > splitAt, take > fst,
   take > splitAt, activate ~ tail, sel ~ afterNth .

  Following symbols are considered recursive:

   {natsFrom, fst, snd, splitAt, u, activate, head, tail, sel,
    afterNth, take}

  The recursion depth is 5 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  natsFrom(; N) -> cons(; N, n__natsFrom(; s(; N)))
      , fst(; pair(; XS, YS)) -> XS
      , snd(; pair(; XS, YS)) -> YS
      , splitAt(0(); XS) -> pair(; nil(), XS)
      , splitAt(s(; N); cons(; X, XS)) ->
        u(N; splitAt(N; activate(; XS)), X, activate(; XS))
      , u(N; pair(; YS, ZS), X, XS) ->
        pair(; cons(; activate(; X), YS), ZS)
      , head(; cons(; N, XS)) -> N
      , tail(cons(; N, XS);) -> activate(; XS)
      , sel(N, XS;) -> head(; afterNth(N; XS))
      , take(N, XS;) -> fst(; splitAt(N; XS))
      , afterNth(N; XS) -> snd(; splitAt(N; XS))
      , natsFrom(; X) -> n__natsFrom(; X)
      , activate(; n__natsFrom(; X)) -> natsFrom(; X)
      , activate(; X) -> X}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

Small POP*

Execution Time (secs)	0.139
Answer	MAYBE
Input	Transformed CSR 04 ExSec4 2 DLMMU04 Z

MAYBE

We consider the following Problem:

  Strict Trs:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , fst(pair(XS, YS)) -> XS
     , snd(pair(XS, YS)) -> YS
     , splitAt(0(), XS) -> pair(nil(), XS)
     , splitAt(s(N), cons(X, XS)) ->
       u(splitAt(N, activate(XS)), N, X, activate(XS))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)	0.627
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 ExSec4 2 DLMMU04 Z

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , fst(pair(XS, YS)) -> XS
     , snd(pair(XS, YS)) -> YS
     , splitAt(0(), XS) -> pair(nil(), XS)
     , splitAt(s(N), cons(X, XS)) ->
       u(splitAt(N, activate(XS)), N, X, activate(XS))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  The input was oriented with the instance of
  Small Polynomial Path Order (WSC,
                             PS,
                             Nat 2-bounded) as induced by the safe mapping

   safe(natsFrom) = {1}, safe(cons) = {1, 2}, safe(n__natsFrom) = {1},
   safe(s) = {1}, safe(fst) = {1}, safe(pair) = {1, 2},
   safe(snd) = {1}, safe(splitAt) = {2}, safe(0) = {}, safe(nil) = {},
   safe(u) = {1, 2, 3, 4}, safe(activate) = {1}, safe(head) = {1},
   safe(tail) = {}, safe(sel) = {}, safe(afterNth) = {},
   safe(take) = {}

  and precedence

   splitAt > u, splitAt > activate, u > activate, activate > natsFrom,
   tail > activate, sel > head, sel > afterNth, afterNth > snd,
   afterNth > splitAt, take > fst, take > splitAt .

  Following symbols are considered recursive:

   {splitAt}

  The recursion depth is 1 .

  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):

   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  natsFrom(; N) -> cons(; N, n__natsFrom(; s(; N)))
      , fst(; pair(; XS, YS)) -> XS
      , snd(; pair(; XS, YS)) -> YS
      , splitAt(0(); XS) -> pair(; nil(), XS)
      , splitAt(s(; N); cons(; X, XS)) ->
        u(; splitAt(N; activate(; XS)), N, X, activate(; XS))
      , u(; pair(; YS, ZS), N, X, XS) ->
        pair(; cons(; activate(; X), YS), ZS)
      , head(; cons(; N, XS)) -> N
      , tail(cons(; N, XS);) -> activate(; XS)
      , sel(N, XS;) -> head(; afterNth(N, XS;))
      , take(N, XS;) -> fst(; splitAt(N; XS))
      , afterNth(N, XS;) -> snd(; splitAt(N; XS))
      , natsFrom(; X) -> n__natsFrom(; X)
      , activate(; n__natsFrom(; X)) -> natsFrom(; X)
      , activate(; X) -> X}
   Weak Trs  : {}

Hurray, we answered YES(?,O(n^1))

Problem Transformed CSR 04 ExSec4 2 DLMMU04 Z

LMPO

MPO

POP*

POP* (PS)

Small POP*

Small POP* (PS)