### Nuprl Lemma : norm-lg_wf

`∀[T:Type]. ∀[N:id-fun(T)]. (norm-lg(N) ∈ id-fun(LabeledGraph(T))) supposing value-type(T)`

Proof

Definitions occuring in Statement :  norm-lg: `norm-lg(N)` labeled-graph: `LabeledGraph(T)` id-fun: `id-fun(T)` value-type: `value-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Lemmas :  norm-list_wf list_wf product-value-type norm-pair_wf list-value-type int-value-type equal-wf-base int_subtype_base id-fun_wf value-type_wf labeled-graph_wf set_wf equal_wf length_wf_nat top_wf dep-isect-subtype int_seg_wf length_wf subtype_rel_list nat_wf subtype_rel_product subtype_base_sq set_subtype_base le_wf zero-le-nat list-set-type2 l_all_wf2 l_member_wf less_than_wf lg-size_wf l_all_iff nat_properties list_subtype_base and_wf pi2_wf pi1_wf_top subtype_top select_wf decidable__lt false_wf less-iff-le add_functionality_wrt_le add-swap add-commutes le-add-cancel sq_stable__le equal_functionality_wrt_subtype_rel2

Latex:
\mforall{}[T:Type].  \mforall{}[N:id-fun(T)].  (norm-lg(N)  \mmember{}  id-fun(LabeledGraph(T)))  supposing  value-type(T)

Date html generated: 2015_07_23-AM-11_05_06
Last ObjectModification: 2015_01_28-PM-11_36_06

Home Index