{ 
the_es:EO. e,e',y:E. (e' before y 
before(e) 
(e' <loc y)) }
{ Proof }
Definitions occuring in Statement :
es-before: before(e),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
all: x:A. B[x],
implies: P Q,
l_before: x before y l
Definitions :
member: t T,
prop: 
,
all: x:A. B[x],
implies: P Q,
rev_implies: P 
Q,
iff: P Q,
so_lambda: 
x.t[x],
and: P 
Q,
not: 
A,
exists: 
x:A. B[x],
length: ||as||,
ycomb: Y,
squash: 
T,
true: True,
subtype: S 
T,
suptype: suptype(S; T),
le: A 
B,
ge: i 
j ,
label: ...$L... t,
false: False,
top: Top,
l_member: (x l),
nat: 
,
cand: A c B,
or: P 
Q,
so_apply: x[s],
guard: {T},
decidable: Dec(P),
l_before: x before y l,
sublist: L1 L2,
int_seg: {i..j
},
increasing: increasing(f;k),
select: l[i],
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
bfalse: ff,
btrue: tt,
lelt: i j < k
Lemmas :
es-first_wf,
bool_wf,
assert_wf,
bnot_wf,
not_wf,
l_before_wf,
es-locl_wf,
false_wf,
all_functionality_wrt_iff,
implies_functionality_wrt_iff,
nil_before,
decidable__es-E-equal,
es-pred_wf,
append_wf,
es-before_wf,
member-es-before,
int_seg_wf,
squash_wf,
true_wf,
length_append,
increasing_wf,
length_wf1,
select_wf,
length_nil,
length_wf_nat,
top_wf,
length_cons,
non_neg_length,
es-before_wf2,
Id_wf,
es-loc_wf,
select_append_front,
le_wf,
es-pred-locl,
not_functionality_wrt_iff,
l_member_wf,
cons_member,
l_before_append_front,
or_functionality_wrt_iff,
nil_member
\mforall{}the$_{es}$:EO. \mforall{}e,e',y:E. (e' before y \mmember{} before(e) {}\mRightarrow{} (e' <loc y))
Date html generated:
2011_08_16-AM-10_37_42
Last ObjectModification:
2010_12_05-PM-11_41_12
Home
Index