---

Step * 1 1 1 2 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. ∀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) ∈ ℤ
19. i < ||L1||
⊢ L1[i] R L2[(i + 1) - ||L1||]
BY
{ ((Assert i ~ ||L1|| - 1 BY Auto) THEN (HypSubst (-1) 0 THENA Auto) THEN Fold `last` 0) }

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) ∈ ℤ
19. i < ||L1||
20. i ~ ||L1|| - 1
⊢ last(L1) R L2[((||L1|| - 1) + 1) - ||L1||]

---

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)
19.  i  <  ||L1||
\mvdash{}  L1[i]  R  L2[(i  +  1)  -  ||L1||]


By

---

Latex:
((Assert  i  \msim{}  ||L1||  -  1  BY  Auto)  THEN  (HypSubst  (-1)  0  THENA  Auto)  THEN  Fold  `last`  0)

---

Home Index