(VAR v w x y z )
(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)
        
)