---

{ [T:Type]
    G:LabeledGraph(T). P:T  .
      (isl(lg-search(G;x.P[x]))  lg-exists(G;x.P[x])) }

{ Proof }

---

Definitions occuring in Statement :  lg-search: lg-search(G;x.P[x]),  lg-exists: lg-exists(G;x.P[x]),  labeled-graph: LabeledGraph(T),  isl: isl(x),  assert: b,  bool: ,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  iff: P  Q,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  lg-search: lg-search(G;x.P[x]),  lg-exists: lg-exists(G;x.P[x]),  let: let,  member: t  T,  iff: P  Q,  assert: b,  isl: isl(x),  ifthenelse: if b then t else f fi ,  so_apply: x[s],  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  btrue: tt,  bfalse: ff,  prop: ,  true: True,  false: False,  bool: ,  int_seg: {i..j},  nat: ,  unit: Unit,  lg-label2: lg-label2(g;x),  it:
Lemmas :  bool_wf,  labeled-graph_wf,  search_property,  lg-size_wf,  lg-label2_wf,  int_seg_wf,  nat_wf,  eq_int_wf,  search_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_eq_int,  false_wf,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff

---

\mforall{}[T:Type].  \mforall{}G:LabeledGraph(T).  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.    (\muparrow{}isl(lg-search(G;x.P[x]))  \mLeftarrow{}{}\mRightarrow{}  lg-exists(G;x.\muparrow{}P[x]))


Date html generated: 2011_08_16-PM-06_46_38
Last ObjectModification: 2011_06_18-AM-10_58_53

Home Index