---

Step * of Lemma strictly-increasing-seq-add2-implies

∀n:ℕ. ∀s:ℕn ⟶ ℕ. ∀x,y:ℕ.
  (strictly-increasing-seq(n + 2;s.x@n.y@n + 1)
  ⇒ {x < y ∧ strictly-increasing-seq(n + 1;s.x@n) ∧ strictly-increasing-seq(n + 1;s.y@n)})
BY
{ (Auto THEN D 0) }

1
1. n : ℕ
2. s : ℕn ⟶ ℕ
3. x : ℕ
4. y : ℕ
5. strictly-increasing-seq(n + 2;s.x@n.y@n + 1)
⊢ x < y

2
1. n : ℕ
2. s : ℕn ⟶ ℕ
3. x : ℕ
4. y : ℕ
5. strictly-increasing-seq(n + 2;s.x@n.y@n + 1)
⊢ strictly-increasing-seq(n + 1;s.x@n) ∧ strictly-increasing-seq(n + 1;s.y@n)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index