MAYBE
MAYBE
TRS:
 {
     sel(s(X), cons(Y, Z)) -> sel(X, Z),
      sel(0(), cons(X, Z)) -> X,
   first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
             first(0(), Z) -> nil(),
                   from(X) -> cons(X, from(s(X))),
    sel1(s(X), cons(Y, Z)) -> sel1(X, Z),
     sel1(0(), cons(X, Z)) -> quote(X),
          quote(sel(X, Z)) -> sel1(X, Z),
               quote(s(X)) -> s1(quote(X)),
                quote(0()) -> 01(),
  first1(s(X), cons(Y, Z)) -> cons1(quote(Y), first1(X, Z)),
            first1(0(), Z) -> nil1(),
        quote1(cons(X, Z)) -> cons1(quote(X), quote1(Z)),
             quote1(nil()) -> nil1(),
       quote1(first(X, Z)) -> first1(X, Z),
             unquote(01()) -> 0(),
            unquote(s1(X)) -> s(unquote(X)),
          unquote1(nil1()) -> nil(),
     unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z)),
               fcons(X, Z) -> cons(X, Z)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
       sel(s(X), cons(Y, Z)) -> sel(X, Z),
        sel(0(), cons(X, Z)) -> X,
     first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)),
               first(0(), Z) -> nil(),
                     from(X) -> cons(X, from(s(X))),
      sel1(s(X), cons(Y, Z)) -> sel1(X, Z),
       sel1(0(), cons(X, Z)) -> quote(X),
            quote(sel(X, Z)) -> sel1(X, Z),
                 quote(s(X)) -> s1(quote(X)),
                  quote(0()) -> 01(),
    first1(s(X), cons(Y, Z)) -> cons1(quote(Y), first1(X, Z)),
              first1(0(), Z) -> nil1(),
          quote1(cons(X, Z)) -> cons1(quote(X), quote1(Z)),
               quote1(nil()) -> nil1(),
         quote1(first(X, Z)) -> first1(X, Z),
               unquote(01()) -> 0(),
              unquote(s1(X)) -> s(unquote(X)),
            unquote1(nil1()) -> nil(),
       unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z)),
                 fcons(X, Z) -> cons(X, Z)
   }
  Fail