---

Step * 1 1 1 2 2 of Lemma firstn-before


1. the_es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ (∀n:ℕ. (n < ||before(e1)|| ⇒ (firstn(n;before(e1)) ~ before(before(e1)[n])))))
4. n : ℕ@i
5. ¬↑first(e)
6. n < ||before(pred(e))|| + 1@i
7. ∀n:ℕ. (n < ||before(pred(e))|| ⇒ (firstn(n;before(pred(e))) ~ before(before(pred(e))[n])))
8. ||before(pred(e))|| ≤ n
⊢ pred(e) ~ [pred(e)][n - ||before(pred(e))||]
BY
{ Subst ⌈n - ||before(pred(e))|| ~ 0⌉ 0⋅ }

1
.....equality..... 
1. the_es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ (∀n:ℕ. (n < ||before(e1)|| ⇒ (firstn(n;before(e1)) ~ before(before(e1)[n])))))
4. n : ℕ@i
5. ¬↑first(e)
6. n < ||before(pred(e))|| + 1@i
7. ∀n:ℕ. (n < ||before(pred(e))|| ⇒ (firstn(n;before(pred(e))) ~ before(before(pred(e))[n])))
8. ||before(pred(e))|| ≤ n
⊢ n - ||before(pred(e))|| ~ 0

2
1. the_es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e) ⇒ (∀n:ℕ. (n < ||before(e1)|| ⇒ (firstn(n;before(e1)) ~ before(before(e1)[n])))))
4. n : ℕ@i
5. ¬↑first(e)
6. n < ||before(pred(e))|| + 1@i
7. ∀n:ℕ. (n < ||before(pred(e))|| ⇒ (firstn(n;before(pred(e))) ~ before(before(pred(e))[n])))
8. ||before(pred(e))|| ≤ n
⊢ pred(e) ~ [pred(e)][0]

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  \mforall{}e1:E
          ((e1  <  e)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (n  <  ||before(e1)||  {}\mRightarrow{}  (firstn(n;before(e1))  \msim{}  before(before(e1)[n])))))
4.  n  :  \mBbbN{}@i
5.  \mneg{}\muparrow{}first(e)
6.  n  <  ||before(pred(e))||  +  1@i
7.  \mforall{}n:\mBbbN{}.  (n  <  ||before(pred(e))||  {}\mRightarrow{}  (firstn(n;before(pred(e)))  \msim{}  before(before(pred(e))[n])))
8.  ||before(pred(e))||  \mleq{}  n
\mvdash{}  pred(e)  \msim{}  [pred(e)][n  -  ||before(pred(e))||]


By

Subst  \mkleeneopen{}n  -  ||before(pred(e))||  \msim{}  0\mkleeneclose{}  0\mcdot{}

---

Home Index