Step
*
of Lemma
rleq2-iff-rnonneg2
∀[x,y:ℕ+ ⟶ ℤ]. (rleq2(x;y)
⇐⇒ rnonneg2(reg-seq-add(y;-(x))))
BY
{ (RepUR ``reg-seq-add rminus`` 0
THEN Auto
THEN All (RepUR ``rleq2 rnonneg2``)
THEN RepeatFor 3 (ParallelLast)
THEN Auto) }
Latex:
Latex:
\mforall{}[x,y:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}]. (rleq2(x;y) \mLeftarrow{}{}\mRightarrow{} rnonneg2(reg-seq-add(y;-(x))))
By
Latex:
(RepUR ``reg-seq-add rminus`` 0
THEN Auto
THEN All (RepUR ``rleq2 rnonneg2``)
THEN RepeatFor 3 (ParallelLast)
THEN Auto)
Home
Index