---

Step * 1 of Lemma eo-strict-forward-E-subtype2

.....subterm..... T:t
1:n
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : {e':E| (loc(e') = loc(e) ∈ Id) ⇒ (e <loc e')} @i
⊢ x ∈ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e <loc e@0 ∨b(¬bloc(e@0) = loc(e))))} 
BY
{ (D (-1)
   THEN (Assert x ∈ es-base-E(eo) BY
               ((D (-2) THEN Fold `es-base-E` (-3)) THEN Auto))
   THEN (Assert ↑(es-dom(eo) x) BY
               (DVar `x' THEN All (Fold `es-dom`) THEN Auto))
   THEN MemTypeCD
   THEN Try (Trivial)) }

1
.....set predicate..... 
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : E@i
5. (loc(x) = loc(e) ∈ Id) ⇒ (e <loc x)@i
6. x ∈ es-base-E(eo)
7. ↑(es-dom(eo) x)
⊢ ↑((es-dom(eo) x) ∧b (e <loc x ∨b(¬bloc(x) = loc(e))))

2
.....wf..... 
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : E@i
5. (loc(x) = loc(e) ∈ Id) ⇒ (e <loc x)@i
6. x ∈ es-base-E(eo)
7. ↑(es-dom(eo) x)
8. e@0 : es-base-E(eo)
⊢ ↑((es-dom(eo) e@0) ∧b (e <loc e@0 ∨b(¬bloc(e@0) = loc(e)))) ∈ Type

---

Latex:


.....subterm.....  T:t
1:n
1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  x  :  \{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  (e  <loc  e')\}  @i
\mvdash{}  x  \mmember{}  \{e@0:es-base-E(eo)|  \muparrow{}((es-dom(eo)  e@0)  \mwedge{}\msubb{}  (e  <loc  e@0  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e@0)  =  loc(e))))\} 


By

(D  (-1)
  THEN  (Assert  x  \mmember{}  es-base-E(eo)  BY
                          ((D  (-2)  THEN  Fold  `es-base-E`  (-3))  THEN  Auto))
  THEN  (Assert  \muparrow{}(es-dom(eo)  x)  BY
                          (DVar  `x'  THEN  All  (Fold  `es-dom`)  THEN  Auto))
  THEN  MemTypeCD
  THEN  Try  (Trivial))

---

Home Index