Library chkissound

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import includeLib.
Require Import baseTac.
Require Import auxdef.

 Lemma store_join_map_join :
    forall Mf x4 x10 Ms x3 b v v´ M´,
                                 MemMod.join x3 Mf x4 ->
  MemMod.join x10 Ms x3->
  mapstoval (b, Int.unsigned Int.zero) Tint32 v x10 ->
            store Tint32 x4 (b, 0%Z) v´ = Some M´->
  exists M1 M2 , MemMod.join M2 Mf M´ /\ MemMod.join M1 Ms M2 /\
                 mapstoval (b, Int.unsigned Int.zero) Tint32 v´ M1.

Lemma checkis_rule_sound: forall Spec sd I r ri x aop isr is ie v cs,
                            RuleSem Spec sd I r ri
                                    ((OS[isr, ie, is, cs] ** LV x @ Tint32 |-> v) //\\ <|aop|>)
                                    (sprim (checkis x))
                                    (OS[isr, ie, is, cs] ** LV x @ Tint32 |-> (is_length is) //\\ <|aop|>).