		Search-engine friendly clone of the ACL2 documentation.

Latchsynth

Vl-modulelist-latchsynth-aux

Signature
(vl-modulelist-latchsynth-aux x careful-p vecp) → (mv new-x addmods)
Arguments: x — Guard (vl-modulelist-p x).; careful-p — Guard (booleanp careful-p).
Returns: new-x — Type (vl-modulelist-p new-x), given the guard.; addmods — Type (vl-modulelist-p addmods), given the guard.

Definitions and Theorems

Function: vl-modulelist-latchsynth-aux

(defun vl-modulelist-latchsynth-aux (x careful-p vecp)
  (declare (xargs :guard (and (vl-modulelist-p x)
                              (booleanp careful-p))))
  (let ((__function__ 'vl-modulelist-latchsynth-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil nil))
         ((mv car addmods1)
          (vl-module-latchsynth (car x)
                                careful-p vecp))
         ((mv cdr addmods2)
          (vl-modulelist-latchsynth-aux (cdr x)
                                        careful-p vecp)))
      (mv (cons car cdr)
          (append-without-guard addmods1 addmods2)))))

Theorem: vl-modulelist-p-of-vl-modulelist-latchsynth-aux.new-x

(defthm vl-modulelist-p-of-vl-modulelist-latchsynth-aux.new-x
  (implies (and (force (vl-modulelist-p x))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?addmods)
                 (vl-modulelist-latchsynth-aux x careful-p vecp)))
             (vl-modulelist-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-modulelist-p-of-vl-modulelist-latchsynth-aux.addmods

(defthm vl-modulelist-p-of-vl-modulelist-latchsynth-aux.addmods
  (implies (and (force (vl-modulelist-p x))
                (force (booleanp careful-p)))
           (b* (((mv ?new-x ?addmods)
                 (vl-modulelist-latchsynth-aux x careful-p vecp)))
             (vl-modulelist-p addmods)))
  :rule-classes :rewrite)