---

Step * 1 1 2 of Lemma fibs_wf

.....eq aux..... 
1. f : ℕ ⟶ ℕ ⟶ ℕ
2. (λx,y. (x + y)) = f ∈ (ℕ ⟶ ℕ ⟶ ℕ)
3. n : ℕ
⊢ istype(primrec(n;Top;λ,T. (ℕ × T)))
BY
{ Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  (\mlambda{}x,y.  (x  +  y))  =  f
3.  n  :  \mBbbN{}
\mvdash{}  istype(primrec(n;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T)))


By

---

Latex:
Auto

---

Home Index