---

Step * 2 2 1 of Lemma fix_property

.....antecedent..... 
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. 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
12. ((f x) = x ∈ T) ∨ h (f x) < h x
13. ¬(x = (f x) ∈ T)
⊢ h (f x) < n - 1
BY
{ (D (-2) THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  T  {}\mrightarrow{}  T
4.  retraction(T;f)
5.  h  :  T  {}\mrightarrow{}  \mBbbN{}
6.  \mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x)
7.  n  :  \mBbbZ{}
8.  0  <  n
9.  \mforall{}x:T.  (h  x  <  n  -  1  {}\mRightarrow{}  (((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x)))
10.  x  :  T
11.  h  x  <  n
12.  ((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x
13.  \mneg{}(x  =  (f  x))
\mvdash{}  h  (f  x)  <  n  -  1


By

---

Latex:
(D  (-2)  THEN  Auto)\mcdot{}

---

Home Index