		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-fsm-namemap-alistlist

Signature
(svtv-fsm-namemap-alistlist alists map overridetype) → stage-alists
Arguments: alists — Guard (svex-alistlist-p alists).; map — Guard (svtv-name-lhs-map-p map).; overridetype — Guard (svar-overridetype-p overridetype).
Returns: stage-alists — Type (svex-alistlist-p stage-alists).

Definitions and Theorems

Function: svtv-fsm-namemap-alistlist

(defun svtv-fsm-namemap-alistlist (alists map overridetype)
  (declare (xargs :guard (and (svex-alistlist-p alists)
                              (svtv-name-lhs-map-p map)
                              (svar-overridetype-p overridetype))))
  (let ((__function__ 'svtv-fsm-namemap-alistlist))
    (declare (ignorable __function__))
    (if (atom alists)
        nil
      (cons (svtv-fsm-namemap-alist-subst (car alists)
                                          map overridetype)
            (svtv-fsm-namemap-alistlist (cdr alists)
                                        map overridetype)))))

Theorem: svex-alistlist-p-of-svtv-fsm-namemap-alistlist

(defthm svex-alistlist-p-of-svtv-fsm-namemap-alistlist
  (b* ((stage-alists
            (svtv-fsm-namemap-alistlist alists map overridetype)))
    (svex-alistlist-p stage-alists))
  :rule-classes :rewrite)

Theorem: svtv-fsm-namemap-alistlist-of-svex-alistlist-fix-alists

(defthm svtv-fsm-namemap-alistlist-of-svex-alistlist-fix-alists
  (equal (svtv-fsm-namemap-alistlist (svex-alistlist-fix alists)
                                     map overridetype)
         (svtv-fsm-namemap-alistlist alists map overridetype)))

Theorem: svtv-fsm-namemap-alistlist-svex-alistlist-equiv-congruence-on-alists

(defthm
 svtv-fsm-namemap-alistlist-svex-alistlist-equiv-congruence-on-alists
 (implies
   (svex-alistlist-equiv alists alists-equiv)
   (equal
        (svtv-fsm-namemap-alistlist alists map overridetype)
        (svtv-fsm-namemap-alistlist alists-equiv map overridetype)))
 :rule-classes :congruence)

Theorem: svtv-fsm-namemap-alistlist-of-svtv-name-lhs-map-fix-map

(defthm svtv-fsm-namemap-alistlist-of-svtv-name-lhs-map-fix-map
 (equal
      (svtv-fsm-namemap-alistlist alists (svtv-name-lhs-map-fix map)
                                  overridetype)
      (svtv-fsm-namemap-alistlist alists map overridetype)))

Theorem: svtv-fsm-namemap-alistlist-svtv-name-lhs-map-equiv-congruence-on-map

(defthm
 svtv-fsm-namemap-alistlist-svtv-name-lhs-map-equiv-congruence-on-map
 (implies
   (svtv-name-lhs-map-equiv map map-equiv)
   (equal
        (svtv-fsm-namemap-alistlist alists map overridetype)
        (svtv-fsm-namemap-alistlist alists map-equiv overridetype)))
 :rule-classes :congruence)

Theorem: svtv-fsm-namemap-alistlist-of-svar-overridetype-fix-overridetype

(defthm
   svtv-fsm-namemap-alistlist-of-svar-overridetype-fix-overridetype
 (equal
   (svtv-fsm-namemap-alistlist alists map
                               (svar-overridetype-fix overridetype))
   (svtv-fsm-namemap-alistlist alists map overridetype)))

Theorem: svtv-fsm-namemap-alistlist-svar-overridetype-equiv-congruence-on-overridetype

(defthm
 svtv-fsm-namemap-alistlist-svar-overridetype-equiv-congruence-on-overridetype
 (implies
   (svar-overridetype-equiv overridetype overridetype-equiv)
   (equal
        (svtv-fsm-namemap-alistlist alists map overridetype)
        (svtv-fsm-namemap-alistlist alists map overridetype-equiv)))
 :rule-classes :congruence)