---

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


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])
12. rel-path(R;[u / v])
13. 0 < ||[u / v]||
14. hd([u / v]) = hd([u / v]) ∈ T
15. y = last([u / v]) ∈ T
⊢ rel-path(R;[z; [u / v]])
BY
{ OnMaybeHyp 11 (\h. (ParallelOp h THEN (All Reduce THEN Auto) THEN CaseNat 0 `i' THEN Reduce 0))⋅ }

1
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 u
12. ∀i:ℕ(||v|| + 1) - 1. ([u / v][i] R [u / v][i + 1])
13. 0 < ||v|| + 1
14. u = u ∈ T
15. y = last([u / v]) ∈ T
16. i : ℕ((||v|| + 1) + 1) - 1
17. i = 0 ∈ ℤ
⊢ z R u

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 u
12. ∀i:ℕ(||v|| + 1) - 1. ([u / v][i] R [u / v][i + 1])
13. 0 < ||v|| + 1
14. u = u ∈ T
15. y = last([u / v]) ∈ T
16. i : ℕ((||v|| + 1) + 1) - 1
17. ¬(i = 0 ∈ ℤ)
⊢ [z; [u / v]][i] R [z; [u / v]][i + 1]

---

Latex:

---

Latex:

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


By

---

Latex:
OnMaybeHyp  11  (\mbackslash{}h.  (ParallelOp  h  THEN  (All  Reduce  THEN  Auto)  THEN  CaseNat  0  `i'  THEN  Reduce  0))\mcdot{}

---

Home Index