{ 
[s:SES]. [es:EO+(Info)]. [thr:Thread]. no_repeats(Act;thr) }
{ Proof }
Definitions occuring in Statement :
ses-thread: Thread,
ses-act: Act,
ses-info: Info,
security-event-structure: SES,
event-ordering+: EO+(Info),
uall: [x:A]. B[x],
no_repeats: no_repeats(T;l)
Definitions :
member: t 
T,
and: P 
Q,
lelt: i 
j < k,
so_lambda: 
x y.t[x; y],
sorted-by: sorted-by(R;L),
int_seg: {i..j
},
all: x:A. B[x],
false: False,
implies: P 
Q,
not: 
A,
prop: 
,
uall: [x:A]. B[x],
le: A B,
uimplies: b supposing a,
ses-thread: Thread
Lemmas :
ses-thread-order,
int_seg_wf,
ses-act_wf,
length_wf1,
le_wf
\mforall{}[s:SES]. \mforall{}[es:EO+(Info)]. \mforall{}[thr:Thread]. no\_repeats(Act;thr)
Date html generated:
2011_08_17-PM-07_32_27
Last ObjectModification:
2011_06_18-PM-01_25_40
Home
Index