---

Step * of Lemma fix_property

∀[T:Type]. ∀eq:EqDecider(T). ∀f:T ⟶ T.  (retraction(T;f) ⇒ (∀x:T. (((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x))))
BY
{ ((RepeatFor 4 ((D 0 THENA Auto))
    THEN (DupHyp (-1) THEN D -1)
    THEN Assert ⌜∀n:ℕ. ∀x:T.  (h x < n ⇒ (((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x)))⌝⋅
    THEN Try (((D 0 THENA Auto) THEN (InstHyp [⌜(h x) + 1⌝;⌜x⌝] (-2)⋅ THENA Auto) THEN Trivial)⋅))
   THEN ((InductionOnNat THENA Auto) THEN (UnivCD THENA Auto))⋅
   ) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
5. h : T ⟶ ℕ
6. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
7. x : T
8. h x < 0
⊢ ((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x)

2
1. [T] : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
5. h : T ⟶ ℕ
6. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
7. n : ℤ
8. [%4] : 0 < n
9. ∀x:T. (h x < n - 1 ⇒ (((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x)))
10. x : T
11. h x < n
⊢ ((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}f:T  {}\mrightarrow{}  T.
        (retraction(T;f)  {}\mRightarrow{}  (\mforall{}x:T.  (((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x))))


By

---

Latex:
((RepeatFor  4  ((D  0  THENA  Auto))
    THEN  (DupHyp  (-1)  THEN  D  -1)
    THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x:T.    (h  x  <  n  {}\mRightarrow{}  (((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x)))\mkleeneclose{}\mcdot{}
    THEN  Try  (((D  0  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}(h  x)  +  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  Trivial)\mcdot{}))
  THEN  ((InductionOnNat  THENA  Auto)  THEN  (UnivCD  THENA  Auto))\mcdot{}
  )

---

Home Index