---

Step * 1 of Lemma urec-is-least-fixedpoint


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
BY
{ (InstHyp [⌜Void⌝] (-1)⋅ THEN Auto THEN RWO "-1<" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F  T)
3.  T  :  Type@i'
4.  F  T  \mequiv{}  T
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  (F\^{}n  -  1  Void)  \msubseteq{}r  T
8.  \mforall{}[x:Type].  ((F  (F\^{}n  -  1  x))  =  (F\^{}n  x))
\mvdash{}  (F\^{}n  Void)  \msubseteq{}r  T


By

---

Latex:
(InstHyp  [\mkleeneopen{}Void\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto  THEN  RWO  "-1<"  0  THEN  Auto)\mcdot{}

---

Home Index