		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-spec-fsm-constraints-for-alists

Signature
(svtv-spec-fsm-constraints-for-alists x stage namemap overridetype bindings) → constraints
Arguments: x — Guard (svar/4vec-alistlist-p x).; stage — Guard (natp stage).; namemap — Guard (svtv-name-lhs-map-p namemap).; overridetype — Guard (svar-overridetype-p overridetype).; bindings — Guard (lhprobe-map-p bindings).
Returns: constraints — Type (lhprobe-constraintlist-p constraints).

Definitions and Theorems

Function: svtv-spec-fsm-constraints-for-alists

(defun svtv-spec-fsm-constraints-for-alists
       (x stage namemap overridetype bindings)
  (declare (xargs :guard (and (svar/4vec-alistlist-p x)
                              (natp stage)
                              (svtv-name-lhs-map-p namemap)
                              (svar-overridetype-p overridetype)
                              (lhprobe-map-p bindings))))
  (let ((__function__ 'svtv-spec-fsm-constraints-for-alists))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (append (svtv-spec-fsm-constraints-for-alist
                   (car x)
                   stage namemap overridetype bindings)
              (svtv-spec-fsm-constraints-for-alists
                   (cdr x)
                   (1+ (lnfix stage))
                   namemap overridetype bindings)))))

Theorem: lhprobe-constraintlist-p-of-svtv-spec-fsm-constraints-for-alists

(defthm
   lhprobe-constraintlist-p-of-svtv-spec-fsm-constraints-for-alists
  (b* ((constraints (svtv-spec-fsm-constraints-for-alists
                         x stage namemap overridetype bindings)))
    (lhprobe-constraintlist-p constraints))
  :rule-classes :rewrite)

Theorem: svtv-spec-fsm-constraints-for-alists-of-svar/4vec-alistlist-fix-x

(defthm
  svtv-spec-fsm-constraints-for-alists-of-svar/4vec-alistlist-fix-x
  (equal (svtv-spec-fsm-constraints-for-alists
              (svar/4vec-alistlist-fix x)
              stage namemap overridetype bindings)
         (svtv-spec-fsm-constraints-for-alists
              x stage namemap overridetype bindings)))

Theorem: svtv-spec-fsm-constraints-for-alists-svar/4vec-alistlist-equiv-congruence-on-x

(defthm
 svtv-spec-fsm-constraints-for-alists-svar/4vec-alistlist-equiv-congruence-on-x
 (implies (svar/4vec-alistlist-equiv x x-equiv)
          (equal (svtv-spec-fsm-constraints-for-alists
                      x stage namemap overridetype bindings)
                 (svtv-spec-fsm-constraints-for-alists
                      x-equiv
                      stage namemap overridetype bindings)))
 :rule-classes :congruence)

Theorem: svtv-spec-fsm-constraints-for-alists-of-nfix-stage

(defthm svtv-spec-fsm-constraints-for-alists-of-nfix-stage
  (equal (svtv-spec-fsm-constraints-for-alists
              x (nfix stage)
              namemap overridetype bindings)
         (svtv-spec-fsm-constraints-for-alists
              x stage namemap overridetype bindings)))

Theorem: svtv-spec-fsm-constraints-for-alists-nat-equiv-congruence-on-stage

(defthm
 svtv-spec-fsm-constraints-for-alists-nat-equiv-congruence-on-stage
 (implies (nat-equiv stage stage-equiv)
          (equal (svtv-spec-fsm-constraints-for-alists
                      x stage namemap overridetype bindings)
                 (svtv-spec-fsm-constraints-for-alists
                      x stage-equiv
                      namemap overridetype bindings)))
 :rule-classes :congruence)

Theorem: svtv-spec-fsm-constraints-for-alists-of-svtv-name-lhs-map-fix-namemap

(defthm
 svtv-spec-fsm-constraints-for-alists-of-svtv-name-lhs-map-fix-namemap
 (equal (svtv-spec-fsm-constraints-for-alists
             x stage (svtv-name-lhs-map-fix namemap)
             overridetype bindings)
        (svtv-spec-fsm-constraints-for-alists
             x stage namemap overridetype bindings)))

Theorem: svtv-spec-fsm-constraints-for-alists-svtv-name-lhs-map-equiv-congruence-on-namemap

(defthm
 svtv-spec-fsm-constraints-for-alists-svtv-name-lhs-map-equiv-congruence-on-namemap
 (implies (svtv-name-lhs-map-equiv namemap namemap-equiv)
          (equal (svtv-spec-fsm-constraints-for-alists
                      x stage namemap overridetype bindings)
                 (svtv-spec-fsm-constraints-for-alists
                      x stage
                      namemap-equiv overridetype bindings)))
 :rule-classes :congruence)

Theorem: svtv-spec-fsm-constraints-for-alists-of-svar-overridetype-fix-overridetype

(defthm
 svtv-spec-fsm-constraints-for-alists-of-svar-overridetype-fix-overridetype
 (equal (svtv-spec-fsm-constraints-for-alists
             x stage namemap
             (svar-overridetype-fix overridetype)
             bindings)
        (svtv-spec-fsm-constraints-for-alists
             x stage namemap overridetype bindings)))

Theorem: svtv-spec-fsm-constraints-for-alists-svar-overridetype-equiv-congruence-on-overridetype

(defthm
 svtv-spec-fsm-constraints-for-alists-svar-overridetype-equiv-congruence-on-overridetype
 (implies (svar-overridetype-equiv overridetype overridetype-equiv)
          (equal (svtv-spec-fsm-constraints-for-alists
                      x stage namemap overridetype bindings)
                 (svtv-spec-fsm-constraints-for-alists
                      x stage
                      namemap overridetype-equiv bindings)))
 :rule-classes :congruence)

Theorem: svtv-spec-fsm-constraints-for-alists-of-lhprobe-map-fix-bindings

(defthm
   svtv-spec-fsm-constraints-for-alists-of-lhprobe-map-fix-bindings
  (equal (svtv-spec-fsm-constraints-for-alists
              x stage namemap
              overridetype (lhprobe-map-fix bindings))
         (svtv-spec-fsm-constraints-for-alists
              x stage namemap overridetype bindings)))

Theorem: svtv-spec-fsm-constraints-for-alists-lhprobe-map-equiv-congruence-on-bindings

(defthm
 svtv-spec-fsm-constraints-for-alists-lhprobe-map-equiv-congruence-on-bindings
 (implies (lhprobe-map-equiv bindings bindings-equiv)
          (equal (svtv-spec-fsm-constraints-for-alists
                      x stage namemap overridetype bindings)
                 (svtv-spec-fsm-constraints-for-alists
                      x stage
                      namemap overridetype bindings-equiv)))
 :rule-classes :congruence)