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 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 rely_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc L
    (PC : prefix_closed sb rf acts) IE EE
    (V : ∀ a (IN: 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)
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (INrf: in_rf (b::acts) L b = res_emp)
    (INesc: in_esc (b::acts) L b = res_emp)
    (INsb: in_sb (b :: acts) L b ≠ Rundef)
    (INsbOK: ∀ a, ¬ sb a b → L (Tsb a b) = res_emp)
    (OUT : outgoing (b::acts) L EE b = res_emp)
    (ND : NoDup (b ::acts))
    (ND' : NoDup EE)
    (LR : label_restr (b::acts) amap sb rf L EE),
  ∃ L',
    ≪ V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::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 ⊕ in_rf (b :: acts) L' b))
               (upd L' (TsbS b) (L' (TsbS b) ⊕ in_sb (b :: acts) L' b ⊕ in_rf (b :: acts) L' b))
               EE σ ≫ ∧
    ≪ GAC: ghost_alloc_conform (b::acts)
               (upd L' (TsbS b)
                    (L' (TsbS b) ⊕ in_sb (b :: acts) L' b
                        ⊕ in_rf (b :: acts) L' b)) EE ≫ ∧
    ≪ RELY: rely IE (in_sb (b::acts) L' b) (amap b)
                  (in_sb (b::acts) L' b ⊕ in_rf (b::acts) L' b) ≫ ∧
    ≪ INesc: in_esc (b::acts) L' b = res_emp ≫ ∧
    ≪ OUT : outgoing (b::acts) L' EE b = res_emp ≫ ∧
    ≪ Esb : ∀ a b, L' (Tsb a b) = L (Tsb a b) ≫ ∧
    ≪ EsbS : ∀ a, L' (TsbS a) = L (TsbS a) ≫ ∧
    ≪ LR : label_restr (b::acts) amap sb rf L' EE ≫.

Lemma rely_compat_post :
  ∀ b acts amap sb rf
    (LAST: ∀ x, ¬ happens_before amap sb rf b x) L EE
    (LR : label_restr (b::acts) amap sb rf L EE)
    (CC: compat amap sb rf L)
    (ND : NoDup (b::acts))
    (OUT : outgoing (b::acts) L EE b = res_emp),
  compat amap sb rf
    (upd L (TsbS b)
         (L (TsbS b) ⊕ in_sb (b::acts) L b ⊕ in_rf (b::acts) L b)).