---

Step * 1 1 of Lemma ball_functionality_wrt_bimplies


1. v1 : 𝔹
2. v2 : 𝔹
3. v3 : 𝔹
4. v4 : 𝔹
⊢ (↑((¬bv1) ∨bv2)) ⇒ ↑v3 supposing ↑v4 ⇒ (↑((¬b(v4 ∧b v1)) ∨b(v3 ∧b v2)))
BY
{ Auto }

---

Latex:

---

Latex:

1.  v1  :  \mBbbB{}
2.  v2  :  \mBbbB{}
3.  v3  :  \mBbbB{}
4.  v4  :  \mBbbB{}
\mvdash{}  (\muparrow{}((\mneg{}\msubb{}v1)  \mvee{}\msubb{}v2))  {}\mRightarrow{}  \muparrow{}v3  supposing  \muparrow{}v4  {}\mRightarrow{}  (\muparrow{}((\mneg{}\msubb{}(v4  \mwedge{}\msubb{}  v1))  \mvee{}\msubb{}(v3  \mwedge{}\msubb{}  v2)))


By

---

Latex:
Auto

---

Home Index