(VAR k m n x y z )
(RULES 
        eq(0, 0) -> true
        eq(0, s(m)) -> false
        eq(s(n), 0) -> false
        eq(s(n), s(m)) -> eq(n, m)
        le(0, m) -> true
        le(s(n), 0) -> false
        le(s(n), s(m)) -> le(n, m)
        min(cons(x, nil)) -> x
        min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
        if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
        if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
        replace(n, m, nil) -> nil
        replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
        if_replace(true, n, m, cons(k, x)) -> cons(m, x)
        if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
        empty(nil) -> true
        empty(cons(n, x)) -> false
        head(cons(n, x)) -> n
        tail(nil) -> nil
        tail(cons(n, x)) -> x
        sort(x) -> sortIter(x, nil)
        sortIter(x, y) -> if(empty(x), x, y, append(y, cons(min(x), nil)))
        if(true, x, y, z) -> y
        if(false, x, y, z) -> sortIter(replace(min(x), head(x), tail(x)), z)
        
)