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.

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 ≫.