Nuprl Lemma : C_TYPEco_size_wf
∀[p:C_TYPEco()]. (C_TYPEco_size(p) ∈ partial(ℕ))
Proof
Definitions occuring in Statement : 
C_TYPEco_size: C_TYPEco_size(p)
, 
C_TYPEco: C_TYPEco()
, 
partial: partial(T)
, 
nat: ℕ
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Lemmas : 
fix_wf_corec-partial1, 
nat_wf, 
set-value-type, 
le_wf, 
int-value-type, 
nat-mono, 
eq_atom_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_eq_atom, 
unit_wf2, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
list_wf, 
subtype_rel_product, 
subtype_rel_self, 
subtype_rel_list, 
subtype_rel_wf, 
strong-continuous-depproduct, 
continuous-constant, 
strong-continuous-list, 
strong-continuous-product, 
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, 
C_TYPEco_wf
\mforall{}[p:C\_TYPEco()].  (C\_TYPEco\_size(p)  \mmember{}  partial(\mBbbN{}))
Date html generated:
2015_07_17-AM-07_42_02
Last ObjectModification:
2015_01_27-AM-09_47_51
Home
Index