{ 
[a,b:Id]. uiff(data(a) = data(b);a = b) }
{ Proof }
Definitions occuring in Statement :
id-sdata: data(x),
sdata: SecurityData,
Id: Id,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
equal: s = t
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
member: t 
T,
and: P 
Q,
uimplies: b supposing a,
prop: 
,
Id: Id,
outl: outl(x),
assert: 
b,
isl: isl(x),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
cand: A c B,
sdata: SecurityData,
id-sdata: data(x),
sq_type: SQType(T),
all: x:A. B[x],
implies: P 
Q,
guard: {T}
Lemmas :
sdata_wf,
id-sdata_wf,
Id_wf,
tree_leaf_one_one,
member_wf,
outl_wf,
subtype_base_sq,
union_subtype_base,
atom2_subtype_base,
atom1_subtype_base
\mforall{}[a,b:Id]. uiff(data(a) = data(b);a = b)
Date html generated:
2011_08_17-PM-07_08_50
Last ObjectModification:
2011_06_18-PM-12_51_54
Home
Index