---

Step * 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)
⊢ ∀x:T. (f**(x) ∈ T)
BY
{ (Assert ⌜∀n:ℕ. ∀x:T.  (h x < n ⇒ (f**(x) ∈ T))⌝⋅
   THEN Try ((Auto THEN Using [`n',⌜(h x) + 1⌝] (BHyp (-2))⋅ THEN Auto'))
   THEN InductionOnNat
   THEN Auto') }

1
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

---

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)
\mvdash{}  \mforall{}x:T.  (f**(x)  \mmember{}  T)


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x:T.    (h  x  <  n  {}\mRightarrow{}  (f**(x)  \mmember{}  T))\mkleeneclose{}\mcdot{}
  THEN  Try  ((Auto  THEN  Using  [`n',\mkleeneopen{}(h  x)  +  1\mkleeneclose{}]  (BHyp  (-2))\mcdot{}  THEN  Auto'))
  THEN  InductionOnNat
  THEN  Auto')

---

Home Index