Nuprl Lemma : lg-out-edges_wf

[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)].  (lg-out-edges(g;x) ∈ ℕlg-size(g) List)


Proof




Definitions occuring in Statement :  lg-out-edges: lg-out-edges(g;x) lg-size: lg-size(g) labeled-graph: LabeledGraph(T) list: List int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T natural_number: $n universe: Type
Lemmas :  length_wf_nat top_wf dep-isect-subtype list_wf int_seg_wf length_wf select_wf nat_wf sq_stable__le lg-size_wf labeled-graph_wf

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].  \mforall{}[x:\mBbbN{}lg-size(g)].    (lg-out-edges(g;x)  \mmember{}  \mBbbN{}lg-size(g)  List)



Date html generated: 2015_07_22-PM-00_28_43
Last ObjectModification: 2015_01_28-PM-11_32_48

Home Index