---

Step * of Lemma urec-is-least-fixedpoint

∀[F:Type ⟶ Type]. ∀T:Type. urec(F) ⊆r T supposing F T ≡ T supposing Monotone(T.F T)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN Unfold `urec` -1
   THEN D_union (-1)
   THEN DoSubsume
   THEN Auto
   THEN RepeatFor 2 (Thin(-1))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (InstLemma `fun_exp_apply_add1` [⌜parm{i'}⌝;⌜Type⌝;⌜n - 1⌝;⌜F⌝]⋅ THENA Auto)
   THEN Subst ⌜(n - 1) + 1 ~ n⌝ (-1)⋅
   THEN Auto) }

1
1. F : Type ⟶ Type
2. Monotone(T.F T)
3. T : Type@i'
4. F T ≡ T
5. n : ℤ
6. 0 < n
7. (F^n - 1 Void) ⊆r T
8. ∀[x:Type]. ((F (F^n - 1 x)) = (F^n x) ∈ Type)
⊢ (F^n Void) ⊆r T

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  \mforall{}T:Type.  urec(F)  \msubseteq{}r  T  supposing  F  T  \mequiv{}  T  supposing  Monotone(T.F  T)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `urec`  -1
  THEN  D\_union  (-1)
  THEN  DoSubsume
  THEN  Auto
  THEN  RepeatFor  2  (Thin(-1))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (InstLemma  `fun\_exp\_apply\_add1`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Subst  \mkleeneopen{}(n  -  1)  +  1  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index