---

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

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint{i:l}(es;X;hdrs;f) ⇒ message-constraint{i:l}(es;X;hdrs;f))
BY
{ (Auto
   THEN UnfoldTopAb 0
   THEN UnfoldTopAb (-1)
   THEN ParallelLast
   THEN Auto
   THEN ExRepD
   THEN (Assert ⌜<loc(e), info(e)> ↓∈ class-output(X;es;bg)⌝⋅
   THENM (BagMemberD (-1)
          THEN SquashExRepD
          THEN BagMemberD (-1)
          THEN RepeatFor 3 (ParallelLast)
          THEN Assert ⌜(e1 < e)⌝⋅
          THEN Auto)
   )) }

1
.....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)

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[X:EClass(Id  \mtimes{}  Message(f))].  \mforall{}[hdrs:Name  List].
    (strong-message-constraint\{i:l\}(es;X;hdrs;f)  {}\mRightarrow{}  message-constraint\{i:l\}(es;X;hdrs;f))


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  0
  THEN  UnfoldTopAb  (-1)
  THEN  ParallelLast
  THEN  Auto
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}<loc(e),  info(e)>  \mdownarrow{}\mmember{}  class-output(X;es;bg)\mkleeneclose{}\mcdot{}
  THENM  (BagMemberD  (-1)
                THEN  SquashExRepD
                THEN  BagMemberD  (-1)
                THEN  RepeatFor  3  (ParallelLast)
                THEN  Assert  \mkleeneopen{}(e1  <  e)\mkleeneclose{}\mcdot{}
                THEN  Auto)
  ))

---

Home Index