{ 
es:EO. m:
. f:m 
E.
((i:m - 1. (f i <loc f (i + 1))) 
(i:m. j:i. (f j <loc f i))) }
{ Proof }
Definitions occuring in Statement :
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
int_seg: {i..j
},
nat_plus: ,
all: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions :
all: x:A. B[x],
int_seg: {i..j},
implies: P Q,
member: t 
T,
prop: 
,
lelt: i 
j < k,
and: P 
Q,
le: A B,
not: 
A,
false: False,
ge: i 
j ,
nat_plus: ,
nat: ,
decidable: Dec(P),
or: P 
Q,
sq_type: SQType(T),
guard: {T},
trans: Trans(T;x,y.E[x; y])
Lemmas :
int_seg_wf,
es-locl_wf,
le_wf,
es-E_wf,
nat_plus_wf,
event_ordering_wf,
nat_wf,
nat_properties,
ge_wf,
decidable__equal_int,
int_sq,
es-locl-trans
\mforall{}es:EO. \mforall{}m:\mBbbN{}\msupplus{}. \mforall{}f:\mBbbN{}m {}\mrightarrow{} E. ((\mforall{}i:\mBbbN{}m - 1. (f i <loc f (i + 1))) {}\mRightarrow{} (\mforall{}i:\mBbbN{}m. \mforall{}j:\mBbbN{}i. (f j <loc f i)))
Date html generated:
2011_08_16-AM-10_56_43
Last ObjectModification:
2010_09_24-PM-08_56_18
Home
Index