---

Step * of Lemma fun_exp_add1-sq2

∀[n:ℕ]. ∀[f,x:Top].  (f^n (f x) ~ f^n + 1 x)
BY
{ ((InstLemma `fun_exp_add-sq` []⋅ THENA Auto)
   THEN ParallelLast
   THEN (InstHyp [⌜1⌝] (-1)⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)) }

1
1. ∀[n,m:ℕ]. ∀[f,x:Top].  (f^n + m x ~ f^n (f^m x))
2. [n] : ℕ
3. ∀[m:ℕ]. ∀[f,x:Top].  (f^n + m x ~ f^n (f^m x))
4. ∀[f,x:Top].  (f^n + 1 x ~ f^n (f^1 x))
5. [f] : Top
6. ∀[x:Top]. (f^n + 1 x ~ f^n (f^1 x))
7. [x] : Top
8. f^n + 1 x ~ f^n (f^1 x)
⊢ f^n (f x) ~ f^n + 1 x

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,x:Top].    (f\^{}n  (f  x)  \msim{}  f\^{}n  +  1  x)


By

---

Latex:
((InstLemma  `fun\_exp\_add-sq`  []\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index