Step
*
1
2
1
1
1
2
of Lemma
urec_induction
.....wf..... 
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) 
⇒ ((F T) ⊆r Base))
4. f : destructor{i:l}(T.F[T])
5. x : urec(F)
6. x ∈ F^urec-level(f;x) Void
7. urec-level(f;x) ∈ ℕ
8. n : ℕ
⊢ istype(x ∈ ⋃n:ℕn.(F^n Void))
BY
{ (At ⌜Type⌝ (D 0)⋅ THEN Fold `prop` 0 THEN BLemma `base-member-prop` THEN Auto) }
Latex:
Latex:
.....wf..... 
1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
3.  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  ((F  T)  \msubseteq{}r  Base))
4.  f  :  destructor\{i:l\}(T.F[T])
5.  x  :  urec(F)
6.  x  \mmember{}  F\^{}urec-level(f;x)  Void
7.  urec-level(f;x)  \mmember{}  \mBbbN{}
8.  n  :  \mBbbN{}
\mvdash{}  istype(x  \mmember{}  \mcup{}n:\mBbbN{}n.(F\^{}n  Void))
By
Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THEN  Fold  `prop`  0  THEN  BLemma  `base-member-prop`  THEN  Auto)
Home
Index