---

Step * 1 1 of Lemma es-eq-wf-base


1. es : EO
⊢ λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1))) ∈ es-base-E(es) ─→ es-base-E(es) ─\000C→ 𝔹
BY
{ RepeatFor 2 ((MemCD THENA Auto)) }

1
.....subterm..... T:t
1:n
1. es : EO
2. e1 : es-base-E(es)@i
3. e2 : es-base-E(es)@i
⊢ loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1)) ∈ 𝔹

---

Latex:



1.  es  :  EO
\mvdash{}  \mlambda{}e1,e2.  (loc(e1)  =  loc(e2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e1;e2))  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e2;e1)))  \mmember{}  es-base-E(es\000C)
    {}\mrightarrow{}  es-base-E(es)
    {}\mrightarrow{}  \mBbbB{}


By

RepeatFor  2  ((MemCD  THENA  Auto))

---

Home Index