---

Step * of Lemma strong-message-constraint-no-rep-large-implies

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ⇒ message-constraint{i:l}(es;X;hdrs;f))
BY
{ (RepUR ``strong-message-constraint-no-rep-large message-constraint`` 0⋅
   THEN (UnivCD THENA Auto)
   THEN (InstHyp [⌈e⌉] (-3)⋅ THENA Auto)
   THEN SquashExRepD
   THEN RepUR ``delivered-with-headers es-le-before`` (-2)
   THEN (RWO "mapfilter-append" (-2) THENA Auto)
   THEN (RWO "mapfilter-singleton" (-2) THENA Auto)
   THEN Reduce (-2)
   THEN (Subst ⌈header(e) ∈b hdrs) ~ tt⌉ (-2)⋅
         THENA ((Assert ⌈↑header(e) ∈b hdrs)⌉⋅ THENM Auto) THEN RWO "assert-deq-member" 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)
        (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'
6. e : E@i'
7. (header(e) ∈ hdrs)@i
8. bg : bag(E)
9. bag-no-repeats(E;bg)
10. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
11. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
12. sub-bag(Id × Message(f);mapfilter(λe.<loc(e), info(e)>;λe.header(e) ∈b hdrs);before(e))
@ map(λe.<loc(e), info(e)>;if tt then [e] else [] fi );class-output(X;es;bg))
13. ∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' )))
⊢ ↓∃e':E. ((e' < e) ∧ <loc(e), info(e)> ∈ X(e'))

---

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-no-rep-large\{i:l\}(es;X;hdrs;f)  {}\mRightarrow{}  message-constraint\{i:l\}(es;X;hdrs;f))


By

---

Latex:
(RepUR  ``strong-message-constraint-no-rep-large  message-constraint``  0\mcdot{}
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  RepUR  ``delivered-with-headers  es-le-before``  (-2)
  THEN  (RWO  "mapfilter-append"  (-2)  THENA  Auto)
  THEN  (RWO  "mapfilter-singleton"  (-2)  THENA  Auto)
  THEN  Reduce  (-2)
  THEN  (Subst  \mkleeneopen{}header(e)  \mmember{}\msubb{}  hdrs)  \msim{}  tt\mkleeneclose{}  (-2)\mcdot{}
              THENA  ((Assert  \mkleeneopen{}\muparrow{}header(e)  \mmember{}\msubb{}  hdrs)\mkleeneclose{}\mcdot{}  THENM  Auto)  THEN  RWO  "assert-deq-member"  0  THEN  Auto)
              ))

---

Home Index