		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-collect-inmap

Signature
(svtv-collect-inmap overridesp x acc) → new-acc
Arguments: overridesp — Guard (booleanp overridesp).; x — Guard (svtv-lines-p x).; acc — Guard (svtv-inputmap-p acc).
Returns: new-acc — Type (svtv-inputmap-p new-acc).

Definitions and Theorems

Function: svtv-collect-inmap

(defun svtv-collect-inmap (overridesp x acc)
 (declare (xargs :guard (and (booleanp overridesp)
                             (svtv-lines-p x)
                             (svtv-inputmap-p acc))))
 (let ((__function__ 'svtv-collect-inmap))
  (declare (ignorable __function__))
  (b*
   (((when (atom x))
     (svtv-inputmap-fix acc))
    ((svtv-line xf) (car x))
    (vars (svtv-entries->vars xf.entries))
    (overrideconds (and overridesp
                        (svtv-entries->overrideconds xf.entries))))
   (svtv-collect-inmap
    overridesp (cdr x)
    (append
         (pairlis$ vars
                   (replicate (len vars)
                              (if overridesp :override-val :input)))
         (pairlis$ overrideconds
                   (replicate (len overrideconds)
                              :override-test))
         acc)))))

Theorem: svtv-inputmap-p-of-svtv-collect-inmap

(defthm svtv-inputmap-p-of-svtv-collect-inmap
  (b* ((new-acc (svtv-collect-inmap overridesp x acc)))
    (svtv-inputmap-p new-acc))
  :rule-classes :rewrite)

Theorem: svtv-collect-inmap-of-bool-fix-overridesp

(defthm svtv-collect-inmap-of-bool-fix-overridesp
  (equal (svtv-collect-inmap (bool-fix overridesp)
                             x acc)
         (svtv-collect-inmap overridesp x acc)))

Theorem: svtv-collect-inmap-iff-congruence-on-overridesp

(defthm svtv-collect-inmap-iff-congruence-on-overridesp
  (implies (iff overridesp overridesp-equiv)
           (equal (svtv-collect-inmap overridesp x acc)
                  (svtv-collect-inmap overridesp-equiv x acc)))
  :rule-classes :congruence)

Theorem: svtv-collect-inmap-of-svtv-lines-fix-x

(defthm svtv-collect-inmap-of-svtv-lines-fix-x
  (equal (svtv-collect-inmap overridesp (svtv-lines-fix x)
                             acc)
         (svtv-collect-inmap overridesp x acc)))

Theorem: svtv-collect-inmap-svtv-lines-equiv-congruence-on-x

(defthm svtv-collect-inmap-svtv-lines-equiv-congruence-on-x
  (implies (svtv-lines-equiv x x-equiv)
           (equal (svtv-collect-inmap overridesp x acc)
                  (svtv-collect-inmap overridesp x-equiv acc)))
  :rule-classes :congruence)

Theorem: svtv-collect-inmap-of-svtv-inputmap-fix-acc

(defthm svtv-collect-inmap-of-svtv-inputmap-fix-acc
  (equal (svtv-collect-inmap overridesp x (svtv-inputmap-fix acc))
         (svtv-collect-inmap overridesp x acc)))

Theorem: svtv-collect-inmap-svtv-inputmap-equiv-congruence-on-acc

(defthm svtv-collect-inmap-svtv-inputmap-equiv-congruence-on-acc
  (implies (svtv-inputmap-equiv acc acc-equiv)
           (equal (svtv-collect-inmap overridesp x acc)
                  (svtv-collect-inmap overridesp x acc-equiv)))
  :rule-classes :congruence)