---

Step * of Lemma ses-sign-has-atom

∀s:SES. ∀es:EO+(Info). ∀e:E. ∀a:Atom1.
  (Sign(e) has a ⇐⇒ (↑e ∈b Sign) ∧ ((a = signature(e) ∈ Atom1) ∨ (a ∈ sdata-atoms(signed(e)))))
BY
{ ((UnivCD THENA Auto) THEN Unfolds ``ses-sig ses-signed class-value-has`` 0 THEN (Decide ↑e ∈b Sign THENA Auto)) }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. ↑e ∈b Sign
⊢ (↑e ∈b Sign) ∧ (¬a#Sign(e):SecurityData × Id × Atom1)
⇐⇒ (↑e ∈b Sign) ∧ ((a = (snd(snd(Sign(e)))) ∈ Atom1) ∨ (a ∈ sdata-atoms(fst(Sign(e)))))

2
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. ¬↑e ∈b Sign
⊢ (↑e ∈b Sign) ∧ (¬a#Sign(e):SecurityData × Id × Atom1)
⇐⇒ (↑e ∈b Sign) ∧ ((a = (snd(snd(Sign(e)))) ∈ Atom1) ∨ (a ∈ sdata-atoms(fst(Sign(e)))))

---

Latex:

---

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}a:Atom1.
    (Sign(e)  has  a  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  ((a  =  signature(e))  \mvee{}  (a  \mmember{}  sdata-atoms(signed(e)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfolds  ``ses-sig  ses-signed  class-value-has``  0
  THEN  (Decide  \muparrow{}e  \mmember{}\msubb{}  Sign  THENA  Auto))

---

Home Index