---

Step * of Lemma fun_exp_add

∀[T:Type]. ∀[n,m:ℕ]. ∀[f:T ⟶ T].  (f^n + m = (f^n o f^m) ∈ (T ⟶ T))
BY
{ (RWO "fun_exp_compose" 0
   THEN Auto'
   THEN Unfold `fun_exp` 0
   THEN (InstLemma `primrec_add` [T ⟶ T;n;m;λx.x;λi,g. (f o g)] THENM (Reduce (-1) THEN RWO "-1" 0))
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RWO  "fun\_exp\_compose"  0
  THEN  Auto'
  THEN  Unfold  `fun\_exp`  0
  THEN  (InstLemma  `primrec\_add`  [T  {}\mrightarrow{}  T;n;m;\mlambda{}x.x;\mlambda{}i,g.  (f  o  g)]  THENM  (Reduce  (-1)  THEN  RWO  "-1"  0))
  THEN  Auto)

---

Home Index