{ 
[s:SES]. [a:Atom1]. (encryption-key-atoms(symmetric-key(a)) ~ [a]) }
{ Proof }
Definitions occuring in Statement :
security-event-structure: SES,
encryption-key-atoms: encryption-key-atoms(k),
symmetric-key: symmetric-key(a),
uall: [x:A]. B[x],
cons: [car / cdr],
nil: [],
sqequal: s ~ t,
atom: Atom$n
Definitions :
uall: [x:A]. B[x],
encryption-key-atoms: encryption-key-atoms(k),
symmetric-key: symmetric-key(a),
member: t 
T
Lemmas :
security-event-structure_wf
\mforall{}[s:SES]. \mforall{}[a:Atom1]. (encryption-key-atoms(symmetric-key(a)) \msim{} [a])
Date html generated:
2011_08_17-PM-07_17_34
Last ObjectModification:
2011_06_18-PM-01_08_16
Home
Index