---

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

.....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)) ∈ 𝔹
BY
{ ((InstLemma `es-loc-wf-base` [⌈es⌉;⌈e1⌉]⋅ THENA Auto)
   THEN (InstLemma `es-loc-wf-base` [⌈es⌉;⌈e2⌉]⋅ THENA Auto)
   THEN ((InstLemma `es-locless-wf-base` [⌈es⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
         THEN InstLemma `es-locless-wf-base` [⌈es⌉;⌈e2⌉;⌈e1⌉]⋅
         THEN Auto)⋅) }

---

Latex:


.....subterm.....  T:t
1:n
1.  es  :  EO
2.  e1  :  es-base-E(es)@i
3.  e2  :  es-base-E(es)@i
\mvdash{}  loc(e1)  =  loc(e2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e1;e2))  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e2;e1))  \mmember{}  \mBbbB{}


By

((InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index