		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-design-lucid

Signature
(vl-design-lucid x &key (paramsp 't) (generatesp 't)) → new-x
Arguments: x — Guard (vl-design-p x).; paramsp — Guard (booleanp paramsp).; generatesp — Guard (booleanp generatesp).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-design-lucid-fn

(defun vl-design-lucid-fn (x paramsp generatesp)
  (declare (xargs :guard (and (vl-design-p x)
                              (booleanp paramsp)
                              (booleanp generatesp))))
  (let ((__function__ 'vl-design-lucid))
    (declare (ignorable __function__))
    (b* ((x (cwtime (hons-copy (vl-design-fix x))
                    :name vl-design-lucid-hons
                    :mintime 1))
         (ss (vl-scopestack-init x))
         (st (cwtime (vl-lucidstate-init x
                                         :paramsp paramsp
                                         :generatesp generatesp)))
         (st (cwtime (vl-design-lucidcheck-main x ss st)))
         (reportcard (cwtime (vl-lucid-dissect st))))
      (vl-scopestacks-free)
      (vl-apply-reportcard x reportcard))))

Theorem: vl-design-p-of-vl-design-lucid

(defthm vl-design-p-of-vl-design-lucid
  (b* ((new-x (vl-design-lucid-fn x paramsp generatesp)))
    (vl-design-p new-x))
  :rule-classes :rewrite)

Theorem: vl-design-lucid-fn-of-vl-design-fix-x

(defthm vl-design-lucid-fn-of-vl-design-fix-x
  (equal (vl-design-lucid-fn (vl-design-fix x)
                             paramsp generatesp)
         (vl-design-lucid-fn x paramsp generatesp)))

Theorem: vl-design-lucid-fn-vl-design-equiv-congruence-on-x

(defthm vl-design-lucid-fn-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design-lucid-fn x paramsp generatesp)
                  (vl-design-lucid-fn x-equiv paramsp generatesp)))
  :rule-classes :congruence)

Theorem: vl-design-lucid-fn-of-bool-fix-paramsp

(defthm vl-design-lucid-fn-of-bool-fix-paramsp
  (equal (vl-design-lucid-fn x (acl2::bool-fix paramsp)
                             generatesp)
         (vl-design-lucid-fn x paramsp generatesp)))

Theorem: vl-design-lucid-fn-iff-congruence-on-paramsp

(defthm vl-design-lucid-fn-iff-congruence-on-paramsp
  (implies (iff paramsp paramsp-equiv)
           (equal (vl-design-lucid-fn x paramsp generatesp)
                  (vl-design-lucid-fn x paramsp-equiv generatesp)))
  :rule-classes :congruence)

Theorem: vl-design-lucid-fn-of-bool-fix-generatesp

(defthm vl-design-lucid-fn-of-bool-fix-generatesp
  (equal (vl-design-lucid-fn x paramsp (acl2::bool-fix generatesp))
         (vl-design-lucid-fn x paramsp generatesp)))

Theorem: vl-design-lucid-fn-iff-congruence-on-generatesp

(defthm vl-design-lucid-fn-iff-congruence-on-generatesp
  (implies (iff generatesp generatesp-equiv)
           (equal (vl-design-lucid-fn x paramsp generatesp)
                  (vl-design-lucid-fn x paramsp generatesp-equiv)))
  :rule-classes :congruence)