---

Step * of Lemma eo-forward-forward

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e1,e2:E].  eo.e1.e2 = eo.e2 ∈ EO+(Info) supposing e1 ≤loc e2 
BY
{ (Auto
   THEN Assert ⌜(λ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) ⟶ 𝔹)⌝⋅
   ) }

1
.....assertion..... 
1. Info : Type
2. eo : EO+(Info)
3. e1 : E
4. e2 : E
5. e1 ≤loc e2 
⊢ (λ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) ⟶ 𝔹)

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

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e1,e2:E].    eo.e1.e2  =  eo.e2  supposing  e1  \mleq{}loc  e2 


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}(\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)))))\mkleeneclose{}\mcdot{}
  )

---

Home Index