		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Lhs-register-indnamememo

Signature
(lhs-register-indnamememo x scope moddb indnamememo) → indnamememo1
Arguments: x — Guard (lhs-p x).; scope — Guard (modscope-p scope).; moddb — Guard (moddb-ok moddb).
Returns: indnamememo1 — Type (equal (len indnamememo1) (len indnamememo)).

Definitions and Theorems

Function: lhs-register-indnamememo

(defun
 lhs-register-indnamememo
 (x scope moddb indnamememo)
 (declare (xargs :stobjs (moddb indnamememo)))
 (declare (xargs :guard (and (lhs-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
      :guard
      (and (modscope-okp scope moddb)
           (svarlist-boundedp (lhs-vars x)
                              (modscope-local-bound scope moddb)))))
 (let
  ((__function__ 'lhs-register-indnamememo))
  (declare (ignorable __function__))
  (b*
   (((mv first rest) (lhs-decomp x))
    ((unless first) indnamememo)
    ((lhrange first) first)
    (indnamememo
     (lhatom-case
         first.atom
         :z indnamememo
         :var (svar-register-indnamememo first.atom.name
                                         scope moddb indnamememo))))
   (lhs-register-indnamememo rest scope moddb indnamememo))))

Theorem: return-type-of-lhs-register-indnamememo

(defthm
    return-type-of-lhs-register-indnamememo
    (b* ((indnamememo1
              (lhs-register-indnamememo x scope moddb indnamememo)))
        (equal (len indnamememo1)
               (len indnamememo)))
    :rule-classes :rewrite)

Theorem: lhs-register-indnamememo-of-lhs-fix-x

(defthm
     lhs-register-indnamememo-of-lhs-fix-x
     (equal (lhs-register-indnamememo (lhs-fix x)
                                      scope moddb indnamememo)
            (lhs-register-indnamememo x scope moddb indnamememo)))

Theorem: lhs-register-indnamememo-lhs-equiv-congruence-on-x

(defthm
 lhs-register-indnamememo-lhs-equiv-congruence-on-x
 (implies
   (lhs-equiv x x-equiv)
   (equal
        (lhs-register-indnamememo x scope moddb indnamememo)
        (lhs-register-indnamememo x-equiv scope moddb indnamememo)))
 :rule-classes :congruence)

Theorem: lhs-register-indnamememo-of-modscope-fix-scope

(defthm
     lhs-register-indnamememo-of-modscope-fix-scope
     (equal (lhs-register-indnamememo x (modscope-fix scope)
                                      moddb indnamememo)
            (lhs-register-indnamememo x scope moddb indnamememo)))

Theorem: lhs-register-indnamememo-modscope-equiv-congruence-on-scope

(defthm
 lhs-register-indnamememo-modscope-equiv-congruence-on-scope
 (implies
   (modscope-equiv scope scope-equiv)
   (equal
        (lhs-register-indnamememo x scope moddb indnamememo)
        (lhs-register-indnamememo x scope-equiv moddb indnamememo)))
 :rule-classes :congruence)

Theorem: lhs-register-indnamememo-of-moddb-fix-moddb

(defthm
     lhs-register-indnamememo-of-moddb-fix-moddb
     (equal (lhs-register-indnamememo x scope (moddb-fix moddb)
                                      indnamememo)
            (lhs-register-indnamememo x scope moddb indnamememo)))

Theorem: lhs-register-indnamememo-moddb-equiv-congruence-on-moddb

(defthm
 lhs-register-indnamememo-moddb-equiv-congruence-on-moddb
 (implies
   (moddb-equiv moddb moddb-equiv)
   (equal
        (lhs-register-indnamememo x scope moddb indnamememo)
        (lhs-register-indnamememo x scope moddb-equiv indnamememo)))
 :rule-classes :congruence)