---

Step * 1 of Lemma ball_functionality_wrt_bimplies


1. T : Type
2. P : T ⟶ 𝔹
3. Q : T ⟶ 𝔹
4. ∀x:T. ↑Q[x] supposing ↑P[x]
5. u : T
6. v : T List
7. ↑((¬b(∀bx(:T) ∈ v. P[x])) ∨b(∀bx(:T) ∈ v. Q[x]))
⊢ ↑((¬b(P[u] ∧b (∀bx(:T) ∈ v. P[x]))) ∨b(Q[u] ∧b (∀bx(:T) ∈ v. Q[x])))
BY
{ ((D 4 With ⌜u⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜∀bx(:T) ∈ v
                                P[x]⌝; ∀bx(:T) ∈ v
                                          Q[x]; Q[u];P[u]]⋅
   THEN All Thin) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  Q  :  T  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}x:T.  \muparrow{}Q[x]  supposing  \muparrow{}P[x]
5.  u  :  T
6.  v  :  T  List
7.  \muparrow{}((\mneg{}\msubb{}(\mforall{}\msubb{}x(:T)  \mmember{}  v.  P[x]))  \mvee{}\msubb{}(\mforall{}\msubb{}x(:T)  \mmember{}  v.  Q[x]))
\mvdash{}  \muparrow{}((\mneg{}\msubb{}(P[u]  \mwedge{}\msubb{}  (\mforall{}\msubb{}x(:T)  \mmember{}  v.  P[x])))  \mvee{}\msubb{}(Q[u]  \mwedge{}\msubb{}  (\mforall{}\msubb{}x(:T)  \mmember{}  v.  Q[x])))


By

---

Latex:
((D  4  With  \mkleeneopen{}u\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}\mforall{}\msubb{}x(:T)  \mmember{}  v
                                                            P[x]\mkleeneclose{};  \mforall{}\msubb{}x(:T)  \mmember{}  v
                                                                                Q[x];  Q[u];P[u]]\mcdot{}
  THEN  All  Thin)

---

Home Index