---

Step * 1 of Lemma eo-forward-trivial


1. Info : Type
2. eo : EO+(Info)
3. e : E
4. ↑first(e)
5. x : es-base-E(eo)
⊢ (es-dom(eo) x) ∧b (e ≤loc x ∨b(¬bloc(x) = loc(e))) = es-dom(eo) x
BY
{ (AutoBoolCase ⌈es-dom(eo) x⌉⋅ THEN (GenConcl ⌈x = e' ∈ E⌉⋅ THENA Auto)) }

1
.....wf..... 
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. ↑first(e)
5. x : es-base-E(eo)
6. ↑(es-dom(eo) x)
⊢ x ∈ E

2
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. ↑first(e)
5. x : es-base-E(eo)
6. ↑(es-dom(eo) x)
7. e' : E@i
8. x = e' ∈ E@i
⊢ e ≤loc e' ∨b(¬bloc(e') = loc(e)) = tt

---

Latex:



1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  \muparrow{}first(e)
5.  x  :  es-base-E(eo)
\mvdash{}  (es-dom(eo)  x)  \mwedge{}\msubb{}  (e  \mleq{}loc  x  \mvee{}\msubb{}(\mneg{}\msubb{}loc(x)  =  loc(e)))  =  es-dom(eo)  x


By

(AutoBoolCase  \mkleeneopen{}es-dom(eo)  x\mkleeneclose{}\mcdot{}  THEN  (GenConcl  \mkleeneopen{}x  =  e'\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index