---

Step * 4 1 1 1 2 of Lemma ses-act-has-atom


1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Key@i
5. a#<k, b>:Key × Atom1 ∈ Type
6. a#b:Atom1 ∈ Type
7. a#d:SecurityData ∈ Type
8. (a = b ∈ Atom1) ∨ (a ∈ sdata-atoms(d) @ encryption-key-atoms(k))@i
⊢ ¬(a#d:SecurityData ∧ a#<k, b>:Key × Atom1)
BY
{ (D 0 THEN Auto THEN D -3) }

1
1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Key@i
5. a#<k, b>:Key × Atom1 ∈ Type
6. a#b:Atom1 ∈ Type
7. a#d:SecurityData ∈ Type
8. a = b ∈ Atom1@i
9. a#d:SecurityData@i
10. a#<k, b>:Key × Atom1@i
⊢ False

2
1. a : Atom1@i
2. b : Atom1@i
3. d : SecurityData@i
4. k : Key@i
5. a#<k, b>:Key × Atom1 ∈ Type
6. a#b:Atom1 ∈ Type
7. a#d:SecurityData ∈ Type
8. (a ∈ sdata-atoms(d) @ encryption-key-atoms(k))@i
9. a#d:SecurityData@i
10. a#<k, b>:Key × Atom1@i
⊢ False

---

Latex:

---

Latex:

1.  a  :  Atom1@i
2.  b  :  Atom1@i
3.  d  :  SecurityData@i
4.  k  :  Key@i
5.  a\#<k,  b>:Key  \mtimes{}  Atom1  \mmember{}  Type
6.  a\#b:Atom1  \mmember{}  Type
7.  a\#d:SecurityData  \mmember{}  Type
8.  (a  =  b)  \mvee{}  (a  \mmember{}  sdata-atoms(d)  @  encryption-key-atoms(k))@i
\mvdash{}  \mneg{}(a\#d:SecurityData  \mwedge{}  a\#<k,  b>:Key  \mtimes{}  Atom1)


By

---

Latex:
(D  0  THEN  Auto  THEN  D  -3)

---

Home Index