---

Step * 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|| + 1) - n + 1]
BY
{ Subst' (||v|| + 1) - n + 1 ~ (||v|| - n + 1) + 1 0 }

1
.....equality..... 
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|| + 1) - n + 1 ~ (||v|| - n + 1) + 1

2
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]

---

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||  +  1)  -  n  +  1]


By

---

Latex:
Subst'  (||v||  +  1)  -  n  +  1  \msim{}  (||v||  -  n  +  1)  +  1  0

---

Home Index