---

Step * 1 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
12. delivered-with-headers(hdrs;es;e) = delivered-with-headers(hdrs;es;e) ∈ bag(Id × Message(f))
⊢ (e ∈ ≤loc(e))
BY
{ EAuto 1 }

---

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
12.  delivered-with-headers(hdrs;es;e)  =  delivered-with-headers(hdrs;es;e)
\mvdash{}  (e  \mmember{}  \mleq{}loc(e))


By

---

Latex:
EAuto  1

---

Home Index