Library crtsound

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 encrit1_rule_sound : forall Spec sd I r ri isr is cs i aop,
                         RuleSem Spec sd I r ri
                (OS[isr, true, is, cs] ** (ATopis i) ** (Apure (i <= INUM)) //\\ <|aop|>)
                  (sprim encrit)
                (OS[isr, false, is, true::cs] ** (invlth_isr I O i)//\\ <|aop|>).

Lemma encrit2_rule_sound : forall Spec sd I r ri isr is cs aop,
                         RuleSem Spec sd I r ri
             (OS[isr, false, is, cs] //\\ <|aop|>)
                  (sprim encrit)
             (OS[isr, false, is, false::cs] //\\ <|aop|>).

Lemma excrit1_rule_sound : forall Spec sd I r ri isr is cs i aop,
                         RuleSem Spec sd I r ri
          (OS[isr, false, is, true::cs] ** (ATopis i) ** (invlth_isr I O i)//\\ <|aop|>)
                  (sprim excrit)
          (OS[isr, true, is, cs] //\\ <|aop|>).

Lemma excrit2_rule_sound : forall Spec sd I r ri isr is cs aop,
                         RuleSem Spec sd I r ri
               (OS[isr, false, is, false::cs] //\\ <|aop|>)
                  (sprim excrit)
               (OS[isr, false, is, cs] //\\ <|aop|>).