(STRATEGY
    INNERMOST)

(VAR
    X X1 X2 Y Z)
(DATATYPES
    A = µX.< 0, n__s(X), n__dbl(X), nil, cons(X, X), n__dbls(X), n__sel(X, X), n__indx(X, X), n__from(X), 01, s1(X) >)
(SIGNATURES
    dbl :: [A] -> A
    dbls :: [A] -> A
    sel :: [A x A] -> A
    indx :: [A x A] -> A
    from :: [A] -> A
    dbl1 :: [A] -> A
    sel1 :: [A x A] -> A
    quote :: [A] -> A
    s :: [A] -> A
    activate :: [A] -> A)
(RULES
    dbl(0()) -> 0()
    dbl(s(X)) ->
      s(n__s(n__dbl(activate(X))))
    dbls(nil()) -> nil()
    dbls(cons(X,Y)) ->
      cons(n__dbl(activate(X))
          ,n__dbls(activate(Y)))
    sel(0(),cons(X,Y)) ->
      activate(X)
    sel(s(X),cons(Y,Z)) ->
      sel(activate(X),activate(Z))
    indx(nil(),X) -> nil()
    indx(cons(X,Y),Z) ->
      cons(n__sel(activate(X)
                 ,activate(Z))
          ,n__indx(activate(Y)
                  ,activate(Z)))
    from(X) -> cons(activate(X)
                   ,n__from(n__s(activate(X))))
    dbl1(0()) -> 01()
    dbl1(s(X)) ->
      s1(s1(dbl1(activate(X))))
    sel1(0(),cons(X,Y)) ->
      activate(X)
    sel1(s(X),cons(Y,Z)) ->
      sel1(activate(X),activate(Z))
    quote(0()) -> 01()
    quote(s(X)) ->
      s1(quote(activate(X)))
    quote(dbl(X)) -> dbl1(X)
    quote(sel(X,Y)) -> sel1(X,Y)
    s(X) -> n__s(X)
    dbl(X) -> n__dbl(X)
    dbls(X) -> n__dbls(X)
    sel(X1,X2) -> n__sel(X1,X2)
    indx(X1,X2) -> n__indx(X1,X2)
    from(X) -> n__from(X)
    activate(n__s(X)) -> s(X)
    activate(n__dbl(X)) -> dbl(X)
    activate(n__dbls(X)) -> dbls(X)
    activate(n__sel(X1,X2)) ->
      sel(X1,X2)
    activate(n__indx(X1,X2)) ->
      indx(X1,X2)
    activate(n__from(X)) -> from(X)
    activate(X) -> X)