Nuprl Lemma : Q-R-pre-preserving-conditional
∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
    ∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f1:{e:E| P1 e}  ⟶ E. ∀f2:{e:E| P2 e}  ⟶ E.
      (f1 is Q1-R1-pre-preserving on P1
         
⇒ f2 is Q2-R2-pre-preserving on P2
         
⇒ [P1? f1 : f2] is Q1 ∨ Q2-R1 ∨ R2-pre-preserving on P1 ∨ P2) supposing 
         ((∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
             ((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))) and 
         (∀e,e':{e:E| P2 e} .  (¬(Q1 (f2 e) (f2 e')))) and 
         (∀e,e':{e:E| P1 e} .  (¬(Q2 (f1 e) (f1 e')))))
Proof
Definitions occuring in Statement : 
Q-R-pre-preserving: f is Q-R-pre-preserving on P
, 
conditional: [P? f : g]
, 
es-E: E
, 
event_ordering: EO
, 
predicate_or: P1 ∨ P2
, 
rel_or: R1 ∨ R2
, 
decidable: Dec(P)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
function: x:A ⟶ B[x]
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
uall: ∀[x:A]. B[x]
, 
uimplies: b supposing a
, 
member: t ∈ T
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
false: False
, 
subtype_rel: A ⊆r B
, 
prop: ℙ
, 
and: P ∧ Q
, 
Q-R-pre-preserving: f is Q-R-pre-preserving on P
, 
predicate_or: P1 ∨ P2
, 
so_apply: x[s]
, 
so_lambda: λ2x.t[x]
, 
or: P ∨ Q
, 
conditional: [P? f : g]
, 
branch: if p:P then A[p] else B fi 
, 
exists: ∃x:A. B[x]
, 
decidable: Dec(P)
, 
rel_or: R1 ∨ R2
, 
infix_ap: x f y
, 
guard: {T}
, 
cand: A c∧ B
Latex:
\mforall{}es:EO
    \mforall{}[P1,P2:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q1,R1,Q2,R2:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}dcd$_{P1}$:e:E  {}\mrightarrow{}  Dec(P1  e).  \mforall{}f1:\{e:E|  P1  e\}    {}\mrightarrow{}  E.  \mforall{}f2:\{e:E|  P2  e\}    {}\mrightarrow{}  E.
            (f1  is  Q1-R1-pre-preserving  on  P1
                  {}\mRightarrow{}  f2  is  Q2-R2-pre-preserving  on  P2
                  {}\mRightarrow{}  [P1?  f1  :  f2]  is  Q1  \mvee{}  Q2-R1  \mvee{}  R2-pre-preserving  on  P1  \mvee{}  P2)  supposing 
                  ((\mforall{}e:\{e:E|  P1  e\}  .  \mforall{}e':\{e:E|  P2  e\}  .
                          ((\mneg{}(Q1  (f1  e)  (f2  e')))
                          \mwedge{}  (\mneg{}(Q1  (f2  e')  (f1  e)))
                          \mwedge{}  (\mneg{}(Q2  (f1  e)  (f2  e')))
                          \mwedge{}  (\mneg{}(Q2  (f2  e')  (f1  e)))))  and 
                  (\mforall{}e,e':\{e:E|  P2  e\}  .    (\mneg{}(Q1  (f2  e)  (f2  e'))))  and 
                  (\mforall{}e,e':\{e:E|  P1  e\}  .    (\mneg{}(Q2  (f1  e)  (f1  e')))))
Date html generated:
2016_05_16-AM-10_19_41
Last ObjectModification:
2015_12_28-PM-09_33_53
Theory : new!event-ordering
Home
Index