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


1. SES@i'
2. es EO+(Info)@i'
3. E@i
4. 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))
BY
(RWO "free-from-atom-pair-iff" THENA Auto) }

1
1. SES@i'
2. es EO+(Info)@i'
3. E@i
4. 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:SecurityData ∧ a#<v3, v4>:Id × Atom1))
⇐⇒ (↑e ∈b Sign) ∧ ((a v4 ∈ Atom1) ∨ (a ∈ sdata-atoms(v1)))


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
6.  v1  :  SecurityData@i
7.  v3  :  Id@i
8.  v4  :  Atom1@i
9.  Sign(e)  =  <v1,  v3,  v4>@i
\mvdash{}  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  (\mneg{}a\#<v1,  v3,  v4>:SecurityData  \mtimes{}  Id  \mtimes{}  Atom1)
\mLeftarrow{}{}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  ((a  =  v4)  \mvee{}  (a  \mmember{}  sdata-atoms(v1)))


By


Latex:
(RWO  "free-from-atom-pair-iff"  0  THENA  Auto)




Home Index