---

Step * 2 2 1 1 of Lemma split-at-first-rel


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. u : T
5. u1 : T
6. v : T List
7. X1 : T List
8. X2 : T List
9. [u1 / v] = (X1 @ X2) ∈ (T List)
10. ∀i:ℕ||X1|| - 1. R[X1[i];X1[i + 1]]
11. (¬False) ⇒ ((¬↑null(X1)) ∧ ¬R[last(X1);hd(X2)] supposing ||X2|| ≥ 1 )
12. R[u;u1]
13. [u; [u1 / v]] = [u / (X1 @ X2)] ∈ (T List)
14. i : ℕ(||X1|| + 1) - 1
⊢ R[[u / X1][i];[u / X1][i + 1]]
BY
{ CaseNat 0 `i' }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. u : T
5. u1 : T
6. v : T List
7. X1 : T List
8. X2 : T List
9. [u1 / v] = (X1 @ X2) ∈ (T List)
10. ∀i:ℕ||X1|| - 1. R[X1[i];X1[i + 1]]
11. (¬False) ⇒ ((¬↑null(X1)) ∧ ¬R[last(X1);hd(X2)] supposing ||X2|| ≥ 1 )
12. R[u;u1]
13. [u; [u1 / v]] = [u / (X1 @ X2)] ∈ (T List)
14. i : ℕ(||X1|| + 1) - 1
15. i = 0 ∈ ℤ
⊢ R[[u / X1][0];[u / X1][0 + 1]]

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. u : T
5. u1 : T
6. v : T List
7. X1 : T List
8. X2 : T List
9. [u1 / v] = (X1 @ X2) ∈ (T List)
10. ∀i:ℕ||X1|| - 1. R[X1[i];X1[i + 1]]
11. (¬False) ⇒ ((¬↑null(X1)) ∧ ¬R[last(X1);hd(X2)] supposing ||X2|| ≥ 1 )
12. R[u;u1]
13. [u; [u1 / v]] = [u / (X1 @ X2)] ∈ (T List)
14. i : ℕ(||X1|| + 1) - 1
15. ¬(i = 0 ∈ ℤ)
⊢ R[[u / X1][i];[u / X1][i + 1]]

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x,y:T.    Dec(R[x;y])
4.  u  :  T
5.  u1  :  T
6.  v  :  T  List
7.  X1  :  T  List
8.  X2  :  T  List
9.  [u1  /  v]  =  (X1  @  X2)
10.  \mforall{}i:\mBbbN{}||X1||  -  1.  R[X1[i];X1[i  +  1]]
11.  (\mneg{}False)  {}\mRightarrow{}  ((\mneg{}\muparrow{}null(X1))  \mwedge{}  \mneg{}R[last(X1);hd(X2)]  supposing  ||X2||  \mgeq{}  1  )
12.  R[u;u1]
13.  [u;  [u1  /  v]]  =  [u  /  (X1  @  X2)]
14.  i  :  \mBbbN{}(||X1||  +  1)  -  1
\mvdash{}  R[[u  /  X1][i];[u  /  X1][i  +  1]]


By

---

Latex:
CaseNat  0  `i'

---

Home Index