		Search-engine friendly clone of the ACL2 documentation.

Bfrstate>=

Signature
(bfrstate>= x y) → *
Arguments: x — Guard (bfrstate-p x).; y — Guard (bfrstate-p y).

Definitions and Theorems

Function: bfrstate>=

(defun bfrstate>= (x y)
  (declare (xargs :guard (and (bfrstate-p x) (bfrstate-p y))))
  (let ((__function__ 'bfrstate>=))
    (declare (ignorable __function__))
    (and (eql (bfrstate->mode x)
              (bfrstate->mode y))
         (>= (bfrstate->bound x)
             (bfrstate->bound y)))))

Theorem: bfrstate>=-self

(defthm bfrstate>=-self
  (bfrstate>= x x))

Theorem: bfrstate>=-implies-mode

(defthm bfrstate>=-implies-mode
  (implies (bfrstate>= x y)
           (equal (bfrstate->mode x)
                  (bfrstate->mode y))))

Theorem: bfrstate>=-implies-bound

(defthm bfrstate>=-implies-bound
  (implies (bfrstate>= x y)
           (>= (bfrstate->bound x)
               (bfrstate->bound y)))
  :rule-classes (:rewrite :linear))

Theorem: bfrstate>=-of-bfrstate-fix-x

(defthm bfrstate>=-of-bfrstate-fix-x
  (equal (bfrstate>= (bfrstate-fix x) y)
         (bfrstate>= x y)))

Theorem: bfrstate>=-bfrstate-equiv-congruence-on-x

(defthm bfrstate>=-bfrstate-equiv-congruence-on-x
  (implies (bfrstate-equiv x x-equiv)
           (equal (bfrstate>= x y)
                  (bfrstate>= x-equiv y)))
  :rule-classes :congruence)

Theorem: bfrstate>=-of-bfrstate-fix-y

(defthm bfrstate>=-of-bfrstate-fix-y
  (equal (bfrstate>= x (bfrstate-fix y))
         (bfrstate>= x y)))

Theorem: bfrstate>=-bfrstate-equiv-congruence-on-y

(defthm bfrstate>=-bfrstate-equiv-congruence-on-y
  (implies (bfrstate-equiv y y-equiv)
           (equal (bfrstate>= x y)
                  (bfrstate>= x y-equiv)))
  :rule-classes :congruence)