---

Step * of Lemma ses-signature-unique2

∀[s:SES]
  ∀[es:EO+(Info)]. ∀[a,b:E(Sign)].
    {(signed(a) = signed(b) ∈ SecurityData) ∧ (signer(a) = signer(b) ∈ Id)} 
    supposing signature(a) = signature(b) ∈ Atom1 
  supposing PropertyO
BY
{ (InstLemma `ses-signature-unique` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN RepeatFor 2 ((ParallelLast THENA Auto))
   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
⊢ {(signed(a) = signed(b) ∈ SecurityData) ∧ (signer(a) = signer(b) ∈ Id)}

---

Latex:

---

Latex:
\mforall{}[s:SES]
    \mforall{}[es:EO+(Info)].  \mforall{}[a,b:E(Sign)].
        \{(signed(a)  =  signed(b))  \mwedge{}  (signer(a)  =  signer(b))\}  supposing  signature(a)  =  signature(b) 
    supposing  PropertyO


By

---

Latex:
(InstLemma  `ses-signature-unique`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  RepeatFor  2  ((ParallelLast  THENA  Auto))
  THEN  Auto)

---

Home Index