---

Step * of Lemma nat-id-fun-ext

∀n:ℕ. (∃m:ℕ [(m = n ∈ ℕ)])
BY
{ Extract of Obid: nat-id-fun-example
  not unfolding  primrec
  finishing with Auto
  normalizes to:
  
  λn.(primrec(n + 1;λn.Ax;λi,x,n. if n=(i + 1) - 1 then if n=0 then 0 else eval n1 = n - 1 in (x n1) + 1 else (x n)) n) \000C}

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}m:\mBbbN{}  [(m  =  n)])


By

---

Latex:
Extract  of  Obid:  nat-id-fun-example
not  unfolding    primrec
finishing  with  Auto
normalizes  to:

\mlambda{}n.(primrec(n  +  1;\mlambda{}n.Ax;\mlambda{}i,x,n.  if  n=(i  +  1)  -  1
                                                                then  if  n=0  then  0  else  eval  n1  =  n  -  1  in  (x  n1)  +  1
                                                                else  (x  n)) 
        n)

---

Home Index