Step * 1 of Lemma ball_functionality_wrt_bimplies


1. Type
2. T ⟶ 𝔹
3. T ⟶ 𝔹
4. ∀x:T. ↑Q[x] supposing ↑P[x]
5. T
6. 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 With ⌜u⌝  THENA Auto)
   THEN RepeatFor (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