---

Step * 1 of Lemma fix-step


1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. x : T
5. retraction(T;f)
⊢ f**(f x) = f**(x) ∈ T
BY
{ xxx((Assert (x = (f x) ∈ T) ⇒ (f**(f x) = f**(x) ∈ T) BY
             Auto)
      THEN RW (AddrC [3] (RecUnfoldC `fix`)) 0
      THEN AutoSplit
      THEN ThinTrivial)xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. x : T
5. retraction(T;f)
6. x = (f x) ∈ T
7. f**(f x) = f**(x) ∈ T
⊢ f**(f x) = x ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  T  {}\mrightarrow{}  T
4.  x  :  T
5.  retraction(T;f)
\mvdash{}  f**(f  x)  =  f**(x)


By

---

Latex:
xxx((Assert  (x  =  (f  x))  {}\mRightarrow{}  (f**(f  x)  =  f**(x))  BY
                      Auto)
        THEN  RW  (AddrC  [3]  (RecUnfoldC  `fix`))  0
        THEN  AutoSplit
        THEN  ThinTrivial)xxx

---

Home Index