{ 
[A:Id]. (encryption-key-atoms(PublicKey(A)) ~ []) }
{ Proof }
Definitions occuring in Statement :
ses-public-key: PublicKey(A),
encryption-key-atoms: encryption-key-atoms(k),
Id: Id,
uall: [x:A]. B[x],
nil: [],
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
encryption-key-atoms: encryption-key-atoms(k),
ses-public-key: PublicKey(A),
member: t 
T
Lemmas :
Id_wf
\mforall{}[A:Id]. (encryption-key-atoms(PublicKey(A)) \msim{} [])
Date html generated:
2011_08_17-PM-07_17_14
Last ObjectModification:
2011_06_18-PM-01_07_40
Home
Index