---

Step * 2 of Lemma event-has*-iff


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. (e has a)@i
⊢ e has* a
BY
{ ((With ⌈e⌉ (D 0)⋅ THEN Auto) THEN BLemma `rel_star_weakening` THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  a  :  Atom1@i
5.  (e  has  a)@i
\mvdash{}  e  has*  a


By

---

Latex:
((With  \mkleeneopen{}e\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  BLemma  `rel\_star\_weakening`  THEN  Auto)

---

Home Index