---

Step * 2 of Lemma fix_property


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)
BY
{ ((InstHyp [⌜x⌝] 6⋅ THENA Auto) THEN (RecUnfold `fix` 0 THEN Unfold `eqof` 0) THEN (SplitOnConclITE THENA Auto))⋅ }

1
.....truecase..... 
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 x) = x ∈ T) ∧ x is f*(x)

2
.....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)

---

Latex:

---

Latex:

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
\mvdash{}  ((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x)


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  (RecUnfold  `fix`  0  THEN  Unfold  `eqof`  0)
  THEN  (SplitOnConclITE  THENA  Auto))\mcdot{}

---

Home Index