		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-spec-fsm-constraints-for-lhprobe

Signature
(svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings) → constraints
Arguments: lhprobe — Guard (lhprobe-p lhprobe).; binding — Guard (svar/4vec-p binding).; bindings — Guard (lhprobe-map-p bindings).
Returns: constraints — Type (lhprobe-constraintlist-p constraints).

Definitions and Theorems

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

(defun svtv-spec-fsm-constraints-for-lhprobe
       (lhprobe binding bindings)
  (declare (xargs :guard (and (lhprobe-p lhprobe)
                              (svar/4vec-p binding)
                              (lhprobe-map-p bindings))))
  (let ((__function__ 'svtv-spec-fsm-constraints-for-lhprobe))
    (declare (ignorable __function__))
    (svar/4vec-case
         binding :4vec
         (list (make-lhprobe-constraint :lhprobe lhprobe
                                        :val (4vec-fix binding)))
         :svar
         (b* ((binding-look (hons-get (svar-fix binding)
                                      (lhprobe-map-fix bindings)))
              ((unless binding-look)
               (list (make-lhprobe-constraint :lhprobe lhprobe
                                              :val (4vec-x))))
              (binding-lhprobe (cdr binding-look))
              ((when (equal binding-lhprobe (lhprobe-fix lhprobe)))
               nil))
           (list (make-lhprobe-constraint :lhprobe lhprobe
                                          :val binding-lhprobe))))))

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

(defthm
  lhprobe-constraintlist-p-of-svtv-spec-fsm-constraints-for-lhprobe
  (b* ((constraints (svtv-spec-fsm-constraints-for-lhprobe
                         lhprobe binding bindings)))
    (lhprobe-constraintlist-p constraints))
  :rule-classes :rewrite)

Theorem: svtv-spec-fsm-constraints-for-lhprobe-of-lhprobe-fix-lhprobe

(defthm svtv-spec-fsm-constraints-for-lhprobe-of-lhprobe-fix-lhprobe
 (equal
  (svtv-spec-fsm-constraints-for-lhprobe (lhprobe-fix lhprobe)
                                         binding bindings)
  (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)))

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

(defthm
 svtv-spec-fsm-constraints-for-lhprobe-lhprobe-equiv-congruence-on-lhprobe
 (implies
  (lhprobe-equiv lhprobe lhprobe-equiv)
  (equal
    (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)
    (svtv-spec-fsm-constraints-for-lhprobe
         lhprobe-equiv binding bindings)))
 :rule-classes :congruence)

Theorem: svtv-spec-fsm-constraints-for-lhprobe-of-svar/4vec-fix-binding

(defthm
     svtv-spec-fsm-constraints-for-lhprobe-of-svar/4vec-fix-binding
 (equal
  (svtv-spec-fsm-constraints-for-lhprobe
       lhprobe (svar/4vec-fix binding)
       bindings)
  (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)))

Theorem: svtv-spec-fsm-constraints-for-lhprobe-svar/4vec-equiv-congruence-on-binding

(defthm
 svtv-spec-fsm-constraints-for-lhprobe-svar/4vec-equiv-congruence-on-binding
 (implies
  (svar/4vec-equiv binding binding-equiv)
  (equal
    (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)
    (svtv-spec-fsm-constraints-for-lhprobe
         lhprobe binding-equiv bindings)))
 :rule-classes :congruence)

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

(defthm
  svtv-spec-fsm-constraints-for-lhprobe-of-lhprobe-map-fix-bindings
 (equal
  (svtv-spec-fsm-constraints-for-lhprobe
       lhprobe
       binding (lhprobe-map-fix bindings))
  (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)))

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

(defthm
 svtv-spec-fsm-constraints-for-lhprobe-lhprobe-map-equiv-congruence-on-bindings
 (implies
  (lhprobe-map-equiv bindings bindings-equiv)
  (equal
    (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)
    (svtv-spec-fsm-constraints-for-lhprobe
         lhprobe binding bindings-equiv)))
 :rule-classes :congruence)