(=> 
 (= {write S a v} {write S_prime a_prime v_prime})
 (=>
  (and
   (/= b a)
   (/= b a_prime))
  (= {read S b} {read S_prime b})))