(COMMENT Cohen Watson, RTA LOOP 65)

(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)
)