---

{ [tg:Id]. [links:IdLnk List].
    (Rcvs(tg) on links  {k:Knd| isrcv(k)}  List) }

{ Proof }

---

Definitions occuring in Statement :  rcvs-on: Rcvs(tg) on links,  isrcv: isrcv(k),  Knd: Knd,  IdLnk: IdLnk,  Id: Id,  assert: b,  uall: [x:A]. B[x],  member: t  T,  set: {x:A| B[x]} ,  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  rcvs-on: Rcvs(tg) on links,  prop: ,  assert: b,  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True
Lemmas :  map_wf,  Knd_wf,  assert_wf,  isrcv_wf,  IdLnk_wf,  Id_wf,  rcv_wf

---

\mforall{}[tg:Id].  \mforall{}[links:IdLnk  List].    (Rcvs(tg)  on  links  \mmember{}  \{k:Knd|  \muparrow{}isrcv(k)\}    List)


Date html generated: 2011_08_10-AM-07_46_38
Last ObjectModification: 2011_06_18-AM-08_12_19

Home Index