---

Step * 1 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
7. loc(e') = loc(e) ∈ Id
⊢ uiff(↑e' = e;(e' = e ∈ E) ∨ ((¬(loc(e') = loc(e) ∈ Id)) ∧ (↑first(e'))))
BY
{ (AutoBoolCase ⌈e' = e⌉⋅ THEN Auto THEN Try ((OrLeft THEN Auto)) THEN D -1 THEN Auto)⋅ }

---

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


By

(AutoBoolCase  \mkleeneopen{}e'  =  e\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Try  ((OrLeft  THEN  Auto))  THEN  D  -1  THEN  Auto)\mcdot{}

---

Home Index