---

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


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:ℕ. (j < ||L|| ⇒ L[||L|| - j + 1] ⇒ last(L))
⊢ equiv-props(L)
BY
{ (Assert ∀j:ℕ||L||. (L[j] ⇒ (∀i:ℕ||L||. L[i])) BY
         RepeatFor 2 ((D 0 THENA Auto))) }

1
.....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:ℕ. (j < ||L|| ⇒ L[||L|| - j + 1] ⇒ last(L))
7. j : ℕ||L||
8. L[j]
⊢ ∀i:ℕ||L||. L[i]

2
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:ℕ. (j < ||L|| ⇒ L[||L|| - j + 1] ⇒ last(L))
7. ∀j:ℕ||L||. (L[j] ⇒ (∀i:ℕ||L||. L[i]))
⊢ equiv-props(L)

---

Latex:

---

Latex:

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.  \mforall{}j:\mBbbN{}.  (j  <  ||L||  {}\mRightarrow{}  L[||L||  -  j  +  1]  {}\mRightarrow{}  last(L))
\mvdash{}  equiv-props(L)


By

---

Latex:
(Assert  \mforall{}j:\mBbbN{}||L||.  (L[j]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||L||.  L[i]))  BY
              RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index