---

Step * of Lemma fadd_increasing

∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ].  (increasing(fadd(f;g);n)) supposing (nondecreasing(g;n) and increasing(f;n))
BY
{ ((((Unfolds ``increasing nondecreasing fadd`` 0 THEN Reduce 0) THEN Auto) THEN AllHyps (InstHyp [i])) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (increasing(fadd(f;g);n))  supposing  (nondecreasing(g;n)  and  increasing(f;n))


By

---

Latex:
((((Unfolds  ``increasing  nondecreasing  fadd``  0  THEN  Reduce  0)  THEN  Auto)
    THEN  AllHyps  (InstHyp  [i])
    )
  THEN  Auto'
  )

---

Home Index