---

Step * of Lemma until-classrel

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
  (v ∈ (X until Y)(e) ⇐⇒ (no Y prior to e) ∧ v ∈ X(e))
BY
{ (Unfold `no-prior-classrel` 0
   THEN ((UnivCD THENA Auto) THEN Assert ⌜v ∈ (X until Y)(e) ⇐⇒ v ∈ X(e) ∧ ∀e'<e.∀w:B. (¬w ∈ Y(e'))⌝⋅)
   ) }

1
.....assertion..... 
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. es : EO+(Info)
7. e : E
8. v : A
⊢ v ∈ (X until Y)(e) ⇐⇒ v ∈ X(e) ∧ ∀e'<e.∀w:B. (¬w ∈ Y(e'))

2
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. es : EO+(Info)
7. e : E
8. v : A
9. v ∈ (X until Y)(e) ⇐⇒ v ∈ X(e) ∧ ∀e'<e.∀w:B. (¬w ∈ Y(e'))
⊢ v ∈ (X until Y)(e) ⇐⇒ ∀e'<e.∀w:B. (¬w ∈ Y(e')) ∧ v ∈ X(e)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:A].
    (v  \mmember{}  (X  until  Y)(e)  \mLeftarrow{}{}\mRightarrow{}  (no  Y  prior  to  e)  \mwedge{}  v  \mmember{}  X(e))


By

---

Latex:
(Unfold  `no-prior-classrel`  0
  THEN  ((UnivCD  THENA  Auto)
              THEN  Assert  \mkleeneopen{}v  \mmember{}  (X  until  Y)(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(e)  \mwedge{}  \mforall{}e'<e.\mforall{}w:B.  (\mneg{}w  \mmember{}  Y(e'))\mkleeneclose{}\mcdot{}
              )
  )

---

Home Index