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.2. Rely


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


This page has been generated by coqdoc