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