---

{ [T:Type]. [L:T List].  (make-lg(L)  LabeledDAG(T)) }

{ Proof }

---

Definitions occuring in Statement :  ldag: LabeledDAG(T),  make-lg: make-lg(L),  uall: [x:A]. B[x],  member: t  T,  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  ldag: LabeledDAG(T),  is-dag: is-dag(g),  make-lg: make-lg(L),  all: x:A. B[x],  lg-size: lg-size(g),  implies: P  Q,  lg-edge: lg-edge(g;a;b),  lg-in-edges: lg-in-edges(g;x),  pi1: fst(t),  pi2: snd(t),  top: Top,  subtype: S  T,  prop: ,  int_seg: {i..j},  false: False,  iff: P  Q,  and: P  Q
Lemmas :  make-lg_wf,  is-dag_wf,  length-map-sq,  top_wf,  select-map,  nil_member,  int_seg_properties,  length_wf1,  l_member_wf,  int_seg_wf

---

\mforall{}[T:Type].  \mforall{}[L:T  List].    (make-lg(L)  \mmember{}  LabeledDAG(T))


Date html generated: 2011_08_16-PM-06_43_47
Last ObjectModification: 2011_06_18-AM-10_55_24

Home Index