---

Step * 1 of Lemma ses-sign-has-atom


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)))))
BY
{ (GenConclAtAddr [1;2;1;2] THEN RepeatFor 2 (D -2) THEN Reduce 0) }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. ↑e ∈b Sign
6. v1 : SecurityData@i
7. v3 : Id@i
8. v4 : Atom1@i
9. Sign(e) = <v1, v3, v4> ∈ (SecurityData × Id × Atom1)@i
⊢ (↑e ∈b Sign) ∧ (¬a#<v1, v3, v4>:SecurityData × Id × Atom1) ⇐⇒ (↑e ∈b Sign) ∧ ((a = v4 ∈ Atom1) ∨ (a ∈ sdata-atoms(v1)\000C))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  a  :  Atom1@i
5.  \muparrow{}e  \mmember{}\msubb{}  Sign
\mvdash{}  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  (\mneg{}a\#Sign(e):SecurityData  \mtimes{}  Id  \mtimes{}  Atom1)
\mLeftarrow{}{}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  ((a  =  (snd(snd(Sign(e)))))  \mvee{}  (a  \mmember{}  sdata-atoms(fst(Sign(e)))))


By

---

Latex:
(GenConclAtAddr  [1;2;1;2]  THEN  RepeatFor  2  (D  -2)  THEN  Reduce  0)

---

Home Index