|
|
|---|
|
|
|
|---|
An 6-bit unsigned bitstruct type.
This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 6-bit integer.
Function:
(defun interp-flags-p (x) (declare (xargs :guard t)) (let ((__function__ 'interp-flags-p)) (declare (ignorable __function__)) (mbe :logic (unsigned-byte-p 6 x) :exec (and (natp x) (< x 64)))))
Theorem:
(defthm interp-flags-p-when-unsigned-byte-p (implies (unsigned-byte-p 6 x) (interp-flags-p x)))
Theorem:
(defthm unsigned-byte-p-when-interp-flags-p (implies (interp-flags-p x) (unsigned-byte-p 6 x)))
Theorem:
(defthm interp-flags-p-compound-recognizer (implies (interp-flags-p x) (natp x)) :rule-classes :compound-recognizer)
Function:
(defun interp-flags-fix (x) (declare (xargs :guard (interp-flags-p x))) (let ((__function__ 'interp-flags-fix)) (declare (ignorable __function__)) (mbe :logic (loghead 6 x) :exec x)))
Theorem:
(defthm interp-flags-p-of-interp-flags-fix (b* ((fty::fixed (interp-flags-fix x))) (interp-flags-p fty::fixed)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags-fix-when-interp-flags-p (implies (interp-flags-p x) (equal (interp-flags-fix x) x)))
Function:
(defun interp-flags-equiv$inline (x y) (declare (xargs :guard (and (interp-flags-p x) (interp-flags-p y)))) (equal (interp-flags-fix x) (interp-flags-fix y)))
Theorem:
(defthm interp-flags-equiv-is-an-equivalence (and (booleanp (interp-flags-equiv x y)) (interp-flags-equiv x x) (implies (interp-flags-equiv x y) (interp-flags-equiv y x)) (implies (and (interp-flags-equiv x y) (interp-flags-equiv y z)) (interp-flags-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm interp-flags-equiv-implies-equal-interp-flags-fix-1 (implies (interp-flags-equiv x x-equiv) (equal (interp-flags-fix x) (interp-flags-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm interp-flags-fix-under-interp-flags-equiv (interp-flags-equiv (interp-flags-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm interp-flags-fix-of-interp-flags-fix-x (equal (interp-flags-fix (interp-flags-fix x)) (interp-flags-fix x)))
Theorem:
(defthm interp-flags-fix-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags-fix x) (interp-flags-fix x-equiv))) :rule-classes :congruence)
Function:
(defun interp-flags (intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (declare (xargs :guard (and (booleanp intro-bvars) (booleanp intro-synvars) (booleanp simplify-logic) (booleanp trace-rewrites) (booleanp make-ites) (booleanp branch-on-ifs)))) (let ((__function__ 'interp-flags)) (declare (ignorable __function__)) (b* ((intro-bvars (bool->bit intro-bvars)) (intro-synvars (bool->bit intro-synvars)) (simplify-logic (bool->bit simplify-logic)) (trace-rewrites (bool->bit trace-rewrites)) (make-ites (bool->bit make-ites)) (branch-on-ifs (bool->bit branch-on-ifs))) (logapp 1 intro-bvars (logapp 1 intro-synvars (logapp 1 simplify-logic (logapp 1 trace-rewrites (logapp 1 make-ites branch-on-ifs))))))))
Theorem:
(defthm interp-flags-p-of-interp-flags (b* ((interp-flags (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs))) (interp-flags-p interp-flags)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags-of-bool-fix-intro-bvars (equal (interp-flags (bool-fix intro-bvars) intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)))
Theorem:
(defthm interp-flags-iff-congruence-on-intro-bvars (implies (iff intro-bvars intro-bvars-equiv) (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars-equiv intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-of-bool-fix-intro-synvars (equal (interp-flags intro-bvars (bool-fix intro-synvars) simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)))
Theorem:
(defthm interp-flags-iff-congruence-on-intro-synvars (implies (iff intro-synvars intro-synvars-equiv) (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars-equiv simplify-logic trace-rewrites make-ites branch-on-ifs))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-of-bool-fix-simplify-logic (equal (interp-flags intro-bvars intro-synvars (bool-fix simplify-logic) trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)))
Theorem:
(defthm interp-flags-iff-congruence-on-simplify-logic (implies (iff simplify-logic simplify-logic-equiv) (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic-equiv trace-rewrites make-ites branch-on-ifs))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-of-bool-fix-trace-rewrites (equal (interp-flags intro-bvars intro-synvars simplify-logic (bool-fix trace-rewrites) make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)))
Theorem:
(defthm interp-flags-iff-congruence-on-trace-rewrites (implies (iff trace-rewrites trace-rewrites-equiv) (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites-equiv make-ites branch-on-ifs))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-of-bool-fix-make-ites (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites (bool-fix make-ites) branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)))
Theorem:
(defthm interp-flags-iff-congruence-on-make-ites (implies (iff make-ites make-ites-equiv) (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites-equiv branch-on-ifs))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-of-bool-fix-branch-on-ifs (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites (bool-fix branch-on-ifs)) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)))
Theorem:
(defthm interp-flags-iff-congruence-on-branch-on-ifs (implies (iff branch-on-ifs branch-on-ifs-equiv) (equal (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs) (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs-equiv))) :rule-classes :congruence)
Function:
(defun interp-flags-equiv-under-mask (x x1 mask) (declare (xargs :guard (and (interp-flags-p x) (interp-flags-p x1) (integerp mask)))) (let ((__function__ 'interp-flags-equiv-under-mask)) (declare (ignorable __function__)) (fty::int-equiv-under-mask (interp-flags-fix x) (interp-flags-fix x1) mask)))
Theorem:
(defthm interp-flags-equiv-under-mask-of-interp-flags-fix-x (equal (interp-flags-equiv-under-mask (interp-flags-fix x) x1 mask) (interp-flags-equiv-under-mask x x1 mask)))
Theorem:
(defthm interp-flags-equiv-under-mask-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags-equiv-under-mask x x1 mask) (interp-flags-equiv-under-mask x-equiv x1 mask))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-equiv-under-mask-of-interp-flags-fix-x1 (equal (interp-flags-equiv-under-mask x (interp-flags-fix x1) mask) (interp-flags-equiv-under-mask x x1 mask)))
Theorem:
(defthm interp-flags-equiv-under-mask-interp-flags-equiv-congruence-on-x1 (implies (interp-flags-equiv x1 x1-equiv) (equal (interp-flags-equiv-under-mask x x1 mask) (interp-flags-equiv-under-mask x x1-equiv mask))) :rule-classes :congruence)
Theorem:
(defthm interp-flags-equiv-under-mask-of-ifix-mask (equal (interp-flags-equiv-under-mask x x1 (ifix mask)) (interp-flags-equiv-under-mask x x1 mask)))
Theorem:
(defthm interp-flags-equiv-under-mask-int-equiv-congruence-on-mask (implies (acl2::int-equiv mask mask-equiv) (equal (interp-flags-equiv-under-mask x x1 mask) (interp-flags-equiv-under-mask x x1 mask-equiv))) :rule-classes :congruence)
Function:
(defun interp-flags->intro-bvars (x) (declare (xargs :guard (interp-flags-p x))) (mbe :logic (let ((x (interp-flags-fix x))) (bit->bool (acl2::part-select x :low 0 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 6) x))))))
Theorem:
(defthm booleanp-of-interp-flags->intro-bvars (b* ((intro-bvars (interp-flags->intro-bvars x))) (booleanp intro-bvars)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags->intro-bvars-of-interp-flags-fix-x (equal (interp-flags->intro-bvars (interp-flags-fix x)) (interp-flags->intro-bvars x)))
Theorem:
(defthm interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags->intro-bvars x) (interp-flags->intro-bvars x-equiv))) :rule-classes :congruence)
Theorem:
(defthm interp-flags->intro-bvars-of-interp-flags (equal (interp-flags->intro-bvars (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)) (bool-fix intro-bvars)))
Theorem:
(defthm interp-flags->intro-bvars-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x interp-flags-equiv-under-mask) (interp-flags-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 1) 0)) (equal (interp-flags->intro-bvars x) (interp-flags->intro-bvars y))))
Function:
(defun interp-flags->intro-synvars (x) (declare (xargs :guard (interp-flags-p x))) (mbe :logic (let ((x (interp-flags-fix x))) (bit->bool (acl2::part-select x :low 1 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 5) (ash (the (unsigned-byte 6) x) -1)))))))
Theorem:
(defthm booleanp-of-interp-flags->intro-synvars (b* ((intro-synvars (interp-flags->intro-synvars x))) (booleanp intro-synvars)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags->intro-synvars-of-interp-flags-fix-x (equal (interp-flags->intro-synvars (interp-flags-fix x)) (interp-flags->intro-synvars x)))
Theorem:
(defthm interp-flags->intro-synvars-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags->intro-synvars x) (interp-flags->intro-synvars x-equiv))) :rule-classes :congruence)
Theorem:
(defthm interp-flags->intro-synvars-of-interp-flags (equal (interp-flags->intro-synvars (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)) (bool-fix intro-synvars)))
Theorem:
(defthm interp-flags->intro-synvars-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x interp-flags-equiv-under-mask) (interp-flags-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 2) 0)) (equal (interp-flags->intro-synvars x) (interp-flags->intro-synvars y))))
Function:
(defun interp-flags->simplify-logic (x) (declare (xargs :guard (interp-flags-p x))) (mbe :logic (let ((x (interp-flags-fix x))) (bit->bool (acl2::part-select x :low 2 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 4) (ash (the (unsigned-byte 6) x) -2)))))))
Theorem:
(defthm booleanp-of-interp-flags->simplify-logic (b* ((simplify-logic (interp-flags->simplify-logic x))) (booleanp simplify-logic)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags->simplify-logic-of-interp-flags-fix-x (equal (interp-flags->simplify-logic (interp-flags-fix x)) (interp-flags->simplify-logic x)))
Theorem:
(defthm interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags->simplify-logic x) (interp-flags->simplify-logic x-equiv))) :rule-classes :congruence)
Theorem:
(defthm interp-flags->simplify-logic-of-interp-flags (equal (interp-flags->simplify-logic (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)) (bool-fix simplify-logic)))
Theorem:
(defthm interp-flags->simplify-logic-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x interp-flags-equiv-under-mask) (interp-flags-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 4) 0)) (equal (interp-flags->simplify-logic x) (interp-flags->simplify-logic y))))
Function:
(defun interp-flags->trace-rewrites (x) (declare (xargs :guard (interp-flags-p x))) (mbe :logic (let ((x (interp-flags-fix x))) (bit->bool (acl2::part-select x :low 3 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 3) (ash (the (unsigned-byte 6) x) -3)))))))
Theorem:
(defthm booleanp-of-interp-flags->trace-rewrites (b* ((trace-rewrites (interp-flags->trace-rewrites x))) (booleanp trace-rewrites)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags->trace-rewrites-of-interp-flags-fix-x (equal (interp-flags->trace-rewrites (interp-flags-fix x)) (interp-flags->trace-rewrites x)))
Theorem:
(defthm interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags->trace-rewrites x) (interp-flags->trace-rewrites x-equiv))) :rule-classes :congruence)
Theorem:
(defthm interp-flags->trace-rewrites-of-interp-flags (equal (interp-flags->trace-rewrites (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)) (bool-fix trace-rewrites)))
Theorem:
(defthm interp-flags->trace-rewrites-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x interp-flags-equiv-under-mask) (interp-flags-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 8) 0)) (equal (interp-flags->trace-rewrites x) (interp-flags->trace-rewrites y))))
Function:
(defun interp-flags->make-ites (x) (declare (xargs :guard (interp-flags-p x))) (mbe :logic (let ((x (interp-flags-fix x))) (bit->bool (acl2::part-select x :low 4 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 2) (ash (the (unsigned-byte 6) x) -4)))))))
Theorem:
(defthm booleanp-of-interp-flags->make-ites (b* ((make-ites (interp-flags->make-ites x))) (booleanp make-ites)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags->make-ites-of-interp-flags-fix-x (equal (interp-flags->make-ites (interp-flags-fix x)) (interp-flags->make-ites x)))
Theorem:
(defthm interp-flags->make-ites-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags->make-ites x) (interp-flags->make-ites x-equiv))) :rule-classes :congruence)
Theorem:
(defthm interp-flags->make-ites-of-interp-flags (equal (interp-flags->make-ites (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)) (bool-fix make-ites)))
Theorem:
(defthm interp-flags->make-ites-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x interp-flags-equiv-under-mask) (interp-flags-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 16) 0)) (equal (interp-flags->make-ites x) (interp-flags->make-ites y))))
Function:
(defun interp-flags->branch-on-ifs (x) (declare (xargs :guard (interp-flags-p x))) (mbe :logic (let ((x (interp-flags-fix x))) (bit->bool (acl2::part-select x :low 5 :width 1))) :exec (bit->bool (the (unsigned-byte 1) (logand (the (unsigned-byte 1) 1) (the (unsigned-byte 1) (ash (the (unsigned-byte 6) x) -5)))))))
Theorem:
(defthm booleanp-of-interp-flags->branch-on-ifs (b* ((branch-on-ifs (interp-flags->branch-on-ifs x))) (booleanp branch-on-ifs)) :rule-classes :rewrite)
Theorem:
(defthm interp-flags->branch-on-ifs-of-interp-flags-fix-x (equal (interp-flags->branch-on-ifs (interp-flags-fix x)) (interp-flags->branch-on-ifs x)))
Theorem:
(defthm interp-flags->branch-on-ifs-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags->branch-on-ifs x) (interp-flags->branch-on-ifs x-equiv))) :rule-classes :congruence)
Theorem:
(defthm interp-flags->branch-on-ifs-of-interp-flags (equal (interp-flags->branch-on-ifs (interp-flags intro-bvars intro-synvars simplify-logic trace-rewrites make-ites branch-on-ifs)) (bool-fix branch-on-ifs)))
Theorem:
(defthm interp-flags->branch-on-ifs-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x interp-flags-equiv-under-mask) (interp-flags-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 32) 0)) (equal (interp-flags->branch-on-ifs x) (interp-flags->branch-on-ifs y))))
Theorem:
(defthm interp-flags-fix-in-terms-of-interp-flags (equal (interp-flags-fix x) (change-interp-flags x)))
Function:
(defun !interp-flags->intro-bvars (intro-bvars x) (declare (xargs :guard (and (booleanp intro-bvars) (interp-flags-p x)))) (mbe :logic (b* ((intro-bvars (bool->bit intro-bvars)) (x (interp-flags-fix x))) (acl2::part-install intro-bvars x :width 1 :low 0)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 2) -2))) (the (unsigned-byte 1) (bool->bit intro-bvars))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->intro-bvars (b* ((new-x (!interp-flags->intro-bvars intro-bvars x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->intro-bvars-of-bool-fix-intro-bvars (equal (!interp-flags->intro-bvars (bool-fix intro-bvars) x) (!interp-flags->intro-bvars intro-bvars x)))
Theorem:
(defthm !interp-flags->intro-bvars-iff-congruence-on-intro-bvars (implies (iff intro-bvars intro-bvars-equiv) (equal (!interp-flags->intro-bvars intro-bvars x) (!interp-flags->intro-bvars intro-bvars-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->intro-bvars-of-interp-flags-fix-x (equal (!interp-flags->intro-bvars intro-bvars (interp-flags-fix x)) (!interp-flags->intro-bvars intro-bvars x)))
Theorem:
(defthm !interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->intro-bvars intro-bvars x) (!interp-flags->intro-bvars intro-bvars x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->intro-bvars-is-interp-flags (equal (!interp-flags->intro-bvars intro-bvars x) (change-interp-flags x :intro-bvars intro-bvars)))
Theorem:
(defthm interp-flags->intro-bvars-of-!interp-flags->intro-bvars (b* ((?new-x (!interp-flags->intro-bvars intro-bvars x))) (equal (interp-flags->intro-bvars new-x) (bool-fix intro-bvars))))
Theorem:
(defthm !interp-flags->intro-bvars-equiv-under-mask (b* ((?new-x (!interp-flags->intro-bvars intro-bvars x))) (interp-flags-equiv-under-mask new-x x -2)))
Function:
(defun !interp-flags->intro-synvars (intro-synvars x) (declare (xargs :guard (and (booleanp intro-synvars) (interp-flags-p x)))) (mbe :logic (b* ((intro-synvars (bool->bit intro-synvars)) (x (interp-flags-fix x))) (acl2::part-install intro-synvars x :width 1 :low 1)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 3) -3))) (the (unsigned-byte 2) (ash (the (unsigned-byte 1) (bool->bit intro-synvars)) 1))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->intro-synvars (b* ((new-x (!interp-flags->intro-synvars intro-synvars x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->intro-synvars-of-bool-fix-intro-synvars (equal (!interp-flags->intro-synvars (bool-fix intro-synvars) x) (!interp-flags->intro-synvars intro-synvars x)))
Theorem:
(defthm !interp-flags->intro-synvars-iff-congruence-on-intro-synvars (implies (iff intro-synvars intro-synvars-equiv) (equal (!interp-flags->intro-synvars intro-synvars x) (!interp-flags->intro-synvars intro-synvars-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->intro-synvars-of-interp-flags-fix-x (equal (!interp-flags->intro-synvars intro-synvars (interp-flags-fix x)) (!interp-flags->intro-synvars intro-synvars x)))
Theorem:
(defthm !interp-flags->intro-synvars-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->intro-synvars intro-synvars x) (!interp-flags->intro-synvars intro-synvars x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->intro-synvars-is-interp-flags (equal (!interp-flags->intro-synvars intro-synvars x) (change-interp-flags x :intro-synvars intro-synvars)))
Theorem:
(defthm interp-flags->intro-synvars-of-!interp-flags->intro-synvars (b* ((?new-x (!interp-flags->intro-synvars intro-synvars x))) (equal (interp-flags->intro-synvars new-x) (bool-fix intro-synvars))))
Theorem:
(defthm !interp-flags->intro-synvars-equiv-under-mask (b* ((?new-x (!interp-flags->intro-synvars intro-synvars x))) (interp-flags-equiv-under-mask new-x x -3)))
Function:
(defun !interp-flags->simplify-logic (simplify-logic x) (declare (xargs :guard (and (booleanp simplify-logic) (interp-flags-p x)))) (mbe :logic (b* ((simplify-logic (bool->bit simplify-logic)) (x (interp-flags-fix x))) (acl2::part-install simplify-logic x :width 1 :low 2)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 4) -5))) (the (unsigned-byte 3) (ash (the (unsigned-byte 1) (bool->bit simplify-logic)) 2))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->simplify-logic (b* ((new-x (!interp-flags->simplify-logic simplify-logic x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->simplify-logic-of-bool-fix-simplify-logic (equal (!interp-flags->simplify-logic (bool-fix simplify-logic) x) (!interp-flags->simplify-logic simplify-logic x)))
Theorem:
(defthm !interp-flags->simplify-logic-iff-congruence-on-simplify-logic (implies (iff simplify-logic simplify-logic-equiv) (equal (!interp-flags->simplify-logic simplify-logic x) (!interp-flags->simplify-logic simplify-logic-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->simplify-logic-of-interp-flags-fix-x (equal (!interp-flags->simplify-logic simplify-logic (interp-flags-fix x)) (!interp-flags->simplify-logic simplify-logic x)))
Theorem:
(defthm !interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->simplify-logic simplify-logic x) (!interp-flags->simplify-logic simplify-logic x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->simplify-logic-is-interp-flags (equal (!interp-flags->simplify-logic simplify-logic x) (change-interp-flags x :simplify-logic simplify-logic)))
Theorem:
(defthm interp-flags->simplify-logic-of-!interp-flags->simplify-logic (b* ((?new-x (!interp-flags->simplify-logic simplify-logic x))) (equal (interp-flags->simplify-logic new-x) (bool-fix simplify-logic))))
Theorem:
(defthm !interp-flags->simplify-logic-equiv-under-mask (b* ((?new-x (!interp-flags->simplify-logic simplify-logic x))) (interp-flags-equiv-under-mask new-x x -5)))
Function:
(defun !interp-flags->trace-rewrites (trace-rewrites x) (declare (xargs :guard (and (booleanp trace-rewrites) (interp-flags-p x)))) (mbe :logic (b* ((trace-rewrites (bool->bit trace-rewrites)) (x (interp-flags-fix x))) (acl2::part-install trace-rewrites x :width 1 :low 3)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 5) -9))) (the (unsigned-byte 4) (ash (the (unsigned-byte 1) (bool->bit trace-rewrites)) 3))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->trace-rewrites (b* ((new-x (!interp-flags->trace-rewrites trace-rewrites x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->trace-rewrites-of-bool-fix-trace-rewrites (equal (!interp-flags->trace-rewrites (bool-fix trace-rewrites) x) (!interp-flags->trace-rewrites trace-rewrites x)))
Theorem:
(defthm !interp-flags->trace-rewrites-iff-congruence-on-trace-rewrites (implies (iff trace-rewrites trace-rewrites-equiv) (equal (!interp-flags->trace-rewrites trace-rewrites x) (!interp-flags->trace-rewrites trace-rewrites-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->trace-rewrites-of-interp-flags-fix-x (equal (!interp-flags->trace-rewrites trace-rewrites (interp-flags-fix x)) (!interp-flags->trace-rewrites trace-rewrites x)))
Theorem:
(defthm !interp-flags->trace-rewrites-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->trace-rewrites trace-rewrites x) (!interp-flags->trace-rewrites trace-rewrites x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->trace-rewrites-is-interp-flags (equal (!interp-flags->trace-rewrites trace-rewrites x) (change-interp-flags x :trace-rewrites trace-rewrites)))
Theorem:
(defthm interp-flags->trace-rewrites-of-!interp-flags->trace-rewrites (b* ((?new-x (!interp-flags->trace-rewrites trace-rewrites x))) (equal (interp-flags->trace-rewrites new-x) (bool-fix trace-rewrites))))
Theorem:
(defthm !interp-flags->trace-rewrites-equiv-under-mask (b* ((?new-x (!interp-flags->trace-rewrites trace-rewrites x))) (interp-flags-equiv-under-mask new-x x -9)))
Function:
(defun !interp-flags->make-ites (make-ites x) (declare (xargs :guard (and (booleanp make-ites) (interp-flags-p x)))) (mbe :logic (b* ((make-ites (bool->bit make-ites)) (x (interp-flags-fix x))) (acl2::part-install make-ites x :width 1 :low 4)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) (bool->bit make-ites)) 4))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->make-ites (b* ((new-x (!interp-flags->make-ites make-ites x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->make-ites-of-bool-fix-make-ites (equal (!interp-flags->make-ites (bool-fix make-ites) x) (!interp-flags->make-ites make-ites x)))
Theorem:
(defthm !interp-flags->make-ites-iff-congruence-on-make-ites (implies (iff make-ites make-ites-equiv) (equal (!interp-flags->make-ites make-ites x) (!interp-flags->make-ites make-ites-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->make-ites-of-interp-flags-fix-x (equal (!interp-flags->make-ites make-ites (interp-flags-fix x)) (!interp-flags->make-ites make-ites x)))
Theorem:
(defthm !interp-flags->make-ites-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->make-ites make-ites x) (!interp-flags->make-ites make-ites x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->make-ites-is-interp-flags (equal (!interp-flags->make-ites make-ites x) (change-interp-flags x :make-ites make-ites)))
Theorem:
(defthm interp-flags->make-ites-of-!interp-flags->make-ites (b* ((?new-x (!interp-flags->make-ites make-ites x))) (equal (interp-flags->make-ites new-x) (bool-fix make-ites))))
Theorem:
(defthm !interp-flags->make-ites-equiv-under-mask (b* ((?new-x (!interp-flags->make-ites make-ites x))) (interp-flags-equiv-under-mask new-x x -17)))
Function:
(defun !interp-flags->branch-on-ifs (branch-on-ifs x) (declare (xargs :guard (and (booleanp branch-on-ifs) (interp-flags-p x)))) (mbe :logic (b* ((branch-on-ifs (bool->bit branch-on-ifs)) (x (interp-flags-fix x))) (acl2::part-install branch-on-ifs x :width 1 :low 5)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 7) -33))) (the (unsigned-byte 6) (ash (the (unsigned-byte 1) (bool->bit branch-on-ifs)) 5))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->branch-on-ifs (b* ((new-x (!interp-flags->branch-on-ifs branch-on-ifs x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->branch-on-ifs-of-bool-fix-branch-on-ifs (equal (!interp-flags->branch-on-ifs (bool-fix branch-on-ifs) x) (!interp-flags->branch-on-ifs branch-on-ifs x)))
Theorem:
(defthm !interp-flags->branch-on-ifs-iff-congruence-on-branch-on-ifs (implies (iff branch-on-ifs branch-on-ifs-equiv) (equal (!interp-flags->branch-on-ifs branch-on-ifs x) (!interp-flags->branch-on-ifs branch-on-ifs-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->branch-on-ifs-of-interp-flags-fix-x (equal (!interp-flags->branch-on-ifs branch-on-ifs (interp-flags-fix x)) (!interp-flags->branch-on-ifs branch-on-ifs x)))
Theorem:
(defthm !interp-flags->branch-on-ifs-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->branch-on-ifs branch-on-ifs x) (!interp-flags->branch-on-ifs branch-on-ifs x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->branch-on-ifs-is-interp-flags (equal (!interp-flags->branch-on-ifs branch-on-ifs x) (change-interp-flags x :branch-on-ifs branch-on-ifs)))
Theorem:
(defthm interp-flags->branch-on-ifs-of-!interp-flags->branch-on-ifs (b* ((?new-x (!interp-flags->branch-on-ifs branch-on-ifs x))) (equal (interp-flags->branch-on-ifs new-x) (bool-fix branch-on-ifs))))
Theorem:
(defthm !interp-flags->branch-on-ifs-equiv-under-mask (b* ((?new-x (!interp-flags->branch-on-ifs branch-on-ifs x))) (interp-flags-equiv-under-mask new-x x 31)))
Function:
(defun interp-flags-debug (x) (declare (xargs :guard (interp-flags-p x))) (let ((__function__ 'interp-flags-debug)) (declare (ignorable __function__)) (b* (((interp-flags x))) (cons (cons 'intro-bvars x.intro-bvars) (cons (cons 'intro-synvars x.intro-synvars) (cons (cons 'simplify-logic x.simplify-logic) (cons (cons 'trace-rewrites x.trace-rewrites) (cons (cons 'make-ites x.make-ites) (cons (cons 'branch-on-ifs x.branch-on-ifs) nil)))))))))
Theorem:
(defthm interp-flags-debug-of-interp-flags-fix-x (equal (interp-flags-debug (interp-flags-fix x)) (interp-flags-debug x)))
Theorem:
(defthm interp-flags-debug-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (interp-flags-debug x) (interp-flags-debug x-equiv))) :rule-classes :congruence)