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)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
es-interface-disjoint: X ⋂ Y = 0,
not: ¬A,
implies: P ⇒ Q,
false: False,
and: P ∧ Q,
subtype_rel: A ⊆r B,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
top: Top,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
es-E-interface: E(X),
Q-R-glues: g glues Ia:Qa ──f⟶ Ib:Rb,
cand: A c∧ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
es-interface-predicate: {I},
predicate_or: P1 ∨ P2,
guard: {T},
exists: ∃x:A. B[x],
predicate_rev_implies: P1 ⇐ P2,
rel_rev_implies: R1 ⇐ R2,
rel-restriction: R|P,
subtype: S ⊆ T,
inject: Inj(A;B;f),
conditional: [P? f : g],
branch: if p:P then A[p] else B fi ,
decidable: Dec(P),
or: P ∨ Q,
sq_type: SQType(T),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
bool-decider: bool-decider(b),
decidable__assert,
uiff: uiff(P;Q),
bfalse: ff,
bool: 𝔹,
unit: Unit,
it: ⋅,
bnot: ¬bb
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:
2016_05_17-AM-07_52_17
Last ObjectModification:
2015_12_29-AM-00_28_35
Theory : event-ordering
Home
Index