		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-hidtrace-mark-interfaces

Signature
(vl-hidtrace-mark-interfaces mtype trace ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; trace — Guard (vl-hidtrace-p trace).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-context1-p ctx).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-hidtrace-mark-interfaces

(defun vl-hidtrace-mark-interfaces (mtype trace ss st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (vl-hidtrace-p trace)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st)
                              (vl-context1-p ctx))))
  (let ((__function__ 'vl-hidtrace-mark-interfaces))
    (declare (ignorable __function__))
    (b* (((when (atom trace))
          (vl-lucidstate-fix st))
         (st (vl-hidstep-mark-interfaces mtype (car trace)
                                         ss st ctx)))
      (vl-hidtrace-mark-interfaces mtype (cdr trace)
                                   ss st ctx))))

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

(defthm vl-lucidstate-p-of-vl-hidtrace-mark-interfaces
  (b* ((new-st (vl-hidtrace-mark-interfaces mtype trace ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-hidtrace-mark-interfaces-of-vl-hidtrace-fix-trace

(defthm vl-hidtrace-mark-interfaces-of-vl-hidtrace-fix-trace
  (equal (vl-hidtrace-mark-interfaces mtype (vl-hidtrace-fix trace)
                                      ss st ctx)
         (vl-hidtrace-mark-interfaces mtype trace ss st ctx)))

Theorem: vl-hidtrace-mark-interfaces-vl-hidtrace-equiv-congruence-on-trace

(defthm
  vl-hidtrace-mark-interfaces-vl-hidtrace-equiv-congruence-on-trace
 (implies
  (vl-hidtrace-equiv trace trace-equiv)
  (equal (vl-hidtrace-mark-interfaces mtype trace ss st ctx)
         (vl-hidtrace-mark-interfaces mtype trace-equiv ss st ctx)))
 :rule-classes :congruence)

Theorem: vl-hidtrace-mark-interfaces-of-vl-scopestack-fix-ss

(defthm vl-hidtrace-mark-interfaces-of-vl-scopestack-fix-ss
 (equal
     (vl-hidtrace-mark-interfaces mtype trace (vl-scopestack-fix ss)
                                  st ctx)
     (vl-hidtrace-mark-interfaces mtype trace ss st ctx)))

Theorem: vl-hidtrace-mark-interfaces-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-hidtrace-mark-interfaces-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-hidtrace-mark-interfaces mtype trace ss st ctx)
         (vl-hidtrace-mark-interfaces mtype trace ss-equiv st ctx)))
 :rule-classes :congruence)

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

(defthm vl-hidtrace-mark-interfaces-of-vl-lucidstate-fix-st
 (equal
  (vl-hidtrace-mark-interfaces mtype trace ss (vl-lucidstate-fix st)
                               ctx)
  (vl-hidtrace-mark-interfaces mtype trace ss st ctx)))

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

(defthm
   vl-hidtrace-mark-interfaces-vl-lucidstate-equiv-congruence-on-st
 (implies
  (vl-lucidstate-equiv st st-equiv)
  (equal (vl-hidtrace-mark-interfaces mtype trace ss st ctx)
         (vl-hidtrace-mark-interfaces mtype trace ss st-equiv ctx)))
 :rule-classes :congruence)

Theorem: vl-hidtrace-mark-interfaces-of-vl-context1-fix-ctx

(defthm vl-hidtrace-mark-interfaces-of-vl-context1-fix-ctx
  (equal (vl-hidtrace-mark-interfaces
              mtype trace ss st (vl-context1-fix ctx))
         (vl-hidtrace-mark-interfaces mtype trace ss st ctx)))

Theorem: vl-hidtrace-mark-interfaces-vl-context1-equiv-congruence-on-ctx

(defthm
    vl-hidtrace-mark-interfaces-vl-context1-equiv-congruence-on-ctx
 (implies
  (vl-context1-equiv ctx ctx-equiv)
  (equal (vl-hidtrace-mark-interfaces mtype trace ss st ctx)
         (vl-hidtrace-mark-interfaces mtype trace ss st ctx-equiv)))
 :rule-classes :congruence)