(STRATEGY
    INNERMOST)

(VAR
    N X X1 X2 Y Z)
(DATATYPES
    A = µX.< cons(X, X), recip(X), n__terms(X), 0, n__add(X, X), n__s(X), n__dbl(X), nil, n__first(X, X) >)
(SIGNATURES
    terms :: [A] -> A
    sqr :: [A] -> A
    dbl :: [A] -> A
    add :: [A x A] -> A
    first :: [A x A] -> A
    s :: [A] -> A
    activate :: [A] -> A)
(RULES
    terms(N) -> cons(recip(sqr(N))
                    ,n__terms(s(N)))
    sqr(0()) -> 0()
    sqr(s(X)) ->
      s(n__add(sqr(activate(X))
              ,dbl(activate(X))))
    dbl(0()) -> 0()
    dbl(s(X)) ->
      s(n__s(n__dbl(activate(X))))
    add(0(),X) -> X
    add(s(X),Y) ->
      s(n__add(activate(X),Y))
    first(0(),X) -> nil()
    first(s(X),cons(Y,Z)) -> cons(Y
                                 ,n__first(activate(X)
                                          ,activate(Z)))
    terms(X) -> n__terms(X)
    add(X1,X2) -> n__add(X1,X2)
    s(X) -> n__s(X)
    dbl(X) -> n__dbl(X)
    first(X1,X2) -> n__first(X1,X2)
    activate(n__terms(X)) ->
      terms(X)
    activate(n__add(X1,X2)) ->
      add(X1,X2)
    activate(n__s(X)) -> s(X)
    activate(n__dbl(X)) -> dbl(X)
    activate(n__first(X1,X2)) ->
      first(X1,X2)
    activate(X) -> X)