Step * 1 2 1 1 1 2 of Lemma urec_induction

.....wf..... 
1. Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆Base)  ((F T) ⊆Base))
4. destructor{i:l}(T.F[T])
5. urec(F)
6. x ∈ F^urec-level(f;x) Void
7. urec-level(f;x) ∈ ℕ
8. : ℕ
⊢ istype(x ∈ ⋃n:ℕn.(F^n Void))
BY
(At ⌜Type⌝ (D 0)⋅ THEN Fold `prop` 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