Nuprl Lemma : Q-R-pre-preserving-conditional

  ∀[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')))))


Definitions occuring in Statement :  Q-R-pre-preserving: is Q-R-pre-preserving on P conditional: [P? g] es-E: E event_ordering: EO predicate_or: P1 ∨ P2 rel_or: R1 ∨ R2 decidable: Dec(P) uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q set: {x:A| B[x]}  apply: 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{}[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