Nuprl Lemma : Q-R-glues-conditional
[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. g1:E(Ib1) E(Ia1). g2:E(Ib2) E(Ia2).
(g1 glues Ia1:Q1 f Ib1:R
g2 glues Ia2:Q2 f Ib2:R
[{Ib1}? g1 : g2] glues [Ia1?Ia2]:Q1|{Ia1} 
Q2|{Ia2} f [Ib1?Ib2]:R) supposing
(Ib1 
Ib2 = 0 and
Ia1 Ia2 = 0)
Proof not projected
Definitions occuring in Statement :
Q-R-glues: g glues Ia:Qa f Ib:Rb,
es-interface-disjoint: X Y = 0,
es-E-interface: E(X),
es-interface-predicate: {I},
cond-class: [X?Y],
in-eclass: e 
X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
conditional: [P? f : g],
es-E: E,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
implies: P Q,
lambda: 
x.A[x],
function: x:A B[x],
universe: Type,
rel_or: R1 R2,
rel-restriction: R|P,
bool-decider: bool-decider(b)
Definitions :
so_lambda: 
x y.t[x; y],
suptype: suptype(S; T),
true: True,
ifthenelse: if b then t else f fi ,
guard: {T},
btrue: tt,
or: P Q,
so_lambda: x.t[x],
subtype: S 
T,
cand: A c
B,
false: False,
assert: 
b,
and: P Q,
not: 
A,
member: t T,
implies: P Q,
es-interface-disjoint: X Y = 0,
uimplies: b supposing a,
es-E-interface: E(X),
prop: ,
all: x:A. B[x],
uall: [x:A]. B[x],
Q-R-glues: g glues Ia:Qa f Ib:Rb,
es-interface-predicate: {I},
rel_rev_implies: R1 
R2,
predicate_rev_implies: P1 P2,
rev_implies: P Q,
exists: 
x:A. B[x],
iff: P Q,
predicate_or: P1 P2,
squash: 
T,
inject: Inj(A;B;f),
bfalse: ff,
branch: if p:P then A[p] else B fi ,
conditional: [P? f : g],
so_apply: x[s1;s2],
sq_type: SQType(T),
so_apply: x[s],
rel-restriction: R|P,
decidable: Dec(P),
sq_stable: SqStable(P),
unit: Unit,
bool: 
,
it: 
Lemmas :
assert_elim,
eclass_wf,
es-interface-disjoint_wf,
es-E-interface-subtype,
bool_subtype_base,
bool_wf,
subtype_base_sq,
is-cond-class,
subtype_rel_self,
subtype_rel_sets,
top_wf,
cond-class_wf,
es-E-interface_wf,
subtype_rel_dep_function,
Q-R-glues_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
es-interface-top,
in-eclass_wf,
assert_wf,
es-interface-conditional-predicate-equivalent,
weak-antecedent-surjection_functionality_wrt_pred_equiv,
conditional_wf-interface,
predicate_or_wf,
es-interface-predicate_wf,
decidable__assert,
bool-decider_wf,
weak-antecedent-surjection-conditional2,
rel_equivalent_inversion,
rel_equivalent_weakening,
rel_implies_weakening,
predicate_implies_weakening,
Q-R-pre-preserving_functionality_wrt_implies,
es-E-interface-subtype_rel,
equal_wf,
exists_wf,
rel-restriction_wf,
rel_or_wf,
subtype_rel_function,
rel_or_idempotent,
predicate_equivalent_weakening,
not_wf,
conditional_wf,
or_wf,
Q-R-pre-preserving-conditional,
rel-restriction-implies,
decidable_wf,
es-interface-conditional-domain-member,
sq_stable__assert,
conditional_wf2,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
uiff_transitivity,
eqtt_to_assert,
iff_weakening_uiff,
cond-class-val,
es-E-interface-conditional-subtype1,
es-E-interface-conditional-subtype2
\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. \mforall{}g1:E(Ib1) {}\mrightarrow{} E(Ia1).
\mforall{}g2:E(Ib2) {}\mrightarrow{} E(Ia2).
(g1 glues Ia1:Q1 {}{}f{}\mrightarrow{} Ib1:R
{}\mRightarrow{} g2 glues Ia2:Q2 {}{}f{}\mrightarrow{} Ib2:R
{}\mRightarrow{} [\{Ib1\}? g1 : g2] glues [Ia1?Ia2]:Q1|\{Ia1\} \mvee{} Q2|\{Ia2\} {}{}f{}\mrightarrow{} [Ib1?Ib2]:R) supposing
(Ib1 \mcap{} Ib2 = 0 and
Ia1 \mcap{} Ia2 = 0)
Date html generated:
2012_01_23-PM-12_28_58
Last ObjectModification:
2011_12_13-PM-02_05_12
Home
Index