---

Step * of Lemma select-map-index_aux

∀[f:Top]. ∀[L:Top List]. ∀[i:ℕ||L||]. ∀[x:ℤ].  (map-index_aux(f;L) x[i] ~ f (x + i) L[i])
BY
{ (Unfold `map-index_aux` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN Try (((RWO "select-cons" 0 THENA Auto) THEN AutoSplit THEN RWW "-4" 0))
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[L:Top  List].  \mforall{}[i:\mBbbN{}||L||].  \mforall{}[x:\mBbbZ{}].    (map-index\_aux(f;L)  x[i]  \msim{}  f  (x  +  i)  L[i])


By

---

Latex:
(Unfold  `map-index\_aux`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (((RWO  "select-cons"  0  THENA  Auto)  THEN  AutoSplit  THEN  RWW  "-4"  0))
  THEN  Auto')

---

Home Index