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

Set Implicit Arguments.

Theorem rule_store_rel PS PSg typ E E' (P: assn PS PSg) (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 PS PSg typ E E' (P: assn PS PSg) (AT: typ ≠ ATna):
  triple (Astar (Arel E (mupd (fun _ ⇒ Afalse) E' P)) (Atriangle P))
         (Estore typ E E')
         (fun _ ⇒ Arainit E).