Step * 2 4 of Lemma rel-path-between-cons


1. Type
2. T ⟶ T ⟶ ℙ
3. List
4. ¬(L [] ∈ (T List))
5. T
6. T
7. T
8. z ∈ T
9. z ∈ supposing False
10. (x hd(L)) ∧ rel-path(R;L) ∧ 0 < ||L|| ∧ (hd(L) hd(L) ∈ T) ∧ (y last(L) ∈ T) supposing ¬False
⊢ last([z L]) ∈ T
BY
(D -1 THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  L  :  T  List
4.  \mneg{}(L  =  [])
5.  x  :  T
6.  y  :  T
7.  z  :  T
8.  x  =  z
9.  y  =  z  supposing  False
10.  (x  R  hd(L))  \mwedge{}  rel-path(R;L)  \mwedge{}  0  <  ||L||  \mwedge{}  (hd(L)  =  hd(L))  \mwedge{}  (y  =  last(L))  supposing  \mneg{}False
\mvdash{}  y  =  last([z  /  L])


By


Latex:
(D  -1  THEN  Auto)




Home Index