---

Step * of Lemma strong-message-constraint-no-rep-large-1hdr

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (no_repeats(Name;hdrs)
  ⇒ strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f)
  ⇒ (∀hdr:Name. ((hdr ∈ hdrs) ⇒ strong-message-constraint-no-rep-large{i:l}(es;X;[hdr];f))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `strong-message-constraint-no-rep-large` 0
   THEN Auto
   THEN Unfold `strong-message-constraint-no-rep-large` (-4)
   THEN (InstHyp [⌈e⌉] (-4)⋅ THENA Auto)
   THEN SquashExRepD
   THEN D 0
   THEN InstConcl [⌈bg⌉]⋅
   THEN Auto
   THEN (Assert ⌈sub-bag(Id × Message(f);delivered-with-headers([hdr];es;e);delivered-with-headers(hdrs;es;e))⌉⋅
   THENM (FLemma `sub-bag_transitivity` [-1;-6] THEN Auto)⋅
   )) }

1
.....assertion..... 
1. f : Name ─→ Type
2. es : EO+(Message(f))
3. X : EClass(Id × Message(f))
4. hdrs : Name List
5. no_repeats(Name;hdrs)@i
6. ∀e:E
     (↓∃bg:bag(E)
        (bag-no-repeats(E;bg)
        ∧ (∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2))))
        ∧ (∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
        ∧ sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
        ∧ (∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' ))))))@i'
7. hdr : Name@i
8. (hdr ∈ hdrs)@i
9. e : E@i'
10. bg : bag(E)
11. bag-no-repeats(E;bg)
12. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
13. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
14. sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
15. ∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' )))
16. bag-no-repeats(E;bg)
17. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
18. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
⊢ sub-bag(Id × Message(f);delivered-with-headers([hdr];es;e);delivered-with-headers(hdrs;es;e))

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `strong-message-constraint-no-rep-large`  0
  THEN  Auto
  THEN  Unfold  `strong-message-constraint-no-rep-large`  (-4)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}bg\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}sub-bag(Id
                              \mtimes{}  Message(f);delivered-with-headers([hdr];es;e);delivered-with-headers(hdrs;es;e))\mkleeneclose{}\mcdot{}
  THENM  (FLemma  `sub-bag\_transitivity`  [-1;-6]  THEN  Auto)\mcdot{}
  ))

---

Home Index