---

Step * 1 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)
⊢ ∀i:ℕ||L1 @ L2|| - 1. (L1 @ L2[i] R L1 @ L2[i + 1])
BY
{ ((D 0 THENA Auto) THEN (InstLemma `int_trichot` [⌜i⌝;⌜||L1|| - 1⌝] ⋅ THENA Auto) THEN SplitOrHyps) }

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
⊢ L1 @ L2[i] R L1 @ L2[i + 1]

2
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]

3
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]

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  (InstLemma  `int\_trichot`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}||L1||  -  1\mkleeneclose{}]  \mcdot{}  THENA  Auto)  THEN  SplitOrHyps)

---

Home Index