---

Step * 2 2 of Lemma select-as-reduce


1. n : ℕ
2. u : Top
3. v : Top List
4. reduce(λu,x. case x of inl(i) => if (i =z n) then inr u  else inl (i + 1) fi  | inr(u) => x;inl 0;v) ~ if ||v|| ≤z n
then inl ||v||
else inr v[||v|| - n + 1] 
fi 
5. n < ||v|| + 1
6. n < ||v||
⊢ v[||v|| - n + 1] ~ [u / v][(||v|| - n + 1) + 1]
BY
{ (RWO "select_cons_tl_sq" 0 THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  u  :  Top
3.  v  :  Top  List
4.  reduce(\mlambda{}u,x.  case  x  of  inl(i)  =>  if  (i  =\msubz{}  n)  then  inr  u    else  inl  (i  +  1)  fi    |  inr(u)  =>  x;inl  0\000C;v) 
\msim{}  if  ||v||  \mleq{}z  n  then  inl  ||v||  else  inr  v[||v||  -  n  +  1]    fi 
5.  n  <  ||v||  +  1
6.  n  <  ||v||
\mvdash{}  v[||v||  -  n  +  1]  \msim{}  [u  /  v][(||v||  -  n  +  1)  +  1]


By

---

Latex:
(RWO  "select\_cons\_tl\_sq"  0  THEN  Auto  THEN  Auto')

---

Home Index