		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidstate-mark

Signature
(vl-lucidstate-mark mtype key occ st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; key — Guard (vl-lucidkey-p key).; occ — Guard (vl-lucidocc-p occ).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-lucidctx-p ctx).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-lucidstate-mark

(defun vl-lucidstate-mark (mtype key occ st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (vl-lucidkey-p key)
                              (vl-lucidocc-p occ)
                              (vl-lucidstate-p st)
                              (vl-lucidctx-p ctx))))
  (let ((__function__ 'vl-lucidstate-mark))
    (declare (ignorable __function__))
    (b* (((vl-lucidstate st))
         (db (vl-luciddb-mark mtype key occ st.db ctx)))
      (change-vl-lucidstate st :db db))))

Theorem: vl-lucidstate-p-of-vl-lucidstate-mark

(defthm vl-lucidstate-p-of-vl-lucidstate-mark
  (b* ((new-st (vl-lucidstate-mark mtype key occ st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-lucidstate-mark-of-vl-lucidkey-fix-key

(defthm vl-lucidstate-mark-of-vl-lucidkey-fix-key
  (equal (vl-lucidstate-mark mtype (vl-lucidkey-fix key)
                             occ st ctx)
         (vl-lucidstate-mark mtype key occ st ctx)))

Theorem: vl-lucidstate-mark-vl-lucidkey-equiv-congruence-on-key

(defthm vl-lucidstate-mark-vl-lucidkey-equiv-congruence-on-key
  (implies (vl-lucidkey-equiv key key-equiv)
           (equal (vl-lucidstate-mark mtype key occ st ctx)
                  (vl-lucidstate-mark mtype key-equiv occ st ctx)))
  :rule-classes :congruence)

Theorem: vl-lucidstate-mark-of-vl-lucidocc-fix-occ

(defthm vl-lucidstate-mark-of-vl-lucidocc-fix-occ
  (equal (vl-lucidstate-mark mtype key (vl-lucidocc-fix occ)
                             st ctx)
         (vl-lucidstate-mark mtype key occ st ctx)))

Theorem: vl-lucidstate-mark-vl-lucidocc-equiv-congruence-on-occ

(defthm vl-lucidstate-mark-vl-lucidocc-equiv-congruence-on-occ
  (implies (vl-lucidocc-equiv occ occ-equiv)
           (equal (vl-lucidstate-mark mtype key occ st ctx)
                  (vl-lucidstate-mark mtype key occ-equiv st ctx)))
  :rule-classes :congruence)

Theorem: vl-lucidstate-mark-of-vl-lucidstate-fix-st

(defthm vl-lucidstate-mark-of-vl-lucidstate-fix-st
  (equal (vl-lucidstate-mark mtype key occ (vl-lucidstate-fix st)
                             ctx)
         (vl-lucidstate-mark mtype key occ st ctx)))

Theorem: vl-lucidstate-mark-vl-lucidstate-equiv-congruence-on-st

(defthm vl-lucidstate-mark-vl-lucidstate-equiv-congruence-on-st
  (implies (vl-lucidstate-equiv st st-equiv)
           (equal (vl-lucidstate-mark mtype key occ st ctx)
                  (vl-lucidstate-mark mtype key occ st-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-lucidstate-mark-of-vl-lucidctx-fix-ctx

(defthm vl-lucidstate-mark-of-vl-lucidctx-fix-ctx
  (equal (vl-lucidstate-mark mtype key occ st (vl-lucidctx-fix ctx))
         (vl-lucidstate-mark mtype key occ st ctx)))

Theorem: vl-lucidstate-mark-vl-lucidctx-equiv-congruence-on-ctx

(defthm vl-lucidstate-mark-vl-lucidctx-equiv-congruence-on-ctx
  (implies (vl-lucidctx-equiv ctx ctx-equiv)
           (equal (vl-lucidstate-mark mtype key occ st ctx)
                  (vl-lucidstate-mark mtype key occ st ctx-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-luciddb-mark