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]
Lemmas : es-E_wf, rel_or_wf, set_wf, or_wf, Q-R-pre-preserving_wf, all_wf, not_wf, decidable_wf, event_ordering_wf, conditional_wf2, equal_wf, branch_wf2
\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: 2015_07_17-AM-09_03_28 Last ObjectModification: 2015_01_27-PM-00_56_47 Home Index