---

{ [k:Knd]. k = rcv(lnk(k),tag(k)) supposing isrcv(k) }

{ Proof }

---

Definitions occuring in Statement :  tagof: tag(k),  lnk: lnk(k),  rcv: rcv(l,tg),  isrcv: isrcv(k),  Knd: Knd,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  equal: s = t
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  assert: b,  isrcv: isrcv(k),  rcv: rcv(l,tg),  lnk: lnk(k),  tagof: tag(k),  member: t  T,  implies: P  Q,  isl: isl(x),  pi1: fst(t),  outl: outl(x),  pi2: snd(t),  btrue: tt,  bfalse: ff,  ifthenelse: if b then t else f fi ,  Knd: Knd,  false: False,  prop:
Lemmas :  rcv_wf,  true_wf,  false_wf,  assert_wf,  isrcv_wf,  Knd_wf

---

\mforall{}[k:Knd].  k  =  rcv(lnk(k),tag(k))  supposing  \muparrow{}isrcv(k)


Date html generated: 2011_08_10-AM-07_47_10
Last ObjectModification: 2011_06_18-AM-08_12_33

Home Index