---

Step * 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)
⊢ strictly-increasing-seq(n;s) ∧ (∀m,i,j:ℕn.  (m < i ⇒ m < j ⇒ (R (s m) (s i) ⇐⇒ R (s m) (s j))))
BY
{ (D 0 THEN Try (Trivial)) }

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)
⊢ ∀m,i,j:ℕn.  (m < i ⇒ m < j ⇒ (R (s m) (s i) ⇐⇒ R (s m) (s j)))

---

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{}  strictly-increasing-seq(n;s)  \mwedge{}  (\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:
(D  0  THEN  Try  (Trivial))

---

Home Index