---

Step * 2 of Lemma ml-select-sq


1. T : Type
2. valueall-type(T)
3. u : T
4. v : T List
5. ∀[n:ℤ]. (ml-select(n;v) ~ v[n])
6. n : ℤ
⊢ if n <z 1 then u else v[n - 1] fi  ~ let x,y = [u / v] 
                                       in if (n) < (1)  then x  else eval m = n - 1 in y[m]
BY
{ (Reduce 0 THEN CallByValueReduce 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[n:\mBbbZ{}].  (ml-select(n;v)  \msim{}  v[n])
6.  n  :  \mBbbZ{}
\mvdash{}  if  n  <z  1  then  u  else  v[n  -  1]  fi    \msim{}  let  x,y  =  [u  /  v] 
                                                                              in  if  (n)  <  (1)    then  x    else  eval  m  =  n  -  1  in  y[m]


By

---

Latex:
(Reduce  0  THEN  CallByValueReduce  0\mcdot{}  THEN  Auto)

---

Home Index