---

Step * 1 1 of Lemma homogeneous-extension-implies


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)
⊢ ∀m,i,j:ℕn.  (m < i ⇒ m < j ⇒ (R (s m) (s i) ⇐⇒ R (s m) (s j)))
BY
{ (ParallelOp -2
   THEN RepeatFor 4 (ParallelLast)
   THEN NthHypSq  (-1) 
   THEN RepeatFor 2 (EqCD)
   THEN RepUR ``seq-add`` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  m  :  \mBbbN{}
5.  strictly-increasing-seq(n  +  1;s.m@n)
6.  \mforall{}m@0,i,j:\mBbbN{}n  +  1.    (m@0  <  i  {}\mRightarrow{}  m@0  <  j  {}\mRightarrow{}  (R  (s.m@n  m@0)  (s.m@n  i)  \mLeftarrow{}{}\mRightarrow{}  R  (s.m@n  m@0)  (s.m@n  j)))
7.  strictly-increasing-seq(n;s)
\mvdash{}  \mforall{}m,i,j:\mBbbN{}n.    (m  <  i  {}\mRightarrow{}  m  <  j  {}\mRightarrow{}  (R  (s  m)  (s  i)  \mLeftarrow{}{}\mRightarrow{}  R  (s  m)  (s  j)))


By

---

Latex:
(ParallelOp  -2
  THEN  RepeatFor  4  (ParallelLast)
  THEN  NthHypSq    (-1) 
  THEN  RepeatFor  2  (EqCD)
  THEN  RepUR  ``seq-add``  0
  THEN  AutoSplit)

---

Home Index