Step
*
of Lemma
rabs_functionality_wrt_bdd-diff
No Annotations
∀x,y:ℕ+ ⟶ ℤ. (bdd-diff(x;y)
⇒ bdd-diff(|x|;|y|))
BY
{ ((RWO "rabs-as-rmax" 0 THEN Auto)
THEN (RWO "-1" 0 THEN Try (Complete (Auto)))
THEN Try (Complete ((RepUR ``rmax rminus`` 0 THEN Auto)))
THEN RelRST
THEN RepUR ``rmax rminus`` 0
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}x,y:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}. (bdd-diff(x;y) {}\mRightarrow{} bdd-diff(|x|;|y|))
By
Latex:
((RWO "rabs-as-rmax" 0 THEN Auto)
THEN (RWO "-1" 0 THEN Try (Complete (Auto)))
THEN Try (Complete ((RepUR ``rmax rminus`` 0 THEN Auto)))
THEN RelRST
THEN RepUR ``rmax rminus`` 0
THEN Auto)
Home
Index