---

Step * 2 3 1 of Lemma rel-path-between-cons


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

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  THEN  All  Reduce)  THEN  Auto')

---

Home Index