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