Nuprl Lemma : lg-label_wf
[T:Type]. [g:LabeledGraph(T)]. [x:
lg-size(g)]. (lg-label(g;x) 
T)
Proof not projected
Definitions occuring in Statement :
lg-label: lg-label(g;x),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
int_seg: {i..j
},
uall: [x:A]. B[x],
member: t T,
natural_number: $n,
universe: Type
Definitions :
so_lambda: 
x.t[x],
all: x:A. B[x],
nat: ,
false: False,
implies: P 
Q,
not: 
A,
le: A 
B,
lg-label: lg-label(g;x),
member: t T,
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
and: P 
Q,
lelt: i j < k,
uimplies: b supposing a,
int_seg: {i..j}
Lemmas :
length_wf,
Error :dep-isect_wf,
int_seg_wf,
nat_wf,
lg-size_wf,
top_wf,
select_wf,
pi1_wf_top,
subtype_rel_self,
subtype_rel_simple_product,
subtype_rel_list
\mforall{}[T:Type]. \mforall{}[g:LabeledGraph(T)]. \mforall{}[x:\mBbbN{}lg-size(g)]. (lg-label(g;x) \mmember{} T)
Date html generated:
2012_01_23-PM-12_38_16
Last ObjectModification:
2011_12_14-PM-11_59_08
Home
Index