		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm-defs

Svtv-probe-to-lhprobe

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

Definitions and Theorems

Function: svtv-probe-to-lhprobe

(defun svtv-probe-to-lhprobe (x namemap)
  (declare (xargs :guard (and (svtv-probe-p x)
                              (svtv-name-lhs-map-p namemap))))
  (let ((__function__ 'svtv-probe-to-lhprobe))
    (declare (ignorable __function__))
    (b* (((svtv-probe x)))
      (make-lhprobe
           :stage x.time
           :lhs (cdr (hons-get x.signal
                               (svtv-name-lhs-map-fix namemap)))))))

Theorem: lhprobe-p-of-svtv-probe-to-lhprobe

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

Theorem: svtv-probe-to-lhprobe-of-svtv-probe-fix-x

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

Theorem: svtv-probe-to-lhprobe-svtv-probe-equiv-congruence-on-x

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

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

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

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

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