Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

C.3.6. Prepare


Lemma in_sb_add :
   a acts b L r,
    In a acts
    NoDup acts
    L (Tsb a b) = res_emp
    in_sb acts (upd L (Tsb a b) r) b = r in_sb acts L b.

Lemma incoming_add b acts L a r :
  In a acts
  NoDup acts
  L (Tsb a b) = res_emp
  incoming acts (upd L (Tsb a b) r) b = r incoming acts L b.

Lemma outgoing_ext_one acts L EE b r :
  outgoing acts L EE b = res_emp
  outgoing acts (upd L (TsbS b) (L (TsbS b) r)) EE b = r.

Lemma outgoing_upd2 b acts L EE a r r_rem c :
  In a acts
  ¬ In b acts
  L (TsbS a) = r r_rem
  L (Tsb a b) = res_emp
  outgoing (b :: acts) (upd (upd L (Tsb a b) r) (TsbS a) r_rem) EE c =
  outgoing (b :: acts) L EE c.

Lemma prepare_step :
   b acts amap sb rf mo sc
    (CONS: Consistent (b :: acts) amap sb rf mo sc)
    (NIN : ¬ In b acts)
    (ND : NoDup (b :: acts)) a
    (SB : sb a b) amap_old sb_old rf_old mo_old sc_old
    (OCON: Consistent acts amap_old sb_old rf_old mo_old sc_old) L EE
    (LR : label_restr acts amap_old sb_old rf_old L EE)
    (NDE : NoDup EE) r r_rem
    (LAB : L (TsbS a) = r r_rem) IE
    (V : a, In a acts valid_node IE acts acts amap_old rf_old L EE a)
    (CC : compat amap_old sb_old rf_old L)
    (CO : conform acts amap_old mo_old L acts)
    (ECO : σ, exch_conform IE acts amap_old sb_old rf_old L L EE σ)
    (GAC : ghost_alloc_conform acts L EE)
    (Ea : x, In x acts amap x = amap_old x)
    (Esb : x y, sb x y sb_old x y x = a y = b)
    (Erf : x, x b rf x = rf_old x)
    (Emo : x, x b y, y b (mo x y mo_old x y))
    (Esc : x, x b y, y b (sc x y sc_old x y)),
   L',
     V : a, In a acts valid_node IE (b :: acts) acts amap rf L' EE a
     CC : compat amap sb rf L'
     CO : conform (b :: acts) amap mo L' acts
     ECO : σ, exch_conform IE (b::acts) amap sb rf
                (upd L' (TsbS b) (L' (TsbS b) in_sb (b :: acts) L' b))
                (upd L' (TsbS b) (L' (TsbS b) in_sb (b :: acts) L' b)) EE σ
     GAC: ghost_alloc_conform (b::acts)
               (upd L' (TsbS b) (L' (TsbS b) in_sb (b :: acts) L' b)) EE
     LAB : L' (TsbS a) = r_rem
     LSB : in_sb (b :: acts) L' b = r
     LR : label_restr (b :: acts) amap sb rf L' EE
     Irf : in_rf (b :: acts) L' b = res_emp
     Iesc: in_esc (b :: acts) L' b = res_emp
     Isb : a', a' a L' (Tsb a' b) = res_emp
     O : outgoing (b :: acts) L' EE b = res_emp
     LEQ : a', a' a L' (TsbS a') = L (TsbS a')
     PC : prefix_closed sb rf acts .

This page has been generated by coqdoc