---

Step * 1 of Lemma app_permf_id

.....subterm..... T:t
1:n
1. m : ℕ
2. n : ℕ
3. i : ℕm + n
⊢ if i <z m then (λx.x) i else ((λx.x) (i - m)) + m fi  = i ∈ ℕm + n
BY
{ AbReduce 0 }

1
1. m : ℕ
2. n : ℕ
3. i : ℕm + n
⊢ if i <z m then i else (i - m) + m fi  = i ∈ ℕm + n

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  i  :  \mBbbN{}m  +  n
\mvdash{}  if  i  <z  m  then  (\mlambda{}x.x)  i  else  ((\mlambda{}x.x)  (i  -  m))  +  m  fi    =  i


By

---

Latex:
AbReduce  0

---

Home Index