		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-probealist-to-lhprobe-map

Signature
(svtv-probealist-to-lhprobe-map x namemap) → map
Arguments: x — Guard (svtv-probealist-p x).; namemap — Guard (svtv-name-lhs-map-p namemap).
Returns: map — Type (lhprobe-map-p map).

Definitions and Theorems

Function: svtv-probealist-to-lhprobe-map

(defun svtv-probealist-to-lhprobe-map (x namemap)
  (declare (xargs :guard (and (svtv-probealist-p x)
                              (svtv-name-lhs-map-p namemap))))
  (let ((__function__ 'svtv-probealist-to-lhprobe-map))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbt (consp (car x)))
          (cons (cons (svar-fix (caar x))
                      (svtv-probe-to-lhprobe (cdar x)
                                             namemap))
                (svtv-probealist-to-lhprobe-map (cdr x)
                                                namemap))
        (svtv-probealist-to-lhprobe-map (cdr x)
                                        namemap)))))

Theorem: lhprobe-map-p-of-svtv-probealist-to-lhprobe-map

(defthm lhprobe-map-p-of-svtv-probealist-to-lhprobe-map
  (b* ((map (svtv-probealist-to-lhprobe-map x namemap)))
    (lhprobe-map-p map))
  :rule-classes :rewrite)

Theorem: svtv-probealist-to-lhprobe-map-of-svtv-probealist-fix-x

(defthm svtv-probealist-to-lhprobe-map-of-svtv-probealist-fix-x
  (equal (svtv-probealist-to-lhprobe-map (svtv-probealist-fix x)
                                         namemap)
         (svtv-probealist-to-lhprobe-map x namemap)))

Theorem: svtv-probealist-to-lhprobe-map-svtv-probealist-equiv-congruence-on-x

(defthm
 svtv-probealist-to-lhprobe-map-svtv-probealist-equiv-congruence-on-x
 (implies (svtv-probealist-equiv x x-equiv)
          (equal (svtv-probealist-to-lhprobe-map x namemap)
                 (svtv-probealist-to-lhprobe-map x-equiv namemap)))
 :rule-classes :congruence)

Theorem: svtv-probealist-to-lhprobe-map-of-svtv-name-lhs-map-fix-namemap

(defthm
    svtv-probealist-to-lhprobe-map-of-svtv-name-lhs-map-fix-namemap
 (equal
  (svtv-probealist-to-lhprobe-map x (svtv-name-lhs-map-fix namemap))
  (svtv-probealist-to-lhprobe-map x namemap)))

Theorem: svtv-probealist-to-lhprobe-map-svtv-name-lhs-map-equiv-congruence-on-namemap

(defthm
 svtv-probealist-to-lhprobe-map-svtv-name-lhs-map-equiv-congruence-on-namemap
 (implies (svtv-name-lhs-map-equiv namemap namemap-equiv)
          (equal (svtv-probealist-to-lhprobe-map x namemap)
                 (svtv-probealist-to-lhprobe-map x namemap-equiv)))
 :rule-classes :congruence)