{ 
[Info:Type]
es:EO+(Info). e1,e2:E. L1,L2:Info List.
(
e
(e1,e2].(es-hist(es;e1;pred(e)) = L1)
(es-hist(es;e;e2) = L2)) supposing
((es-hist(es;e1;e2) = (L1 @ L2)) and
(
(L2 = [])) and
((L1 = []))) }
{ Proof }
Definitions occuring in Statement :
es-hist: es-hist(es;e1;e2),
event-ordering+: EO+(Info),
existse-between3: e(e1,e2].P[e],
es-pred: pred(e),
es-E: E,
append: as @ bs,
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
not: A,
and: P Q,
nil: [],
list: type List,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
uimplies: b supposing a,
not: A,
member: t T,
implies: P 
Q,
false: False,
top: Top,
subtype: S 
T,
prop: 
,
existse-between3: e(e1,e2].P[e],
and: P Q,
exists: x:A. B[x],
cand: A c B,
assert: 
b,
bfalse: ff,
ifthenelse: if b then t else f fi ,
guard: {T},
or: P 
Q,
es-hist: es-hist(es;e1;e2),
rev_implies: P 
Q,
iff: P Q,
sq_type: SQType(T),
decidable: Dec(P)
Lemmas :
length-append,
top_wf,
length_wf1,
length-map,
es-interval_wf,
pos_length,
es-subinterval,
es-interval-non-zero,
length_wf_nat,
es-hist_wf,
append_wf,
not_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
es-locl_wf,
es-le_wf,
es-pred_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
false_wf,
es-locl-first,
es-interval-partition,
map_wf,
es-info_wf,
map_append_sq,
es-interval_wf2,
Id_wf,
es-loc_wf,
general-append-cancellation,
decidable__equal_int
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}e1,e2:E. \mforall{}L1,L2:Info List.
(\mexists{}e\mmember{}(e1,e2].(es-hist(es;e1;pred(e)) = L1) \mwedge{} (es-hist(es;e;e2) = L2)) supposing
((es-hist(es;e1;e2) = (L1 @ L2)) and
(\mneg{}(L2 = [])) and
(\mneg{}(L1 = [])))
Date html generated:
2011_08_16-AM-11_27_22
Last ObjectModification:
2011_06_20-AM-00_27_30
Home
Index