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