(VAR v x y z )
(RULES 
        *(0, x) -> 0
        *(1, x) -> x
        *(2, 2) -> .(1, 0)
        *(3, x) -> .(x, *(min, x))
        *(min, min) -> 1
        *(2, min) -> .(min, 2)
        *(.(x, y), z) -> .(*(x, z), *(y, z))
        *(+(y, z), x) -> +(*(x, y), *(x, z))
        +(0, x) -> x
        +(x, x) -> *(2, x)
        +(1, 2) -> 3
        +(1, min) -> 0
        +(2, min) -> 1
        +(3, x) -> .(1, +(min, x))
        +(.(x, y), z) -> .(x, +(y, z))
        +(*(2, x), x) -> *(3, x)
        +(*(min, x), x) -> 0
        +(*(2, v), *(min, v)) -> v
        .(min, 3) -> min
        .(x, min) -> .(+(min, x), 3)
        .(0, x) -> x
        .(x, .(y, z)) -> .(+(x, y), z)
        
)