---

Step * 1 of Lemma decidable_functionality


1. [P] : ℙ
2. [Q] : ℙ
3. P ⇐⇒ Q
4. Dec(P)
⊢ Dec(Q)
BY
{ (Using [`A',⌜P⌝] (BackThruLemma `iff_preserves_decidability`) THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  P  \mLeftarrow{}{}\mRightarrow{}  Q
4.  Dec(P)
\mvdash{}  Dec(Q)


By

---

Latex:
(Using  [`A',\mkleeneopen{}P\mkleeneclose{}]  (BackThruLemma  `iff\_preserves\_decidability`)  THEN  Auto)

---

Home Index