---

Step * of Lemma fshift_increasing

∀[n:ℕ]. ∀[x:ℤ]. ∀[f:ℕn ⟶ ℤ].  (increasing(fshift(f;x);n + 1)) supposing (x < f 0 and 0 < n and increasing(f;n))
BY
{ (Unfolds ``increasing fshift`` 0
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit
   THEN Subst' (i + 1) - 1 ~ (i - 1) + 1 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (increasing(fshift(f;x);n  +  1))  supposing  (x  <  f  0  and  0  <  n  and  increasing(f;n))


By

---

Latex:
(Unfolds  ``increasing  fshift``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit
  THEN  Subst'  (i  +  1)  -  1  \msim{}  (i  -  1)  +  1  0
  THEN  Auto)

---

Home Index