{ 
es:EO. m:
. f:m 
E.
((i:m - 1. (f i <loc f (i + 1))) 
(i:m. j:i + 1. f j 
loc f i )) }
{ Proof }
Definitions occuring in Statement :
es-le: e loc e' ,
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,
lelt: i j < k,
not: 
A,
prop: 
,
and: P 
Q,
le: A B,
false: False,
es-le: e loc e' ,
guard: {T},
or: P 
Q,
nat_plus: ,
decidable: Dec(P),
sq_type: SQType(T)
Lemmas :
es-increasing-sequence,
decidable__equal_int,
int_seg_wf,
es-locl_wf,
le_wf,
es-E_wf,
nat_plus_wf,
event_ordering_wf,
int_sq,
es-le_wf
\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 + 1. f j \mleq{}loc f i ))
Date html generated:
2011_08_16-AM-10_56_48
Last ObjectModification:
2010_09_24-PM-08_56_12
Home
Index