---

Step * 1 1 1 of Lemma es-base-pred-less


1. es : EO@i'
2. es-eq(es) ∈ EqDecider(es-base-E(es))
3. e : es-base-E(es)@i
4. ¬↑(es-eq(es) pred1(e) e)@i
5. loc(pred1(e)) = loc(e) ∈ Id
6. ¬(e < pred1(e))
7. ∀x:es-base-E(es). ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x))))
8. ∀x,y:es-base-E(es).
     ((loc(x) = loc(y) ∈ Id)
     ⇒ (((x < y) ⇐⇒ ↑es-locless(es;x;y))
        ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))))
9. es-locless(es;pred1(e);e) ∈ 𝔹
10. es-locless(es;e;pred1(e)) ∈ 𝔹
11. ¬↑es-locless(es;pred1(e);e)
⊢ ↑es-locless(es;pred1(e);e)
BY
{ Assert ⌈pred1(e) = e ∈ es-base-E(es)⌉⋅ }

1
.....assertion..... 
1. es : EO@i'
2. es-eq(es) ∈ EqDecider(es-base-E(es))
3. e : es-base-E(es)@i
4. ¬↑(es-eq(es) pred1(e) e)@i
5. loc(pred1(e)) = loc(e) ∈ Id
6. ¬(e < pred1(e))
7. ∀x:es-base-E(es). ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x))))
8. ∀x,y:es-base-E(es).
     ((loc(x) = loc(y) ∈ Id)
     ⇒ (((x < y) ⇐⇒ ↑es-locless(es;x;y))
        ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))))
9. es-locless(es;pred1(e);e) ∈ 𝔹
10. es-locless(es;e;pred1(e)) ∈ 𝔹
11. ¬↑es-locless(es;pred1(e);e)
⊢ pred1(e) = e ∈ es-base-E(es)

2
1. es : EO@i'
2. es-eq(es) ∈ EqDecider(es-base-E(es))
3. e : es-base-E(es)@i
4. ¬↑(es-eq(es) pred1(e) e)@i
5. loc(pred1(e)) = loc(e) ∈ Id
6. ¬(e < pred1(e))
7. ∀x:es-base-E(es). ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x))))
8. ∀x,y:es-base-E(es).
     ((loc(x) = loc(y) ∈ Id)
     ⇒ (((x < y) ⇐⇒ ↑es-locless(es;x;y))
        ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))))
9. es-locless(es;pred1(e);e) ∈ 𝔹
10. es-locless(es;e;pred1(e)) ∈ 𝔹
11. ¬↑es-locless(es;pred1(e);e)
12. pred1(e) = e ∈ es-base-E(es)
⊢ ↑es-locless(es;pred1(e);e)

---

Latex:



1.  es  :  EO@i'
2.  es-eq(es)  \mmember{}  EqDecider(es-base-E(es))
3.  e  :  es-base-E(es)@i
4.  \mneg{}\muparrow{}(es-eq(es)  pred1(e)  e)@i
5.  loc(pred1(e))  =  loc(e)
6.  \mneg{}(e  <  pred1(e))
7.  \mforall{}x:es-base-E(es).  ((x  <  e)  {}\mRightarrow{}  (loc(x)  =  loc(e))  {}\mRightarrow{}  ((pred1(e)  <  e)  \mwedge{}  (\mneg{}(pred1(e)  <  x))))
8.  \mforall{}x,y:es-base-E(es).
          ((loc(x)  =  loc(y))
          {}\mRightarrow{}  (((x  <  y)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}es-locless(es;x;y))
                \mwedge{}  ((\mneg{}\muparrow{}es-locless(es;x;y))  {}\mRightarrow{}  (\mneg{}\muparrow{}es-locless(es;y;x))  {}\mRightarrow{}  (x  =  y))))
9.  es-locless(es;pred1(e);e)  \mmember{}  \mBbbB{}
10.  es-locless(es;e;pred1(e))  \mmember{}  \mBbbB{}
11.  \mneg{}\muparrow{}es-locless(es;pred1(e);e)
\mvdash{}  \muparrow{}es-locless(es;pred1(e);e)


By

Assert  \mkleeneopen{}pred1(e)  =  e\mkleeneclose{}\mcdot{}

---

Home Index