		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-design-lucidcheck-main

Signature
(vl-design-lucidcheck-main x ss st) → new-st
Arguments: x — Guard (vl-design-p x).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-design-lucidcheck-main

(defun vl-design-lucidcheck-main (x ss st)
  (declare (xargs :guard (and (vl-design-p x)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st))))
  (let ((__function__ 'vl-design-lucidcheck-main))
    (declare (ignorable __function__))
    (b* (((vl-design x))
         (st (vl-modulelist-lucidcheck x.mods ss st))
         (st (vl-interfacelist-lucidcheck x.interfaces ss st))
         (st (vl-packagelist-lucidcheck x.packages ss st))
         (st (vl-vardecllist-lucidcheck x.vardecls ss st))
         (st (vl-fundecllist-lucidcheck x.fundecls ss st))
         (st (vl-taskdecllist-lucidcheck x.taskdecls ss st))
         (st (vl-paramdecllist-lucidcheck x.paramdecls ss st))
         (st (vl-dpiimportlist-lucidcheck x.dpiimports ss st))
         (st (vl-dpiexportlist-lucidcheck x.dpiexports ss st))
         (st (vl-typedeflist-lucidcheck x.typedefs ss st)))
      st)))

Theorem: vl-lucidstate-p-of-vl-design-lucidcheck-main

(defthm vl-lucidstate-p-of-vl-design-lucidcheck-main
  (b* ((new-st (vl-design-lucidcheck-main x ss st)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-design-lucidcheck-main-of-vl-design-fix-x

(defthm vl-design-lucidcheck-main-of-vl-design-fix-x
  (equal (vl-design-lucidcheck-main (vl-design-fix x)
                                    ss st)
         (vl-design-lucidcheck-main x ss st)))

Theorem: vl-design-lucidcheck-main-vl-design-equiv-congruence-on-x

(defthm vl-design-lucidcheck-main-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design-lucidcheck-main x ss st)
                  (vl-design-lucidcheck-main x-equiv ss st)))
  :rule-classes :congruence)

Theorem: vl-design-lucidcheck-main-of-vl-scopestack-fix-ss

(defthm vl-design-lucidcheck-main-of-vl-scopestack-fix-ss
  (equal (vl-design-lucidcheck-main x (vl-scopestack-fix ss)
                                    st)
         (vl-design-lucidcheck-main x ss st)))

Theorem: vl-design-lucidcheck-main-vl-scopestack-equiv-congruence-on-ss

(defthm
     vl-design-lucidcheck-main-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-design-lucidcheck-main x ss st)
                  (vl-design-lucidcheck-main x ss-equiv st)))
  :rule-classes :congruence)

Theorem: vl-design-lucidcheck-main-of-vl-lucidstate-fix-st

(defthm vl-design-lucidcheck-main-of-vl-lucidstate-fix-st
  (equal (vl-design-lucidcheck-main x ss (vl-lucidstate-fix st))
         (vl-design-lucidcheck-main x ss st)))

Theorem: vl-design-lucidcheck-main-vl-lucidstate-equiv-congruence-on-st

(defthm
     vl-design-lucidcheck-main-vl-lucidstate-equiv-congruence-on-st
  (implies (vl-lucidstate-equiv st st-equiv)
           (equal (vl-design-lucidcheck-main x ss st)
                  (vl-design-lucidcheck-main x ss st-equiv)))
  :rule-classes :congruence)