{ 
[Info,A,B:Type].
es:EO+(Info). X:EClass(A). Y:EClass(B).
[R:E(X) 
A B 
]
(e
X(x) 
c
Y(y) such that
R[e;x;y]
f:E(X) E(Y)
(Bij(E(X);E(Y);f)
(e:E(X). (e c
f e R[e;X(e);Y(f e)])))) supposing
((b1,b2:E(Y). e:E(X).
(R[e;X(e);Y(b1)] R[e;X(e);Y(b2)] (b1 = b2))) and
(b:B. a1,a2:E(X). (R[a1;X(a1);b] R[a2;X(a2);b] (a1 = a2)))) \000C}
{ Proof }
Definitions occuring in Statement :
es-class-causal-rel: es-class-causal-rel,
es-E-interface: E(X),
eclass-val: X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-causle: e c e',
biject: Bij(A;B;f),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2;s3],
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
prop: ,
uimplies: b supposing a,
implies: P Q,
so_apply: x[s1;s2;s3],
iff: P Q,
exists: x:A. B[x],
and: P Q,
member: t T,
assert: 
b,
so_lambda: 
x y.t[x; y],
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
rev_implies: P Q,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
biject: Bij(A;B;f),
inject: Inj(A;B;f),
surject: Surj(A;B;f),
cand: A c B,
pi1: fst(t),
es-class-causal-rel: es-class-causal-rel,
so_apply: x[s1;s2],
top: Top,
squash: 
T,
es-E-interface: E(X),
sq_type: SQType(T),
guard: {T},
subtype: S 
T
Lemmas :
eclass-val_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
es-E-interface_wf,
es-interface-top,
es-class-causal-rel_wf,
biject_wf,
es-causle_wf,
eclass_wf,
assert_elim,
in-eclass_wf,
es-E-interface-subtype_rel,
es-interface-val_wf2,
es-interface-subtype_rel2,
top_wf,
squash_wf,
true_wf,
event_ordering_wf,
assert_wf
\mforall{}[Info,A,B:Type].
\mforall{}es:EO+(Info). \mforall{}X:EClass(A). \mforall{}Y:EClass(B).
\mforall{}[R:E(X) {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}]
(e\mmember{}X(x) \mLeftarrow{}c\mRightarrow{} Y(y) such that
R[e;x;y]
\mLeftarrow{}{}\mRightarrow{} \mexists{}f:E(X) {}\mrightarrow{} E(Y)
(Bij(E(X);E(Y);f) \mwedge{} (\mforall{}e:E(X). (e c\mleq{} f e \mwedge{} R[e;X(e);Y(f e)])))) supposing
((\mforall{}b1,b2:E(Y). \mforall{}e:E(X). (R[e;X(e);Y(b1)] {}\mRightarrow{} R[e;X(e);Y(b2)] {}\mRightarrow{} (b1 = b2))) and
(\mforall{}b:B. \mforall{}a1,a2:E(X). (R[a1;X(a1);b] {}\mRightarrow{} R[a2;X(a2);b] {}\mRightarrow{} (a1 = a2))))
Date html generated:
2011_08_16-PM-06_11_38
Last ObjectModification:
2011_06_20-AM-01_49_22
Home
Index