---

{ [k:Knd]. locl(act(k)) = k supposing islocal(k) }

{ Proof }

---

Definitions occuring in Statement :  actof: act(k),  locl: locl(a),  islocal: islocal(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,  islocal: islocal(k),  locl: locl(a),  actof: act(k),  member: t  T,  bnot: b,  isl: isl(x),  outr: outr(x),  btrue: tt,  bfalse: ff,  ifthenelse: if b then t else f fi ,  Knd: Knd,  false: False,  rcv: rcv(l,tg),  prop:
Lemmas :  false_wf,  locl_wf,  true_wf,  assert_wf,  islocal_wf,  Knd_wf

---

\mforall{}[k:Knd].  locl(act(k))  =  k  supposing  \muparrow{}islocal(k)


Date html generated: 2011_08_10-AM-07_46_03
Last ObjectModification: 2011_06_18-AM-08_11_54

Home Index