---

Step * 1 1 1 2 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. ∀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)
17. i : ℕ||L1 @ L2|| - 1
18. i = (||L1|| - 1) ∈ ℤ
⊢ L1 @ L2[i] R L1 @ L2[i + 1]
BY
{ (RWO "select_append" 0 THEN Auto) }

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)
17. i : ℕ||L1 @ L2|| - 1
18. i = (||L1|| - 1) ∈ ℤ
⊢ if i <z ||L1|| then L1[i] else L2[i - ||L1||] fi  R if i + 1 <z ||L1|| then L1[i + 1] else L2[(i + 1) - ||L1||] fi 

---

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.  \mforall{}i:\mBbbN{}||L1||  -  1.  (L1[i]  R  L1[i  +  1])
9.  0  <  ||L1||
10.  x  =  hd(L1)
11.  y  =  last(L1)
12.  \mforall{}i:\mBbbN{}||L2||  -  1.  (L2[i]  R  L2[i  +  1])
13.  0  <  ||L2||
14.  y  =  hd(L2)
15.  z  =  last(L2)
16.  Refl(T;v1,v2.R  v1  v2)
17.  i  :  \mBbbN{}||L1  @  L2||  -  1
18.  i  =  (||L1||  -  1)
\mvdash{}  L1  @  L2[i]  R  L1  @  L2[i  +  1]


By

---

Latex:
(RWO  "select\_append"  0  THEN  Auto)

---

Home Index