---

Step * of Lemma p-fun-exp-compose

∀[T:Type]. ∀[n:ℕ]. ∀[h,f:T ⟶ (T + Top)].  (f^n o h = primrec(n;h;λi,g. f o g) ∈ (T ⟶ (T + Top)))
BY
{ (InductionOnNat THEN RepUR ``p-fun-exp`` 0) }

1
1. T : Type
2. n : ℤ
⊢ ∀[h,f:T ⟶ (T + Top)].  (p-id() o h = h ∈ (T ⟶ (T + Top)))

2
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[h,f:T ⟶ (T + Top)].  (f^n - 1 o h = primrec(n - 1;h;λi,g. f o g) ∈ (T ⟶ (T + Top)))
⊢ ∀[h,f:T ⟶ (T + Top)].  (primrec(n;p-id();λi,g. f o g) o h = primrec(n;h;λi,g. f o g) ∈ (T ⟶ (T + Top)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[h,f:T  {}\mrightarrow{}  (T  +  Top)].    (f\^{}n  o  h  =  primrec(n;h;\mlambda{}i,g.  f  o  g))


By

---

Latex:
(InductionOnNat  THEN  RepUR  ``p-fun-exp``  0)

---

Home Index