---

Step * 1 of Lemma strong-message-constraint-implies-message-constraint

.....assertion..... 
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. X : EClass(Id × Message(f))
4. hdrs : Name List
5. ∀e:E
     (↓∃bg:bag(E)
        ((∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
        ∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))@i'
6. e : E@i'
7. bg : bag(E)
8. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
9. sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
10. (header(e) ∈ hdrs)@i
⊢ <loc(e), info(e)> ↓∈ class-output(X;es;bg)
BY
{ (D (-2) THEN RWO "-2" 0 THEN Auto THEN BagMemberD 0 THEN D 0⋅ THEN Auto THEN OrLeft THEN Auto)⋅ }

1
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. X : EClass(Id × Message(f))
4. hdrs : Name List
5. ∀e:E
     (↓∃bg:bag(E)
        ((∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
        ∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))@i'
6. e : E@i'
7. bg : bag(E)
8. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
9. cs : bag(Id × Message(f))
10. class-output(X;es;bg) = (delivered-with-headers(hdrs;es;e) + cs) ∈ bag(Id × Message(f))
11. (header(e) ∈ hdrs)@i
⊢ <loc(e), info(e)> ↓∈ delivered-with-headers(hdrs;es;e)

---

Latex:

---

Latex:
.....assertion..... 
1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  X  :  EClass(Id  \mtimes{}  Message(f))
4.  hdrs  :  Name  List
5.  \mforall{}e:E
          (\mdownarrow{}\mexists{}bg:bag(E)
                ((\mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e)))
                \mwedge{}  sub-bag(Id  \mtimes{}  Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))@i'
6.  e  :  E@i'
7.  bg  :  bag(E)
8.  \mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e))
9.  sub-bag(Id  \mtimes{}  Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
10.  (header(e)  \mmember{}  hdrs)@i
\mvdash{}  <loc(e),  info(e)>  \mdownarrow{}\mmember{}  class-output(X;es;bg)


By

---

Latex:
(D  (-2)  THEN  RWO  "-2"  0  THEN  Auto  THEN  BagMemberD  0  THEN  D  0\mcdot{}  THEN  Auto  THEN  OrLeft  THEN  Auto)\mcdot{}

---

Home Index