Step
*
of Lemma
implies-equiv-props
∀L:ℙ List+. ((∀i:ℕ||L|| - 1. (L[i] 
⇒ L[i + 1])) 
⇒ (last(L) 
⇒ hd(L)) 
⇒ equiv-props(L))
BY
{ Auto }
1
1. L : ℙ List+
2. ∀i:ℕ||L|| - 1. (L[i] 
⇒ L[i + 1])
3. last(L) 
⇒ hd(L)
⊢ equiv-props(L)
Latex:
Latex:
\mforall{}L:\mBbbP{}  List\msupplus{}.  ((\mforall{}i:\mBbbN{}||L||  -  1.  (L[i]  {}\mRightarrow{}  L[i  +  1]))  {}\mRightarrow{}  (last(L)  {}\mRightarrow{}  hd(L))  {}\mRightarrow{}  equiv-props(L))
By
Latex:
Auto
Home
Index