{
[A:Id].
(PublicKey(A)
Key)
}
{
Proof
}
Definitions occuring in Statement
:
ses-public-key:
PublicKey(A)
,
encryption-key:
Key
,
Id:
Id
,
uall:
[x:A].
B[x]
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
encryption-key:
Key
,
ses-public-key:
PublicKey(A)
Lemmas
:
Id_wf
\mforall{}[A:Id]. (PublicKey(A) \mmember{} Key)
Date html generated: 2011_08_17-PM-07_16_34
Last ObjectModification: 2011_06_18-PM-01_06_29
Home
Index
[x:A]. B[x], [A:Id]. (PublicKey(A) 
Key) }[x:A]. B[x], T[x:A]. B[x], T,