---

Step * 1 1 of Lemma fix_wf


1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. h : T ⟶ ℕ
5. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
6. n : ℤ
7. 0 < n
8. ∀x:T. (h x < n - 1 ⇒ (f**(x) ∈ T))
9. x : T
10. h x < n
⊢ f**(x) ∈ T
BY
{ (RecUnfold `fix` 0
   THEN SplitOnConclITE
   THEN Auto
   THEN BackThruSomeHyp
   THEN InstHyp [⌜x⌝] 5⋅
   THEN Auto
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  T  {}\mrightarrow{}  T
4.  h  :  T  {}\mrightarrow{}  \mBbbN{}
5.  \mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x)
6.  n  :  \mBbbZ{}
7.  0  <  n
8.  \mforall{}x:T.  (h  x  <  n  -  1  {}\mRightarrow{}  (f**(x)  \mmember{}  T))
9.  x  :  T
10.  h  x  <  n
\mvdash{}  f**(x)  \mmember{}  T


By

---

Latex:
(RecUnfold  `fix`  0
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  Auto)

---

Home Index