Step * 1 1 of Lemma homogeneous-extension-implies


1. : ℕ ⟶ ℕ ⟶ ℙ
2. : ℕ
3. : ℕn ⟶ ℕ
4. : ℕ
5. strictly-increasing-seq(n 1;s.m@n)
6. ∀m@0,i,j:ℕ1.  (m@0 <  m@0 <  (R (s.m@n m@0) (s.m@n i) ⇐⇒ (s.m@n m@0) (s.m@n j)))
7. strictly-increasing-seq(n;s)
⊢ ∀m,i,j:ℕn.  (m <  m <  (R (s m) (s i) ⇐⇒ (s m) (s j)))
BY
(ParallelOp -2
   THEN RepeatFor (ParallelLast)
   THEN NthHypSq  (-1) 
   THEN RepeatFor (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