Nuprl Lemma : MMTreeco_size_wf

[T:Type]. ∀[p:MMTreeco(T)].  (MMTreeco_size(p) ∈ partial(ℕ))


Proof




Definitions occuring in Statement :  MMTreeco_size: MMTreeco_size(p) MMTreeco: MMTreeco(T) partial: partial(T) nat: uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  fix_wf_corec-partial1 nat_wf set-value-type le_wf int-value-type nat-mono eq_atom_wf bool_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom eqtt_to_assert assert_of_eq_atom list_wf subtype_rel_product subtype_rel_list subtype_rel_wf strong-continuous-depproduct continuous-constant strong-continuous-list continuous-id subtype_rel_weakening atom_subtype_base false_wf inclusion-partial add-wf-partial-nat sum-partial-nat length_wf_nat select_wf sq_stable__le int_seg_wf length_wf partial_wf MMTreeco_wf
\mforall{}[T:Type].  \mforall{}[p:MMTreeco(T)].    (MMTreeco\_size(p)  \mmember{}  partial(\mBbbN{}))



Date html generated: 2015_07_17-AM-07_46_45
Last ObjectModification: 2015_01_27-AM-09_39_40

Home Index