---

Step * of Lemma ses-msg-cases

∀[ses:SES]
  ∀[es:EO+(Info)]
    ((∀[e:E]. isMsg(e) ~ ff supposing ↑e ∈b Sign)
    ∧ (∀[e:E]. isMsg(e) ~ ff supposing ↑e ∈b Verify)
    ∧ (∀[e:E]. isMsg(e) ~ ff supposing ↑e ∈b Encrypt)
    ∧ (∀[e:E]. isMsg(e) ~ ff supposing ↑e ∈b Decrypt)
    ∧ (∀[e:E]. isMsg(e) ~ ff supposing ↑e ∈b New)
    ∧ (∀[e:E]. isMsg(e) ~ tt supposing ↑e ∈b Send)
    ∧ (∀[e:E]. isMsg(e) ~ tt supposing ↑e ∈b Rcv)) 
  supposing ActionsDisjoint
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (SplitAndConcl
         THEN RepeatFor 2 ((D 0 THENA Auto))
         THEN (Unfold `ses-disjoint` 2
               THEN (Unfold `ses-msg` 0
                     THEN ((InstHyp [⌜es⌝] 2⋅ THENA Auto) THEN ExRepD)
                     THEN ((InstHyp [⌜e⌝] (-1)⋅ THENA Auto)
                           THEN SplitAndHyps
                           THEN ThinTrivial
                           THEN (AutoBoolCase ⌜e ∈b Send⌝⋅ THENA Auto)
                           THEN ThinTrivial
                           THEN Try (Arith⋅))
                     THEN (AutoBoolCase ⌜e ∈b Rcv⌝⋅ THENA Auto)
                     THEN ThinTrivial
                     THEN Try (Arith⋅))⋅
               )⋅)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[ses:SES]
    \mforall{}[es:EO+(Info)]
        ((\mforall{}[e:E].  isMsg(e)  \msim{}  ff  supposing  \muparrow{}e  \mmember{}\msubb{}  Sign)
        \mwedge{}  (\mforall{}[e:E].  isMsg(e)  \msim{}  ff  supposing  \muparrow{}e  \mmember{}\msubb{}  Verify)
        \mwedge{}  (\mforall{}[e:E].  isMsg(e)  \msim{}  ff  supposing  \muparrow{}e  \mmember{}\msubb{}  Encrypt)
        \mwedge{}  (\mforall{}[e:E].  isMsg(e)  \msim{}  ff  supposing  \muparrow{}e  \mmember{}\msubb{}  Decrypt)
        \mwedge{}  (\mforall{}[e:E].  isMsg(e)  \msim{}  ff  supposing  \muparrow{}e  \mmember{}\msubb{}  New)
        \mwedge{}  (\mforall{}[e:E].  isMsg(e)  \msim{}  tt  supposing  \muparrow{}e  \mmember{}\msubb{}  Send)
        \mwedge{}  (\mforall{}[e:E].  isMsg(e)  \msim{}  tt  supposing  \muparrow{}e  \mmember{}\msubb{}  Rcv)) 
    supposing  ActionsDisjoint


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (SplitAndConcl
              THEN  RepeatFor  2  ((D  0  THENA  Auto))
              THEN  (Unfold  `ses-disjoint`  2
                          THEN  (Unfold  `ses-msg`  0
                                      THEN  ((InstHyp  [\mkleeneopen{}es\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  ExRepD)
                                      THEN  ((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                                                  THEN  SplitAndHyps
                                                  THEN  ThinTrivial
                                                  THEN  (AutoBoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  Send\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                  THEN  ThinTrivial
                                                  THEN  Try  (Arith\mcdot{}))
                                      THEN  (AutoBoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  Rcv\mkleeneclose{}\mcdot{}  THENA  Auto)
                                      THEN  ThinTrivial
                                      THEN  Try  (Arith\mcdot{}))\mcdot{}
                          )\mcdot{})\mcdot{}
  )

---

Home Index