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