---

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


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)
BY
{ ((D 0 THEN Auto)
   THEN With ⌈delivered-with-headers(hdrs;es;e)⌉ (D 0)⋅
   THEN Auto
   THEN Unfold `delivered-with-headers` 0
   THEN BLemma `member-mapfilter`
   THEN Reduce 0
   THEN Auto
   THEN With ⌈e⌉ (D 0)⋅
   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
12. delivered-with-headers(hdrs;es;e) = delivered-with-headers(hdrs;es;e) ∈ bag(Id × Message(f))
⊢ (e ∈ ≤loc(e))

---

Latex:

---

Latex:

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.  cs  :  bag(Id  \mtimes{}  Message(f))
10.  class-output(X;es;bg)  =  (delivered-with-headers(hdrs;es;e)  +  cs)
11.  (header(e)  \mmember{}  hdrs)@i
\mvdash{}  <loc(e),  info(e)>  \mdownarrow{}\mmember{}  delivered-with-headers(hdrs;es;e)


By

---

Latex:
((D  0  THEN  Auto)
  THEN  With  \mkleeneopen{}delivered-with-headers(hdrs;es;e)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Unfold  `delivered-with-headers`  0
  THEN  BLemma  `member-mapfilter`
  THEN  Reduce  0
  THEN  Auto
  THEN  With  \mkleeneopen{}e\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index