(VAR k m n x )
(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(0, nil)) -> 0
        min(cons(s(n), nil)) -> s(n)
        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))
        sort(nil) -> nil
        sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))
        
)