---

Step * 1 1 1 3 of Lemma Q-R-pre-preserving-conditional


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. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. y : ¬(P1 e)
19. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)
20. x : P1 e'
21. (dcd_P1 e') = (inl x) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f2 e) (f1 e')
⊢ (R1 ∨ R2) e e'
BY
{ (RepUR ``rel_or infix_ap`` (-1)
   THEN D -1
   THEN OnMaybeHyp 13 (\h. (InstHyp [⌈e'⌉;⌈e⌉] h⋅ THEN Auto THEN DSetVars THEN SplitOrHyps THEN Complete (Auto)))) }

---

Latex:



1.  es  :  EO@i'
2.  [P1]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [P2]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [Q1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [R1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
6.  [Q2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
7.  [R2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
8.  dcd$_{P1}$  :  e:E  {}\mrightarrow{}  Dec(P1  e)@i
9.  f1  :  \{e:E|  P1  e\}    {}\mrightarrow{}  E@i
10.  f2  :  \{e:E|  P2  e\}    {}\mrightarrow{}  E@i
11.  \mforall{}e,e':\{e:E|  P1  e\}  .    (\mneg{}(Q2  (f1  e)  (f1  e')))
12.  \mforall{}e,e':\{e:E|  P2  e\}  .    (\mneg{}(Q1  (f2  e)  (f2  e')))
13.  \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))))
14.  \mforall{}e,e':\{e:E|  P1  e\}  .    ((Q1  (f1  e)  (f1  e'))  {}\mRightarrow{}  (R1  e  e'))@i
15.  \mforall{}e,e':\{e:E|  P2  e\}  .    ((Q2  (f2  e)  (f2  e'))  {}\mRightarrow{}  (R2  e  e'))@i
16.  e  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
17.  e'  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
18.  y  :  \mneg{}(P1  e)
19.  (dcd$_{P1}$  e)  =  (inr  y  )
20.  x  :  P1  e'
21.  (dcd$_{P1}$  e')  =  (inl  x)
22.  (Q1  \mvee{}  Q2)  (f2  e)  (f1  e')
\mvdash{}  (R1  \mvee{}  R2)  e  e'


By

(RepUR  ``rel\_or  infix\_ap``  (-1)
  THEN  D  -1
  THEN  OnMaybeHyp  13  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  h\mcdot{}
                                                    THEN  Auto
                                                    THEN  DSetVars
                                                    THEN  SplitOrHyps
                                                    THEN  Complete  (Auto))))

---

Home Index