---

Step * 2 of Lemma eo-forward-forward


1. Info : Type
2. eo : EO+(Info)
3. e1 : E
4. e2 : E
5. e1 ≤loc e2 
6. (λe.(((eo."dom" e) ∧b (e1 ≤loc e ∨b(¬bloc(e) = loc(e1)))) ∧b (e2 ≤loc e ∨b(¬bloc(e) = loc(e2)))))
= (λe.((eo."dom" e) ∧b (e2 ≤loc e ∨b(¬bloc(e) = loc(e2)))))
∈ (es-base-E(eo) ─→ 𝔹)
⊢ eo.e1.e2 = eo.e2 ∈ EO+(Info)
BY
{ ((All (\h. RepUR ``eo-forward eo-restrict`` h)⋅ THEN (RWO "record-update-update" 0 THENA Auto))
   THEN HypSubst (-1) 0
   THEN (Fold `eo-reset-dom` 0 THEN Auto)⋅)⋅ }

---

Latex:



1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e1  \mleq{}loc  e2 
6.  (\mlambda{}e.(((eo."dom"  e)  \mwedge{}\msubb{}  (e1  \mleq{}loc  e  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e)  =  loc(e1))))  \mwedge{}\msubb{}  (e2  \mleq{}loc  e  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e)  =  loc(e2)))))
=  (\mlambda{}e.((eo."dom"  e)  \mwedge{}\msubb{}  (e2  \mleq{}loc  e  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e)  =  loc(e2)))))
\mvdash{}  eo.e1.e2  =  eo.e2


By

((All  (\mbackslash{}h.  RepUR  ``eo-forward  eo-restrict``  h)\mcdot{}  THEN  (RWO  "record-update-update"  0  THENA  Auto))
  THEN  HypSubst  (-1)  0
  THEN  (Fold  `eo-reset-dom`  0  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index