---

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


1. es : EO
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
⊢ x = y ∈ es-base-E(es) ⇐⇒ ↑(loc(x) = loc(y) ∧b (¬bes-locless(es;x;y)) ∧b (¬bes-locless(es;y;x)))
BY
{ ((InstLemma `es-loc-wf-base` [⌈es⌉;⌈x⌉]⋅ THENA Auto)
   THEN (InstLemma `es-loc-wf-base` [⌈es⌉;⌈y⌉]⋅ THENA Auto)
   THEN ((InstLemma `es-locless-wf-base` [⌈es⌉;⌈x⌉;⌈y⌉]⋅ THENA Auto)
         THEN InstLemma `es-locless-wf-base` [⌈es⌉;⌈y⌉;⌈x⌉]⋅
         THEN Auto)⋅)⋅ }

1
1. es : EO
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
4. loc(x) ∈ Id
5. loc(y) ∈ Id
6. es-locless(es;x;y) ∈ 𝔹
7. es-locless(es;y;x) ∈ 𝔹
8. x = y ∈ es-base-E(es)@i
⊢ loc(x) = loc(y) ∈ Id

2
1. es : EO
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
4. loc(x) ∈ Id
5. loc(y) ∈ Id
6. es-locless(es;x;y) ∈ 𝔹
7. es-locless(es;y;x) ∈ 𝔹
8. x = y ∈ es-base-E(es)@i
9. loc(x) = loc(y) ∈ Id
⊢ ¬↑es-locless(es;x;y)

3
1. es : EO
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
4. loc(x) ∈ Id
5. loc(y) ∈ Id
6. es-locless(es;x;y) ∈ 𝔹
7. es-locless(es;y;x) ∈ 𝔹
8. x = y ∈ es-base-E(es)@i
9. loc(x) = loc(y) ∈ Id
10. ¬↑es-locless(es;x;y)
⊢ ¬↑es-locless(es;y;x)

4
1. es : EO
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
4. loc(x) ∈ Id
5. loc(y) ∈ Id
6. es-locless(es;x;y) ∈ 𝔹
7. es-locless(es;y;x) ∈ 𝔹
8. ↑(loc(x) = loc(y) ∧b (¬bes-locless(es;x;y)) ∧b (¬bes-locless(es;y;x)))@i
⊢ x = y ∈ es-base-E(es)

---

Latex:



1.  es  :  EO
2.  x  :  es-base-E(es)@i
3.  y  :  es-base-E(es)@i
\mvdash{}  x  =  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(loc(x)  =  loc(y)  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;x;y))  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;y;x)))


By

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

---

Home Index