---

Step * of Lemma homogeneous-extension-implies

∀R:ℕ ⟶ ℕ ⟶ ℙ. ∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀m:ℕ.  (homogeneous(R;n + 1;s.m@n) ⇒ homogeneous(R;n;s))
BY
{ (Auto
   THEN ParallelLast
   THEN D -1
   THEN (Assert strictly-increasing-seq(n;s) BY
               (RepeatFor 2 (ParallelOp -2)
                THEN ParallelLast
                THEN NthHypEq  (-1)
                THEN EqCD
                THEN Auto
                THEN RepUR ``seq-add`` 0
                THEN AutoSplit))) }

1
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. m : ℕ
5. strictly-increasing-seq(n + 1;s.m@n)
6. ∀m@0,i,j:ℕn + 1.  (m@0 < i ⇒ m@0 < j ⇒ (R (s.m@n m@0) (s.m@n i) ⇐⇒ R (s.m@n m@0) (s.m@n j)))
7. strictly-increasing-seq(n;s)
⊢ strictly-increasing-seq(n;s) ∧ (∀m,i,j:ℕn.  (m < i ⇒ m < j ⇒ (R (s m) (s i) ⇐⇒ R (s m) (s j))))

---

Latex:

---

Latex:
\mforall{}R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}.  \mforall{}m:\mBbbN{}.    (homogeneous(R;n  +  1;s.m@n)  {}\mRightarrow{}  homogeneous(R;n;s))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  D  -1
  THEN  (Assert  strictly-increasing-seq(n;s)  BY
                          (RepeatFor  2  (ParallelOp  -2)
                            THEN  ParallelLast
                            THEN  NthHypEq    (-1)
                            THEN  EqCD
                            THEN  Auto
                            THEN  RepUR  ``seq-add``  0
                            THEN  AutoSplit)))

---

Home Index