Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple.

Set Implicit Arguments.

Theorem rule_store_rel typ E E´ P (TYP: release_typ typ) (NORM: normalizable P) :
  triple (Astar (Arel E (mupd (fun _ ⇒ Afalse) E´ P)) P)
         (Estore typ E E´)
         (fun _ ⇒ Arainit E).

Theorem rule_store_rlx E E´ P :
  triple (Astar (Arel E (mupd (fun _ ⇒ Afalse) E´ P)) (Atriangle P))
         (Estore ATrlx E E´)
         (fun _ ⇒ Arainit E).