---

Step * of Lemma baf-bar-monotone

∀R,T:ℕ ⟶ ℕ ⟶ ℙ. ∀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
{ (Auto
   THEN RepeatFor 6 (ParallelOp -3)
   THEN NthHypEq (-3)
   THEN EqCD
   THEN Auto
   THEN (RepUR ``seq-add`` 0 THEN AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}R,T:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  \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:
(Auto
  THEN  RepeatFor  6  (ParallelOp  -3)
  THEN  NthHypEq  (-3)
  THEN  EqCD
  THEN  Auto
  THEN  (RepUR  ``seq-add``  0  THEN  AutoSplit))

---

Home Index