Step
*
1
2
1
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 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)
BY
{ TACTIC:(RepUR ``seq-add`` 0 THEN AutoSplit) }
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
22. i = (n + 1) ∈ ℤ
⊢ R (s m) q ⇐⇒ R (s m) if j=n + 1 then q else if j=n then p else (s j)
2
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. ¬(i = (n + 1) ∈ ℤ)
16. j : ℕn + 2
17. m < i
18. m < j
19. ¬(i < n + 1 ∧ j < n + 1)
20. m < n - 1
21. R (s m) (s (n - 1)) ⇐⇒ R (s m) p
22. R (s m) (s (n - 1)) ⇐⇒ R (s m) q
⊢ R (s m) if i=n then p else (s i) ⇐⇒ R (s m) if j=n + 1 then q else if j=n then p else (s 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 m) (s (n - 1)) \mLeftarrow{}{}\mRightarrow{} R (s m) p
21. R (s m) (s (n - 1)) \mLeftarrow{}{}\mRightarrow{} R (s m) q
\mvdash{} R (s m) (s.p@n.q@n + 1 i) \mLeftarrow{}{}\mRightarrow{} R (s m) (s.p@n.q@n + 1 j)
By
Latex:
TACTIC:(RepUR ``seq-add`` 0 THEN AutoSplit)
Home
Index