---

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


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. l1 : Name List
9. l2 : Name List
10. hdrs = (l1 @ [hdr] @ l2) ∈ (Name List)
11. e : E@i'
12. bg : bag(E)
13. bag-no-repeats(E;bg)
14. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
15. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
16. sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
17. ∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' )))
18. bag-no-repeats(E;bg)
19. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
20. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
21. (λe.header(e) ∈b l1 @ [hdr] @ l2)) = (λe.(header(e) ∈b l1) ∨bheader(e) ∈b [hdr]) ∨bheader(e) ∈b l2))) ∈ (E ─→ 𝔹)
⊢ sub-bag(Id × Message(f);mapfilter(λe.<loc(e), info(e)>;λe.header(e) ∈b [hdr]);≤loc(e));mapfilter(λe.<loc(e), info(e)>;
                                                                                                   λe.(header(e) ∈b l1)
                                                                                                      ∨bheader(e) ∈b 
                                                                                                          [hdr])
                                                                                                      ∨bheader(e) ∈b 
                                                                                                          l2));
                                                                                                   ≤loc(e)))
BY
{ ((BLemma `mapfilter-subbag` THEN Auto) THEN (All Reduce THEN AutoBoolCase ⌈header(t) ∈b l1)⌉⋅))⋅ }

1
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. l1 : Name List
9. l2 : Name List
10. hdrs = (l1 @ [hdr / l2]) ∈ (Name List)
11. e : E@i'
12. bg : bag(E)
13. bag-no-repeats(E;bg)
14. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
15. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
16. sub-bag(Id × Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
17. ∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' )))
18. bag-no-repeats(E;bg)
19. ∀e1,e2:E.  (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2)))
20. ∀e':E. (e' ↓∈ bg ⇒ (e' < e))
21. (λe.header(e) ∈b l1 @ [hdr / l2]))
= (λe.(header(e) ∈b l1) ∨b((NameDeq hdr header(e)) ∨bff) ∨bheader(e) ∈b l2)))
∈ (E ─→ 𝔹)
22. t : {a:E| loc(a) = loc(e) ∈ Id} @i'
23. ¬(header(t) ∈ l1)
24. ↑((NameDeq hdr header(t)) ∨bff)@i
⊢ (header(t) ∈ l1) ∨ ((hdr = header(t) ∈ Name) ∨ False) ∨ (header(t) ∈ l2)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  es  :  EO+(Message(f))
3.  X  :  EClass(Id  \mtimes{}  Message(f))
4.  hdrs  :  Name  List
5.  no\_repeats(Name;hdrs)@i
6.  \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'
7.  hdr  :  Name@i
8.  l1  :  Name  List
9.  l2  :  Name  List
10.  hdrs  =  (l1  @  [hdr]  @  l2)
11.  e  :  E@i'
12.  bg  :  bag(E)
13.  bag-no-repeats(E;bg)
14.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
15.  \mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e))
16.  sub-bag(Id  \mtimes{}  Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
17.  \mforall{}e':E.  ((e'  <  e)  {}\mRightarrow{}  (\mexists{}e'':E.  (e''  \mdownarrow{}\mmember{}  bg  \mwedge{}  e'  \mleq{}loc  e''  )))
18.  bag-no-repeats(E;bg)
19.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
20.  \mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e))
21.  (\mlambda{}e.header(e)  \mmember{}\msubb{}  l1  @  [hdr]  @  l2))
=  (\mlambda{}e.(header(e)  \mmember{}\msubb{}  l1)  \mvee{}\msubb{}header(e)  \mmember{}\msubb{}  [hdr])  \mvee{}\msubb{}header(e)  \mmember{}\msubb{}  l2)))
\mvdash{}  sub-bag(Id  \mtimes{}  Message(f);mapfilter(\mlambda{}e.<loc(e),  info(e)>
                                                                        \mlambda{}e.header(e)  \mmember{}\msubb{}  [hdr]);
                                                                        \mleq{}loc(e));mapfilter(\mlambda{}e.<loc(e),  info(e)>
                                                                                                              \mlambda{}e.(header(e)  \mmember{}\msubb{}  l1)
                                                                                                                    \mvee{}\msubb{}header(e)  \mmember{}\msubb{}  [hdr])
                                                                                                                    \mvee{}\msubb{}header(e)  \mmember{}\msubb{}  l2));
                                                                                                              \mleq{}loc(e)))


By

---

Latex:
((BLemma  `mapfilter-subbag`  THEN  Auto)  THEN  (All  Reduce  THEN  AutoBoolCase  \mkleeneopen{}header(t)  \mmember{}\msubb{}  l1)\mkleeneclose{}\mcdot{}))\mcdot{}

---

Home Index