{ 
[Info:Type]
es:EO+(Info). X:EClass(Top). e:E. sorted-by(
x,y.(x <loc y);
(X)(e)) }
{ Proof }
Definitions occuring in Statement :
es-interface-predecessors: (X)(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-E: E,
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
lambda: x.A[x],
universe: Type,
sorted-by: sorted-by(R;L)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
member: t 
T,
nat: 
,
implies: P 
Q,
ge: i 
j ,
le: A B,
not: 
A,
false: False,
prop: 
,
squash: 
T,
true: True,
so_lambda: 
x y.t[x; y],
top: Top,
so_lambda: x.t[x],
l_all: (xL.P[x]),
rev_implies: P 
Q,
ifthenelse: if b then t else f fi ,
iff: P Q,
and: P 
Q,
btrue: tt,
bfalse: ff,
es-E-interface: E(X),
subtype: S 
T,
cand: A c B,
append: as @ bs,
sorted-by: sorted-by(R;L),
length: ||as||,
ycomb: Y,
strongwellfounded: SWellFounded(R[x; y]),
exists: 
x:A. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
uimplies: b supposing a,
bool: 
,
unit: Unit,
int_seg: {i..j
},
lelt: i j < k,
it: 
Lemmas :
es-causl-swellfnd,
event-ordering+_inc,
nat_properties,
ge_wf,
nat_wf,
le_wf,
es-causl_wf,
es-E_wf,
eclass_wf,
top_wf,
event-ordering+_wf,
es-E-interface_wf,
Id_wf,
es-loc_wf,
l_member_wf,
property-from-l_member,
sq_stable__equal,
list-set-type2,
es-interface-predecessors_wf,
es-locl_wf,
in-eclass_wf,
es-prior-interface_wf,
es-interface-subtype_rel2,
bool_wf,
assert_wf,
not_wf,
bnot_wf,
sorted-by_wf,
squash_wf,
true_wf,
es-interface-predecessors-general-step,
iff_weakening_uiff,
eqtt_to_assert,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot,
eclass-val_wf2,
es-E-interface-subtype_rel,
es-prior-interface-causl,
sorted-by-append1,
es-interface-predecessors-le,
es-prior-interface-val,
es-locl_transitivity1,
append-nil,
int_seg_wf
\mforall{}[Info:Type]. \mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}e:E. sorted-by(\mlambda{}x,y.(x <loc y);\mleq{}(X)(e))
Date html generated:
2011_08_16-PM-05_18_28
Last ObjectModification:
2011_06_20-AM-01_19_59
Home
Index