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
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 ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
conditional: [P? f : g],
es-E: E,
rel-restriction: R|P,
rel_or: R1 ∨ R2,
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,
bool-decider: bool-decider(b)
Lemmas :
assert_wf,
in-eclass_wf,
es-interface-subtype_rel2,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
top_wf,
Q-R-glues_wf,
subtype_rel_dep_function,
es-E-interface_wf,
cond-class_wf,
es-E-interface-conditional-subtype2,
es-E-interface-conditional-subtype1,
es-interface-disjoint_wf,
eclass_wf,
es-interface-predicate_wf,
predicate_or_wf,
interface_predicate_set_lemma,
conditional_wf-interface,
weak-antecedent-surjection_functionality_wrt_pred_equiv,
es-interface-conditional-predicate-equivalent,
decidable__assert,
bool-decider_wf,
weak-antecedent-surjection-conditional2,
is-cond-class,
rel_or_wf,
rel-restriction_wf,
set_wf,
exists_wf,
equal_wf,
subtype_rel_self,
Q-R-pre-preserving_functionality_wrt_implies,
predicate_implies_weakening,
rel_implies_weakening,
rel_equivalent_weakening,
rel_equivalent_inversion,
rel_or_idempotent,
predicate_equivalent_weakening,
es-E-interface-property,
rel-restriction-implies,
Q-R-pre-preserving-conditional,
decidable_wf,
es-interface-conditional-domain-member,
equal_functionality_wrt_subtype_rel2,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
bool_cases,
eqtt_to_assert,
eqff_to_assert,
assert_of_bnot,
conditional_wf2,
es-E-interface-conditional,
cond-class-val,
iff_weakening_equal,
eclass-val_wf,
bool_cases_sqequal,
assert-bnot
Latex:
\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:
2015_07_21-PM-04_10_32
Last ObjectModification:
2015_02_04-PM-06_17_32
Home
Index