---

Step * 1 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. ||v|| ≤ n
7. ||v|| = n ∈ ℤ
⊢ u ~ [u / v][(||v|| + 1) - n + 1]
BY
{ (HypSubst' -1 0 THEN Subst' (n + 1) - n + 1 ~ 0 0 THEN Reduce 0 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.  ||v||  \mleq{}  n
7.  ||v||  =  n
\mvdash{}  u  \msim{}  [u  /  v][(||v||  +  1)  -  n  +  1]


By

---

Latex:
(HypSubst'  -1  0  THEN  Subst'  (n  +  1)  -  n  +  1  \msim{}  0  0  THEN  Reduce  0  THEN  Auto)

---

Home Index