{ 
[i:Id]. [k:Knd]. (locknd(i;k) 
LocKnd) }
{ Proof }
Definitions occuring in Statement :
locknd: locknd(i;k),
LocKnd: LocKnd,
Knd: Knd,
Id: Id,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
LocKnd: LocKnd,
locknd: locknd(i;k),
kindcase: kindcase(k;a.f[a];l,t.g[l; t]),
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
ifthenelse: if b then t else f fi ,
islocal: islocal(k),
lnk: lnk(k),
bnot: 
b,
isl: isl(x),
pi1: fst(t),
outl: outl(x),
btrue: tt,
bfalse: ff,
uimplies: b supposing a,
and: P 
Q,
Knd: Knd,
assert: 
b,
so_apply: x[s],
so_apply: x[s1;s2],
uiff: uiff(P;Q),
prop: 
,
false: False,
rcv: rcv(l,tg),
locl: locl(a)
Lemmas :
kindcase_wf,
Id_wf,
ldst_wf,
IdLnk_wf,
assert-hasloc,
rcv_wf,
assert_wf,
isrcv_wf,
locl_wf,
hasloc_wf,
Knd_wf
\mforall{}[i:Id]. \mforall{}[k:Knd]. (locknd(i;k) \mmember{} LocKnd)
Date html generated:
2011_08_10-AM-07_51_59
Last ObjectModification:
2011_06_18-AM-08_14_19
Home
Index