		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex->a4vec-memotable-correctp

Signature
(svex->a4vec-memotable-correctp memo env masks) → *
Arguments: memo — Guard (svex-aig-memotable-p memo).; env — Guard (svex-a4vec-env-p env).; masks — Guard (svex-mask-alist-p masks).

Definitions and Theorems

Function: svex->a4vec-memotable-correctp

(defun svex->a4vec-memotable-correctp (memo env masks)
  (declare (xargs :guard (and (svex-aig-memotable-p memo)
                              (svex-a4vec-env-p env)
                              (svex-mask-alist-p masks))))
  (let ((__function__ 'svex->a4vec-memotable-correctp))
    (declare (ignorable __function__))
    (if (atom memo)
        t
      (and (or (not (mbt (consp (car memo))))
               (equal (svex->a4vec (caar memo) env masks)
                      (a4vec-fix (cdar memo))))
           (svex->a4vec-memotable-correctp (cdr memo)
                                           env masks)))))

Theorem: svex->a4vec-memotable-correctp-implies-lookup

(defthm svex->a4vec-memotable-correctp-implies-lookup
  (implies (and (svex->a4vec-memotable-correctp memo env masks)
                (hons-assoc-equal x memo))
           (a4vec-equiv (cdr (hons-assoc-equal x memo))
                        (svex->a4vec x env masks))))

Theorem: svex->a4vec-memotable-correctp-implies-lookup-fix

(defthm svex->a4vec-memotable-correctp-implies-lookup-fix
 (implies
     (and (svex->a4vec-memotable-correctp memo env masks)
          (hons-assoc-equal x (svex-aig-memotable-fix memo)))
     (equal (cdr (hons-assoc-equal x (svex-aig-memotable-fix memo)))
            (svex->a4vec x env masks))))

Theorem: svex->a4vec-memotable-correctp-of-cons

(defthm svex->a4vec-memotable-correctp-of-cons
  (implies (and (svex->a4vec-memotable-correctp memo env masks)
                (a4vec-equiv val (svex->a4vec x env masks)))
           (svex->a4vec-memotable-correctp (cons (cons x val) memo)
                                           env masks)))

Theorem: svex->a4vec-memotable-correctp-of-nil

(defthm svex->a4vec-memotable-correctp-of-nil
  (svex->a4vec-memotable-correctp nil env masks))

Theorem: svex->a4vec-memotable-correctp-of-svex-aig-memotable-fix-memo

(defthm
      svex->a4vec-memotable-correctp-of-svex-aig-memotable-fix-memo
  (equal
       (svex->a4vec-memotable-correctp (svex-aig-memotable-fix memo)
                                       env masks)
       (svex->a4vec-memotable-correctp memo env masks)))

Theorem: svex->a4vec-memotable-correctp-svex-aig-memotable-equiv-congruence-on-memo

(defthm
 svex->a4vec-memotable-correctp-svex-aig-memotable-equiv-congruence-on-memo
 (implies
      (svex-aig-memotable-equiv memo memo-equiv)
      (equal (svex->a4vec-memotable-correctp memo env masks)
             (svex->a4vec-memotable-correctp memo-equiv env masks)))
 :rule-classes :congruence)

Theorem: svex->a4vec-memotable-correctp-of-svex-a4vec-env-fix-env

(defthm svex->a4vec-memotable-correctp-of-svex-a4vec-env-fix-env
  (equal
       (svex->a4vec-memotable-correctp memo (svex-a4vec-env-fix env)
                                       masks)
       (svex->a4vec-memotable-correctp memo env masks)))

Theorem: svex->a4vec-memotable-correctp-svex-a4vec-env-equiv-congruence-on-env

(defthm
 svex->a4vec-memotable-correctp-svex-a4vec-env-equiv-congruence-on-env
 (implies
      (svex-a4vec-env-equiv env env-equiv)
      (equal (svex->a4vec-memotable-correctp memo env masks)
             (svex->a4vec-memotable-correctp memo env-equiv masks)))
 :rule-classes :congruence)

Theorem: svex->a4vec-memotable-correctp-of-svex-mask-alist-fix-masks

(defthm svex->a4vec-memotable-correctp-of-svex-mask-alist-fix-masks
  (equal (svex->a4vec-memotable-correctp
              memo env (svex-mask-alist-fix masks))
         (svex->a4vec-memotable-correctp memo env masks)))

Theorem: svex->a4vec-memotable-correctp-svex-mask-alist-equiv-congruence-on-masks

(defthm
 svex->a4vec-memotable-correctp-svex-mask-alist-equiv-congruence-on-masks
 (implies
      (svex-mask-alist-equiv masks masks-equiv)
      (equal (svex->a4vec-memotable-correctp memo env masks)
             (svex->a4vec-memotable-correctp memo env masks-equiv)))
 :rule-classes :congruence)