		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-alwayslist-edgesynth

Extends vl-always-edgesynth to a list of always blocks.

Signature
(vl-alwayslist-edgesynth x scary-regs vars cvtregs delta &key vecp) → (mv new-x cvtregs delta)
Arguments: x — Guard (vl-alwayslist-p x).; scary-regs — Guard (string-listp scary-regs).; vars — Guard (vl-vardecllist-p vars).; cvtregs — Guard (string-listp cvtregs).; delta — Guard (vl-delta-p delta).
Returns: new-x — Type (vl-alwayslist-p new-x), given the guard.; cvtregs — Type (string-listp cvtregs), given the guard.; delta — Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-alwayslist-edgesynth-fn

(defun vl-alwayslist-edgesynth-fn
       (x scary-regs vars cvtregs delta vecp)
  (declare (xargs :guard (and (vl-alwayslist-p x)
                              (string-listp scary-regs)
                              (vl-vardecllist-p vars)
                              (string-listp cvtregs)
                              (vl-delta-p delta))))
  (let ((__function__ 'vl-alwayslist-edgesynth))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil cvtregs delta))
         ((mv new-car? cvtregs delta)
          (vl-always-edgesynth (car x)
                               scary-regs vars cvtregs delta
                               :vecp vecp))
         ((mv new-cdr cvtregs delta)
          (vl-alwayslist-edgesynth (cdr x)
                                   scary-regs vars cvtregs delta
                                   :vecp vecp))
         (new-x (if new-car? (cons new-car? new-cdr)
                  new-cdr)))
      (mv new-x cvtregs delta))))

Theorem: vl-alwayslist-p-of-vl-alwayslist-edgesynth.new-x

(defthm vl-alwayslist-p-of-vl-alwayslist-edgesynth.new-x
  (implies (and (force (vl-alwayslist-p x))
                (force (string-listp scary-regs))
                (force (vl-vardecllist-p vars))
                (force (string-listp cvtregs))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?cvtregs ?delta)
                 (vl-alwayslist-edgesynth-fn
                      x scary-regs vars cvtregs delta vecp)))
             (vl-alwayslist-p new-x)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-alwayslist-edgesynth.cvtregs

(defthm string-listp-of-vl-alwayslist-edgesynth.cvtregs
  (implies (and (force (vl-alwayslist-p x))
                (force (string-listp scary-regs))
                (force (vl-vardecllist-p vars))
                (force (string-listp cvtregs))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?cvtregs ?delta)
                 (vl-alwayslist-edgesynth-fn
                      x scary-regs vars cvtregs delta vecp)))
             (string-listp cvtregs)))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-alwayslist-edgesynth.delta

(defthm vl-delta-p-of-vl-alwayslist-edgesynth.delta
  (implies (and (force (vl-alwayslist-p x))
                (force (string-listp scary-regs))
                (force (vl-vardecllist-p vars))
                (force (string-listp cvtregs))
                (force (vl-delta-p delta)))
           (b* (((mv ?new-x ?cvtregs ?delta)
                 (vl-alwayslist-edgesynth-fn
                      x scary-regs vars cvtregs delta vecp)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)