---

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

.....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))
BY
{ ((RWO "l_member_decomp" (-11) THENA Auto)
   THEN ExRepD
   THEN (HypSubst' (-11) 0 THENA Auto)
   THEN Unfold `delivered-with-headers` 0
   THEN (Assert ⌈(λe.header(e) ∈b l1 @ [hdr] @ l2))
                 = (λe.(header(e) ∈b l1) ∨bheader(e) ∈b [hdr]) ∨bheader(e) ∈b l2)))
                 ∈ (E ─→ 𝔹)⌉⋅
         THENA (EqCD THEN Auto THEN RepeatFor 2 ((RWO "deq-member-append" 0 THEN Auto)))
         )
   THEN (RWO "-1" 0 THENA Auto)) }

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) ∨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)))

---

Latex:

---

Latex:
.....assertion..... 
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.  (hdr  \mmember{}  hdrs)@i
9.  e  :  E@i'
10.  bg  :  bag(E)
11.  bag-no-repeats(E;bg)
12.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
13.  \mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e))
14.  sub-bag(Id  \mtimes{}  Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))
15.  \mforall{}e':E.  ((e'  <  e)  {}\mRightarrow{}  (\mexists{}e'':E.  (e''  \mdownarrow{}\mmember{}  bg  \mwedge{}  e'  \mleq{}loc  e''  )))
16.  bag-no-repeats(E;bg)
17.  \mforall{}e1,e2:E.    (e1  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  e2  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (\mneg{}(e1  <loc  e2)))
18.  \mforall{}e':E.  (e'  \mdownarrow{}\mmember{}  bg  {}\mRightarrow{}  (e'  <  e))
\mvdash{}  sub-bag(Id  \mtimes{}  Message(f);delivered-with-headers([hdr];es;e);delivered-with-headers(hdrs;es;e))


By

---

Latex:
((RWO  "l\_member\_decomp"  (-11)  THENA  Auto)
  THEN  ExRepD
  THEN  (HypSubst'  (-11)  0  THENA  Auto)
  THEN  Unfold  `delivered-with-headers`  0
  THEN  (Assert  \mkleeneopen{}(\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)))\mkleeneclose{}\mcdot{}
              THENA  (EqCD  THEN  Auto  THEN  RepeatFor  2  ((RWO  "deq-member-append"  0  THEN  Auto)))
              )
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index