Library clistisound

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

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

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

Lemma sti2_rule_sound : forall Spec sd I r ri isr is aop,
                         RuleSem Spec sd I r ri
              (OS[isr, true, is, nil] //\\ <|aop|>)
                  (sprim sti)
              (OS[isr, true, is, nil] //\\ <|aop|>).