{ 
[a,b:Atom1]. uiff(data(a) = data(b);a = b) }
{ Proof }
Definitions occuring in Statement :
atom-sdata: data(a),
sdata: SecurityData,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
equal: s = t,
atom: Atom$n
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
member: t 
T,
and: P 
Q,
uimplies: b supposing a,
prop: 
,
outr: outr(x),
assert: 
b,
bnot: 
b,
isl: isl(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
true: True,
sdata: SecurityData,
atom-sdata: data(a)
Lemmas :
sdata_wf,
atom-sdata_wf,
tree_leaf_one_one,
Id_wf,
outr_wf,
assert_wf,
bnot_wf,
isl_wf
\mforall{}[a,b:Atom1]. uiff(data(a) = data(b);a = b)
Date html generated:
2011_08_17-PM-07_09_00
Last ObjectModification:
2011_06_18-PM-12_52_10
Home
Index