(STRATEGY
    INNERMOST)

(VAR
    accu l orig x y)
(DATATYPES
    A = µX.< nil, 0, cons(X, X), s(X), false, true, undefined >)
(SIGNATURES
    length :: [A] -> A
    lt :: [A x A] -> A
    head :: [A] -> A
    tail :: [A] -> A
    reverse :: [A] -> A
    rev :: [A x A x A x A] -> A
    if :: [A x A x A x A x A] -> A)
(RULES
    length(nil()) -> 0()
    length(cons(x,l)) ->
      s(length(l))
    lt(x,0()) -> false()
    lt(0(),s(y)) -> true()
    lt(s(x),s(y)) -> lt(x,y)
    head(cons(x,l)) -> x
    head(nil()) -> undefined()
    tail(nil()) -> nil()
    tail(cons(x,l)) -> l
    reverse(l) -> rev(0(),l,nil(),l)
    rev(x,l,accu,orig) -> if(lt(x
                               ,length(orig))
                            ,x
                            ,l
                            ,accu
                            ,orig)
    if(true(),x,l,accu,orig) ->
      rev(s(x)
         ,tail(l)
         ,cons(head(l),accu)
         ,orig)
    if(false(),x,l,accu,orig) ->
      accu)