Library OSIntExitPure

Require Import ucert.

Lemma simpl_inv_excrit´
: forall P i,
    Aisr empisr ** OSInv ** invlth_isr´ I 1 i ** P ==>
         Aisr empisr ** invlth_isr I 0%nat i ** P.

Lemma simpl_inv_excrit´´:
  forall P i v´0,
    (
      forall j : nat,
        (0 <= j < i)%nat -> (isrupd v´0 i false) j = false) ->
    Aisr (isrupd v´0 i false) ** invlth_isr I 0%nat i ** P ==>
         Aisr (isrupd v´0 i false) ** OSInv ** invlth_isr´ I 1 i ** P.
  Lemma xx:forall e e0 m ir a b c P, (e, e0, m, ir,a,b,c) |= P -> (e, e0, m, ir,a,b,c) |= Aisr ir ** P.

  Lemma temp: forall s i P,
                (forall j : nat, (0 <= j < S (S i))%nat -> (getisr (gettaskst s)) j = false) ->
                s|= P ** starinv_isr I 0%nat (S i) ->
                s |= P ** OSInv ** (if true then atoy_inv´ else Aemp).
    Lemma xxx: forall m s P X x0,
                  (forall j : nat, (0 <= j < 2)%nat -> getisr (gettaskst s) j = false) ->
                  (m<2)%nat ->
                  s |= (([|x0 m%nat = true|] //\\
                                             Aisr x0) \\//
                                                      ([|x0 m%nat = false|] //\\
                                                                            Aisr x0) ** X) ** P ->
                  s |= X ** P.
  Qed.

Qed.

Lemma simpl_inv_excrit´´´:
  forall P i v´0,
    (
      forall j : nat,
        (0 <= j < i)%nat -> (isrupd v´0 i false) j = false) ->
    Aisr (isrupd v´0 i false) ** OSInv ** invlth_isr´ I 1 i ** P ==>
         Aisr (isrupd v´0 i false) ** invlth_isr I 0%nat i ** P.
  Lemma temp´: forall s i P,
                (forall j : nat, (0 <= j < S (S i))%nat -> (getisr (gettaskst s)) j = false) ->
                s |= P ** OSInv ** (if true then atoy_inv´ else Aemp) ->
                s |= P ** starinv_isr I 0%nat (S i).
    Lemma xxx´: forall m s P X,
                  (forall j : nat, (0 <= j < 2)%nat -> getisr (gettaskst s) j = false) ->
                  (m<2)%nat ->
                  s |= X ** P ->
                  s |= (([|getisr (gettaskst s) m%nat = true|] //\\
                                             Aisr (getisr (gettaskst s))) \\//
                                                      ([|getisr (gettaskst s) m%nat = false|] //\\
                                                                            Aisr (getisr (gettaskst s))) ** X) ** P .
    Lemma sss:forall s P, s|=OSInv ** P -> s |= OSInv ** A_isr_is_prop ** P.
      Lemma sss´:forall s P, s|= A_isr_is_prop ** P -> s|=A_isr_is_prop ** A_isr_is_prop ** P.
    Qed.

    Lemma starinv_prop1_rev´
     : forall (j i : hid) (I : Inv) P,
       P ** starinv_isr I i j ** starinv_isr I (S (i + j)) 0%nat ==>
                  P ** starinv_isr I i (S j).

  Qed.
Qed.

Lemma invlth_isr_invlth_isr´_imp:
  forall s x si P i,
    s|=ATopis x ** invlth_isr I 0%nat x ** Ais (i::si) ** isrclr ** P ->
    s|=OSInv ** invlth_isr´ I 1 i ** Ais (i::si) ** Aisr empisr ** P.
  Require Import mathlib.
  Lemma atopis_eq:
    forall s i x si P,
      s |= ATopis x ** Ais (i :: si) ** P -> x= i.




Qed.

Lemma elim_a_isr_is_prop´: forall isr is s P , isr_is_prop isr is -> s |= Aisr isr **
                                                                      Ais is **
                                                                      A_isr_is_prop ** P -> s|= Aisr isr ** Ais is ** P .