Nuprl Lemma : lg-label-wf_dag
∀[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 unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
ldag: LabeledDAG(T)
, 
subtype_rel: A ⊆r B
, 
nat: ℕ
Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledDAG(T)].  \mforall{}[i:\mBbbN{}lg-size(g)].    (lg-label(g;i)  \mmember{}  T)
Date html generated:
2016_05_17-AM-10_12_06
Last ObjectModification:
2015_12_29-PM-05_31_37
Theory : process-model
Home
Index