Nuprl Lemma : Q-R-glues-split
∀[Info:Type]. ∀[P:es:EO+(Info) ⟶ E ⟶ ℙ].
∀p:∀es:EO+(Info). ∀e:E. Dec(P[es;e])
∀[A,B:Type].
∀Ia:EClass(A). ∀Ib:EClass(B).
((Singlevalued(Ia) ∧ Singlevalued(Ib))
⇒ (∀g1:es:EO+(Info) ⟶ E(Ib) ⟶ E. ∀q:∀es:EO+(Info). ∀e:E. Dec((↑e ∈b Ib) c∧ P[es;g1 es e]). ∀es:EO+(Info).
∀[Q,R:E ⟶ E ⟶ ℙ].
((∀x,y:E. ((Q x y) ⇒ (P[es;x] ⇐⇒ P[es;y])))
⇒ (∀f:E(Ia) ⟶ B. ∀g2:E(Ib) ⟶ E.
(g1 es glues (Ia|p):Q ──f⟶ (Ib|q):R
⇒ g2 glues (Ia|¬p):Q ──f⟶ (Ib|¬q):R
⇒ [λe.P[es;g1 es e]? g1 es : g2] glues Ia:Q ──f⟶ Ib:R)))))
Proof
Definitions occuring in Statement :
Q-R-glues: g glues Ia:Qa ──f⟶ Ib:Rb,
es-interface-co-restrict: (I|¬p),
es-interface-restrict: (I|p),
es-E-interface: E(X),
sv-class: Singlevalued(X),
in-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
conditional: [P? f : g],
es-E: E,
compose: f o g,
assert: ↑b,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
cand: A c∧ B,
prop: ℙ,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
and: P ∧ Q,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
top: Top,
cand: A c∧ B,
es-E-interface: E(X),
es-interface-predicate: {I},
rel-restriction: R|P,
rel_or: R1 ∨ R2,
rel_equivalent: R1 ⇐⇒ R2,
infix_ap: x f y,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
decidable: Dec(P),
or: P ∨ Q,
es-E: E,
sq_stable: SqStable(P),
squash: ↓T,
guard: {T},
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
not: ¬A,
false: False,
conditional: [P? f : g],
compose: f o g,
branch: if p:P then A[p] else B fi ,
sq_type: SQType(T),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True
Latex:
\mforall{}[Info:Type]. \mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
\mforall{}p:\mforall{}es:EO+(Info). \mforall{}e:E. Dec(P[es;e])
\mforall{}[A,B:Type].
\mforall{}Ia:EClass(A). \mforall{}Ib:EClass(B).
((Singlevalued(Ia) \mwedge{} Singlevalued(Ib))
{}\mRightarrow{} (\mforall{}g1:es:EO+(Info) {}\mrightarrow{} E(Ib) {}\mrightarrow{} E. \mforall{}q:\mforall{}es:EO+(Info). \mforall{}e:E.
Dec((\muparrow{}e \mmember{}\msubb{} Ib) c\mwedge{} P[es;g1 es e]). \mforall{}es:EO+(Info).
\mforall{}[Q,R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
((\mforall{}x,y:E. ((Q x y) {}\mRightarrow{} (P[es;x] \mLeftarrow{}{}\mRightarrow{} P[es;y])))
{}\mRightarrow{} (\mforall{}f:E(Ia) {}\mrightarrow{} B. \mforall{}g2:E(Ib) {}\mrightarrow{} E.
(g1 es glues (Ia|p):Q {}{}f{}\mrightarrow{} (Ib|q):R
{}\mRightarrow{} g2 glues (Ia|\mneg{}p):Q {}{}f{}\mrightarrow{} (Ib|\mneg{}q):R
{}\mRightarrow{} [\mlambda{}e.P[es;g1 es e]? g1 es : g2] glues Ia:Q {}{}f{}\mrightarrow{} Ib:R)))))
Date html generated:
2016_05_17-AM-07_53_12
Last ObjectModification:
2016_01_17-PM-03_10_36
Theory : event-ordering
Home
Index