(and

; test out solver for write=write

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


; test out solver for write=s

(=>
 (and
  (= {write bS {+ bz ba} bv} aaa)
  (= {write bS {+ bz ba} {read aa zz}} aa)
  (= {write bS {+ bz ba} bv} c))
 (and
  (ite
   (= {+ x y} {+ bz ba})
   (= {read aaa {+ x y}} bv)
   true)
  (= {read aa zz} {read aa {+ bz ba}})))


; test out canonizer for write(S,a,read(S,a))

(=>
 (= S S1)
 (= {write S a {read S1 a}} S))
 

; test out solver for write(write(write(S,a,v),a1,v1),a2,v2)

(=>
 (= {write {write {write S a v} a1 v1} a2 v2} S)
 (and
  (= {read S a2} v2)
  (=>
   (and (not (= a a1)) (not (= a a2)))
   (= {read S a} v))))

)