---

Step * of Lemma ses-D-implies

∀s:SES. (PropertyD ⇒ {ses-D-public(s) ∧ ses-D-private(s)} supposing PropertyK)
BY
{ (Auto
   THEN Unfold `ses-D` 2
   THEN (D 0 THEN UnfoldTopAb 0 THEN ParallelOp 2 THEN Thin 2)
   THEN (Auto
         THEN (InstHyp [⌜e⌝] 4⋅ THENA Auto)
         THEN (Unfolds ``ses-decrypted ses-cipher ses-decryption-key`` -1
               THEN Unfolds ``ses-crypt ses-encrypted ses-encryption-key`` -1
               )
         THEN (HypSubst' (-2) (-1)
               THEN Reduce (-1)
               THEN ParallelLast
               THEN Auto
               THEN (Unfold `ses-K` 2 THEN Auto)
               THEN Thin (-1)
               THEN ((FHyp 4 [-1] ORELSE FHyp 3 [-1]) THENA Auto)
               THEN Thin (-2)
               THEN RepeatFor 3 (MoveToConcl (-1))
               THEN GenConclAtAddr[1;3;1]
               THEN RepeatFor 2 (D -2)
               THEN Reduce 0
               THEN Auto)⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}s:SES.  (PropertyD  {}\mRightarrow{}  \{ses-D-public(s)  \mwedge{}  ses-D-private(s)\}  supposing  PropertyK)


By

---

Latex:
(Auto
  THEN  Unfold  `ses-D`  2
  THEN  (D  0  THEN  UnfoldTopAb  0  THEN  ParallelOp  2  THEN  Thin  2)
  THEN  (Auto
              THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
              THEN  (Unfolds  ``ses-decrypted  ses-cipher  ses-decryption-key``  -1
                          THEN  Unfolds  ``ses-crypt  ses-encrypted  ses-encryption-key``  -1
                          )
              THEN  (HypSubst'  (-2)  (-1)
                          THEN  Reduce  (-1)
                          THEN  ParallelLast
                          THEN  Auto
                          THEN  (Unfold  `ses-K`  2  THEN  Auto)
                          THEN  Thin  (-1)
                          THEN  ((FHyp  4  [-1]  ORELSE  FHyp  3  [-1])  THENA  Auto)
                          THEN  Thin  (-2)
                          THEN  RepeatFor  3  (MoveToConcl  (-1))
                          THEN  GenConclAtAddr[1;3;1]
                          THEN  RepeatFor  2  (D  -2)
                          THEN  Reduce  0
                          THEN  Auto)\mcdot{})\mcdot{})

---

Home Index