{ 
[i:Id]. [k:{k:Knd| 
hasloc(k;i)} ]. (kindname(i;k) 
MaName) }
{ Proof }
Definitions occuring in Statement :
kindname: kindname(i;k),
MaName: MaName,
hasloc: hasloc(k;i),
Knd: Knd,
Id: Id,
assert: b,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]}
Definitions :
uall: [x:A]. B[x],
member: t T,
MaName: MaName,
kindname: kindname(i;k),
prop: 
,
assert: b,
LocKnd: LocKnd,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
sq_type: SQType(T),
uimplies: b supposing a,
all: x:A. B[x],
implies: P 
Q,
guard: {T}
Lemmas :
Id_wf,
Knd_wf,
assert_wf,
hasloc_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_elim
\mforall{}[i:Id]. \mforall{}[k:\{k:Knd| \muparrow{}hasloc(k;i)\} ]. (kindname(i;k) \mmember{} MaName)
Date html generated:
2011_08_10-AM-07_52_09
Last ObjectModification:
2011_06_18-AM-08_14_26
Home
Index