---

Step * 1 2 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
11. i < i1
⊢ [y; x] ⊆ L
BY
{ (Unfold `sublist` 0
   THEN Reduce 0
   THEN InstConcl   [λj.if (j =z 0) then i else i1 fi ]⋅
   THEN Reduce 0
   THEN Auto'
   THEN Try ((Unfold `label` 0 THEN Reduce 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. i < i1
⊢ increasing(λj.if (j =z 0) then i else i1 fi ;2)

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
12. increasing(λj.if (j =z 0) then i else i1 fi ;2)
13. j : ℕ2
⊢ [y; x][j] = L[if (j =z 0) then i else i1 fi ] ∈ T

---

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]
11.  i  <  i1
\mvdash{}  [y;  x]  \msubseteq{}  L


By

---

Latex:
(Unfold  `sublist`  0
  THEN  Reduce  0
  THEN  InstConcl    [\mlambda{}j.if  (j  =\msubz{}  0)  then  i  else  i1  fi  ]\mcdot{}
  THEN  Reduce  0
  THEN  Auto'
  THEN  Try  ((Unfold  `label`  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index