Nuprl Lemma : lg-label_wf

{

[T:Type].

[g:LabeledDAG(T)].

[i:

lg-size(g)]. (lg-label(g;i)

T) }

{ Proof }

Definitions occuring in Statement : ldag: LabeledDAG(T), lg-label: lg-label(g;x), lg-size: lg-size(g), int_seg: {i..j

}, uall:

[x:A]. B[x], member: t

T, natural_number: $n, universe: Type
Definitions : uall:

[x:A]. B[x], ldag: LabeledDAG(T), member: t

T, nat:

, prop:

Lemmas : lg-label_wf, int_seg_wf, lg-size_wf, nat_wf, labeled-graph_wf, is-dag_wf

\mforall{}[T:Type]. \mforall{}[g:LabeledDAG(T)]. \mforall{}[i:\mBbbN{}lg-size(g)]. (lg-label(g;i) \mmember{} T) Date html generated: 2011_08_16-PM-06_44_01 Last ObjectModification: 2011_06_18-AM-10_55_44 Home Index