		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-fsm-namemap-envlist

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

Definitions and Theorems

Function: svtv-fsm-namemap-envlist

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

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

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

Theorem: svtv-fsm-namemap-envlist-of-svex-envlist-fix-envs

(defthm svtv-fsm-namemap-envlist-of-svex-envlist-fix-envs
  (equal (svtv-fsm-namemap-envlist (svex-envlist-fix envs)
                                   map overridetype)
         (svtv-fsm-namemap-envlist envs map overridetype)))

Theorem: svtv-fsm-namemap-envlist-svex-envlist-equiv-congruence-on-envs

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

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

(defthm svtv-fsm-namemap-envlist-of-svtv-name-lhs-map-fix-map
  (equal (svtv-fsm-namemap-envlist envs (svtv-name-lhs-map-fix map)
                                   overridetype)
         (svtv-fsm-namemap-envlist envs map overridetype)))

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

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

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

(defthm
     svtv-fsm-namemap-envlist-of-svar-overridetype-fix-overridetype
 (equal
     (svtv-fsm-namemap-envlist envs map
                               (svar-overridetype-fix overridetype))
     (svtv-fsm-namemap-envlist envs map overridetype)))

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

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