(STRATEGY
    INNERMOST)

(VAR
    w ws xs y ys z zs)
(DATATYPES
    A = µX.< nil, cons(X, X), succ(X), zero >)
(SIGNATURES
    r :: [A x A x A x A] -> A)
(RULES
    r(xs,ys,zs,nil()) -> xs
    r(xs,nil(),zs,cons(w,ws)) ->
      r(xs
       ,xs
       ,cons(succ(zero()),zs)
       ,ws)
    r(xs
     ,cons(y,ys)
     ,nil()
     ,cons(w,ws)) -> r(xs
                      ,xs
                      ,cons(succ(zero()),nil())
                      ,ws)
    r(xs
     ,cons(y,ys)
     ,cons(z,zs)
     ,cons(w,ws)) -> r(ys
                      ,cons(y,ys)
                      ,zs
                      ,cons(succ(zero()),cons(w,ws))))