---

Step * 1 2 of Lemma assert-eo-forward-first


1. [Info] : Type
2. eo : EO+(Info)@i'
3. e : E@i
4. e' : E@i
5. first(e') ~ if loc(e') = loc(e) then e' = e else first(e') fi 
6. E ⊆r E
7. ¬(loc(e') = loc(e) ∈ Id)
⊢ uiff(↑first(e');(e' = e ∈ E) ∨ ((¬(loc(e') = loc(e) ∈ Id)) ∧ (↑first(e'))))
BY
{ (SplitOnHypITE -3  THEN Auto THEN Try ((OrRight THEN Auto)) THEN D (-1) THEN Auto) }

1
1. Info : Type
2. eo : EO+(Info)@i'
3. e : E@i
4. e' : E@i
5. first(e') ~ first(e')
6. E ⊆r E
7. ¬(loc(e') = loc(e) ∈ Id)
8. ¬(loc(e') = loc(e) ∈ Id)
9. e' = e ∈ E
⊢ ↑first(e')

---

Latex:



1.  [Info]  :  Type
2.  eo  :  EO+(Info)@i'
3.  e  :  E@i
4.  e'  :  E@i
5.  first(e')  \msim{}  if  loc(e')  =  loc(e)  then  e'  =  e  else  first(e')  fi 
6.  E  \msubseteq{}r  E
7.  \mneg{}(loc(e')  =  loc(e))
\mvdash{}  uiff(\muparrow{}first(e');(e'  =  e)  \mvee{}  ((\mneg{}(loc(e')  =  loc(e)))  \mwedge{}  (\muparrow{}first(e'))))


By

(SplitOnHypITE  -3    THEN  Auto  THEN  Try  ((OrRight  THEN  Auto))  THEN  D  (-1)  THEN  Auto)

---

Home Index