---

Step * of Lemma ses-cipher-unique2

∀[s:SES]
  ∀[es:EO+(Info)]. ∀[a,b:E(Encrypt)].
    {(plainText(a) = plainText(b) ∈ SecurityData) ∧ (key(a) = key(b) ∈ Key)} 
    supposing cipherText(a) = cipherText(b) ∈ Atom1 
  supposing PropertyO
BY
{ RemoveUniform Auto Auto }

1
∀s:SES
  (PropertyO
  ⇒ (∀es:EO+(Info). ∀a,b:E(Encrypt).
        ((cipherText(a) = cipherText(b) ∈ Atom1)
        ⇒ {(plainText(a) = plainText(b) ∈ SecurityData) ∧ (key(a) = key(b) ∈ Key)})))

---

Latex:

---

Latex:
\mforall{}[s:SES]
    \mforall{}[es:EO+(Info)].  \mforall{}[a,b:E(Encrypt)].
        \{(plainText(a)  =  plainText(b))  \mwedge{}  (key(a)  =  key(b))\}  supposing  cipherText(a)  =  cipherText(b) 
    supposing  PropertyO


By

---

Latex:
RemoveUniform  Auto  Auto

---

Home Index