---

Step * 1 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
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
BY
{ ((CaseNat 0 `j' THEN Reduce 0 THEN Try (Trivial)) THEN (CaseNat 1 `j' THEN Reduce 0 THEN Try (Trivial)) THEN Auto') }

---

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]
8.  \mforall{}i@0:\mBbbN{}1.  if  (i@0  =\msubz{}  0)  then  i  else  i  +  1  fi    <  if  (i@0  +  1  =\msubz{}  0)  then  i  else  i  +  1  fi 
9.  j  :  \mBbbN{}2
\mvdash{}  [x;  y][j]  =  L[if  (j  =\msubz{}  0)  then  i  else  i  +  1  fi  ]


By

---

Latex:
((CaseNat  0  `j'  THEN  Reduce  0  THEN  Try  (Trivial))
  THEN  (CaseNat  1  `j'  THEN  Reduce  0  THEN  Try  (Trivial))
  THEN  Auto')

---

Home Index