		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-dissect-database

Signature
(vl-lucid-dissect-database db reportcard st) → reportcard
Arguments: db — Already shrunk.
Guard (vl-luciddb-p db).; reportcard — Guard (vl-reportcard-p reportcard).; st — Guard (vl-lucidstate-p st).
Returns: reportcard — Type (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vl-lucid-dissect-database

(defun vl-lucid-dissect-database (db reportcard st)
  (declare (xargs :guard (and (vl-luciddb-p db)
                              (vl-reportcard-p reportcard)
                              (vl-lucidstate-p st))))
  (let ((__function__ 'vl-lucid-dissect-database))
    (declare (ignorable __function__))
    (b* ((db (vl-luciddb-fix db))
         ((when (atom db))
          (vl-reportcard-fix reportcard))
         ((cons key val) (car db))
         (reportcard (vl-lucid-dissect-pair key val reportcard st)))
      (vl-lucid-dissect-database (cdr db)
                                 reportcard st))))

Theorem: vl-reportcard-p-of-vl-lucid-dissect-database

(defthm vl-reportcard-p-of-vl-lucid-dissect-database
  (b* ((reportcard (vl-lucid-dissect-database db reportcard st)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-lucid-dissect-database-of-vl-luciddb-fix-db

(defthm vl-lucid-dissect-database-of-vl-luciddb-fix-db
  (equal (vl-lucid-dissect-database (vl-luciddb-fix db)
                                    reportcard st)
         (vl-lucid-dissect-database db reportcard st)))

Theorem: vl-lucid-dissect-database-vl-luciddb-equiv-congruence-on-db

(defthm vl-lucid-dissect-database-vl-luciddb-equiv-congruence-on-db
  (implies
       (vl-luciddb-equiv db db-equiv)
       (equal (vl-lucid-dissect-database db reportcard st)
              (vl-lucid-dissect-database db-equiv reportcard st)))
  :rule-classes :congruence)

Theorem: vl-lucid-dissect-database-of-vl-reportcard-fix-reportcard

(defthm vl-lucid-dissect-database-of-vl-reportcard-fix-reportcard
 (equal (vl-lucid-dissect-database db (vl-reportcard-fix reportcard)
                                   st)
        (vl-lucid-dissect-database db reportcard st)))

Theorem: vl-lucid-dissect-database-vl-reportcard-equiv-congruence-on-reportcard

(defthm
 vl-lucid-dissect-database-vl-reportcard-equiv-congruence-on-reportcard
 (implies
      (vl-reportcard-equiv reportcard reportcard-equiv)
      (equal (vl-lucid-dissect-database db reportcard st)
             (vl-lucid-dissect-database db reportcard-equiv st)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-database-of-vl-lucidstate-fix-st

(defthm vl-lucid-dissect-database-of-vl-lucidstate-fix-st
 (equal
    (vl-lucid-dissect-database db reportcard (vl-lucidstate-fix st))
    (vl-lucid-dissect-database db reportcard st)))

Theorem: vl-lucid-dissect-database-vl-lucidstate-equiv-congruence-on-st

(defthm
     vl-lucid-dissect-database-vl-lucidstate-equiv-congruence-on-st
  (implies
       (vl-lucidstate-equiv st st-equiv)
       (equal (vl-lucid-dissect-database db reportcard st)
              (vl-lucid-dissect-database db reportcard st-equiv)))
  :rule-classes :congruence)