Require Import Omega.
Require Import Vbase Arith Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsGlobal.

Hint Immediate plus_n_O mult_n_O.

Local Open Scope string_scope.

Set Implicit Arguments.

Definition is_pred A (rel : A → A → Prop) B a :=
  ∃ b, In b B ∧ clos_refl_trans A rel a b.

Definition depth_metric A (rel: A → A → Prop) V acts :=
  length (filter (mydecf (is_pred rel acts)) V).

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.

Lemma clos_trans_hbE :
  ∀ lab sb rf a b (HB: clos_trans actid (happens_before lab sb rf) a b),
    happens_before lab sb rf a b.

Lemma length_filter_imp :
  ∀ A (f g : A → Prop) (IMP : ∀ x, f x → g x) l,
    length (filter (mydecf f) l) ≤
    length (filter (mydecf g) l).

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.

Lemma edge_depth_ind lab sb rf V
  (IRR : irreflexive (happens_before lab sb rf) )
  (HC: prefix_closed sb rf V) (P : tagged_edge → Prop) :
  (∀ edge
    (IH: ∀ edge'
            (LT: happens_before lab sb rf (te_src edge') (te_src edge)),
      P edge')
    (IN : In (te_src edge) V),
    P edge) →
  ∀ edge, In (te_src edge) V → P edge.

Lemma res_get_plus_alloc r r' l :
  res_get (res_plus r r') l ≠ p_bot →
  res_get r l ≠ p_bot ∨ res_get r' l ≠ p_bot.

Lemma res_get_rsum_alloc rl l :
  res_get (rsum rl) l ≠ p_bot →
  ∃ r, In r rl ∧ res_get r l ≠ p_bot.

Lemma incoming_allocated :
  ∀ acts L b l (IN: res_get (incoming acts L b) l ≠ p_bot),
    ∃ te, te_tgt te = Some b ∧ res_get (L te) l ≠ p_bot.

Lemma res_get_plus_bot r r' (D: res_plus r r' ≠ Rundef) l :
  res_get (res_plus r r') l = p_bot ↔ res_get r l = p_bot ∧ res_get r' l = p_bot.

Lemma res_get_rsum_bot rl (D: rsum rl ≠ Rundef) l :
  res_get (rsum rl) l = p_bot ↔ ∀ r, In r rl → res_get r l = p_bot.

Lemma guar_allocated :
  ∀ IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l
    (GET: res_get r l = p_bot)
    (NA: ¬ ∃ l' n, act = Aalloc l' n ∧ l' ≤ l ≤ l' + n),
    r_sb ⊕ r_rf ≠ Rundef ∧
    res_get r_sb l = p_bot ∧
    res_get r_rf l = p_bot.

Lemma outgoing_allocated :
   ∀ IE acts M amap rf L E edge
     (V: valid_node IE acts M amap rf L E (te_src edge)) l
     (G: res_get (L edge) l ≠ p_bot)
     (IN: ∀ b, te_tgt edge = Some b → In b acts)
     (IN': ∀ σ a, edge = TescS σ a → In σ E)
     (NA: ¬ ∃ l' n, amap (te_src edge) = Aalloc l' n ∧ l' ≤ l ≤ l' + n),
   res_get (incoming acts L (te_src edge)) l ≠ p_bot.

Lemma nemp_of_get_at r l τ S : res_get r l = p_at τ S → r ≠ res_emp.

Lemma nemp_of_get_nbot r l : res_get r l ≠ p_bot → r ≠ res_emp.

Hint Resolve nemp_of_get_at nemp_of_get_nbot.

Lemma prefix_closed_pres_in sb rf N a :
  prefix_closed sb rf N →
  In a N →
  pres_in sb rf a N.

Lemma hb_one :
  ∀ acts amap sb rf L E
    (LR : label_restr acts amap sb rf L E) te b,
  te_tgt te = Some b →
  L te ≠ res_emp →
  happens_before amap sb rf (te_src te) b.

Lemma lab_src_in_acts :
  ∀ acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (LR : label_restr acts amap sb rf L E) te
    (G : L te ≠ res_emp),
  In (te_src te) acts.

Lemma lab_tgt_in_acts :
  ∀ acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (LR : label_restr acts amap sb rf L E) te
    (G : L te ≠ res_emp) b
    (T : te_tgt te = Some b),
  In b acts.

Lemma visible_allocation_one :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) te l
    (G: res_get (L te) l ≠ p_bot) (X: In (te_src te) N),
  ∃ a l' n, may_happens_before amap sb rf a (te_src te) ∧
            amap a = Aalloc l' n ∧
            l' ≤ l ≤ l' + n.

Lemma visible_allocation :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b (IN: pres_in sb rf b N) l
    (G: res_get (incoming acts L b) l ≠ p_bot),
  ∃ a l' n, happens_before amap sb rf a b ∧
            amap a = Aalloc l' n ∧
            l' ≤ l ≤ l' + n.

Definition is_na r l v := ∃ k, res_get r l = p_na k v.

Lemma res_get_plus_naE r r' l k v :
  res_get (res_plus r r') l = p_na k v →
  ∃ k, res_get r l = p_na k v ∨ res_get r' l = p_na k v.

Lemma res_get_rsum_naE rl l k v :
  res_get (rsum rl) l = p_na k v →
  ∃ r k, In r rl ∧ res_get r l = p_na k v.

Lemma is_na_plusE r r' l v :
  is_na (res_plus r r') l v → is_na r l v ∨ is_na r' l v.

Lemma is_na_rsumE rl l v :
  is_na (rsum rl) l v → ∃ r, In r rl ∧ is_na r l v.

Lemma incoming_na :
  ∀ acts L b l v (IN: is_na (incoming acts L b) l v),
    ∃ te, te_tgt te = Some b ∧ is_na (L te) l v.

Lemma is_na_plus r r' (D: res_plus r r' ≠ Rundef) l v :
  is_na (res_plus r r') l v ↔
  is_na r l v ∨ is_na r' l v.

Lemma is_na_rsum rl (D: rsum rl ≠ Rundef) l v :
  is_na (rsum rl) l v ↔ ∃ r, In r rl ∧ is_na r l v.

Lemma guar_na_sb :
  ∀ IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l v
    (GET: is_na r_sb l v)
    (NW: ¬ is_writeLV act l v),
    is_na r l v.

Lemma guar_na_rf :
  ∀ IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l v
    (GET: is_na r_rf l v)
    (NW: ¬ is_writeLV act l v),
    is_na r l v.

Lemma guar_def :
  ∀ IE (r_pre r : resource) (act : act) (r_sb r_rf : resource),
  guar IE r_pre r act r_sb r_rf →
  r_sb ≠ Rundef ∧ r_rf ≠ Rundef.

Lemma outgoing_na :
   ∀ IE acts M amap rf L E edge
     (V: valid_node IE acts M amap rf L E (te_src edge)) l v
     (G: is_na (L edge) l v)
     (IN: ∀ b, te_tgt edge = Some b → In b acts)
     (IN': ∀ σ a, edge = TescS σ a → In σ E)
     (NW: ¬ is_writeLV (amap (te_src edge)) l v),
   is_na (incoming acts L (te_src edge)) l v.

Lemma res_get_plus_na_or_bot r r' l v :
  is_na r l v ∨ res_get r l = p_bot →
  is_na r' l v ∨ res_get r' l = p_bot →
  is_na (r ⊕ r') l v ∨ res_get (r ⊕ r') l = p_bot.

Lemma res_get_rsum_na_or_bot rl l v :
  (∀ r, In r rl → is_na r l v ∨ res_get r l = p_bot) →
  is_na (rsum rl) l v ∨ res_get (rsum rl) l = p_bot.

Lemma compat_def2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR : label_restr acts amap sb rf L E)
    (CC : compat amap sb rf L) edge
    (NE : L edge ≠ res_emp) edge'
    (NE': L edge' ≠ res_emp)
    (NEQ : edge ≠ edge')
    (NHB : ∀ b (TGT: te_tgt edge = Some b)
             (MHB: may_happens_before amap sb rf b (te_src edge')), False)
    (NHB': ∀ b (TGT: te_tgt edge' = Some b)
             (MHB: may_happens_before amap sb rf b (te_src edge)), False)
    (DEF : L edge ⊕ L edge' = Rundef),
  False.

Lemma hb_irr :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) a
    (HB: happens_before amap sb rf a a),
    False.

Lemma compat_inc :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a,
  incoming acts L a ≠ Rundef.

Lemma compat_inc_sink :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a b,
  a = b ∨
  happens_before amap sb rf a b ∨
  L (TsbS b) ⊕ incoming acts L a ≠ Rundef.

Lemma compat_inc_nonsink :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a edge b
    (E : te_tgt edge = Some b),
  may_happens_before amap sb rf a (te_src edge) ∨
  may_happens_before amap sb rf b a ∨
  L edge ⊕ incoming acts L a ≠ Rundef.

Definition writeL_pre x :=
  match x with
    | p_bot ⇒ False
    | p_na k v ⇒ k = pe_full
    | _ ⇒ True
  end.

Lemma is_writeL_inc IE acts M amap rf a l L E :
  is_writeL (amap a) l →
  valid_node IE acts M amap rf L E a →
  writeL_pre (res_get (incoming acts L a) l).

Lemma is_writeL_in IE acts M amap rf a l L E :
  is_writeL (amap a) l →
  valid_node IE acts M amap rf L E a →
  ∃ edge', te_tgt edge' = Some a ∧ res_get (L edge') l ≠ p_bot.

Lemma res_plus_is_na_writeL_pre r r' l v :
  is_na r l v →
  writeL_pre (res_get r' l) →
  r ⊕ r' = Rundef.

Lemma visible_na_one :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) te
    (IN : In (te_src te) N) b
    (T : te_tgt te = Some b) l v
    (G : is_na (L te) l v),
  ∃ a,
    ≪ HB : happens_before amap sb rf a b ≫ ∧
    ≪ WRI: is_writeLV (amap a) l v ≫ ∧
    ≪ OTH: ∀ a' (W: is_writeL (amap a') l) (N: In a' N)
              (HB1: ¬ may_happens_before amap sb rf b a'),
              may_happens_before amap sb rf a' a ≫.

Lemma visible_na :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) (ND: NoDup acts) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l v
    (G : is_na (incoming acts L b) l v),
  ∃ a,
    ≪ HB : happens_before amap sb rf a b ≫ ∧
    ≪ WRI: is_writeLV (amap a) l v ≫ ∧
    ≪ OTH: ∀ a' (W: is_writeL (amap a') l) (N: In a' N)
              (NMHB: ¬ may_happens_before amap sb rf b a'),
              may_happens_before amap sb rf a' a ≫.

Lemma res_get_plus_uninitE r r' l :
  res_get (res_plus r r') l = p_uninit →
  res_get r l = p_uninit ∨ res_get r' l = p_uninit.

Lemma res_get_rsum_uninitE rl l :
  res_get (rsum rl) l = p_uninit →
  ∃ r, In r rl ∧ res_get r l = p_uninit.

Lemma res_get_plus_uninit r r' (D: res_plus r r' ≠ Rundef) l :
  res_get (res_plus r r') l = p_uninit ↔
  res_get r l = p_uninit ∨ res_get r' l = p_uninit.

Lemma res_get_rsum_uninit rl (D: rsum rl ≠ Rundef) l :
  res_get (rsum rl) l = p_uninit ↔
  ∃ r, In r rl ∧ res_get r l = p_uninit.

Lemma incoming_uninit :
  ∀ acts L b l (IN: res_get (incoming acts L b) l = p_uninit),
    ∃ te, te_tgt te = Some b ∧ res_get (L te) l = p_uninit.

Lemma mhb_hb_trans:
  ∀ (amap : actid → act) (sb : actid → actid → Prop)
    (rf : actid → option actid) (a b c : actid),
  may_happens_before amap sb rf a b →
  happens_before amap sb rf b c → happens_before amap sb rf a c.

Lemma helper_out_def :
  ∀ a acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts)
    (ND': NoDup E)
    (CC: compat amap sb rf L)
    (LR : label_restr acts amap sb rf L E),
  outgoing acts L E a ≠ Rundef.

Lemma outgoing_uninit :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) edge l
    (GG : res_get (L edge) l = p_uninit),
  res_get (outgoing acts L E (te_src edge)) l = p_uninit.

Lemma vnode_uninit :
  ∀ acts M amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) IE edge
    (V: valid_node IE acts M amap rf L E (te_src edge)) l
    (GG : res_get (L edge) l = p_uninit)
    (NA : ¬ ∃ l' n, amap (te_src edge) = Aalloc l' n ∧
                         l' ≤ l ≤ l' + n),
  res_get (incoming acts L (te_src edge)) l = p_uninit.

Lemma is_writeL_out :
  ∀ acts M amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) edge l
    (GG: res_get (L edge) l = p_uninit)
    (W : is_writeL (amap (te_src edge)) l) IE
    (V : valid_node IE acts M amap rf L E (te_src edge)),
  False.

Lemma visible_uninit2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l
    (IN: res_get (incoming acts L b) l = p_uninit) a
    (W: is_writeL (amap a) l)
    (PI': pres_in sb rf a N)
    (J : res_get (incoming acts L a) l ≠ p_bot),
    may_happens_before amap sb rf b a.

Lemma visible_uninit :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND' : NoDup E) L
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l
    (IN: res_get (incoming acts L b) l = p_uninit) a
    (W: is_writeL (amap a) l) (INa: In a N),
    may_happens_before amap sb rf b a.

Lemma incoming_atomic :
  ∀ acts L b l τ S (GG: res_get (incoming acts L b) l = p_at τ S) s
    (IN : In s (SL_list S)),
    ∃ te S', te_tgt te = Some b ∧ res_get (L te) l = p_at τ S'
      ∧ In s (SL_list S').

Lemma res_get_plus_at_iff :
  ∀ r r' (D: r ⊕ r' ≠ Rundef) l τ s,
    (∃ S',
      res_get (r ⊕ r') l = p_at τ S' ∧
      In s (SL_list S')) ↔
    (∃ S,
      res_get r l = p_at τ S ∧
      In s (SL_list S)) ∨
    (∃ S,
      res_get r' l = p_at τ S ∧
      In s (SL_list S)).

Lemma res_get_rsum_at_iff :
  ∀ rl (D: rsum rl ≠ Rundef) l τ s,
    (∃ S',
       res_get (rsum rl) l = p_at τ S' ∧
       In s (SL_list S')) ↔
    (∃ r S,
       In r rl ∧
       res_get r l = p_at τ S ∧
       In s (SL_list S)).

Lemma outgoing_atomic :
   ∀ acts amap sb rf mo sc L edge
     (CONS: Consistent acts amap sb rf mo sc)
     (ND: NoDup acts) E (ND' : NoDup E)
     (CC: compat amap sb rf L)
     (LR : label_restr acts amap sb rf L E) l τ S
     (G: res_get (L edge) l = p_at τ S) s
     (IN: In s (SL_list S)),
   ∃ S',
     res_get (outgoing acts L E (te_src edge)) l = p_at τ S' ∧
     In s (SL_list S').

Lemma vnode_atomic :
   ∀ acts M amap sb rf mo sc L edge
     (CONS: Consistent acts amap sb rf mo sc)
     (ND: NoDup acts) E (ND': NoDup E)
     (CC: compat amap sb rf L)
     (LR : label_restr acts amap sb rf L E) IE
     (V: valid_node IE acts M amap rf L E (te_src edge)) l τ S
     (G: res_get (L edge) l = p_at τ S) s
     (IN: In s (SL_list S))
     (NW: ¬ is_writeL (amap (te_src edge)) l ∨ ¬ is_release (amap (te_src edge))),
   ∃ S',
     res_get (incoming acts L (te_src edge)) l = p_at τ S' ∧
     In s (SL_list S').

Lemma visible_atomic2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (CC: compat amap sb rf L)
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a) te
    (PC: prefix_closed sb rf N) l τ S
    (G : res_get (L te) l = p_at τ S) s
    (IN: In s (SL_list S))
    (INn: In (te_src te) N),
  ∃ a,
    ≪ MHB : may_happens_before amap sb rf a (te_src te) ≫ ∧
    ≪ WA : is_writeL (amap a) l ≫ ∧
    ≪ RELA: is_release (amap a) ≫ ∧
    ∃ Sout,
    ≪ Gout: res_get (out_rf acts L a) l = p_at τ Sout ≫ ∧
    ≪ Iout: get_state Sout = s ≫ ∧
    ≪ NEW : ∀ Sin (Gin: res_get (incoming acts L a) l = p_at τ Sin),
               ¬ In s (SL_list Sin) ≫.

Lemma res_get_plus_back :
  ∀ r1 r2 l τ S
    (G : res_get (res_plus r1 r2) l = p_at τ S)
    (NBOT : res_get r1 l ≠ p_bot),
    ∃ S_pre,
      res_get r1 l = p_at τ S_pre ∧
      (∀ x, In x (SL_list S_pre) → In x (SL_list S)).

Lemma get_state_eq1 :
  ∀ acts L a r r'
    (VG : valid_ghost (incoming acts L a) (r ⊕ r')) IE l0 v
    (G : atomic_guar IE r l0 v (out_sb acts L a) (out_rf acts L a))
    (LR: res_lt (res_strip (incoming acts L a)) r) l τ Sin
    (Gin : res_get (incoming acts L a) l = p_at τ Sin) Sout
    (Gout : res_get (out_rf acts L a) l = p_at τ Sout) s''
    (Iout : In s'' (SL_list Sout))
    (NIin : ¬ In s'' (SL_list Sin)),
  get_state Sout = s''.

Lemma get_state_eq2 :
  ∀ IE acts N amap rf L E a
         (V : valid_node IE acts N amap rf L E a) l τ Sin
         (Gin : res_get (incoming acts L a) l = p_at τ Sin) Sout
         (Gout : res_get (out_rf acts L a) l = p_at τ Sout) s''
         (Iout : In s'' (SL_list Sout))
         (NIin : ¬ In s'' (SL_list Sin)),
    get_state Sout = s''.

Lemma visible_atomic :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (CC: compat amap sb rf L)
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b (IN: pres_in sb rf b N) l τ S
    (IN: res_get (incoming acts L b) l = p_at τ S),
  ∃ a S',
    happens_before amap sb rf a b ∧
    is_writeL (amap a) l ∧ is_release (amap a) ∧
    res_get (out_rf acts L a) l = p_at τ S' ∧
    slist_lt S S' ∧ slist_lt S' S.

Lemma visible_atomic2_cor :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (CC: compat amap sb rf L) N M IE
    (V : ∀ a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b l τ S
    (G : res_get (incoming acts L b) l = p_at τ S) s
    (LR : label_restr acts amap sb rf L E)
    (IN: In s (SL_list S))
    (PI: pres_in sb rf b N),
  ∃ a Sout,
    ≪ MHB : may_happens_before amap sb rf a b ≫ ∧
    ≪ AW : is_writeL (amap a) l ≫ ∧
    ≪ AREL: is_release (amap a) ≫ ∧
    ≪ Gout: res_get (out_rf acts L a) l = p_at τ Sout ≫ ∧
    ≪ Iout: get_state Sout = s ≫ ∧
    ≪ Va : valid_node IE acts M amap rf L E a ≫ ∧
    ≪ NEW : ∀ Sin (Gin: res_get (incoming acts L a) l = p_at τ Sin),
               ¬ In s (SL_list Sin) ≫.

Lemma exists_immediate_helper :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b::acts)) E (ND' : NoDup E) M L
    (CC: compat amap sb rf L)
    (LR : label_restr (b::acts) amap sb rf L E) IE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) M amap rf L E a)
    (PC : prefix_closed sb rf acts)
    (PI : pres_in sb rf b acts) l τ S
    (GET : res_get (incoming (b :: acts) L b) l = p_at τ S)
    (CO: conform (b::acts) amap mo L acts)
    (WRI: is_writeL (amap b) l),
  ∃ a,
    ≪ MO : immediate mo a b ≫ ∧
    ≪ Wa : is_writeL (amap a) l ≫ ∧
    ≪ RELa: is_release (amap a) ≫ ∧
    ≪ INa: In a acts ≫.