---

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


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))
+ [<loc(e), info(e)>];class-output(X;es;bg))
13. ∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' )))
14. sub-bag(Id × Message(f);[<loc(e), info(e)>];class-output(X;es;bg))
⊢ ↓∃e':E. ((e' < e) ∧ <loc(e), info(e)> ∈ X(e'))
BY
{ (Try (Fold `single-bag` (-1))
   THEN (FLemma `sub-bag-singleton-left` [-1] THENA Auto)
   THEN RepeatFor 2 ((BagMemberD (-1) THEN SquashExRepD))
   THEN (InstHyp [⌈e1⌉] (-9)⋅ THENA Auto)
   THEN D 0
   THEN InstConcl [⌈e'⌉]⋅
   THEN Auto) }

---

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)
                (bag-no-repeats(E;bg)
                \mwedge{}  (\mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2))))
                \mwedge{}  (\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))
                \mwedge{}  (\mforall{}e':E.  ((e'  <  e)  {}\mRightarrow{}  (\mexists{}e'':E.  (e''  \mdownarrow{}\mmember{}  bg  \mwedge{}  e'  \mleq{}loc  e''  ))))))@i'
6.  e  :  E@i'
7.  (header(e)  \mmember{}  hdrs)@i
8.  bg  :  bag(E)
9.  bag-no-repeats(E;bg)
10.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
11.  \mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e))
12.  sub-bag(Id  \mtimes{}  Message(f);mapfilter(\mlambda{}e.<loc(e),  info(e)>\mlambda{}e.header(e)  \mmember{}\msubb{}  hdrs);before(e))
+  [<loc(e),  info(e)>];class-output(X;es;bg))
13.  \mforall{}e':E.  ((e'  <  e)  {}\mRightarrow{}  (\mexists{}e'':E.  (e''  \mdownarrow{}\mmember{}  bg  \mwedge{}  e'  \mleq{}loc  e''  )))
14.  sub-bag(Id  \mtimes{}  Message(f);[<loc(e),  info(e)>];class-output(X;es;bg))
\mvdash{}  \mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  <loc(e),  info(e)>  \mmember{}  X(e'))


By

---

Latex:
(Try  (Fold  `single-bag`  (-1))
  THEN  (FLemma  `sub-bag-singleton-left`  [-1]  THENA  Auto)
  THEN  RepeatFor  2  ((BagMemberD  (-1)  THEN  SquashExRepD))
  THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-9)\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index