		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Lhprobe/4vec-change-override

Signature
(lhprobe/4vec-change-override x type) → new-x
Arguments: x — Guard (lhprobe/4vec-p x).; type — Guard (svar-overridetype-p type).
Returns: new-x — Type (lhprobe/4vec-p new-x).

Definitions and Theorems

Function: lhprobe/4vec-change-override

(defun lhprobe/4vec-change-override (x type)
  (declare (xargs :guard (and (lhprobe/4vec-p x)
                              (svar-overridetype-p type))))
  (let ((__function__ 'lhprobe/4vec-change-override))
    (declare (ignorable __function__))
    (lhprobe/4vec-case x
                       :4vec (4vec-fix x)
                       :lhprobe (lhprobe-change-override x type))))

Theorem: lhprobe/4vec-p-of-lhprobe/4vec-change-override

(defthm lhprobe/4vec-p-of-lhprobe/4vec-change-override
  (b* ((new-x (lhprobe/4vec-change-override x type)))
    (lhprobe/4vec-p new-x))
  :rule-classes :rewrite)

Theorem: lhprobe/4vec-change-override-of-lhprobe/4vec-fix-x

(defthm lhprobe/4vec-change-override-of-lhprobe/4vec-fix-x
  (equal (lhprobe/4vec-change-override (lhprobe/4vec-fix x)
                                       type)
         (lhprobe/4vec-change-override x type)))

Theorem: lhprobe/4vec-change-override-lhprobe/4vec-equiv-congruence-on-x

(defthm
    lhprobe/4vec-change-override-lhprobe/4vec-equiv-congruence-on-x
  (implies (lhprobe/4vec-equiv x x-equiv)
           (equal (lhprobe/4vec-change-override x type)
                  (lhprobe/4vec-change-override x-equiv type)))
  :rule-classes :congruence)

Theorem: lhprobe/4vec-change-override-of-svar-overridetype-fix-type

(defthm lhprobe/4vec-change-override-of-svar-overridetype-fix-type
  (equal
       (lhprobe/4vec-change-override x (svar-overridetype-fix type))
       (lhprobe/4vec-change-override x type)))

Theorem: lhprobe/4vec-change-override-svar-overridetype-equiv-congruence-on-type

(defthm
 lhprobe/4vec-change-override-svar-overridetype-equiv-congruence-on-type
 (implies (svar-overridetype-equiv type type-equiv)
          (equal (lhprobe/4vec-change-override x type)
                 (lhprobe/4vec-change-override x type-equiv)))
 :rule-classes :congruence)