---

Step * 1 1 of Lemma global-order-pairwise-compat-msg-interface-constraint


1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E
     ((msg-header(last(map(λx.info(x);≤loc(e)))) ∈ hdrs)
     ⇒ (↓∃e':E
           ((e' < e)
           ∧ (∃delay:ℤ
               make-msg-interface(delay;loc(e);last(map(λx.info(x);≤loc(e)))) ↓∈ snd(F 
                                                                                     loc(e')*(firstn(||map(λx.info(x);
                                                                                                           ≤loc(e'))|| 
               - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (header(e) ∈ hdrs)@i
12. ∃e':E
     ((e' < e)
     ∧ (∃delay:ℤ
         make-msg-interface(delay;loc(e);info(e)) ↓∈ snd(F loc(e')*(firstn(||map(λx.info(x);≤loc(e'))|| 
         - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))))
⊢ ∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))
BY
{ (RepeatFor 2 ((ParallelLast THEN Auto))
   THEN (Unfold `classrel` 0 THEN Fold `class-ap` 0)
   THEN NthHypEq (-2)
   THEN EqCD
   THEN Auto) }

1
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E
     ((msg-header(last(map(λx.info(x);≤loc(e)))) ∈ hdrs)
     ⇒ (↓∃e':E
           ((e' < e)
           ∧ (∃delay:ℤ
               make-msg-interface(delay;loc(e);last(map(λx.info(x);≤loc(e)))) ↓∈ snd(F 
                                                                                     loc(e')*(firstn(||map(λx.info(x);
                                                                                                           ≤loc(e'))|| 
               - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (header(e) ∈ hdrs)@i
12. e' : E
13. (e' < e)
14. delay : ℤ
15. make-msg-interface(delay;loc(e);info(e)) ↓∈ snd(F loc(e')*(firstn(||map(λx.info(x);≤loc(e'))|| 
- 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))
16. (e' < e)
⊢ X(e')
= (snd(F loc(e')*(firstn(||≤loc(e')|| - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e'))))))
∈ bag(Interface)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type@i'
2.  hdrs  :  Name  List@i
3.  X  :  EClass(Interface)@i'
4.  F  :  Id  {}\mrightarrow{}  hdataflow(Message(f);Interface)@i'
5.  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.    (X(e)  =  (snd(F  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))@i'
6.  eo  :  EO+(Message(f))@i'
7.  \mforall{}e:E
          ((msg-header(last(map(\mlambda{}x.info(x);\mleq{}loc(e))))  \mmember{}  hdrs)
          {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                      ((e'  <  e)
                      \mwedge{}  (\mexists{}delay:\mBbbZ{}
                              make-msg-interface(delay;loc(e);last(map(\mlambda{}x.info(x);
                                                                                                                \mleq{}loc(e))))  \mdownarrow{}\mmember{}  snd(F 
                                                                                                                                                    loc(e')*(firstn(||...|| 
                              -  1;map(\mlambda{}x.info(x);\mleq{}loc(e'))))(last(map(\mlambda{}x.info(x);\mleq{}loc(e')))))))))@i
8.  e  :  E@i
9.  \mforall{}e:E.  (last(map(\mlambda{}x.info(x);\mleq{}loc(e)))  \msim{}  info(e))
10.  last(map(\mlambda{}x.info(x);\mleq{}loc(e)))  \msim{}  info(e)
11.  (header(e)  \mmember{}  hdrs)@i
12.  \mexists{}e':E
          ((e'  <  e)
          \mwedge{}  (\mexists{}delay:\mBbbZ{}
                  make-msg-interface(delay;loc(e);info(e))  \mdownarrow{}\mmember{}  snd(F 
                                                                                                                  loc(e')*(firstn(||map(\mlambda{}x.info(x);
                                                                                                                                                              \mleq{}loc(e'))|| 
                  -  1;map(\mlambda{}x.info(x);\mleq{}loc(e'))))(last(map(\mlambda{}x.info(x);\mleq{}loc(e')))))))
\mvdash{}  \mexists{}e':E.  \mexists{}delay:\mBbbZ{}.  ((e'  <  e)  \mwedge{}  make-msg-interface(delay;loc(e);info(e))  \mmember{}  X(e'))


By

---

Latex:
(RepeatFor  2  ((ParallelLast  THEN  Auto))
  THEN  (Unfold  `classrel`  0  THEN  Fold  `class-ap`  0)
  THEN  NthHypEq  (-2)
  THEN  EqCD
  THEN  Auto)

---

Home Index