---

Step * 1 1 of Lemma app_permf_id


1. m : ℕ
2. n : ℕ
3. i : ℕm + n
⊢ if i <z m then i else (i - m) + m fi  = i ∈ ℕm + n
BY
{ (SplitOnConclITE THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(SplitOnConclITE  THEN  Auto)

---

Home Index