{ 
[the_es:EO]. [e:E]. [n:
].
firstn(n + 1;
loc(e)) ~ loc(before(e)[n]) supposing n < ||before(e)|| }
{ Proof }
Definitions occuring in Statement :
es-le-before: loc(e),
es-before: before(e),
es-E: E,
event_ordering: EO,
select: l[i],
firstn: firstn(n;as),
length: ||as||,
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
less_than: a < b,
add: n + m,
natural_number: $n,
sqequal: s ~ t
Definitions :
member: t 
T,
prop: 
,
es-le-before: loc(e),
top: Top,
int_seg: {i..j
},
all: x:A. B[x],
subtype: S 
T,
lelt: i j < k,
le: A B,
and: P 
Q,
not: 
A,
implies: P 
Q,
false: False,
nat: ,
uall: [x:A]. B[x],
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T}
Lemmas :
firstn-before,
length_wf1,
es-E_wf,
es-before_wf,
nat_wf,
event_ordering_wf,
firstn_append,
es-before_wf2,
top_wf,
Id_wf,
es-loc_wf,
le_wf,
firstn_decomp,
subtype_base_sq,
int_subtype_base
\mforall{}[the$_{es}$:EO]. \mforall{}[e:E]. \mforall{}[n:\mBbbN{}]. firstn(n + 1;\mleq{}loc(e)) \msim{} \mleq{}loc(before(e)[n]) su\000Cpposing n < ||before(e)||
Date html generated:
2011_08_16-AM-10_43_36
Last ObjectModification:
2011_06_18-AM-09_19_45
Home
Index