---

Step * 1 of Lemma ses-signature-unique2


1. s : SES
2. PropertyO
3. es : EO+(Info)
4. a : E(Sign)
5. ∀[b:E(Sign)]. Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1) supposing signature(a) = signature(b) ∈ Atom1
6. b : E(Sign)
7. signature(a) = signature(b) ∈ Atom1
⊢ {(signed(a) = signed(b) ∈ SecurityData) ∧ (signer(a) = signer(b) ∈ Id)}
BY
{ (InstHyp [⌈b⌉] (-3)⋅ THEN Auto) }

1
1. s : SES
2. PropertyO
3. es : EO+(Info)
4. a : E(Sign)
5. ∀[b:E(Sign)]. Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1) supposing signature(a) = signature(b) ∈ Atom1
6. b : E(Sign)
7. signature(a) = signature(b) ∈ Atom1
8. Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1)
⊢ {(signed(a) = signed(b) ∈ SecurityData) ∧ (signer(a) = signer(b) ∈ Id)}

---

Latex:

---

Latex:

1.  s  :  SES
2.  PropertyO
3.  es  :  EO+(Info)
4.  a  :  E(Sign)
5.  \mforall{}[b:E(Sign)].  Sign(a)  =  Sign(b)  supposing  signature(a)  =  signature(b)
6.  b  :  E(Sign)
7.  signature(a)  =  signature(b)
\mvdash{}  \{(signed(a)  =  signed(b))  \mwedge{}  (signer(a)  =  signer(b))\}


By

---

Latex:
(InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)

---

Home Index