---

Step * of Lemma iterated-conjugate

∀[T:Type]. ∀[f,g,h:T ⟶ T]. ∀[m:ℕ].  ((λf.(g o (f o h))^m f) = (g^m o (f o h^m)) ∈ (T ⟶ T))
BY
{ xxx(PrimrecInductionOn `m' THEN Auto)xxx }

1
1. T : Type
2. f : T ⟶ T
3. g : T ⟶ T
4. h : T ⟶ T
5. m : ℤ
6. ¬m < 1
7. 0 < m
8. (λf.(g o (f o h))^m - 1 f) = (g^m - 1 o (f o h^m - 1)) ∈ (T ⟶ T)
⊢ (g o ((λf.(g o (f o h))^m - 1 f) o h)) = ((g o g^m - 1) o (f o (h o h^m - 1))) ∈ (T ⟶ T)

---

Latex:

---

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


By

---

Latex:
xxx(PrimrecInductionOn  `m'  THEN  Auto)xxx

---

Home Index