{
[a:Atom1].
(symmetric-key(a)
Key)
}
{
Proof
}
Definitions occuring in Statement
:
symmetric-key:
symmetric-key(a)
,
encryption-key:
Key
,
uall:
[x:A].
B[x]
,
member:
t
T
,
atom:
Atom$n
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
encryption-key:
Key
,
symmetric-key:
symmetric-key(a)
Lemmas
:
Id_wf
\mforall{}[a:Atom1]. (symmetric-key(a) \mmember{} Key)
Date html generated: 2011_08_17-PM-07_11_10
Last ObjectModification: 2011_06_18-PM-12_55_26
Home
Index
[x:A]. B[x], [a:Atom1]. (symmetric-key(a) 
Key) }[x:A]. B[x], T, [x:A]. B[x], T,