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