Step
*
2
4
of Lemma
rel-path-between-cons
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. L : T List
4. ¬(L = [] ∈ (T List))
5. x : T
6. y : T
7. z : T
8. x = z ∈ T
9. y = z ∈ T supposing False
10. (x R hd(L)) ∧ rel-path(R;L) ∧ 0 < ||L|| ∧ (hd(L) = hd(L) ∈ T) ∧ (y = last(L) ∈ T) supposing ¬False
⊢ y = 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