---

Step * of Lemma ses-public-one-one

∀[A,B:Id].  uiff(PublicKey(A) = PublicKey(B) ∈ Key;A = B ∈ Id)
BY
{ (Unfolds``encryption-key ses-public-key`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Id].    uiff(PublicKey(A)  =  PublicKey(B);A  =  B)


By

---

Latex:
(Unfolds``encryption-key  ses-public-key``  0  THEN  Auto)

---

Home Index