---

Step * 1 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
⊢ uiff(↑if loc(e') = loc(e) then e' = e else first(e') fi ;(e' = e ∈ E) ∨ ((¬(loc(e') = loc(e) ∈ Id)) ∧ (↑first(e'))))
BY
{ OldAutoSplit }

1
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(↑e' = e;(e' = e ∈ E) ∨ ((¬(loc(e') = loc(e) ∈ Id)) ∧ (↑first(e'))))

2
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'))))

---

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
\mvdash{}  uiff(\muparrow{}if  loc(e')  =  loc(e)  then  e'  =  e  else  first(e')  fi  ;(e'  =  e)
\mvee{}  ((\mneg{}(loc(e')  =  loc(e)))  \mwedge{}  (\muparrow{}first(e'))))


By

OldAutoSplit

---

Home Index