(define-rule array-read-over-write ((t ?Array) (i ?) (e ?))
  (select (store t i e) i) e)

(define-cond-rule array-read-over-write2 ((t ?Array) (i ?) (j ?) (e ?))
  (not (= i j)) (select (store t i e) j) (select t j))

(define-rule array-store-overwrite ((t ?Array) (i ?) (e ?) (f ?))
  (store (store t i e) i f)
  (store t i f))

(define-rule array-store-self ((t ?Array) (i ?))
  (store t i (select t i))
  t)
