---

Step * 1 of Lemma decidable__uimplies

.....decidable?..... 
1. [P] : ℙ
2. Q : ⋂x:P. ℙ@i'
3. Dec(P)@i
4. Dec(Q) supposing P@i
⊢ Dec(Q supposing P)
BY
{ (Unfold `decidable` 0 THEN (D (-2))) }

1
1. [P] : ℙ
2. Q : ⋂x:P. ℙ@i'
3. P@i
4. Dec(Q) supposing P@i
⊢ Q supposing P ∨ (¬Q supposing P)

2
1. [P] : ℙ
2. Q : ⋂x:P. ℙ@i'
3. ¬P@i
4. Dec(Q) supposing P@i
⊢ Q supposing P ∨ (¬Q supposing P)

---

Latex:

---

Latex:
.....decidable?..... 
1.  [P]  :  \mBbbP{}
2.  Q  :  \mcap{}x:P.  \mBbbP{}@i'
3.  Dec(P)@i
4.  Dec(Q)  supposing  P@i
\mvdash{}  Dec(Q  supposing  P)


By

---

Latex:
(Unfold  `decidable`  0  THEN  (D  (-2)))

---

Home Index