(VAR m n x y )
(RULES 
        eq(0, 0) -> true
        eq(0, s(x)) -> false
        eq(s(x), 0) -> false
        eq(s(x), s(y)) -> eq(x, y)
        le(0, y) -> true
        le(s(x), 0) -> false
        le(s(x), s(y)) -> le(x, y)
        app(nil, y) -> y
        app(add(n, x), y) -> add(n, app(x, y))
        min(add(n, nil)) -> n
        min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x)))
        if_min(true, add(n, add(m, x))) -> min(add(n, x))
        if_min(false, add(n, add(m, x))) -> min(add(m, x))
        rm(n, nil) -> nil
        rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
        if_rm(true, n, add(m, x)) -> rm(n, x)
        if_rm(false, n, add(m, x)) -> add(m, rm(n, x))
        minsort(nil, nil) -> nil
        minsort(add(n, x), y) -> if_minsort(eq(n, min(add(n, x))), add(n, x), y)
        if_minsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
        if_minsort(false, add(n, x), y) -> minsort(x, add(n, y))
        
)