---

Step * 2 3 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
⊢ rel-path(R;[z / L])
BY
{ DVar `L' }

1
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])

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. u : T
4. v : T List
5. ¬([u / v] = [] ∈ (T List))
6. x : T
7. y : T
8. z : T
9. x = z ∈ T
10. y = z ∈ T supposing False
11. (x R hd([u / v]))
    ∧ rel-path(R;[u / v])
    ∧ 0 < ||[u / v]||
    ∧ (hd([u / v]) = hd([u / v]) ∈ T)
    ∧ (y = last([u / v]) ∈ T) 
    supposing ¬False
⊢ rel-path(R;[z; [u / v]])

---

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{}  rel-path(R;[z  /  L])


By

---

Latex:
DVar  `L'

---

Home Index