{ 
s:SES. es:EO+(Info).
[P:E 
E Atom1 
]
((e1,e2:E.
((x,y:E.
(e1 c
x
x c y
y c e2
((e1 < x) 
(y < e2))
(a:Atom1. (ses-flow(s;es;a;x;y) P[x;y;a]))))
(a:Atom1. (ses-flow(s;es;a;e1;e2) P[e1;e2;a]))))
{e1,e2:E. a:Atom1. (ses-flow(s;es;a;e1;e2) P[e1;e2;a])}) }
{ Proof }
Definitions occuring in Statement :
ses-flow: ses-flow(s;es;a;e1;e2),
ses-info: Info,
security-event-structure: SES,
event-ordering+: EO+(Info),
es-causle: e c e',
es-causl: (e < e'),
es-E: E,
uall: [x:A]. B[x],
prop: ,
guard: {T},
so_apply: x[s1;s2;s3],
all: x:A. B[x],
implies: P Q,
or: P Q,
function: x:A B[x],
atom: Atom$n
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
prop: ,
implies: P Q,
or: P Q,
so_apply: x[s1;s2;s3],
member: t 
T,
nat: 
,
le: A B,
ge: i 
j ,
not: 
A,
false: False,
guard: {T},
uimplies: b supposing a,
decidable: Dec(P),
ses-flow: ses-flow(s;es;a;e1;e2),
ycomb: Y,
and: P 
Q,
exists: 
x:A. B[x],
es-E-interface: E(X),
subtype: S 
T,
!hyp_hide: x
Lemmas :
es-E_wf,
event-ordering+_inc,
ses-info_wf,
es-causle_wf,
es-causl_wf,
ses-flow_wf,
event-ordering+_wf,
security-event-structure_wf,
nat_properties,
ge_wf,
nat_wf,
le_wf,
es-rank_wf,
es-rank_le,
es-rank_property,
decidable__es-causle,
es-causle_weakening_locl,
es-causl_transitivity1,
es-causl_transitivity2,
es-causle_weakening,
es-causl_weakening
\mforall{}s:SES. \mforall{}es:EO+(Info).
\mforall{}[P:E {}\mrightarrow{} E {}\mrightarrow{} Atom1 {}\mrightarrow{} \mBbbP{}]
((\mforall{}e1,e2:E.
((\mforall{}x,y:E.
(e1 c\mleq{} x
{}\mRightarrow{} x c\mleq{} y
{}\mRightarrow{} y c\mleq{} e2
{}\mRightarrow{} ((e1 < x) \mvee{} (y < e2))
{}\mRightarrow{} (\mforall{}a:Atom1. (ses-flow(s;es;a;x;y) {}\mRightarrow{} P[x;y;a]))))
{}\mRightarrow{} (\mforall{}a:Atom1. (ses-flow(s;es;a;e1;e2) {}\mRightarrow{} P[e1;e2;a]))))
{}\mRightarrow{} \{\mforall{}e1,e2:E. \mforall{}a:Atom1. (ses-flow(s;es;a;e1;e2) {}\mRightarrow{} P[e1;e2;a])\})
Date html generated:
2011_08_17-PM-07_19_29
Last ObjectModification:
2011_06_18-PM-01_11_48
Home
Index