---

Step * of Lemma ses-signature-unique

∀[s:SES]
  ∀[es:EO+(Info)]. ∀[a,b:E(Sign)].
    Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1) supposing signature(a) = signature(b) ∈ Atom1 
  supposing PropertyO
BY
{ (Auto THEN RepeatFor 3 (MoveToConcl (-1)) THEN CausalInd' THEN Auto) }

1
1. s : SES
2. PropertyO
3. es : EO+(Info)
4. a : E(Sign)@i
5. ∀a1:E(Sign)
     ((a1 < a)
     ⇒ (∀b:E(Sign). ((signature(a1) = signature(b) ∈ Atom1) ⇒ (Sign(a1) = Sign(b) ∈ (SecurityData × Id × Atom1)))))
6. b : E(Sign)@i
7. signature(a) = signature(b) ∈ Atom1@i
⊢ Sign(a) = Sign(b) ∈ (SecurityData × Id × Atom1)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  3  (MoveToConcl  (-1))  THEN  CausalInd'  THEN  Auto)

---

Home Index