---

Step * of Lemma b-almost-full-filter

∀A,B:ℕ ⟶ ℕ ⟶ ℙ.
  ((b-almost-full(n,m.A[n;m]) ⇒ b-almost-full(n,m.B[n;m]) ⇒ b-almost-full(n,m.A[n;m] ∧ B[n;m]))
  ∧ ((∀n,m:ℕ.  (A[n;m] ⇒ B[n;m])) ⇒ b-almost-full(n,m.A[n;m]) ⇒ b-almost-full(n,m.B[n;m]))
  ∧ b-almost-full(n,m.True))
BY
{ Auto }

1
1. A : ℕ ⟶ ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℕ ⟶ ℙ@i'
3. b-almost-full(n,m.A[n;m])@i
4. b-almost-full(n,m.B[n;m])@i
⊢ b-almost-full(n,m.A[n;m] ∧ B[n;m])

2
1. A : ℕ ⟶ ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℕ ⟶ ℙ@i'
3. ∀n,m:ℕ.  (A[n;m] ⇒ B[n;m])@i
4. b-almost-full(n,m.A[n;m])@i
5. b-almost-full(n,m.B[n;m]) ⇒ b-almost-full(n,m.A[n;m] ∧ B[n;m])
⊢ b-almost-full(n,m.B[n;m])

3
1. A : ℕ ⟶ ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℕ ⟶ ℙ@i'
3. b-almost-full(n,m.A[n;m]) ⇒ b-almost-full(n,m.B[n;m]) ⇒ b-almost-full(n,m.A[n;m] ∧ B[n;m])
4. (∀n,m:ℕ.  (A[n;m] ⇒ B[n;m])) ⇒ b-almost-full(n,m.A[n;m]) ⇒ b-almost-full(n,m.B[n;m])
⊢ b-almost-full(n,m.True)

---

Latex:

---

Latex:
\mforall{}A,B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}.
    ((b-almost-full(n,m.A[n;m])  {}\mRightarrow{}  b-almost-full(n,m.B[n;m])  {}\mRightarrow{}  b-almost-full(n,m.A[n;m]  \mwedge{}  B[n;m]))
    \mwedge{}  ((\mforall{}n,m:\mBbbN{}.    (A[n;m]  {}\mRightarrow{}  B[n;m]))  {}\mRightarrow{}  b-almost-full(n,m.A[n;m])  {}\mRightarrow{}  b-almost-full(n,m.B[n;m]))
    \mwedge{}  b-almost-full(n,m.True))


By

---

Latex:
Auto

---

Home Index