---

Step * of 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')))))
BY
{ ((Auto
    THEN (Assert [P1? f1 : f2] ∈ {t:E| P1[t] ∨ P2[t]}  ─→ E BY
                ((InstLemma `conditional_wf2` [⌈E⌉;⌈E⌉;⌈P1⌉;⌈P2⌉;⌈dcd_P1⌉;⌈f1⌉;⌈f2⌉]⋅ THENA Auto)
                 THEN (RepUR ``conditional so_apply`` -1 THEN RepUR ``conditional`` 0)
                 THEN Trivial))
    )
   THEN All (Unfolds ``Q-R-pre-preserving predicate_or``)
   THEN SplitAndHyps
   THEN (D 0 THENA Auto)
   THEN (Reduce 0 THEN Auto)⋅) }

1
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e}  ─→ E@i
10. f2 : {e:E| P2 e}  ─→ E@i
11. ∀e,e':{e:E| P1 e} .  (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} .  (¬(Q1 (f2 e) (f2 e')))
13. ∀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))))
14. ∀e,e':{e:E| P1 e} .  ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} .  ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. [P1? f1 : f2] ∈ {t:E| P1[t] ∨ P2[t]}  ─→ E
17. e : {e:E| (λx.((P1 x) ∨ (P2 x))) e} @i
18. e' : {e:E| (P1 e) ∨ (P2 e)} @i
19. (Q1 ∨ Q2) ([P1? f1 : f2] e) ([P1? f1 : f2] e')@i
⊢ (R1 ∨ R2) e e'

---

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


By

((Auto
    THEN  (Assert  [P1?  f1  :  f2]  \mmember{}  \{t:E|  P1[t]  \mvee{}  P2[t]\}    {}\mrightarrow{}  E  BY
                            ((InstLemma  `conditional\_wf2`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}P1\mkleeneclose{};\mkleeneopen{}P2\mkleeneclose{};\mkleeneopen{}dcd$_{P1}$\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{}\000C;\mkleeneopen{}f2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  (RepUR  ``conditional  so\_apply``  -1  THEN  RepUR  ``conditional``  0)
                              THEN  Trivial))
    )
  THEN  All  (Unfolds  ``Q-R-pre-preserving  predicate\_or``)
  THEN  SplitAndHyps
  THEN  (D  0  THENA  Auto)
  THEN  (Reduce  0  THEN  Auto)\mcdot{})

---

Home Index