---

Step * 1 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) ∨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)
BY
{ (RW assert_pushdownC (-1) 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.  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{}((NameDeq  hdr  header(e))  \mvee{}\msubb{}ff)  \mvee{}\msubb{}header(e)  \mmember{}\msubb{}  l2)))
22.  t  :  \{a:E|  loc(a)  =  loc(e)\}  @i'
23.  \mneg{}(header(t)  \mmember{}  l1)
24.  \muparrow{}((NameDeq  hdr  header(t))  \mvee{}\msubb{}ff)@i
\mvdash{}  (header(t)  \mmember{}  l1)  \mvee{}  ((hdr  =  header(t))  \mvee{}  False)  \mvee{}  (header(t)  \mmember{}  l2)


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index