---

Step * 1 2 1 1 of Lemma implies-equiv-props

.....aux..... 
1. L : ℙ List+
2. ∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])
3. last(L) ⇒ hd(L)
4. hd(L) ⇒ (∀i:ℕ||L||. L[i])
5. last(L) ⇒ (∀i:ℕ||L||. L[i])
6. j : ℤ
7. [%5] : 0 < j
8. j - 1 < ||L|| ⇒ L[||L|| - (j - 1) + 1] ⇒ last(L)
9. j < ||L||
10. L[||L|| - j + 1]
⊢ last(L)
BY
{ (D -3 THENA Auto) }

1
1. L : ℙ List+
2. ∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])
3. last(L) ⇒ hd(L)
4. hd(L) ⇒ (∀i:ℕ||L||. L[i])
5. last(L) ⇒ (∀i:ℕ||L||. L[i])
6. j : ℤ
7. [%5] : 0 < j
8. j < ||L||
9. L[||L|| - j + 1]
10. L[||L|| - (j - 1) + 1] ⇒ last(L)
⊢ last(L)

---

Latex:

---

Latex:
.....aux..... 
1.  L  :  \mBbbP{}  List\msupplus{}
2.  \mforall{}i:\mBbbN{}||L||  -  1.  (L[i]  {}\mRightarrow{}  L[i  +  1])
3.  last(L)  {}\mRightarrow{}  hd(L)
4.  hd(L)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||L||.  L[i])
5.  last(L)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||L||.  L[i])
6.  j  :  \mBbbZ{}
7.  [\%5]  :  0  <  j
8.  j  -  1  <  ||L||  {}\mRightarrow{}  L[||L||  -  (j  -  1)  +  1]  {}\mRightarrow{}  last(L)
9.  j  <  ||L||
10.  L[||L||  -  j  +  1]
\mvdash{}  last(L)


By

---

Latex:
(D  -3  THENA  Auto)

---

Home Index