---

{ [T:Type]
    g:LabeledGraph(T). i:lg-size(g). a,b:lg-size(g) - 1.
      (lg-connected(lg-remove(g;i);a;b)
       lg-connected(g;if a <z i then a else a + 1 fi ;if b <z i
         then b
         else b + 1
         fi )) }

{ Proof }

---

Definitions occuring in Statement :  lg-connected: lg-connected(g;a;b),  lg-remove: lg-remove(g;n),  lg-size: lg-size(g),  labeled-graph: LabeledGraph(T),  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  int_seg: {i..j},  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  subtract: n - m,  add: n + m,  natural_number: $n,  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  int_seg: {i..j},  implies: P  Q,  lg-connected: lg-connected(g;a;b),  member: t  T,  infix_ap: x f y,  rel_plus: R,  exists: x:A. B[x],  prop: ,  nat: ,  le: A  B,  not: A,  false: False,  lelt: i  j < k,  and: P  Q,  rel_exp: R^n,  ifthenelse: if b then t else f fi ,  ycomb: Y,  eq_int: (i = j),  btrue: tt,  bfalse: ff,  cand: A c B,  or: P  Q,  guard: {T},  nat_plus: ,  decidable: Dec(P),  sq_type: SQType(T),  uimplies: b supposing a,  iff: P  Q,  rev_implies: P  Q,  subtype: S  T
Lemmas :  lg-size-remove,  nat_plus_properties,  rel_exp_wf,  le_wf,  int_seg_wf,  lg-edge_wf,  lg-remove_wf,  lg-size_wf,  nat_wf,  decidable__equal_int,  subtype_base_sq,  int_subtype_base,  nat_plus_inc,  ifthenelse_wf,  lt_int_wf,  lg-connected_wf,  labeled-graph_wf,  int_seg_properties,  lg-edge-remove,  member_wf,  rel_exp_iff

---

\mforall{}[T:Type]
    \mforall{}g:LabeledGraph(T).  \mforall{}i:\mBbbN{}lg-size(g).  \mforall{}a,b:\mBbbN{}lg-size(g)  -  1.
        (lg-connected(lg-remove(g;i);a;b)
        {}\mRightarrow{}  lg-connected(g;if  a  <z  i  then  a  else  a  +  1  fi  ;if  b  <z  i  then  b  else  b  +  1  fi  ))


Date html generated: 2011_08_16-PM-06_40_43
Last ObjectModification: 2011_06_20-AM-01_59_45

Home Index