		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Make-simple-lhs

Signature
(make-simple-lhs &key width (rsh '0) var) → lhs
Arguments: width — Guard (posp width).; rsh — Guard (natp rsh).; var — Guard (svar-p var).
Returns: lhs — Type (lhs-p lhs).

Definitions and Theorems

Function: make-simple-lhs-fn

(defun make-simple-lhs-fn (width rsh var)
 (declare (xargs :guard (and (posp width)
                             (natp rsh)
                             (svar-p var))))
 (let ((__function__ 'make-simple-lhs))
  (declare (ignorable __function__))
  (list (make-lhrange :w width
                      :atom (make-lhatom-var :name var :rsh rsh)))))

Theorem: lhs-p-of-make-simple-lhs

(defthm lhs-p-of-make-simple-lhs
  (b* ((lhs (make-simple-lhs-fn width rsh var)))
    (lhs-p lhs))
  :rule-classes :rewrite)

Theorem: vars-of-make-simple-lhs

(defthm vars-of-make-simple-lhs
  (b* ((?lhs (make-simple-lhs-fn width rsh var)))
    (equal (lhs-vars lhs)
           (list (svar-fix var)))))

Theorem: make-simple-lhs-fn-of-pos-fix-width

(defthm make-simple-lhs-fn-of-pos-fix-width
  (equal (make-simple-lhs-fn (pos-fix width)
                             rsh var)
         (make-simple-lhs-fn width rsh var)))

Theorem: make-simple-lhs-fn-pos-equiv-congruence-on-width

(defthm make-simple-lhs-fn-pos-equiv-congruence-on-width
  (implies (pos-equiv width width-equiv)
           (equal (make-simple-lhs-fn width rsh var)
                  (make-simple-lhs-fn width-equiv rsh var)))
  :rule-classes :congruence)

Theorem: make-simple-lhs-fn-of-nfix-rsh

(defthm make-simple-lhs-fn-of-nfix-rsh
  (equal (make-simple-lhs-fn width (nfix rsh)
                             var)
         (make-simple-lhs-fn width rsh var)))

Theorem: make-simple-lhs-fn-nat-equiv-congruence-on-rsh

(defthm make-simple-lhs-fn-nat-equiv-congruence-on-rsh
  (implies (nat-equiv rsh rsh-equiv)
           (equal (make-simple-lhs-fn width rsh var)
                  (make-simple-lhs-fn width rsh-equiv var)))
  :rule-classes :congruence)

Theorem: make-simple-lhs-fn-of-svar-fix-var

(defthm make-simple-lhs-fn-of-svar-fix-var
  (equal (make-simple-lhs-fn width rsh (svar-fix var))
         (make-simple-lhs-fn width rsh var)))

Theorem: make-simple-lhs-fn-svar-equiv-congruence-on-var

(defthm make-simple-lhs-fn-svar-equiv-congruence-on-var
  (implies (svar-equiv var var-equiv)
           (equal (make-simple-lhs-fn width rsh var)
                  (make-simple-lhs-fn width rsh var-equiv)))
  :rule-classes :congruence)