		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svex-monotonic-p

Definitions and Theorems

Theorem: svex-eval-equiv-implies-equal-svex-monotonic-p-1

(defthm svex-eval-equiv-implies-equal-svex-monotonic-p-1
  (implies (svex-eval-equiv x x-equiv)
           (equal (svex-monotonic-p x)
                  (svex-monotonic-p x-equiv)))
  :rule-classes (:congruence))

Theorem: svex-var-monotonic

(defthm svex-var-monotonic
  (svex-monotonic-p (svex-var k)))