---

Step * 1 1 1 2 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
6. v1 : SecurityData@i
7. v3 : Id@i
8. v4 : Atom1@i
9. Sign(e) = <v1, v3, v4> ∈ (SecurityData × Id × Atom1)@i
10. a#v1:SecurityData ∈ Type
11. ↑e ∈b Sign@i
12. (a = v4 ∈ Atom1) ∨ (a ∈ sdata-atoms(v1))@i
⊢ ¬(a#v1:SecurityData ∧ a#<v3, v4>:Id × Atom1)
BY
{ (At ⌈Type⌉ (D 0)⋅ THEN Auto) }

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
10. a#v1:SecurityData ∈ Type
11. ↑e ∈b Sign@i
12. (a = v4 ∈ Atom1) ∨ (a ∈ sdata-atoms(v1))@i
13. a#v1:SecurityData@i
14. a#<v3, v4>:Id × Atom1@i
⊢ False

---

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


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index