(STRATEGY
    INNERMOST)

(VAR
    v w x y z)
(DATATYPES
    A = µX.< nil, cons(X, X), 0, s(X) >)
(SIGNATURES
    sort :: [A] -> A
    insert :: [A x A] -> A
    choose :: [A x A x A x A] -> A)
(RULES
    sort(nil()) -> nil()
    sort(cons(x,y)) -> insert(x
                             ,sort(y))
    insert(x,nil()) -> cons(x,nil())
    insert(x,cons(v,w)) -> choose(x
                                 ,cons(v,w)
                                 ,x
                                 ,v)
    choose(x,cons(v,w),y,0()) ->
      cons(x,cons(v,w))
    choose(x,cons(v,w),0(),s(z)) ->
      cons(v,insert(x,w))
    choose(x,cons(v,w),s(y),s(z)) ->
      choose(x,cons(v,w),y,z))