; ~ (store(v, i, e)[j] = x /\ v[j] = y /\ x >= e /\ x > y)

(not
 (and
  (=
    {read {write v i e} j}
    x)
  (= {read v j} y)
  { >= x e }
  { > x y }
 )
)