---

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

.....wf..... 
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) ∈ ℙ
BY
{ (MemCD THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
2:n
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)
⊢ [P1? f : g] e ∈ E

---

Latex:


.....wf..... 
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.  \mneg{}(P1  e)
\mvdash{}  Q1  ([P1?  f  :  g]  e)  \mmember{}  \mBbbP{}


By

(MemCD  THEN  Try  (Complete  (Auto)))

---

Home Index