---

Step * 1 of Lemma iterated-conjugate


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)
BY
{ (RWO "-1" 0
   THEN Auto
   THEN Ext
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 3 ((EqCD THEN Auto))
   THEN (RWO "fun_exp_add1-sq fun_exp_add1-sq2" 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  g  :  T  {}\mrightarrow{}  T
4.  h  :  T  {}\mrightarrow{}  T
5.  m  :  \mBbbZ{}
6.  \mneg{}m  <  1
7.  0  <  m
8.  (\mlambda{}f.(g  o  (f  o  h))\^{}m  -  1  f)  =  (g\^{}m  -  1  o  (f  o  h\^{}m  -  1))
\mvdash{}  (g  o  ((\mlambda{}f.(g  o  (f  o  h))\^{}m  -  1  f)  o  h))  =  ((g  o  g\^{}m  -  1)  o  (f  o  (h  o  h\^{}m  -  1)))


By

---

Latex:
(RWO  "-1"  0
  THEN  Auto
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  3  ((EqCD  THEN  Auto))
  THEN  (RWO  "fun\_exp\_add1-sq  fun\_exp\_add1-sq2"  0  THEN  Auto)\mcdot{})

---

Home Index