((a0 = "--"
      & x1 -- x2 = x1 + -(x2))
      & P0) & 
     ((a0 = "<"
      & (x1 < x2 == x1 <= x2
      & ~x1 eq x2)) & 
     (a0 = "eq" & (
     x1 eq x2 == x1 + 0 = x2 + 0)) & P0) & P0
\