---

Step * 1 1 1 1 of Lemma assert-es-ble-base


1. es : EO@i'
2. e : es-base-E(es)@i
3. e' : es-base-E(es)@i
4. ∀[e:es-base-E(es)]. (loc(e) ∈ Id)
5. (e < e') ∈ ℙ
6. es-locless(es;e;e') ∈ 𝔹
7. e = e' ∈ 𝔹
⊢ ((↑es-locless(es;e;e')) ∧ (loc(e) = loc(e') ∈ Id)) ∨ (e = e' ∈ es-base-E(es))
⇐⇒ ((loc(e) = loc(e') ∈ Id) ∧ (e < e')) ∨ (e = e' ∈ es-base-E(es))
BY
{ (Decide ⌈loc(e) = loc(e') ∈ Id⌉⋅ THEN Auto THEN SplitOrHyps THEN Auto) }

1
1. es : EO@i'
2. e : es-base-E(es)@i
3. e' : es-base-E(es)@i
4. ∀[e:es-base-E(es)]. (loc(e) ∈ Id)
5. (e < e') ∈ ℙ
6. es-locless(es;e;e') ∈ 𝔹
7. e = e' ∈ 𝔹
8. loc(e) = loc(e') ∈ Id
9. ↑es-locless(es;e;e')@i
10. loc(e) = loc(e') ∈ Id@i
⊢ ((loc(e) = loc(e') ∈ Id) ∧ (e < e')) ∨ (e = e' ∈ es-base-E(es))

2
1. es : EO@i'
2. e : es-base-E(es)@i
3. e' : es-base-E(es)@i
4. ∀[e:es-base-E(es)]. (loc(e) ∈ Id)
5. (e < e') ∈ ℙ
6. es-locless(es;e;e') ∈ 𝔹
7. e = e' ∈ 𝔹
8. loc(e) = loc(e') ∈ Id
9. loc(e) = loc(e') ∈ Id@i
10. (e < e')@i
⊢ ((↑es-locless(es;e;e')) ∧ (loc(e) = loc(e') ∈ Id)) ∨ (e = e' ∈ es-base-E(es))

---

Latex:



1.  es  :  EO@i'
2.  e  :  es-base-E(es)@i
3.  e'  :  es-base-E(es)@i
4.  \mforall{}[e:es-base-E(es)].  (loc(e)  \mmember{}  Id)
5.  (e  <  e')  \mmember{}  \mBbbP{}
6.  es-locless(es;e;e')  \mmember{}  \mBbbB{}
7.  e  =  e'  \mmember{}  \mBbbB{}
\mvdash{}  ((\muparrow{}es-locless(es;e;e'))  \mwedge{}  (loc(e)  =  loc(e')))  \mvee{}  (e  =  e')
\mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  loc(e'))  \mwedge{}  (e  <  e'))  \mvee{}  (e  =  e')


By

(Decide  \mkleeneopen{}loc(e)  =  loc(e')\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  SplitOrHyps  THEN  Auto)

---

Home Index