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

.....aux..... 
1. : ℙ List+
2. ∀i:ℕ||L|| 1. (L[i]  L[i 1])
3. last(L)  hd(L)
4. hd(L)
5. : ℕ||L||
6. 0 < ||L||
⊢ L[0]
BY
(Subst' L[0] hd(L) THEN Auto) }


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||
6.  0  <  ||L||
\mvdash{}  L[0]


By


Latex:
(Subst'  L[0]  \msim{}  hd(L)  0  THEN  Auto)




Home Index