		Search-engine friendly clone of the ACL2 documentation.

Shadowcheck

Vl-shadowcheck-interfaces

Signature
(vl-shadowcheck-interfaces x st) → (mv st new-x)
Arguments: x — Guard (vl-interfacelist-p x).; st — Guard (vl-shadowcheck-state-p st).
Returns: st — Type (vl-shadowcheck-state-p st).; new-x — Type (vl-interfacelist-p new-x).

Definitions and Theorems

Function: vl-shadowcheck-interfaces

(defun vl-shadowcheck-interfaces (x st)
  (declare (xargs :guard (and (vl-interfacelist-p x)
                              (vl-shadowcheck-state-p st))))
  (let ((__function__ 'vl-shadowcheck-interfaces))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv (vl-shadowcheck-state-fix st) nil))
         ((mv st car)
          (vl-shadowcheck-interface (car x) st))
         ((mv st rest)
          (vl-shadowcheck-interfaces (cdr x) st)))
      (mv st (cons car rest)))))

Theorem: vl-shadowcheck-state-p-of-vl-shadowcheck-interfaces.st

(defthm vl-shadowcheck-state-p-of-vl-shadowcheck-interfaces.st
  (b* (((mv ?st ?new-x)
        (vl-shadowcheck-interfaces x st)))
    (vl-shadowcheck-state-p st))
  :rule-classes :rewrite)

Theorem: vl-interfacelist-p-of-vl-shadowcheck-interfaces.new-x

(defthm vl-interfacelist-p-of-vl-shadowcheck-interfaces.new-x
  (b* (((mv ?st ?new-x)
        (vl-shadowcheck-interfaces x st)))
    (vl-interfacelist-p new-x))
  :rule-classes :rewrite)

Theorem: vl-shadowcheck-interfaces-of-vl-interfacelist-fix-x

(defthm vl-shadowcheck-interfaces-of-vl-interfacelist-fix-x
  (equal (vl-shadowcheck-interfaces (vl-interfacelist-fix x)
                                    st)
         (vl-shadowcheck-interfaces x st)))

Theorem: vl-shadowcheck-interfaces-vl-interfacelist-equiv-congruence-on-x

(defthm
   vl-shadowcheck-interfaces-vl-interfacelist-equiv-congruence-on-x
  (implies (vl-interfacelist-equiv x x-equiv)
           (equal (vl-shadowcheck-interfaces x st)
                  (vl-shadowcheck-interfaces x-equiv st)))
  :rule-classes :congruence)

Theorem: vl-shadowcheck-interfaces-of-vl-shadowcheck-state-fix-st

(defthm vl-shadowcheck-interfaces-of-vl-shadowcheck-state-fix-st
  (equal (vl-shadowcheck-interfaces x (vl-shadowcheck-state-fix st))
         (vl-shadowcheck-interfaces x st)))

Theorem: vl-shadowcheck-interfaces-vl-shadowcheck-state-equiv-congruence-on-st

(defthm
 vl-shadowcheck-interfaces-vl-shadowcheck-state-equiv-congruence-on-st
 (implies (vl-shadowcheck-state-equiv st st-equiv)
          (equal (vl-shadowcheck-interfaces x st)
                 (vl-shadowcheck-interfaces x st-equiv)))
 :rule-classes :congruence)