---

Step * 1 1 of Lemma rel-path-between-append


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. L1 : T List
4. L2 : T List
5. x : T
6. y : T
7. z : T
8. rel-path(R;L1)
9. 0 < ||L1||
10. x = hd(L1) ∈ T
11. y = last(L1) ∈ T
12. rel-path(R;L2)
13. 0 < ||L2||
14. y = hd(L2) ∈ T
15. z = last(L2) ∈ T
16. Refl(T;v1,v2.R v1 v2)
⊢ rel-path(R;L1 @ L2)
BY
{ All (RepUR ``rel-path``) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. L1 : T List
4. L2 : T List
5. x : T
6. y : T
7. z : T
8. ∀i:ℕ||L1|| - 1. (L1[i] R L1[i + 1])
9. 0 < ||L1||
10. x = hd(L1) ∈ T
11. y = last(L1) ∈ T
12. ∀i:ℕ||L2|| - 1. (L2[i] R L2[i + 1])
13. 0 < ||L2||
14. y = hd(L2) ∈ T
15. z = last(L2) ∈ T
16. Refl(T;v1,v2.R v1 v2)
⊢ ∀i:ℕ||L1 @ L2|| - 1. (L1 @ L2[i] R L1 @ L2[i + 1])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  L1  :  T  List
4.  L2  :  T  List
5.  x  :  T
6.  y  :  T
7.  z  :  T
8.  rel-path(R;L1)
9.  0  <  ||L1||
10.  x  =  hd(L1)
11.  y  =  last(L1)
12.  rel-path(R;L2)
13.  0  <  ||L2||
14.  y  =  hd(L2)
15.  z  =  last(L2)
16.  Refl(T;v1,v2.R  v1  v2)
\mvdash{}  rel-path(R;L1  @  L2)


By

---

Latex:
All  (RepUR  ``rel-path``)

---

Home Index