---

Step * 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)
5. i : ℕ||L||
⊢ L[i]
BY
{ (Assert ∀n:ℕ. (n < ||L|| ⇒ L[n]) BY
         (InductionOnNat THEN Auto)) }

1
.....aux..... 
1. L : ℙ List+
2. ∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])
3. last(L) ⇒ hd(L)
4. hd(L)
5. i : ℕ||L||
6. 0 < ||L||
⊢ L[0]

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

3
1. L : ℙ List+
2. ∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])
3. last(L) ⇒ hd(L)
4. hd(L)
5. i : ℕ||L||
6. ∀n:ℕ. (n < ||L|| ⇒ L[n])
⊢ L[i]

---

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)
5.  i  :  \mBbbN{}||L||
\mvdash{}  L[i]


By

---

Latex:
(Assert  \mforall{}n:\mBbbN{}.  (n  <  ||L||  {}\mRightarrow{}  L[n])  BY
              (InductionOnNat  THEN  Auto))

---

Home Index