{ 
[Info:Type]
es:EO+(Info)
[T:Type]
X:EClass(T). P:E(X) 
.
[R:Id E(X) 
]
L:Id List
((x
L.
y:E(X). (R[x;y] 
(
P[y])))
(e:{e:E(X)| P[e]}
(||L|| 
||filter(
e.P[e];(X)(e))||))) supposing
((0 < ||L||) and
no_repeats(Id;L))
supposing x1,x2:Id. y:E(X). (R[x1;y] R[x2;y] (x1 = x2))
supposing e1,e2:E(X).
(loc(e1) = loc(e2)) supposing ((P[e2]) and (P[e1])) }
{ 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-loc: loc(e),
Id: Id,
length: ||as||,
assert: b,
bool: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2],
so_apply: x[s],
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
lambda: x.A[x],
function: x:A B[x],
list: type List,
natural_number: $n,
universe: Type,
equal: s = t,
l_all: (xL.P[x]),
no_repeats: no_repeats(T;l),
filter: filter(P;l)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
prop: ,
implies: P Q,
so_apply: x[s1;s2],
no_repeats: no_repeats(T;l),
exists: x:A. B[x],
and: P Q,
le: A B,
member: t T,
not: 
A,
false: False,
so_lambda: 
x.t[x],
nat_plus: 
,
so_lambda: x y.t[x; y],
assert: b,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
es-E-interface: E(X),
nat: ,
sq_type: SQType(T),
guard: {T},
cand: A c B,
subtype: S 
T
Lemmas :
assert_wf,
es-E-interface_wf,
es-interface-top,
Id_wf,
select_wf,
not_wf,
nat_wf,
length_wf1,
l_all_exists_injection,
filter-interface-predecessors-lower-bound3,
int_seg_wf,
l_all_wf2,
l_member_wf,
no_repeats_wf,
es-loc_wf,
event-ordering+_inc,
bool_wf,
eclass_wf,
es-E_wf,
event-ordering+_wf,
subtype_base_sq,
bool_subtype_base,
assert_elim
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[T:Type]
\mforall{}X:EClass(T). \mforall{}P:E(X) {}\mrightarrow{} \mBbbB{}.
\mforall{}[R:Id {}\mrightarrow{} E(X) {}\mrightarrow{} \mBbbP{}]
\mforall{}L:Id List
((\mforall{}x\mmember{}L.\mexists{}y:E(X). (R[x;y] \mwedge{} (\muparrow{}P[y])))
{}\mRightarrow{} (\mexists{}e:\{e:E(X)| \muparrow{}P[e]\} . (||L|| \mleq{} ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||))) supposing
((0 < ||L||) and
no\_repeats(Id;L))
supposing \mforall{}x1,x2:Id. \mforall{}y:E(X). (R[x1;y] {}\mRightarrow{} R[x2;y] {}\mRightarrow{} (x1 = x2))
supposing \mforall{}e1,e2:E(X). (loc(e1) = loc(e2)) supposing ((\muparrow{}P[e2]) and (\muparrow{}P[e1]))
Date html generated:
2011_08_16-PM-05_23_42
Last ObjectModification:
2011_06_20-AM-01_22_47
Home
Index