---

Step * 1 of Lemma b-almost-full-intersection

.....antecedent..... 
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. T : ℕ ⟶ ℕ ⟶ ℙ
3. b-almost-full(n,m.R[n;m])
4. b-almost-full(n,m.T[n;m])
⊢ ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
    (baf-bar(n,m.R[n;m];n,m.T[n;m];n;s)
    ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ baf-bar(n,m.R[n;m];n,m.T[n;m];n + 1;s.m@n))))
BY
{ TACTIC:(Auto THEN BLemma `baf-bar-monotone` THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  T  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  b-almost-full(n,m.R[n;m])
4.  b-almost-full(n,m.T[n;m])
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}s:\{s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}|  strictly-increasing-seq(n;s)\}  .
        (baf-bar(n,m.R[n;m];n,m.T[n;m];n;s)
        {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  (strictly-increasing-seq(n  +  1;s.m@n)  {}\mRightarrow{}  baf-bar(n,m.R[n;m];n,m.T[n;m];n  +  1;s.m@n))))


By

---

Latex:
TACTIC:(Auto  THEN  BLemma  `baf-bar-monotone`  THEN  Auto)

---

Home Index