---

Step * of Lemma p-fun-exp-add

∀[T:Type]. ∀[n,m:ℕ]. ∀[f:T ⟶ (T + Top)].  (f^n + m = f^n o f^m ∈ (T ⟶ (T + Top)))
BY
{ (Auto
   THEN RWO "p-fun-exp-compose" 0
   THEN Auto'
   THEN Unfold `p-fun-exp` 0
   THEN (GenConcl p-id() = id ∈ (T ⟶ (T + Top))⋅ THENA Auto)
   THEN RWO "primrec_add" 0
   THEN Auto
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[f:T  {}\mrightarrow{}  (T  +  Top)].    (f\^{}n  +  m  =  f\^{}n  o  f\^{}m)


By

---

Latex:
(Auto
  THEN  RWO  "p-fun-exp-compose"  0
  THEN  Auto'
  THEN  Unfold  `p-fun-exp`  0
  THEN  (GenConcl  p-id()  =  id\mcdot{}  THENA  Auto)
  THEN  RWO  "primrec\_add"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index