---

Step * of Lemma member-useable-atoms

∀s:SES
  (ActionsDisjoint
  ⇒ (∀es:EO+(Info). ∀e:E. ∀a:Atom1.
        ((a ∈ UseableAtoms(e))
        ⇐⇒ ((↑e ∈b Rcv) ∧ (a ∈ sdata-atoms(Rcv(e))))
            ∨ ((↑e ∈b Decrypt) ∧ (a ∈ sdata-atoms(plainText(e))))
            ∨ ((↑e ∈b New) ∧ (a = New(e) ∈ Atom1))
            ∨ ((↑e ∈b Sign) ∧ (a = signature(e) ∈ Atom1))
            ∨ ((↑e ∈b Encrypt) ∧ (a = cipherText(e) ∈ Atom1)))))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN Unfold `ses-useable-atoms` 0
   THEN Unfold `ses-disjoint` 2
   THEN ((InstHyp [⌈es⌉] 2⋅ THENM Thin 2) THENA Auto)
   THEN (D -1 THEN (InstHyp [⌈e⌉] (-1)⋅ THENA Auto) THEN Thin (-2))
   THEN SplitAndHyps
   THEN Repeat ((WeakAutoSplit THEN ThinTrivial THEN Try (Arith)))
   THEN ((RepeatFor 2 (D 0) THENA Auto)
         THEN SplitOrHyps
         THEN SplitAndHyps
         THEN ThinTrivial
         THEN Try (Arith)
         THEN Auto
         THEN AllHyps h.(RWO "member_singleton" h THEN Auto) ⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}a:Atom1.
                ((a  \mmember{}  UseableAtoms(e))
                \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  Rcv)  \mwedge{}  (a  \mmember{}  sdata-atoms(Rcv(e))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (a  \mmember{}  sdata-atoms(plainText(e))))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  New)  \mwedge{}  (a  =  New(e)))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  (a  =  signature(e)))
                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (a  =  cipherText(e))))))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  Unfold  `ses-useable-atoms`  0
  THEN  Unfold  `ses-disjoint`  2
  THEN  ((InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  2\mcdot{}  THENM  Thin  2)  THENA  Auto)
  THEN  (D  -1  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Thin  (-2))
  THEN  SplitAndHyps
  THEN  Repeat  ((WeakAutoSplit  THEN  ThinTrivial  THEN  Try  (Arith)))
  THEN  ((RepeatFor  2  (D  0)  THENA  Auto)
              THEN  SplitOrHyps
              THEN  SplitAndHyps
              THEN  ThinTrivial
              THEN  Try  (Arith)
              THEN  Auto
              THEN  AllHyps  h.(RWO  "member\_singleton"  h  THEN  Auto)  \mcdot{})\mcdot{})

---

Home Index