---

Step * 1 of Lemma l_tricotomy


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
⊢ ((x = y ∈ T) ∨ [x; y] ⊆ L) ∨ [y; x] ⊆ L
BY
{ ((Tricotomy i1 i⋅ THENL [((Sel 1 (D 0)) THENM (Sel 2 (D 0))); ((Sel 1 (D 0)) THENM (Sel 1 (D 0))); (Sel 2 (D 0))])
   THEN Auto
   ) }

1
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
⊢ [x; y] ⊆ L

2
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. i < i1
⊢ [y; x] ⊆ L

---

Latex:

---

Latex:

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]
\mvdash{}  ((x  =  y)  \mvee{}  [x;  y]  \msubseteq{}  L)  \mvee{}  [y;  x]  \msubseteq{}  L


By

---

Latex:
((Tricotomy  i1  i\mcdot{}
    THENL  [((Sel  1  (D  0))  THENM  (Sel  2  (D  0)));  ((Sel  1  (D  0))  THENM  (Sel  1  (D  0)));  (Sel  2  (D  0))]
  )
  THEN  Auto
  )

---

Home Index