{ 
[a:Atom1]. [x,y:Id]. (<<data(a), data(y)>, data(x)> 
SecurityData) }
{ Proof }
Definitions occuring in Statement :
sdata-pair: <d1, d2>,
atom-sdata: data(a),
id-sdata: data(x),
sdata: SecurityData,
Id: Id,
uall: [x:A]. B[x],
member: t T,
atom: Atom$n
Definitions :
uall: [x:A]. B[x],
member: t T
Lemmas :
sdata-pair_wf,
atom-sdata_wf,
id-sdata_wf,
Id_wf
\mforall{}[a:Atom1]. \mforall{}[x,y:Id]. (<<data(a), data(y)>, data(x)> \mmember{} SecurityData)
Date html generated:
2011_08_17-PM-07_09_48
Last ObjectModification:
2011_06_18-PM-12_53_41
Home
Index