---

Step * of Lemma es-eq-wf-base

∀[es:EO]. (es-eq(es) ∈ EqDecider(es-base-E(es)))
BY
{ ProveWfLemma }

1
1. es : EO
⊢ λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1))) ∈ EqDecider(es-base-E(es))

---

Latex:

---

Latex:
\mforall{}[es:EO].  (es-eq(es)  \mmember{}  EqDecider(es-base-E(es)))


By

---

Latex:
ProveWfLemma

---

Home Index