MAYBE
Time: 0.003763
TRS:
 {              dbl 0() -> 0(),
                dbl s X -> s s dbl X,
             dbls nil() -> nil(),
        dbls cons(X, Y) -> cons(dbl X, dbls Y),
   sel(0(), cons(X, Y)) -> X,
   sel(s X, cons(Y, Z)) -> sel(X, Z),
         indx(nil(), X) -> nil(),
    indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                 from X -> cons(X, from s X),
               dbl1 0() -> 01(),
               dbl1 s X -> s1 s1 dbl1 X,
  sel1(0(), cons(X, Y)) -> X,
  sel1(s X, cons(Y, Z)) -> sel1(X, Z),
              quote 0() -> 01(),
            quote dbl X -> dbl1 X,
              quote s X -> s1 quote X,
        quote sel(X, Y) -> sel1(X, Y)}
 DP:
  DP:
   {              dbl# s X -> dbl# X,
          dbls# cons(X, Y) -> dbl# X,
          dbls# cons(X, Y) -> dbls# Y,
     sel#(s X, cons(Y, Z)) -> sel#(X, Z),
      indx#(cons(X, Y), Z) -> sel#(X, Z),
      indx#(cons(X, Y), Z) -> indx#(Y, Z),
                   from# X -> from# s X,
                 dbl1# s X -> dbl1# X,
    sel1#(s X, cons(Y, Z)) -> sel1#(X, Z),
              quote# dbl X -> dbl1# X,
                quote# s X -> quote# X,
          quote# sel(X, Y) -> sel1#(X, Y)}
  TRS:
  {              dbl 0() -> 0(),
                 dbl s X -> s s dbl X,
              dbls nil() -> nil(),
         dbls cons(X, Y) -> cons(dbl X, dbls Y),
    sel(0(), cons(X, Y)) -> X,
    sel(s X, cons(Y, Z)) -> sel(X, Z),
          indx(nil(), X) -> nil(),
     indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                  from X -> cons(X, from s X),
                dbl1 0() -> 01(),
                dbl1 s X -> s1 s1 dbl1 X,
   sel1(0(), cons(X, Y)) -> X,
   sel1(s X, cons(Y, Z)) -> sel1(X, Z),
               quote 0() -> 01(),
             quote dbl X -> dbl1 X,
               quote s X -> s1 quote X,
         quote sel(X, Y) -> sel1(X, Y)}
  UR:
   {}
   EDG:
    {(from# X -> from# s X, from# X -> from# s X)}
    STATUS:
     arrows: 0.993056
     SCCS (1):
      Scc:
       {from# X -> from# s X}
      
      SCC (1):
       Strict:
        {from# X -> from# s X}
       Weak:
       {              dbl 0() -> 0(),
                      dbl s X -> s s dbl X,
                   dbls nil() -> nil(),
              dbls cons(X, Y) -> cons(dbl X, dbls Y),
         sel(0(), cons(X, Y)) -> X,
         sel(s X, cons(Y, Z)) -> sel(X, Z),
               indx(nil(), X) -> nil(),
          indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)),
                       from X -> cons(X, from s X),
                     dbl1 0() -> 01(),
                     dbl1 s X -> s1 s1 dbl1 X,
        sel1(0(), cons(X, Y)) -> X,
        sel1(s X, cons(Y, Z)) -> sel1(X, Z),
                    quote 0() -> 01(),
                  quote dbl X -> dbl1 X,
                    quote s X -> s1 quote X,
              quote sel(X, Y) -> sel1(X, Y)}
       Open