{ 
[Info:Type]
es:EO+(Info)
[Q1,Q2,R:E 
E 
]. [A,B:Type].
Ia1,Ia2:EClass(A). Ib1,Ib2:EClass(B). f:E([Ia1?Ia2]) B.
(Ia1:Q1 f Ib1:R
Ia2:Q2 f Ib2:R
[Ia1?Ia2]:Q1|{Ia1} 
Q2|{Ia2} f [Ib1?Ib2]:R) supposing
(Ib1 
Ib2 = 0 and
Ia1 Ia2 = 0) }
{ Proof }
Definitions occuring in Statement :
Q-R-glued: Ia:Qa f Ib:Rb,
es-interface-disjoint: X Y = 0,
es-E-interface: E(X),
es-interface-predicate: {I},
cond-class: [X?Y],
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
universe: Type,
rel_or: R1 R2,
rel-restriction: R|P
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
prop: ,
es-E-interface: E(X),
uimplies: b supposing a,
es-interface-disjoint: X Y = 0,
implies: P Q,
Q-R-glued: Ia:Qa f Ib:Rb,
member: t 
T,
not: 
A,
and: P 
Q,
assert: 
b,
false: False,
cand: A c B,
or: P Q,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
so_lambda: 
x y.t[x; y],
exists: 
x:A. B[x],
rev_implies: P 
Q,
iff: P Q,
sq_type: SQType(T),
guard: {T},
so_apply: x[s1;s2],
subtype: S 
T
Lemmas :
assert_wf,
in-eclass_wf,
es-interface-top,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
cond-class_wf,
es-interface-conditional-domain-iff,
subtype_base_sq,
bool_wf,
bool_subtype_base,
top_wf,
es-E-interface_wf,
Q-R-glues-property,
subtype_rel_function,
es-E-interface-conditional-subtype2,
subtype_rel_self,
Q-R-glued_wf,
es-E-interface-conditional-subtype1,
es-interface-disjoint_wf,
eclass_wf,
assert_elim,
conditional_wf-interface2,
Q-R-glues_wf,
rel_or_wf,
rel-restriction_wf,
es-interface-predicate_wf,
Q-R-glues-conditional
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[Q1,Q2,R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]. \mforall{}[A,B:Type].
\mforall{}Ia1,Ia2:EClass(A). \mforall{}Ib1,Ib2:EClass(B). \mforall{}f:E([Ia1?Ia2]) {}\mrightarrow{} B.
(Ia1:Q1 \mrightarrow{}{}f{}\mrightarrow{} Ib1:R
{}\mRightarrow{} Ia2:Q2 \mrightarrow{}{}f{}\mrightarrow{} Ib2:R
{}\mRightarrow{} [Ia1?Ia2]:Q1|\{Ia1\} \mvee{} Q2|\{Ia2\} \mrightarrow{}{}f{}\mrightarrow{} [Ib1?Ib2]:R) supposing
(Ib1 \mcap{} Ib2 = 0 and
Ia1 \mcap{} Ia2 = 0)
Date html generated:
2011_08_16-PM-06_00_07
Last ObjectModification:
2011_06_20-AM-01_42_19
Home
Index