---

{ [T:Type]. g:LabeledGraph(T). a,b:lg-size(g).  Dec(lg-edge(g;a;b)) }

{ Proof }

---

Definitions occuring in Statement :  lg-edge: lg-edge(g;a;b),  lg-size: lg-size(g),  labeled-graph: LabeledGraph(T),  int_seg: {i..j},  decidable: Dec(P),  uall: [x:A]. B[x],  all: x:A. B[x],  natural_number: $n,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  lg-edge: lg-edge(g;a;b),  member: t  T,  subtype: S  T,  int_seg: {i..j},  implies: P  Q,  nat:
Lemmas :  decidable__l_member,  decidable__equal_int,  lg-in-edges_wf,  int_seg_wf,  lg-size_wf,  nat_wf,  labeled-graph_wf

---

\mforall{}[T:Type].  \mforall{}g:LabeledGraph(T).  \mforall{}a,b:\mBbbN{}lg-size(g).    Dec(lg-edge(g;a;b))


Date html generated: 2011_08_16-PM-06_40_18
Last ObjectModification: 2011_06_20-AM-01_59_17

Home Index