---

Step * 2 2 1 1 of Lemma fun_exp-mul


1. T : Type
2. f : T ⟶ T
3. n : ℤ
4. 0 < n
5. ∀[m:ℕ]. ∀[x:T].  ((f^(n - 1) * m x) = (λx.(f^m x)^n - 1 x) ∈ T)
6. m : ℕ
7. x : T
⊢ (f^m (λx.(f^m x)^n - 1 x)) = (λx.(f^m x)^n x) ∈ T
BY
{ ((RW (AddrC [3;1] funexpTopC) 0 THENA Auto) THEN (SplitOnConclITE THEN Auto) THEN Reduce 0) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}[m:\mBbbN{}].  \mforall{}[x:T].    ((f\^{}(n  -  1)  *  m  x)  =  (\mlambda{}x.(f\^{}m  x)\^{}n  -  1  x))
6.  m  :  \mBbbN{}
7.  x  :  T
\mvdash{}  (f\^{}m  (\mlambda{}x.(f\^{}m  x)\^{}n  -  1  x))  =  (\mlambda{}x.(f\^{}m  x)\^{}n  x)


By

---

Latex:
((RW  (AddrC  [3;1]  funexpTopC)  0  THENA  Auto)  THEN  (SplitOnConclITE  THEN  Auto)  THEN  Reduce  0)

---

Home Index