Nuprl Lemma : lg-nil_wf_dag
∀[T:Type]. (lg-nil() ∈ LabeledDAG(T))
Proof
Definitions occuring in Statement :
ldag: LabeledDAG(T),
lg-nil: lg-nil(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
lg-nil_wf,
is-dag_wf,
length_of_nil_lemma,
less_than_transitivity1,
less_than_irreflexivity,
int_seg_wf
Latex:
\mforall{}[T:Type]. (lg-nil() \mmember{} LabeledDAG(T))
Date html generated:
2015_07_23-AM-11_04_39
Last ObjectModification:
2015_01_28-PM-11_34_11
Home
Index