---

Step * 1 1 1 of Lemma l_tricotomy

.....falsecase..... 
1. T : Type
2. x : T
3. y : T
4. L : T List
5. i1 : ℕ
6. i1 < ||L||
7. x = L[i1] ∈ T
8. i : ℕ
9. i < ||L||
10. y = L[i] ∈ T
11. i1 < i
12. increasing(λj.if (j =z 0) then i1 else i fi ;2)
13. j : ℕ2
14. ¬(j = 0 ∈ ℤ)
⊢ [x; y][j] = L[i] ∈ T
BY
{ ((Subst' j = 1 ∈ ℤ 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....falsecase..... 
1.  T  :  Type
2.  x  :  T
3.  y  :  T
4.  L  :  T  List
5.  i1  :  \mBbbN{}
6.  i1  <  ||L||
7.  x  =  L[i1]
8.  i  :  \mBbbN{}
9.  i  <  ||L||
10.  y  =  L[i]
11.  i1  <  i
12.  increasing(\mlambda{}j.if  (j  =\msubz{}  0)  then  i1  else  i  fi  ;2)
13.  j  :  \mBbbN{}2
14.  \mneg{}(j  =  0)
\mvdash{}  [x;  y][j]  =  L[i]


By

---

Latex:
((Subst'  j  =  1  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index