{ 
es:EO. L:E List.
L':E List
(L 
L'
L' L
(a,b:E. ((a 
L') 
(b L') (a < b) a before b L'))
no_repeats(E;L')) }
{ Proof }
Definitions occuring in Statement :
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
list: type List,
no_repeats: no_repeats(T;l),
l_before: x before y l,
l_member: (x l),
l_contains: A B
Definitions :
all: x:A. B[x],
member: t T,
exists: x:A. B[x],
and: P Q,
implies: P Q,
cand: A c B,
prop: 
,
l_contains: A B,
l_all: (xL.P[x]),
or: P 
Q,
guard: {T},
so_lambda: 
x.t[x],
rev_implies: P 
Q,
iff: P Q,
top: Top,
subtype: S T,
append: as @ bs,
false: False,
decidable: Dec(P),
so_apply: x[s],
length: ||as||,
hd: hd(l),
ycomb: Y,
es-causle: e c
e',
not: 
A
Lemmas :
es-E_wf,
event_ordering_wf,
l_contains_nil,
nil_member,
l_member_wf,
no_repeats_nil,
l_contains_wf,
es-causl_wf,
l_before_wf,
no_repeats_wf,
decidable__l_member,
decidable__es-E-equal,
l_contains_cons,
cons_member,
split-at-first,
es-causle_wf,
decidable__es-causle,
l_all_wf2,
append_wf,
implies_functionality_wrt_iff,
member_append,
length_wf1,
non_neg_length,
length_wf_nat,
top_wf,
es-causl_transitivity2,
es-causl_transitivity1,
es-causle_weakening_locl,
es-le_weakening_eq,
l_before_append_iff,
l_before_member,
cons_before,
no_repeats-permute,
no_repeats_cons,
and_functionality_wrt_iff,
all_functionality_wrt_iff,
or_functionality_wrt_iff,
es-causle_weakening,
es-causl_irreflexivity,
not_functionality_wrt_iff,
l_member-permute,
not_wf
\mforall{}es:EO. \mforall{}L:E List.
\mexists{}L':E List
(L \msubseteq{} L'
\mwedge{} L' \msubseteq{} L
\mwedge{} (\mforall{}a,b:E. ((a \mmember{} L') {}\mRightarrow{} (b \mmember{} L') {}\mRightarrow{} (a < b) {}\mRightarrow{} a before b \mmember{} L'))
\mwedge{} no\_repeats(E;L'))
Date html generated:
2011_08_16-AM-10_36_07
Last ObjectModification:
2010_09_24-PM-09_07_50
Home
Index