---

Step * of Lemma strictly-increasing-seq-add

∀[n:ℕ]. ∀[s:ℕn ⟶ ℤ].
  ∀x,y:ℕ.  (x < y ⇒ strictly-increasing-seq(n + 1;s.x@n) ⇒ strictly-increasing-seq(n + 2;s.x@n.y@n + 1))
BY
{ (Intros THEN ParallelLast THEN Auto THEN (Decide ⌜j = (n + 1) ∈ ℤ⌝⋅ THENA Auto)) }

1
1. n : ℕ
2. s : ℕn ⟶ ℤ
3. x : ℕ
4. y : ℕ
5. x < y
6. ∀j:ℕn + 1. ∀i:ℕj.  s.x@n i < s.x@n j
7. j : ℕn + 2
8. i : ℕj
9. j = (n + 1) ∈ ℤ
⊢ s.x@n.y@n + 1 i < s.x@n.y@n + 1 j

2
1. n : ℕ
2. s : ℕn ⟶ ℤ
3. x : ℕ
4. y : ℕ
5. x < y
6. ∀j:ℕn + 1. ∀i:ℕj.  s.x@n i < s.x@n j
7. j : ℕn + 2
8. i : ℕj
9. ¬(j = (n + 1) ∈ ℤ)
⊢ s.x@n.y@n + 1 i < s.x@n.y@n + 1 j

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    \mforall{}x,y:\mBbbN{}.
        (x  <  y  {}\mRightarrow{}  strictly-increasing-seq(n  +  1;s.x@n)  {}\mRightarrow{}  strictly-increasing-seq(n  +  2;s.x@n.y@n  +  1))


By

---

Latex:
(Intros  THEN  ParallelLast  THEN  Auto  THEN  (Decide  \mkleeneopen{}j  =  (n  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index