---

Step * of Lemma thread-messages_wf

∀[s:SES]. ∀[es:EO+(Info)]. ∀[thr:E List].  (thread-messages(thr) ∈ {e:E| (↑e ∈b Send) ∨ (↑e ∈b Rcv)}  List)
BY
{ (Auto THEN Unfold `thread-messages` 0 THEN Unfold `ses-msg` 0) }

1
1. s : SES
2. es : EO+(Info)
3. thr : E List
⊢ filter(λe.(e ∈b Send ∨be ∈b Rcv);thr) ∈ {e:E| (↑e ∈b Send) ∨ (↑e ∈b Rcv)}  List

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[es:EO+(Info)].  \mforall{}[thr:E  List].
    (thread-messages(thr)  \mmember{}  \{e:E|  (\muparrow{}e  \mmember{}\msubb{}  Send)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  Rcv)\}    List)


By

---

Latex:
(Auto  THEN  Unfold  `thread-messages`  0  THEN  Unfold  `ses-msg`  0)

---

Home Index