---

Step * 2 2 of Lemma fix_property

.....falsecase..... 
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
12. ((f x) = x ∈ T) ∨ h (f x) < h x
13. ¬(x = (f x) ∈ T)
⊢ ((f f**(f x)) = f**(f x) ∈ T) ∧ f**(f x) is f*(x)
BY
{ (InstHyp [⌜f x⌝] (-5)⋅ THEN Auto)⋅ }

1
.....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

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
12. ((f x) = x ∈ T) ∨ h (f x) < h x
13. ¬(x = (f x) ∈ T)
14. (f f**(f x)) = f**(f x) ∈ T
15. f**(f x) is f*(f x)
16. (f f**(f x)) = f**(f x) ∈ T
⊢ f**(f x) is f*(x)

---

Latex:

---

Latex:
.....falsecase..... 
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.  [\%4]  :  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{}  ((f  f**(f  x))  =  f**(f  x))  \mwedge{}  f**(f  x)  is  f*(x)


By

---

Latex:
(InstHyp  [\mkleeneopen{}f  x\mkleeneclose{}]  (-5)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index