---

Step * 1 2 2 of Lemma weak-antecedent-conditional


1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [Q1] : E ─→ ℙ
4. [P2] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. dcd_P1 : e:E ─→ Dec(P1 e)@i
7. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
8. g : {e:E| P2 e}  ─→ {e:E| Q2 e} @i
9. ∀e:{e:E| P1 e} . (f e c≤ e ∧ (Q1 (f e)))@i
10. ∀e:{e:E| P2 e} . (g e c≤ e ∧ (Q2 (g e)))@i
11. e : {e:E| (P1 e) ∨ (P2 e)} @i
12. [P1? f : g] e c≤ e
13. Dec(P1 e)
⊢ (Q1 ([P1? f : g] e)) ∨ (Q2 ([P1? f : g] e))
BY
{ D (-1) }

1
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [Q1] : E ─→ ℙ
4. [P2] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. dcd_P1 : e:E ─→ Dec(P1 e)@i
7. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
8. g : {e:E| P2 e}  ─→ {e:E| Q2 e} @i
9. ∀e:{e:E| P1 e} . (f e c≤ e ∧ (Q1 (f e)))@i
10. ∀e:{e:E| P2 e} . (g e c≤ e ∧ (Q2 (g e)))@i
11. e : {e:E| (P1 e) ∨ (P2 e)} @i
12. [P1? f : g] e c≤ e
13. P1 e
⊢ (Q1 ([P1? f : g] e)) ∨ (Q2 ([P1? f : g] e))

2
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [Q1] : E ─→ ℙ
4. [P2] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. dcd_P1 : e:E ─→ Dec(P1 e)@i
7. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
8. g : {e:E| P2 e}  ─→ {e:E| Q2 e} @i
9. ∀e:{e:E| P1 e} . (f e c≤ e ∧ (Q1 (f e)))@i
10. ∀e:{e:E| P2 e} . (g e c≤ e ∧ (Q2 (g e)))@i
11. e : {e:E| (P1 e) ∨ (P2 e)} @i
12. [P1? f : g] e c≤ e
13. ¬(P1 e)
⊢ (Q1 ([P1? f : g] e)) ∨ (Q2 ([P1? f : g] e))

---

Latex:



1.  es  :  EO@i'
2.  [P1]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q1]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [P2]  :  E  {}\mrightarrow{}  \mBbbP{}
5.  [Q2]  :  E  {}\mrightarrow{}  \mBbbP{}
6.  dcd$_{P1}$  :  e:E  {}\mrightarrow{}  Dec(P1  e)@i
7.  f  :  \{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\}  @i
8.  g  :  \{e:E|  P2  e\}    {}\mrightarrow{}  \{e:E|  Q2  e\}  @i
9.  \mforall{}e:\{e:E|  P1  e\}  .  (f  e  c\mleq{}  e  \mwedge{}  (Q1  (f  e)))@i
10.  \mforall{}e:\{e:E|  P2  e\}  .  (g  e  c\mleq{}  e  \mwedge{}  (Q2  (g  e)))@i
11.  e  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
12.  [P1?  f  :  g]  e  c\mleq{}  e
13.  Dec(P1  e)
\mvdash{}  (Q1  ([P1?  f  :  g]  e))  \mvee{}  (Q2  ([P1?  f  :  g]  e))


By

D  (-1)

---

Home Index