---

Step * 1 2 1 1 of Lemma non-homogeneous-add


1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. p : ℕ
5. q : ℕ
6. p < q
7. strictly-increasing-seq(n + 1;s.p@n)
8. ∀m,i,j:ℕn + 1.  (m < i ⇒ m < j ⇒ (R (s.p@n m) (s.p@n i) ⇐⇒ R (s.p@n m) (s.p@n j)))
9. strictly-increasing-seq(n + 1;s.q@n)
10. ∀m,i,j:ℕn + 1.  (m < i ⇒ m < j ⇒ (R (s.q@n m) (s.q@n i) ⇐⇒ R (s.q@n m) (s.q@n j)))
11. 0 < n
12. R (s (n - 1)) p ⇐⇒ R (s (n - 1)) q
13. m : ℕn + 2
14. i : ℕn + 2
15. j : ℕn + 2
16. m < i
17. m < j
18. ¬(i < n + 1 ∧ j < n + 1)
19. m < n - 1
20. R (s.p@n m) (s.p@n (n - 1)) ⇐⇒ R (s.p@n m) (s.p@n n)
21. R (s.q@n m) (s.q@n (n - 1)) ⇐⇒ R (s.q@n m) (s.q@n n)
⊢ R (s.p@n m) (s.p@n.q@n + 1 i) ⇐⇒ R (s.p@n m) (s.p@n.q@n + 1 j)
BY
{ (((Assert s.p@n m ~ s m BY (RepUR ``seq-add`` 0 THEN AutoSplit)) THEN RWO "-1" 0 THEN RWO "-1" (-3))
   THEN (Assert s.q@n m ~ s m BY
               (RepUR ``seq-add`` 0 THEN AutoSplit))
   THEN RWO "-1" (-3)
   THEN ((Assert s.p@n (n - 1) ~ s (n - 1) BY (RepUR ``seq-add`` 0 THEN AutoSplit)) THEN RWO "-1" (-5))
   THEN (Assert s.q@n (n - 1) ~ s (n - 1) BY
               (RepUR ``seq-add`` 0 THEN AutoSplit))
   THEN RWO "-1" (-5)
   THEN RepeatFor 4 (Thin (-1))
   THEN RepUR ``seq-add`` -2
   THEN RepUR ``seq-add`` -1) }

1
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. p : ℕ
5. q : ℕ
6. p < q
7. strictly-increasing-seq(n + 1;s.p@n)
8. ∀m,i,j:ℕn + 1.  (m < i ⇒ m < j ⇒ (R (s.p@n m) (s.p@n i) ⇐⇒ R (s.p@n m) (s.p@n j)))
9. strictly-increasing-seq(n + 1;s.q@n)
10. ∀m,i,j:ℕn + 1.  (m < i ⇒ m < j ⇒ (R (s.q@n m) (s.q@n i) ⇐⇒ R (s.q@n m) (s.q@n j)))
11. 0 < n
12. R (s (n - 1)) p ⇐⇒ R (s (n - 1)) q
13. m : ℕn + 2
14. i : ℕn + 2
15. j : ℕn + 2
16. m < i
17. m < j
18. ¬(i < n + 1 ∧ j < n + 1)
19. m < n - 1
20. R (s m) (s (n - 1)) ⇐⇒ R (s m) p
21. R (s m) (s (n - 1)) ⇐⇒ R (s m) q
⊢ R (s m) (s.p@n.q@n + 1 i) ⇐⇒ R (s m) (s.p@n.q@n + 1 j)

---

Latex:

---

Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  p  :  \mBbbN{}
5.  q  :  \mBbbN{}
6.  p  <  q
7.  strictly-increasing-seq(n  +  1;s.p@n)
8.  \mforall{}m,i,j:\mBbbN{}n  +  1.    (m  <  i  {}\mRightarrow{}  m  <  j  {}\mRightarrow{}  (R  (s.p@n  m)  (s.p@n  i)  \mLeftarrow{}{}\mRightarrow{}  R  (s.p@n  m)  (s.p@n  j)))
9.  strictly-increasing-seq(n  +  1;s.q@n)
10.  \mforall{}m,i,j:\mBbbN{}n  +  1.    (m  <  i  {}\mRightarrow{}  m  <  j  {}\mRightarrow{}  (R  (s.q@n  m)  (s.q@n  i)  \mLeftarrow{}{}\mRightarrow{}  R  (s.q@n  m)  (s.q@n  j)))
11.  0  <  n
12.  R  (s  (n  -  1))  p  \mLeftarrow{}{}\mRightarrow{}  R  (s  (n  -  1))  q
13.  m  :  \mBbbN{}n  +  2
14.  i  :  \mBbbN{}n  +  2
15.  j  :  \mBbbN{}n  +  2
16.  m  <  i
17.  m  <  j
18.  \mneg{}(i  <  n  +  1  \mwedge{}  j  <  n  +  1)
19.  m  <  n  -  1
20.  R  (s.p@n  m)  (s.p@n  (n  -  1))  \mLeftarrow{}{}\mRightarrow{}  R  (s.p@n  m)  (s.p@n  n)
21.  R  (s.q@n  m)  (s.q@n  (n  -  1))  \mLeftarrow{}{}\mRightarrow{}  R  (s.q@n  m)  (s.q@n  n)
\mvdash{}  R  (s.p@n  m)  (s.p@n.q@n  +  1  i)  \mLeftarrow{}{}\mRightarrow{}  R  (s.p@n  m)  (s.p@n.q@n  +  1  j)


By

---

Latex:
(((Assert  s.p@n  m  \msim{}  s  m  BY  (RepUR  ``seq-add``  0  THEN  AutoSplit))  THEN  RWO  "-1"  0  THEN  RWO  "-1"  (-3))
  THEN  (Assert  s.q@n  m  \msim{}  s  m  BY
                          (RepUR  ``seq-add``  0  THEN  AutoSplit))
  THEN  RWO  "-1"  (-3)
  THEN  ((Assert  s.p@n  (n  -  1)  \msim{}  s  (n  -  1)  BY
                            (RepUR  ``seq-add``  0  THEN  AutoSplit))
              THEN  RWO  "-1"  (-5)
              )
  THEN  (Assert  s.q@n  (n  -  1)  \msim{}  s  (n  -  1)  BY
                          (RepUR  ``seq-add``  0  THEN  AutoSplit))
  THEN  RWO  "-1"  (-5)
  THEN  RepeatFor  4  (Thin  (-1))
  THEN  RepUR  ``seq-add``  -2
  THEN  RepUR  ``seq-add``  -1)

---

Home Index