---

Step * 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))
@ 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'))
BY
{ (Reduce (-2) THEN Try (Fold `bag-append` (-2)) THEN (FLemma `sub-bag-append-left2` [-2] THENA 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))
+ [<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'))

---

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))
@  map(\mlambda{}e.<loc(e),  info(e)>if  tt  then  [e]  else  []  fi  );class-output(X;es;bg))
13.  \mforall{}e':E.  ((e'  <  e)  {}\mRightarrow{}  (\mexists{}e'':E.  (e''  \mdownarrow{}\mmember{}  bg  \mwedge{}  e'  \mleq{}loc  e''  )))
\mvdash{}  \mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  <loc(e),  info(e)>  \mmember{}  X(e'))


By

---

Latex:
(Reduce  (-2)  THEN  Try  (Fold  `bag-append`  (-2))  THEN  (FLemma  `sub-bag-append-left2`  [-2]  THENA  Auto))

---

Home Index