{ 
[es:EO]. [e,e':E]. hd([e, e']) = e supposing e 
loc e' }
{ Proof }
Definitions occuring in Statement :
es-interval: [e, e'],
es-le: e loc e' ,
es-E: E,
event_ordering: EO,
hd: hd(l),
uimplies: b supposing a,
uall: [x:A]. B[x],
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
es-le: e loc e' ,
member: t 
T,
and: P 
Q,
cand: A c B,
or: P 
Q,
guard: {T},
length: ||as||,
select: l[i],
hd: hd(l),
implies: P 
Q,
all: x:A. B[x],
ycomb: Y,
prop: 
,
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
bfalse: ff,
btrue: tt,
not: A,
ge: i 
j ,
le: A B,
false: False,
squash: 
T,
true: True,
iff: P 
Q,
rev_implies: P Q,
l_member: (x l),
exists: 
x:A. B[x],
nat: 
,
decidable: Dec(P),
sq_type: SQType(T)
Lemmas :
es-le_wf,
es-E_wf,
event_ordering_wf,
es-locl_wf,
member-es-interval,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
es-interval_wf,
length_wf1,
l_before-es-interval,
hd_wf,
es-le-trans2,
squash_wf,
true_wf,
es-locl-antireflexive
\mforall{}[es:EO]. \mforall{}[e,e':E]. hd([e, e']) = e supposing e \mleq{}loc e'
Date html generated:
2011_08_16-AM-10_39_31
Last ObjectModification:
2011_06_18-AM-09_18_15
Home
Index