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