Library ToyIntPure

Require Import ucert.

Lemma ih_no_lvar´
: forall (aop : absop) (isrreg : isr) (si : is) (cs : cs) (ie : ie),
    <|| aop ||> ** Aisr isrreg ** Ais si ** Acs cs ** Aie ie ** isr_inv ** (OSInv ** atoy_inv) ** A_dom_lenv nil==>
        <|| aop ||> **
        Aisr isrreg ** Ais si ** Acs cs ** Aie ie ** [|exists k,gettopis si = k /\ forall j, (0 <= j < k)%nat -> isrreg j = false|] ** OSInv ** atoy_inv ** A_dom_lenv nil .

Lemma toyint_sti_inv_elim:
  forall ir si P,
    (forall j : nat,
       (0 <= j < gettopis (1%nat :: si))%nat ->
       isrupd ir 1%nat true j = false) ->
    Aisr (isrupd ir 1%nat true) ** Ais (1%nat::si) ** OSInv ** atoy_inv ** P ==>
         Aisr (isrupd ir 1%nat true) ** Ais (1%nat::si) ** ATopis 1%nat ** invlth_isr I 0%nat 1%nat ** atoy_inv´ ** [|isr_is_prop (isrupd ir 1%nat true) (1%nat::si)|] ** P.
  Lemma xx: forall ir si s P, s|= Aisr ir ** Ais si ** (EX (isr : isr) (is : is),
                                                        Aisr isr ** Ais is ** [|isr_is_prop isr is|]) ** P -> s |= Aisr ir ** Ais si ** [|isr_is_prop ir si|] ** P.
  Lemma xxx: forall ir s P,
    s |= Aisr (isrupd ir 1%nat true) ** P ->
    s |= (([|isrupd ir 1%nat true 1%nat = true|] //\\
        Aisr (isrupd ir 1%nat true)) \\//
       ([|isrupd ir 1%nat true 1%nat = false|] //\\
                                               Aisr (isrupd ir 1%nat true)) ** atoy_inv) ** P.
  Lemma xxxx: forall ir s P,
                isrupd ir 1%nat true 0%nat = false ->
                s |= OSInv ** Aisr (isrupd ir 1%nat true) ** P ->
    s |= (([|isrupd ir 1%nat true 0%nat = true|] //\\
        Aisr (isrupd ir 1%nat true)) \\//
       ([|isrupd ir 1%nat true 0%nat = false|] //\\
        Aisr (isrupd ir 1%nat true)) ** OSInv) ** P.
  Lemma xx´: forall si s P, s |= Ais (1%nat :: si) ** P -> s|= Ais (1%nat :: si) ** ATopis 1%nat ** P.
Qed.