Require Export Arith_compl.
Require Export Lists_replace.
Require Export BV.

Definition addr := nat. Definition Memo := list BV. Definition MemoSize := length (A:=BV).
Definition MemoEmpty (n : nat) (v : BV) : Memo := list_const BV n v.

Definition MemoZone : Memo -> addr -> nat -> Memo := sublist BV.

Definition MemoRead : Memo -> addr -> Memo := elemlist BV.
Definition MemoWrite : Memo -> addr -> BV -> Memo := replace BV.

Definition AddrOK (m : Memo) (a : addr) : Prop := a < MemoSize m.

Definition MMemo (v : BV) : Memo := v :: nil.

Lemma read_write :
 forall (m : Memo) (a : addr) (v : BV),
 AddrOK m a -> MemoRead (MemoWrite m a v) a = MMemo v.
unfold Memo, AddrOK, MemoRead, MemoWrite, MMemo in |- *.
unfold MemoSize in |- *. intros. apply replace_ok; auto with v62.
Qed.