---

Step * 1 of Lemma ml-select-sq


1. T : Type
2. valueall-type(T)
3. n : ℤ
⊢ let x,y = [] 
  in if n <z 1 then x else ml-select(n - 1;y) fi  ~ ⊥
BY
{ ((RWO  "stuck-spread" 0 THEN Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  n  :  \mBbbZ{}
\mvdash{}  let  x,y  =  [] 
    in  if  n  <z  1  then  x  else  ml-select(n  -  1;y)  fi    \msim{}  \mbot{}


By

---

Latex:
((RWO    "stuck-spread"  0  THEN  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index