---

{ [i,j:Id]. [k1,k2:Knd].
    (locknd(i;k1) = locknd(j;k2)) supposing ((k1 = k2) and (isrcv(k1))) }

{ Proof }

---

Definitions occuring in Statement :  locknd: locknd(i;k),  LocKnd: LocKnd,  isrcv: isrcv(k),  Knd: Knd,  Id: Id,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  equal: s = t
Definitions :  uall: [x:A]. B[x],  Id: Id,  Knd: Knd,  uimplies: b supposing a,  member: t  T,  IdLnk: IdLnk,  all: x:A. B[x],  so_lambda: x.t[x],  prop: ,  rcv: rcv(l,tg),  lnk: lnk(k),  LocKnd: LocKnd,  locknd: locknd(i;k),  kindcase: kindcase(k;a.f[a];l,t.g[l; t]),  pi1: fst(t),  outl: outl(x),  ifthenelse: if b then t else f fi ,  islocal: islocal(k),  bnot: b,  isl: isl(x),  btrue: tt,  bfalse: ff,  and: P  Q,  sq_type: SQType(T),  so_apply: x[s],  implies: P  Q,  guard: {T},  rev_implies: P  Q,  iff: P  Q
Lemmas :  subtype_base_sq,  Knd_wf,  union_subtype_base,  IdLnk_wf,  product_subtype_base,  atom2_subtype_base,  isrcv-implies,  assert_wf,  isrcv_wf,  Id_wf,  ldst_wf,  lnk_wf,  hasloc_wf,  iff_weakening_uiff,  assert-hasloc

---

\mforall{}[i,j:Id].  \mforall{}[k1,k2:Knd].    (locknd(i;k1)  =  locknd(j;k2))  supposing  ((k1  =  k2)  and  (\muparrow{}isrcv(k1)))


Date html generated: 2011_08_10-AM-07_52_04
Last ObjectModification: 2011_06_18-AM-08_14_21

Home Index