---

{ [a:Id  Id  Id]. [b:Id]. [S:Id List]. [G:Graph(S)]. [k:Knd].
    (graph-rcvset(a;b;S;G;k)  ) }

{ Proof }

---

Definitions occuring in Statement :  graph-rcvset: graph-rcvset(a;b;S;G;k),  id-graph: Graph(S),  Knd: Knd,  Id: Id,  bool: ,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  graph-rcvset: graph-rcvset(a;b;S;G;k),  band: p  q,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  prop: ,  ifthenelse: if b then t else f fi ,  bfalse: ff,  subtype: S  T,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  uimplies: b supposing a,  it:
Lemmas :  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  eq_id_wf,  tagof_wf,  uiff_transitivity,  assert-eq-id,  lname_wf,  lnk_wf,  lsrc_wf,  ldst_wf,  deq-member_wf,  iff_transitivity,  l_member_wf,  assert-deq-member,  Id_wf,  id-deq_wf,  bnot_wf,  not_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_iff,  bfalse_wf,  not_functionality_wrt_uiff,  Knd_wf,  id-graph_wf

---

\mforall{}[a:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id].  \mforall{}[b:Id].  \mforall{}[S:Id  List].  \mforall{}[G:Graph(S)].  \mforall{}[k:Knd].    (graph-rcvset(a;b;S;G;k)  \mmember{}  \mBbbB{})


Date html generated: 2011_08_10-AM-07_50_41
Last ObjectModification: 2011_06_18-AM-08_13_43

Home Index