---

Step * 1 of Lemma adjacent-before


1. [T] : Type
2. L : T List
3. x : T
4. y : T
5. i : ℕ||L|| - 1
6. x = L[i] ∈ T
7. y = L[i + 1] ∈ T
⊢ ∃f:ℕ2 ⟶ ℕ||L||. (increasing(f;2) ∧ (∀j:ℕ2. ([x; y][j] = L[f j] ∈ T)))
BY
{ ((InstConcl [⌜λj.if (j =z 0) then i else i + 1 fi ⌝]⋅ THENA Auto') THEN RepUR ``increasing`` 0 THEN Auto) }

1
1. T : Type
2. L : T List
3. x : T
4. y : T
5. i : ℕ||L|| - 1
6. x = L[i] ∈ T
7. y = L[i + 1] ∈ T
8. ∀i@0:ℕ1. if (i@0 =z 0) then i else i + 1 fi  < if (i@0 + 1 =z 0) then i else i + 1 fi 
9. j : ℕ2
⊢ [x; y][j] = L[if (j =z 0) then i else i + 1 fi ] ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  x  :  T
4.  y  :  T
5.  i  :  \mBbbN{}||L||  -  1
6.  x  =  L[i]
7.  y  =  L[i  +  1]
\mvdash{}  \mexists{}f:\mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||L||.  (increasing(f;2)  \mwedge{}  (\mforall{}j:\mBbbN{}2.  ([x;  y][j]  =  L[f  j])))


By

---

Latex:
((InstConcl  [\mkleeneopen{}\mlambda{}j.if  (j  =\msubz{}  0)  then  i  else  i  +  1  fi  \mkleeneclose{}]\mcdot{}  THENA  Auto')
  THEN  RepUR  ``increasing``  0
  THEN  Auto)

---

Home Index