Nuprl 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
Proof
Definitions occuring in Statement :
ses-msg: isMsg(e),
ses-disjoint: ActionsDisjoint,
ses-decrypt: Decrypt,
ses-encrypt: Encrypt,
ses-verify: Verify,
ses-sign: Sign,
ses-rcv: Rcv,
ses-send: Send,
ses-new: New,
ses-info: Info,
security-event-structure: SES,
in-eclass: e ∈b X,
event-ordering+: EO+(Info),
es-E: E,
assert: ↑b,
bfalse: ff,
btrue: tt,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
ses-disjoint: ActionsDisjoint,
ses-msg: isMsg(e),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
cand: A c∧ B,
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
top: Top,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
not: ¬A,
prop: ℙ,
bfalse: ff,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
true: True
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
Date html generated:
2016_05_17-PM-00_29_30
Last ObjectModification:
2016_01_18-AM-07_44_01
Theory : event-logic-applications
Home
Index