---

{ [T:Type]. [g:LabeledGraph(T)].
    [i:lg-size(g)]. lg-acyclic(lg-remove(g;i)) supposing lg-acyclic(g) }

{ Proof }

---

Definitions occuring in Statement :  lg-acyclic: lg-acyclic(g),  lg-remove: lg-remove(g;n),  lg-size: lg-size(g),  labeled-graph: LabeledGraph(T),  int_seg: {i..j},  uimplies: b supposing a,  uall: [x:A]. B[x],  natural_number: $n,  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  lg-acyclic: lg-acyclic(g),  int_seg: {i..j},  member: t  T,  all: x:A. B[x],  not: A,  implies: P  Q,  false: False,  lelt: i  j < k,  nat: ,  and: P  Q,  le: A  B,  rev_implies: P  Q,  iff: P  Q,  sq_type: SQType(T),  guard: {T},  prop:
Lemmas :  subtype_base_sq,  int_subtype_base,  ifthenelse_wf,  lt_int_wf,  int_seg_wf,  lg-size_wf,  nat_wf,  le_wf,  lg-connected_wf,  lg-remove_wf,  lg-acyclic_wf,  labeled-graph_wf,  lg-size-remove,  lg-connected-remove

---

\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].
    \mforall{}[i:\mBbbN{}lg-size(g)].  lg-acyclic(lg-remove(g;i))  supposing  lg-acyclic(g)


Date html generated: 2011_08_16-PM-06_41_05
Last ObjectModification: 2011_06_20-AM-02_00_14

Home Index