Nuprl Lemma : lg-size_wf
[T:Type]. [g:LabeledGraph(T)]. (lg-size(g) 
)
Proof not projected
Definitions occuring in Statement :
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
nat: ,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
implies: P 
Q,
all: x:A. B[x],
member: t T,
uall: [x:A]. B[x],
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T)
Lemmas :
labeled-graph_wf,
top_wf,
length_wf_nat
\mforall{}[T:Type]. \mforall{}[g:LabeledGraph(T)]. (lg-size(g) \mmember{} \mBbbN{})
Date html generated:
2012_01_23-PM-12_36_20
Last ObjectModification:
2011_12_13-PM-05_47_24
Home
Index