{ 
[Info:Type]
es:EO+(Info). X:EClass(Top). e:E(X). A,B:E(X) List.
(
p:E(X)
(p 
loc e
((X)(p) = A)
(filter(
a.p <loc a;(X)(e)) = B)
(p <loc e) supposing 
null(B)
(p = last(A)))) supposing
((null(A)) and
((X)(e) = (A @ B))) }
{ 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-bless: e <loc e',
es-le: e loc e' ,
es-locl: (e <loc e'),
es-E: E,
append: as @ bs,
null: null(as),
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
and: P Q,
lambda: x.A[x],
list: type List,
universe: Type,
equal: s = t,
filter: filter(P;l),
last: last(L)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
top: Top,
uimplies: b supposing a,
not: A,
exists: x:A. B[x],
and: P Q,
iseg: l1 l2,
member: t 
T,
implies: P 
Q,
false: False,
prop: 
,
subtype: S 
T,
cand: A c B,
so_lambda: 
x y.t[x; y],
es-E-interface: E(X),
iff: P 
Q,
assert: b,
irrefl: Irrefl(T;x,y.E[x; y]),
anti_sym: AntiSym(T;x,y.R[x; y]),
trans: Trans(T;x,y.E[x; y]),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
rev_implies: P Q,
squash: 
T,
or: P 
Q,
so_apply: x[s1;s2],
sq_type: SQType(T),
guard: {T},
es-le: e loc e' ,
null: null(as),
length: ||as||,
ycomb: Y,
bfalse: ff
Lemmas :
iseg-interface-predecessors,
assert_wf,
null_wf3,
top_wf,
es-E-interface_wf,
append_wf,
not_wf,
es-le_wf,
event-ordering+_inc,
es-interface-predecessors_wf,
Id_wf,
es-loc_wf,
filter_wf,
es-bless_wf,
es-locl_wf,
es-E_wf,
eclass_wf,
event-ordering+_wf,
iseg-remainder-as-filter,
es-locl-antireflexive,
es-locl_transitivity2,
es-le_weakening,
es-locl_irreflexivity,
subtype_base_sq,
bool_wf,
bool_subtype_base,
in-eclass_wf,
es-interface-predecessors-sorted-by-locl,
assert-es-bless,
assert_elim,
length_wf1,
length-append,
squash_wf,
true_wf,
non_neg_length,
length_wf_nat
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}e:E(X). \mforall{}A,B:E(X) List.
(\mexists{}p:E(X)
(p \mleq{}loc e
\mwedge{} (\mleq{}(X)(p) = A)
\mwedge{} (filter(\mlambda{}a.p <loc a;\mleq{}(X)(e)) = B)
\mwedge{} (p <loc e) supposing \mneg{}\muparrow{}null(B)
\mwedge{} (p = last(A)))) supposing
((\mneg{}\muparrow{}null(A)) and
(\mleq{}(X)(e) = (A @ B)))
Date html generated:
2011_08_16-PM-05_22_10
Last ObjectModification:
2011_06_20-AM-01_21_51
Home
Index