Step * 1 of Lemma select-as-reduce


1. : ℕ
2. Top
3. Top List
4. reduce(λu,x. case of inl(i) => if (i =z n) then inr u  else inl (i 1) fi  inr(u) => x;inl 0;v) if ||v|| ≤n
then inl ||v||
else inr v[||v|| 1] 
fi 
5. n < ||v|| 1
6. ||v|| ≤ n
7. ||v|| n ∈ ℤ
⊢ [u v][(||v|| 1) 1]
BY
(HypSubst' -1 THEN Subst' (n 1) THEN Reduce 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