{ 
[s:SES]. [es:EO+(Info)]. [thr:E List].
(thread-messages(thr) 
{e:E| (
e 
Send) 
(e Rcv)} List) }
{ Proof }
Definitions occuring in Statement :
thread-messages: thread-messages(thr),
ses-rcv: Rcv,
ses-send: Send,
ses-info: Info,
security-event-structure: SES,
in-eclass: e X,
event-ordering+: EO+(Info),
es-E: E,
assert: b,
uall: [x:A]. B[x],
or: P Q,
member: t T,
set: {x:A| B[x]} ,
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
thread-messages: thread-messages(thr),
ses-msg: isMsg(e),
or: P Q,
bor: p q,
all: x:A. B[x],
top: Top,
so_lambda: 
x y.t[x; y],
prop: 
,
implies: P 
Q,
so_lambda: x.t[x],
guard: {T},
bfalse: ff,
ifthenelse: if b then t else f fi ,
and: P 
Q,
uimplies: b supposing a,
so_apply: x[s1;s2],
so_apply: x[s],
decidable: Dec(P),
subtype: S 
T
Lemmas :
es-E_wf,
event-ordering+_inc,
ses-info_wf,
event-ordering+_wf,
security-event-structure_wf,
filter_type,
bor_wf,
in-eclass_wf,
ses-send_wf,
es-interface-subtype_rel2,
sdata_wf,
top_wf,
ses-rcv_wf,
subtype_rel_list,
assert_wf,
subtype_rel_sets,
subtype_rel_self,
decidable__assert,
not_assert_elim,
bool_wf
\mforall{}[s:SES]. \mforall{}[es:EO+(Info)]. \mforall{}[thr:E List].
(thread-messages(thr) \mmember{} \{e:E| (\muparrow{}e \mmember{}\msubb{} Send) \mvee{} (\muparrow{}e \mmember{}\msubb{} Rcv)\} List)
Date html generated:
2011_08_17-PM-07_31_21
Last ObjectModification:
2011_06_18-PM-01_24_08
Home
Index