{ 
[Info:Type]
es:EO+(Info). X:EClass(Top). e:E(X). L:E(X) List.
(L 
(X)(e)
(
null(L))
((
null(L))
(
p:E(X). (p loc e (L = (X)(p)) (p = last(L)))))) }
{ Proof }
Definitions occuring in Statement :
es-interface-predecessors: (X)(e),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-E: E,
null: null(as),
assert: b,
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
not: A,
or: P Q,
and: P Q,
list: type List,
universe: Type,
equal: s = t,
iseg: l1 l2,
last: last(L)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
iff: P Q,
or: P Q,
and: P Q,
exists: x:A. B[x],
implies: P Q,
rev_implies: P Q,
member: t 
T,
prop: 
,
cand: A c B,
guard: {T},
subtype: S 
T,
so_lambda: 
x y.t[x; y],
top: Top,
not: A,
false: False,
es-E-interface: E(X),
assert: b,
trans: Trans(T;x,y.E[x; y]),
anti_sym: AntiSym(T;x,y.R[x; y]),
set-equal: set-equal(T;x;y),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
so_lambda: x.t[x],
irrefl: Irrefl(T;x,y.E[x; y]),
label: ...$L... t,
es-le: e loc e' ,
decidable: Dec(P),
uimplies: b supposing a,
so_apply: x[s1;s2],
sq_type: SQType(T),
so_apply: x[s],
null: null(as),
bfalse: ff
Lemmas :
decidable__assert,
null_wf3,
not_wf,
assert_wf,
iseg_wf,
es-E-interface_wf,
es-interface-predecessors_wf,
Id_wf,
es-loc_wf,
es-le_wf,
event-ordering+_inc,
es-E_wf,
last_wf,
eclass_wf,
top_wf,
event-ordering+_wf,
member-interface-predecessors,
last_member,
iseg_member,
es-interface-predecessors-sorted-by-locl,
iseg-sorted-by,
es-locl_wf,
sorted-by-strict-unique,
es-locl_transitivity2,
es-le_weakening,
es-locl_irreflexivity,
subtype_base_sq,
bool_wf,
bool_subtype_base,
in-eclass_wf,
es-locl-antireflexive,
property-from-l_member,
sq_stable__equal,
l_member_wf,
assert_elim,
member-iseg-sorted-by,
decidable__equal_es-E-interface,
es-le_transitivity,
nil_iseg,
length_wf_nat,
nat_wf,
member_wf,
es-interface-predecessors-iseg
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}e:E(X). \mforall{}L:E(X) List.
(L \mleq{} \mleq{}(X)(e)
\mLeftarrow{}{}\mRightarrow{} (\muparrow{}null(L)) \mvee{} ((\mneg{}\muparrow{}null(L)) \mwedge{} (\mexists{}p:E(X). (p \mleq{}loc e \mwedge{} (L = \mleq{}(X)(p)) \mwedge{} (p = last(L))))))
Date html generated:
2011_08_16-PM-05_21_57
Last ObjectModification:
2011_06_20-AM-01_21_44
Home
Index