		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-dissect-database

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

Definitions and Theorems

Function: vl-lucid-dissect-database

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

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

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

Theorem: vl-typocandidates-p-of-vl-lucid-dissect-database.typos

(defthm vl-typocandidates-p-of-vl-lucid-dissect-database.typos
  (b* (((mv ?reportcard ?typos)
        (vl-lucid-dissect-database db reportcard st typos)))
    (vl-typocandidates-p typos))
  :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 typos)
         (vl-lucid-dissect-database db reportcard st typos)))

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 typos)
          (vl-lucid-dissect-database db-equiv reportcard st typos)))
 :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 typos)
        (vl-lucid-dissect-database db reportcard st typos)))

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 typos)
          (vl-lucid-dissect-database db reportcard-equiv st typos)))
 :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)
                                typos)
     (vl-lucid-dissect-database db reportcard st typos)))

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 typos)
          (vl-lucid-dissect-database db reportcard st-equiv typos)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-database-of-vl-typocandidates-fix-typos

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

Theorem: vl-lucid-dissect-database-vl-typocandidates-equiv-congruence-on-typos

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