Nuprl Lemma : ses-public-one-one
∀[A,B:Id]. uiff(PublicKey(A) = PublicKey(B) ∈ Key;A = B ∈ Id)
Proof
Definitions occuring in Statement :
ses-public-key: PublicKey(A),
encryption-key: Key,
Id: Id,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
and_wf,
equal_wf,
Id_wf,
outl_wf,
assert_wf,
isl_wf
Latex:
\mforall{}[A,B:Id]. uiff(PublicKey(A) = PublicKey(B);A = B)
Date html generated:
2015_07_23-PM-00_04_17
Last ObjectModification:
2015_01_29-AM-07_46_07
Home
Index