---

Step * 1 of Lemma until-classrel

.....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'))
BY
{ (Auto
   THEN Auto
   THEN All (RepUR ``classrel until-class``)
   THEN Try ((Unhide THEN Auto))
   THEN (InstLemma  `class-pred-cases` [⌈Info⌉;⌈B⌉;⌈Y⌉;⌈es⌉;⌈e⌉]⋅ THENA Auto)
   THEN D -1
   THEN ExRepD) }

1
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 ↓∈ case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e@i
10. ∃e'<e.((↓∃v:B. v ∈ Y(e')) ∧ ∀e''<e.(↓∃v:B. v ∈ Y(e'')) ⇒ e'' ≤loc e' )
∧ (class-pred(Y;es;e) = (inl e') ∈ (E + Top))
⊢ v ↓∈ X es 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 ↓∈ case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e@i
10. ∀e'<e.∀v:B. (¬v ∈ Y(e'))
11. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
⊢ v ↓∈ X es e

3
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 ↓∈ case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e@i
10. ∃e'<e.((↓∃v:B. v ∈ Y(e')) ∧ ∀e''<e.(↓∃v:B. v ∈ Y(e'')) ⇒ e'' ≤loc e' )
∧ (class-pred(Y;es;e) = (inl e') ∈ (E + Top))
⊢ ∀e'<e.∀w:B. (¬w ↓∈ Y es e')

4
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 ↓∈ case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e@i
10. ∀e'<e.∀v:B. (¬v ∈ Y(e'))
11. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
⊢ ∀e'<e.∀w:B. (¬w ↓∈ Y es e')

5
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 es e@i
10. ∀e'<e.∀w:B. (¬w ↓∈ Y es e')@i
11. ∃e'<e.((↓∃v:B. v ∈ Y(e')) ∧ ∀e''<e.(↓∃v:B. v ∈ Y(e'')) ⇒ e'' ≤loc e' )
∧ (class-pred(Y;es;e) = (inl e') ∈ (E + Top))
⊢ v ↓∈ case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e

6
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 es e@i
10. ∀e'<e.∀w:B. (¬w ↓∈ Y es e')@i
11. ∀e'<e.∀v:B. (¬v ∈ Y(e'))
12. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
⊢ v ↓∈ case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e

---

Latex:

---

Latex:
.....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
\mvdash{}  v  \mmember{}  (X  until  Y)(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(e)  \mwedge{}  \mforall{}e'<e.\mforall{}w:B.  (\mneg{}w  \mmember{}  Y(e'))


By

---

Latex:
(Auto
  THEN  Auto
  THEN  All  (RepUR  ``classrel  until-class``)
  THEN  Try  ((Unhide  THEN  Auto))
  THEN  (InstLemma    `class-pred-cases`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index