Nuprl Lemma : norm-lg_wf
[T:Type]. [N:id-fun(T)]. (norm-lg(N) 
id-fun(LabeledGraph(T))) supposing value-type(T)
Proof not projected
Definitions occuring in Statement :
norm-lg: norm-lg(N),
labeled-graph: LabeledGraph(T),
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
universe: Type,
id-fun: id-fun(T),
value-type: value-type(T)
Definitions :
all: x:A. B[x],
so_lambda: 
x.t[x],
norm-lg: norm-lg(N),
member: t T,
id-fun: id-fun(T),
uimplies: b supposing a,
uall: [x:A]. B[x],
implies: P 
Q,
prop: 
,
int_seg: {i..j
},
subtype: S 
T,
top: Top,
labeled-graph: LabeledGraph(T),
cand: A c
B,
and: P Q,
spreadn: spread3,
lelt: i 
j < k,
l_all: (xL.P[x]),
pi1: fst(t),
pi2: snd(t),
le: A B,
not: 
A,
false: False,
squash: 
T,
true: True,
so_apply: x[s],
nat: 
,
l_member: (x l),
exists: 
x:A. B[x],
sq_type: SQType(T),
guard: {T},
lg-size: lg-size(g)
Lemmas :
value-type_wf,
id-fun_wf,
int-value-type,
list-value-type,
norm-pair_wf,
product-value-type,
norm-list_wf,
labeled-graph_wf,
equal_wf,
subtype_rel_set_simple,
subtype_rel_self,
subtype_rel_simple_product,
subtype_rel_list,
lelt_wf,
nat_wf,
lg-size_wf,
int_seg_wf,
top_wf,
le_wf,
l_member_wf,
l_all_wf2,
list-set-type2,
less_than_wf,
and_wf,
subtype_base_sq,
list_subtype_base,
int_subtype_base,
pi2_wf,
pi1_wf_top,
select_wf,
length_wf,
length_wf_nat
\mforall{}[T:Type]. \mforall{}[N:id-fun(T)]. (norm-lg(N) \mmember{} id-fun(LabeledGraph(T))) supposing value-type(T)
Date html generated:
2012_01_23-PM-12_41_30
Last ObjectModification:
2011_12_20-PM-12_32_11
Home
Index