Define default Smtlink hint interface
Function:
(defun pseudo-term-fix (x) (declare (xargs :guard (pseudo-termp x))) (let ((acl2::__function__ 'pseudo-term-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (pseudo-termp x) x nil) :exec x)))
Theorem:
(defthm pseudo-termp-of-pseudo-term-fix (b* ((fixed (pseudo-term-fix x))) (pseudo-termp fixed)) :rule-classes :rewrite)
Theorem:
(defthm equal-fixed-and-x-of-pseudo-termp (b* ((fixed (pseudo-term-fix x))) (implies (pseudo-termp x) (equal fixed x))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-fix-idempotent-lemma (equal (pseudo-term-fix (pseudo-term-fix x)) (pseudo-term-fix x)))
Function:
(defun pseudo-term-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (pseudo-termp acl2::x) (pseudo-termp acl2::y)))) (equal (pseudo-term-fix acl2::x) (pseudo-term-fix acl2::y)))
Theorem:
(defthm pseudo-term-equiv-is-an-equivalence (and (booleanp (pseudo-term-equiv x y)) (pseudo-term-equiv x x) (implies (pseudo-term-equiv x y) (pseudo-term-equiv y x)) (implies (and (pseudo-term-equiv x y) (pseudo-term-equiv y z)) (pseudo-term-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm pseudo-term-equiv-implies-equal-pseudo-term-fix-1 (implies (pseudo-term-equiv acl2::x x-equiv) (equal (pseudo-term-fix acl2::x) (pseudo-term-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm pseudo-term-fix-under-pseudo-term-equiv (pseudo-term-equiv (pseudo-term-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-pseudo-term-fix-1-forward-to-pseudo-term-equiv (implies (equal (pseudo-term-fix acl2::x) acl2::y) (pseudo-term-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-pseudo-term-fix-2-forward-to-pseudo-term-equiv (implies (equal acl2::x (pseudo-term-fix acl2::y)) (pseudo-term-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-equiv-of-pseudo-term-fix-1-forward (implies (pseudo-term-equiv (pseudo-term-fix acl2::x) acl2::y) (pseudo-term-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-equiv-of-pseudo-term-fix-2-forward (implies (pseudo-term-equiv acl2::x (pseudo-term-fix acl2::y)) (pseudo-term-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun pseudo-term-list-fix (x) (declare (xargs :guard (pseudo-term-listp x))) (let ((acl2::__function__ 'pseudo-term-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (consp x) (cons (pseudo-term-fix (car x)) (pseudo-term-list-fix (cdr x))) nil) :exec x)))
Theorem:
(defthm pseudo-term-listp-of-pseudo-term-list-fix (b* ((new-x (pseudo-term-list-fix x))) (pseudo-term-listp new-x)) :rule-classes :rewrite)
Theorem:
(defthm acl2-count-<=-pseudo-term-list-fix (b* ((new-x (pseudo-term-list-fix x))) (<= (acl2-count new-x) (acl2-count x))) :rule-classes :linear)
Theorem:
(defthm equal-pseudo-term-list-fix (b* ((new-x (pseudo-term-list-fix x))) (implies (pseudo-term-listp x) (equal new-x x))) :rule-classes :rewrite)
Theorem:
(defthm len-equal-pseudo-term-list-fix (b* ((new-x (pseudo-term-list-fix x))) (implies (pseudo-term-listp x) (equal (len new-x) (len x)))) :rule-classes :linear)
Theorem:
(defthm pseudo-term-list-fix-idempotent-lemma (equal (pseudo-term-list-fix (pseudo-term-list-fix x)) (pseudo-term-list-fix x)))
Function:
(defun pseudo-term-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (pseudo-term-listp acl2::x) (pseudo-term-listp acl2::y)))) (equal (pseudo-term-list-fix acl2::x) (pseudo-term-list-fix acl2::y)))
Theorem:
(defthm pseudo-term-list-equiv-is-an-equivalence (and (booleanp (pseudo-term-list-equiv x y)) (pseudo-term-list-equiv x x) (implies (pseudo-term-list-equiv x y) (pseudo-term-list-equiv y x)) (implies (and (pseudo-term-list-equiv x y) (pseudo-term-list-equiv y z)) (pseudo-term-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm pseudo-term-list-equiv-implies-equal-pseudo-term-list-fix-1 (implies (pseudo-term-list-equiv acl2::x x-equiv) (equal (pseudo-term-list-fix acl2::x) (pseudo-term-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm pseudo-term-list-fix-under-pseudo-term-list-equiv (pseudo-term-list-equiv (pseudo-term-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Function:
(defun pseudo-term-list-list-fix (x) (declare (xargs :guard (pseudo-term-list-listp x))) (let ((acl2::__function__ 'pseudo-term-list-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (consp x) (cons (pseudo-term-list-fix (car x)) (pseudo-term-list-list-fix (cdr x))) nil) :exec x)))
Theorem:
(defthm pseudo-term-list-listp-of-pseudo-term-list-list-fix (b* ((fixed (pseudo-term-list-list-fix x))) (pseudo-term-list-listp fixed)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-list-list-fix-idempotent-lemma (equal (pseudo-term-list-list-fix (pseudo-term-list-list-fix x)) (pseudo-term-list-list-fix x)))
Function:
(defun pseudo-term-list-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (pseudo-term-list-listp acl2::x) (pseudo-term-list-listp acl2::y)))) (equal (pseudo-term-list-list-fix acl2::x) (pseudo-term-list-list-fix acl2::y)))
Theorem:
(defthm pseudo-term-list-list-equiv-is-an-equivalence (and (booleanp (pseudo-term-list-list-equiv x y)) (pseudo-term-list-list-equiv x x) (implies (pseudo-term-list-list-equiv x y) (pseudo-term-list-list-equiv y x)) (implies (and (pseudo-term-list-list-equiv x y) (pseudo-term-list-list-equiv y z)) (pseudo-term-list-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm pseudo-term-list-list-equiv-implies-equal-pseudo-term-list-list-fix-1 (implies (pseudo-term-list-list-equiv acl2::x x-equiv) (equal (pseudo-term-list-list-fix acl2::x) (pseudo-term-list-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm pseudo-term-list-list-fix-under-pseudo-term-list-list-equiv (pseudo-term-list-list-equiv (pseudo-term-list-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-pseudo-term-list-list-fix-1-forward-to-pseudo-term-list-list-equiv (implies (equal (pseudo-term-list-list-fix acl2::x) acl2::y) (pseudo-term-list-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-pseudo-term-list-list-fix-2-forward-to-pseudo-term-list-list-equiv (implies (equal acl2::x (pseudo-term-list-list-fix acl2::y)) (pseudo-term-list-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-list-list-equiv-of-pseudo-term-list-list-fix-1-forward (implies (pseudo-term-list-list-equiv (pseudo-term-list-list-fix acl2::x) acl2::y) (pseudo-term-list-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-list-list-equiv-of-pseudo-term-list-list-fix-2-forward (implies (pseudo-term-list-list-equiv acl2::x (pseudo-term-list-list-fix acl2::y)) (pseudo-term-list-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun pseudo-term-alistp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'pseudo-term-alistp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (consp (car x)) (pseudo-termp (caar x)) (pseudo-termp (cdar x)) (pseudo-term-alistp (cdr x))))))
Theorem:
(defthm pseudo-term-alistp-of-revappend (equal (pseudo-term-alistp (revappend acl2::x acl2::y)) (and (pseudo-term-alistp (acl2::list-fix acl2::x)) (pseudo-term-alistp acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-remove (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-last (implies (pseudo-term-alistp (double-rewrite acl2::x)) (pseudo-term-alistp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-nthcdr (implies (pseudo-term-alistp (double-rewrite acl2::x)) (pseudo-term-alistp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-butlast (implies (pseudo-term-alistp (double-rewrite acl2::x)) (pseudo-term-alistp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-update-nth (implies (pseudo-term-alistp (double-rewrite acl2::x)) (iff (pseudo-term-alistp (update-nth acl2::n acl2::y acl2::x)) (and (and (consp acl2::y) (pseudo-termp (car acl2::y)) (pseudo-termp (cdr acl2::y))) (or (<= (nfix acl2::n) (len acl2::x)) (and (consp nil) (pseudo-termp (car nil)) (pseudo-termp (cdr nil))))))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-repeat (iff (pseudo-term-alistp (acl2::repeat acl2::n acl2::x)) (or (and (consp acl2::x) (pseudo-termp (car acl2::x)) (pseudo-termp (cdr acl2::x))) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-take (implies (pseudo-term-alistp (double-rewrite acl2::x)) (iff (pseudo-term-alistp (take acl2::n acl2::x)) (or (and (consp nil) (pseudo-termp (car nil)) (pseudo-termp (cdr nil))) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-union-equal (equal (pseudo-term-alistp (union-equal acl2::x acl2::y)) (and (pseudo-term-alistp (acl2::list-fix acl2::x)) (pseudo-term-alistp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-intersection-equal-2 (implies (pseudo-term-alistp (double-rewrite acl2::y)) (pseudo-term-alistp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-intersection-equal-1 (implies (pseudo-term-alistp (double-rewrite acl2::x)) (pseudo-term-alistp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-set-difference-equal (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (pseudo-term-alistp acl2::y)) (equal (pseudo-term-alistp acl2::x) (true-listp acl2::x))) (implies (and (pseudo-term-alistp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (pseudo-term-alistp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-rcons (iff (pseudo-term-alistp (acl2::rcons acl2::a acl2::x)) (and (and (consp acl2::a) (pseudo-termp (car acl2::a)) (pseudo-termp (cdr acl2::a))) (pseudo-term-alistp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-append (equal (pseudo-term-alistp (append acl2::a acl2::b)) (and (pseudo-term-alistp (acl2::list-fix acl2::a)) (pseudo-term-alistp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-rev (equal (pseudo-term-alistp (acl2::rev acl2::x)) (pseudo-term-alistp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-duplicated-members (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-difference (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-intersect-2 (implies (pseudo-term-alistp acl2::y) (pseudo-term-alistp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-intersect-1 (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-union (iff (pseudo-term-alistp (set::union acl2::x acl2::y)) (and (pseudo-term-alistp (set::sfix acl2::x)) (pseudo-term-alistp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-mergesort (iff (pseudo-term-alistp (set::mergesort acl2::x)) (pseudo-term-alistp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-delete (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-insert (iff (pseudo-term-alistp (set::insert acl2::a acl2::x)) (and (pseudo-term-alistp (set::sfix acl2::x)) (and (consp acl2::a) (pseudo-termp (car acl2::a)) (pseudo-termp (cdr acl2::a))))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-sfix (iff (pseudo-term-alistp (set::sfix acl2::x)) (or (pseudo-term-alistp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-list-fix (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-pseudo-term-alistp-compound-recognizer (implies (pseudo-term-alistp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm pseudo-term-alistp-when-not-consp (implies (not (consp acl2::x)) (equal (pseudo-term-alistp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-cdr-when-pseudo-term-alistp (implies (pseudo-term-alistp (double-rewrite acl2::x)) (pseudo-term-alistp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-cons (equal (pseudo-term-alistp (cons acl2::a acl2::x)) (and (and (consp acl2::a) (pseudo-termp (car acl2::a)) (pseudo-termp (cdr acl2::a))) (pseudo-term-alistp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-remove-assoc (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (remove-assoc-equal acl2::name acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-put-assoc (implies (and (pseudo-term-alistp acl2::x)) (iff (pseudo-term-alistp (put-assoc-equal acl2::name acl2::val acl2::x)) (and (pseudo-termp acl2::name) (pseudo-termp acl2::val)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-fast-alist-clean (implies (pseudo-term-alistp acl2::x) (pseudo-term-alistp (fast-alist-clean acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-hons-shrink-alist (implies (and (pseudo-term-alistp acl2::x) (pseudo-term-alistp acl2::y)) (pseudo-term-alistp (hons-shrink-alist acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-term-alistp-of-hons-acons (equal (pseudo-term-alistp (hons-acons acl2::a acl2::n acl2::x)) (and (pseudo-termp acl2::a) (pseudo-termp acl2::n) (pseudo-term-alistp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-termp-of-cdr-of-hons-assoc-equal-when-pseudo-term-alistp (implies (pseudo-term-alistp acl2::x) (iff (pseudo-termp (cdr (hons-assoc-equal acl2::k acl2::x))) (or (hons-assoc-equal acl2::k acl2::x) (pseudo-termp nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm alistp-when-pseudo-term-alistp-rewrite (implies (pseudo-term-alistp acl2::x) (alistp acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm alistp-when-pseudo-term-alistp (implies (pseudo-term-alistp acl2::x) (alistp acl2::x)) :rule-classes :tau-system)
Theorem:
(defthm pseudo-termp-of-cdar-when-pseudo-term-alistp (implies (pseudo-term-alistp acl2::x) (iff (pseudo-termp (cdar acl2::x)) (or (consp acl2::x) (pseudo-termp nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm pseudo-termp-of-caar-when-pseudo-term-alistp (implies (pseudo-term-alistp acl2::x) (iff (pseudo-termp (caar acl2::x)) (or (consp acl2::x) (pseudo-termp nil)))) :rule-classes ((:rewrite)))
Function:
(defun pseudo-term-alist-fix$inline (x) (declare (xargs :guard (pseudo-term-alistp x))) (let ((acl2::__function__ 'pseudo-term-alist-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (if (consp (car x)) (cons (cons (pseudo-term-fix (caar x)) (pseudo-term-fix (cdar x))) (pseudo-term-alist-fix (cdr x))) (pseudo-term-alist-fix (cdr x)))) :exec x)))
Theorem:
(defthm pseudo-term-alistp-of-pseudo-term-alist-fix (b* ((fty::newx (pseudo-term-alist-fix$inline x))) (pseudo-term-alistp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-alist-fix-when-pseudo-term-alistp (implies (pseudo-term-alistp x) (equal (pseudo-term-alist-fix x) x)))
Function:
(defun pseudo-term-alist-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (pseudo-term-alistp acl2::x) (pseudo-term-alistp acl2::y)))) (equal (pseudo-term-alist-fix acl2::x) (pseudo-term-alist-fix acl2::y)))
Theorem:
(defthm pseudo-term-alist-equiv-is-an-equivalence (and (booleanp (pseudo-term-alist-equiv x y)) (pseudo-term-alist-equiv x x) (implies (pseudo-term-alist-equiv x y) (pseudo-term-alist-equiv y x)) (implies (and (pseudo-term-alist-equiv x y) (pseudo-term-alist-equiv y z)) (pseudo-term-alist-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm pseudo-term-alist-equiv-implies-equal-pseudo-term-alist-fix-1 (implies (pseudo-term-alist-equiv acl2::x x-equiv) (equal (pseudo-term-alist-fix acl2::x) (pseudo-term-alist-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm pseudo-term-alist-fix-under-pseudo-term-alist-equiv (pseudo-term-alist-equiv (pseudo-term-alist-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-pseudo-term-alist-fix-1-forward-to-pseudo-term-alist-equiv (implies (equal (pseudo-term-alist-fix acl2::x) acl2::y) (pseudo-term-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-pseudo-term-alist-fix-2-forward-to-pseudo-term-alist-equiv (implies (equal acl2::x (pseudo-term-alist-fix acl2::y)) (pseudo-term-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-alist-equiv-of-pseudo-term-alist-fix-1-forward (implies (pseudo-term-alist-equiv (pseudo-term-alist-fix acl2::x) acl2::y) (pseudo-term-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-alist-equiv-of-pseudo-term-alist-fix-2-forward (implies (pseudo-term-alist-equiv acl2::x (pseudo-term-alist-fix acl2::y)) (pseudo-term-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm cons-of-pseudo-term-fix-k-under-pseudo-term-alist-equiv (pseudo-term-alist-equiv (cons (cons (pseudo-term-fix acl2::k) acl2::v) acl2::x) (cons (cons acl2::k acl2::v) acl2::x)))
Theorem:
(defthm cons-pseudo-term-equiv-congruence-on-k-under-pseudo-term-alist-equiv (implies (pseudo-term-equiv acl2::k k-equiv) (pseudo-term-alist-equiv (cons (cons acl2::k acl2::v) acl2::x) (cons (cons k-equiv acl2::v) acl2::x))) :rule-classes :congruence)
Theorem:
(defthm cons-of-pseudo-term-fix-v-under-pseudo-term-alist-equiv (pseudo-term-alist-equiv (cons (cons acl2::k (pseudo-term-fix acl2::v)) acl2::x) (cons (cons acl2::k acl2::v) acl2::x)))
Theorem:
(defthm cons-pseudo-term-equiv-congruence-on-v-under-pseudo-term-alist-equiv (implies (pseudo-term-equiv acl2::v v-equiv) (pseudo-term-alist-equiv (cons (cons acl2::k acl2::v) acl2::x) (cons (cons acl2::k v-equiv) acl2::x))) :rule-classes :congruence)
Theorem:
(defthm cons-of-pseudo-term-alist-fix-y-under-pseudo-term-alist-equiv (pseudo-term-alist-equiv (cons acl2::x (pseudo-term-alist-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-pseudo-term-alist-equiv-congruence-on-y-under-pseudo-term-alist-equiv (implies (pseudo-term-alist-equiv acl2::y y-equiv) (pseudo-term-alist-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm pseudo-term-alist-fix-of-acons (equal (pseudo-term-alist-fix (cons (cons acl2::a acl2::b) x)) (cons (cons (pseudo-term-fix acl2::a) (pseudo-term-fix acl2::b)) (pseudo-term-alist-fix x))))
Theorem:
(defthm pseudo-term-alist-fix-of-append (equal (pseudo-term-alist-fix (append std::a std::b)) (append (pseudo-term-alist-fix std::a) (pseudo-term-alist-fix std::b))))
Theorem:
(defthm consp-car-of-pseudo-term-alist-fix (equal (consp (car (pseudo-term-alist-fix x))) (consp (pseudo-term-alist-fix x))))
Function:
(defun true-list-fix (lst) (declare (xargs :guard (true-listp lst))) (let ((acl2::__function__ 'true-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (consp lst) (cons (car lst) (true-list-fix (cdr lst))) nil) :exec lst)))
Theorem:
(defthm true-listp-of-true-list-fix (b* ((fixed-lst (true-list-fix lst))) (true-listp fixed-lst)) :rule-classes :rewrite)
Theorem:
(defthm true-list-fix-idempotent-lemma (equal (true-list-fix (true-list-fix x)) (true-list-fix x)))
Theorem:
(defthm true-list-fix-preserve-length (equal (len (true-list-fix x)) (len x)))
Function:
(defun true-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (true-listp acl2::x) (true-listp acl2::y)))) (equal (true-list-fix acl2::x) (true-list-fix acl2::y)))
Theorem:
(defthm true-list-equiv-is-an-equivalence (and (booleanp (true-list-equiv x y)) (true-list-equiv x x) (implies (true-list-equiv x y) (true-list-equiv y x)) (implies (and (true-list-equiv x y) (true-list-equiv y z)) (true-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm true-list-equiv-implies-equal-true-list-fix-1 (implies (true-list-equiv acl2::x x-equiv) (equal (true-list-fix acl2::x) (true-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm true-list-fix-under-true-list-equiv (true-list-equiv (true-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-true-list-fix-1-forward-to-true-list-equiv (implies (equal (true-list-fix acl2::x) acl2::y) (true-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-true-list-fix-2-forward-to-true-list-equiv (implies (equal acl2::x (true-list-fix acl2::y)) (true-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm true-list-equiv-of-true-list-fix-1-forward (implies (true-list-equiv (true-list-fix acl2::x) acl2::y) (true-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm true-list-equiv-of-true-list-fix-2-forward (implies (true-list-equiv acl2::x (true-list-fix acl2::y)) (true-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun hint-pair-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'hint-pair-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(thm hints))) :exec (fty::alist-with-carsp x '(thm hints))) (b* ((thm (cdr (std::da-nth 0 x))) (hints (cdr (std::da-nth 1 x)))) (and (pseudo-termp thm) (true-listp hints))))))
Theorem:
(defthm consp-when-hint-pair-p (implies (hint-pair-p x) (consp x)) :rule-classes :compound-recognizer)
Function:
(defun hint-pair-fix$inline (x) (declare (xargs :guard (hint-pair-p x))) (let ((acl2::__function__ 'hint-pair-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((thm (pseudo-term-fix (cdr (std::da-nth 0 x)))) (hints (true-list-fix (cdr (std::da-nth 1 x))))) (list (cons 'thm thm) (cons 'hints hints))) :exec x)))
Theorem:
(defthm hint-pair-p-of-hint-pair-fix (b* ((new-x (hint-pair-fix$inline x))) (hint-pair-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm hint-pair-fix-when-hint-pair-p (implies (hint-pair-p x) (equal (hint-pair-fix x) x)))
Function:
(defun hint-pair-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (hint-pair-p acl2::x) (hint-pair-p acl2::y)))) (equal (hint-pair-fix acl2::x) (hint-pair-fix acl2::y)))
Theorem:
(defthm hint-pair-equiv-is-an-equivalence (and (booleanp (hint-pair-equiv x y)) (hint-pair-equiv x x) (implies (hint-pair-equiv x y) (hint-pair-equiv y x)) (implies (and (hint-pair-equiv x y) (hint-pair-equiv y z)) (hint-pair-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm hint-pair-equiv-implies-equal-hint-pair-fix-1 (implies (hint-pair-equiv acl2::x x-equiv) (equal (hint-pair-fix acl2::x) (hint-pair-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm hint-pair-fix-under-hint-pair-equiv (hint-pair-equiv (hint-pair-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-hint-pair-fix-1-forward-to-hint-pair-equiv (implies (equal (hint-pair-fix acl2::x) acl2::y) (hint-pair-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-hint-pair-fix-2-forward-to-hint-pair-equiv (implies (equal acl2::x (hint-pair-fix acl2::y)) (hint-pair-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm hint-pair-equiv-of-hint-pair-fix-1-forward (implies (hint-pair-equiv (hint-pair-fix acl2::x) acl2::y) (hint-pair-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm hint-pair-equiv-of-hint-pair-fix-2-forward (implies (hint-pair-equiv acl2::x (hint-pair-fix acl2::y)) (hint-pair-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun hint-pair->thm$inline (x) (declare (xargs :guard (hint-pair-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'hint-pair->thm)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (pseudo-term-fix (cdr (std::da-nth 0 x)))) :exec (cdr (std::da-nth 0 x)))))
Theorem:
(defthm pseudo-termp-of-hint-pair->thm (b* ((thm (hint-pair->thm$inline x))) (pseudo-termp thm)) :rule-classes :rewrite)
Theorem:
(defthm hint-pair->thm$inline-of-hint-pair-fix-x (equal (hint-pair->thm$inline (hint-pair-fix x)) (hint-pair->thm$inline x)))
Theorem:
(defthm hint-pair->thm$inline-hint-pair-equiv-congruence-on-x (implies (hint-pair-equiv x x-equiv) (equal (hint-pair->thm$inline x) (hint-pair->thm$inline x-equiv))) :rule-classes :congruence)
Function:
(defun hint-pair->hints$inline (x) (declare (xargs :guard (hint-pair-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'hint-pair->hints)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (true-list-fix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm true-listp-of-hint-pair->hints (b* ((hints (hint-pair->hints$inline x))) (true-listp hints)) :rule-classes :rewrite)
Theorem:
(defthm hint-pair->hints$inline-of-hint-pair-fix-x (equal (hint-pair->hints$inline (hint-pair-fix x)) (hint-pair->hints$inline x)))
Theorem:
(defthm hint-pair->hints$inline-hint-pair-equiv-congruence-on-x (implies (hint-pair-equiv x x-equiv) (equal (hint-pair->hints$inline x) (hint-pair->hints$inline x-equiv))) :rule-classes :congruence)
Function:
(defun hint-pair (thm hints) (declare (xargs :guard (and (pseudo-termp thm) (true-listp hints)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'hint-pair)) (declare (ignorable acl2::__function__)) (b* ((thm (mbe :logic (pseudo-term-fix thm) :exec thm)) (hints (mbe :logic (true-list-fix hints) :exec hints))) (list (cons 'thm thm) (cons 'hints hints)))))
Theorem:
(defthm hint-pair-p-of-hint-pair (b* ((x (hint-pair thm hints))) (hint-pair-p x)) :rule-classes :rewrite)
Theorem:
(defthm hint-pair->thm-of-hint-pair (equal (hint-pair->thm (hint-pair thm hints)) (pseudo-term-fix thm)))
Theorem:
(defthm hint-pair->hints-of-hint-pair (equal (hint-pair->hints (hint-pair thm hints)) (true-list-fix hints)))
Theorem:
(defthm hint-pair-of-fields (equal (hint-pair (hint-pair->thm x) (hint-pair->hints x)) (hint-pair-fix x)))
Theorem:
(defthm hint-pair-fix-when-hint-pair (equal (hint-pair-fix x) (hint-pair (hint-pair->thm x) (hint-pair->hints x))))
Theorem:
(defthm equal-of-hint-pair (equal (equal (hint-pair thm hints) x) (and (hint-pair-p x) (equal (hint-pair->thm x) (pseudo-term-fix thm)) (equal (hint-pair->hints x) (true-list-fix hints)))))
Theorem:
(defthm hint-pair-of-pseudo-term-fix-thm (equal (hint-pair (pseudo-term-fix thm) hints) (hint-pair thm hints)))
Theorem:
(defthm hint-pair-pseudo-term-equiv-congruence-on-thm (implies (pseudo-term-equiv thm thm-equiv) (equal (hint-pair thm hints) (hint-pair thm-equiv hints))) :rule-classes :congruence)
Theorem:
(defthm hint-pair-of-true-list-fix-hints (equal (hint-pair thm (true-list-fix hints)) (hint-pair thm hints)))
Theorem:
(defthm hint-pair-true-list-equiv-congruence-on-hints (implies (true-list-equiv hints hints-equiv) (equal (hint-pair thm hints) (hint-pair thm hints-equiv))) :rule-classes :congruence)
Theorem:
(defthm hint-pair-fix-redef (equal (hint-pair-fix x) (hint-pair (hint-pair->thm x) (hint-pair->hints x))) :rule-classes :definition)
Function:
(defun hint-pair-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'hint-pair-listp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (hint-pair-p (car x)) (hint-pair-listp (cdr x))))))
Theorem:
(defthm hint-pair-listp-of-cons (equal (hint-pair-listp (cons acl2::a acl2::x)) (and (hint-pair-p acl2::a) (hint-pair-listp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-cdr-when-hint-pair-listp (implies (hint-pair-listp (double-rewrite acl2::x)) (hint-pair-listp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-when-not-consp (implies (not (consp acl2::x)) (equal (hint-pair-listp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-p-of-car-when-hint-pair-listp (implies (hint-pair-listp acl2::x) (iff (hint-pair-p (car acl2::x)) (or (consp acl2::x) (hint-pair-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-hint-pair-listp-compound-recognizer (implies (hint-pair-listp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm hint-pair-listp-of-list-fix (implies (hint-pair-listp acl2::x) (hint-pair-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-sfix (iff (hint-pair-listp (set::sfix acl2::x)) (or (hint-pair-listp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-insert (iff (hint-pair-listp (set::insert acl2::a acl2::x)) (and (hint-pair-listp (set::sfix acl2::x)) (hint-pair-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-delete (implies (hint-pair-listp acl2::x) (hint-pair-listp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-mergesort (iff (hint-pair-listp (set::mergesort acl2::x)) (hint-pair-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-union (iff (hint-pair-listp (set::union acl2::x acl2::y)) (and (hint-pair-listp (set::sfix acl2::x)) (hint-pair-listp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-intersect-1 (implies (hint-pair-listp acl2::x) (hint-pair-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-intersect-2 (implies (hint-pair-listp acl2::y) (hint-pair-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-difference (implies (hint-pair-listp acl2::x) (hint-pair-listp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-duplicated-members (implies (hint-pair-listp acl2::x) (hint-pair-listp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-rev (equal (hint-pair-listp (acl2::rev acl2::x)) (hint-pair-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-append (equal (hint-pair-listp (append acl2::a acl2::b)) (and (hint-pair-listp (acl2::list-fix acl2::a)) (hint-pair-listp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-rcons (iff (hint-pair-listp (acl2::rcons acl2::a acl2::x)) (and (hint-pair-p acl2::a) (hint-pair-listp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-p-when-member-equal-of-hint-pair-listp (and (implies (and (member-equal acl2::a acl2::x) (hint-pair-listp acl2::x)) (hint-pair-p acl2::a)) (implies (and (hint-pair-listp acl2::x) (member-equal acl2::a acl2::x)) (hint-pair-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (hint-pair-listp acl2::y)) (equal (hint-pair-listp acl2::x) (true-listp acl2::x))) (implies (and (hint-pair-listp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (hint-pair-listp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-set-difference-equal (implies (hint-pair-listp acl2::x) (hint-pair-listp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-intersection-equal-1 (implies (hint-pair-listp (double-rewrite acl2::x)) (hint-pair-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-intersection-equal-2 (implies (hint-pair-listp (double-rewrite acl2::y)) (hint-pair-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-union-equal (equal (hint-pair-listp (union-equal acl2::x acl2::y)) (and (hint-pair-listp (acl2::list-fix acl2::x)) (hint-pair-listp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-take (implies (hint-pair-listp (double-rewrite acl2::x)) (iff (hint-pair-listp (take acl2::n acl2::x)) (or (hint-pair-p nil) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-repeat (iff (hint-pair-listp (acl2::repeat acl2::n acl2::x)) (or (hint-pair-p acl2::x) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-p-of-nth-when-hint-pair-listp (implies (and (hint-pair-listp acl2::x) (< (nfix acl2::n) (len acl2::x))) (hint-pair-p (nth acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-update-nth (implies (hint-pair-listp (double-rewrite acl2::x)) (iff (hint-pair-listp (update-nth acl2::n acl2::y acl2::x)) (and (hint-pair-p acl2::y) (or (<= (nfix acl2::n) (len acl2::x)) (hint-pair-p nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-butlast (implies (hint-pair-listp (double-rewrite acl2::x)) (hint-pair-listp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-nthcdr (implies (hint-pair-listp (double-rewrite acl2::x)) (hint-pair-listp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-last (implies (hint-pair-listp (double-rewrite acl2::x)) (hint-pair-listp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-remove (implies (hint-pair-listp acl2::x) (hint-pair-listp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm hint-pair-listp-of-revappend (equal (hint-pair-listp (revappend acl2::x acl2::y)) (and (hint-pair-listp (acl2::list-fix acl2::x)) (hint-pair-listp acl2::y))) :rule-classes ((:rewrite)))
Function:
(defun hint-pair-list-fix$inline (x) (declare (xargs :guard (hint-pair-listp x))) (let ((acl2::__function__ 'hint-pair-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (cons (hint-pair-fix (car x)) (hint-pair-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm hint-pair-listp-of-hint-pair-list-fix (b* ((fty::newx (hint-pair-list-fix$inline x))) (hint-pair-listp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm hint-pair-list-fix-when-hint-pair-listp (implies (hint-pair-listp x) (equal (hint-pair-list-fix x) x)))
Function:
(defun hint-pair-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (hint-pair-listp acl2::x) (hint-pair-listp acl2::y)))) (equal (hint-pair-list-fix acl2::x) (hint-pair-list-fix acl2::y)))
Theorem:
(defthm hint-pair-list-equiv-is-an-equivalence (and (booleanp (hint-pair-list-equiv x y)) (hint-pair-list-equiv x x) (implies (hint-pair-list-equiv x y) (hint-pair-list-equiv y x)) (implies (and (hint-pair-list-equiv x y) (hint-pair-list-equiv y z)) (hint-pair-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm hint-pair-list-equiv-implies-equal-hint-pair-list-fix-1 (implies (hint-pair-list-equiv acl2::x x-equiv) (equal (hint-pair-list-fix acl2::x) (hint-pair-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm hint-pair-list-fix-under-hint-pair-list-equiv (hint-pair-list-equiv (hint-pair-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-hint-pair-list-fix-1-forward-to-hint-pair-list-equiv (implies (equal (hint-pair-list-fix acl2::x) acl2::y) (hint-pair-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-hint-pair-list-fix-2-forward-to-hint-pair-list-equiv (implies (equal acl2::x (hint-pair-list-fix acl2::y)) (hint-pair-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm hint-pair-list-equiv-of-hint-pair-list-fix-1-forward (implies (hint-pair-list-equiv (hint-pair-list-fix acl2::x) acl2::y) (hint-pair-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm hint-pair-list-equiv-of-hint-pair-list-fix-2-forward (implies (hint-pair-list-equiv acl2::x (hint-pair-list-fix acl2::y)) (hint-pair-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm car-of-hint-pair-list-fix-x-under-hint-pair-equiv (hint-pair-equiv (car (hint-pair-list-fix acl2::x)) (car acl2::x)))
Theorem:
(defthm car-hint-pair-list-equiv-congruence-on-x-under-hint-pair-equiv (implies (hint-pair-list-equiv acl2::x x-equiv) (hint-pair-equiv (car acl2::x) (car x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cdr-of-hint-pair-list-fix-x-under-hint-pair-list-equiv (hint-pair-list-equiv (cdr (hint-pair-list-fix acl2::x)) (cdr acl2::x)))
Theorem:
(defthm cdr-hint-pair-list-equiv-congruence-on-x-under-hint-pair-list-equiv (implies (hint-pair-list-equiv acl2::x x-equiv) (hint-pair-list-equiv (cdr acl2::x) (cdr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cons-of-hint-pair-fix-x-under-hint-pair-list-equiv (hint-pair-list-equiv (cons (hint-pair-fix acl2::x) acl2::y) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-hint-pair-equiv-congruence-on-x-under-hint-pair-list-equiv (implies (hint-pair-equiv acl2::x x-equiv) (hint-pair-list-equiv (cons acl2::x acl2::y) (cons x-equiv acl2::y))) :rule-classes :congruence)
Theorem:
(defthm cons-of-hint-pair-list-fix-y-under-hint-pair-list-equiv (hint-pair-list-equiv (cons acl2::x (hint-pair-list-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-hint-pair-list-equiv-congruence-on-y-under-hint-pair-list-equiv (implies (hint-pair-list-equiv acl2::y y-equiv) (hint-pair-list-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-hint-pair-list-fix (equal (consp (hint-pair-list-fix acl2::x)) (consp acl2::x)))
Theorem:
(defthm hint-pair-list-fix-under-iff (iff (hint-pair-list-fix acl2::x) (consp acl2::x)))
Theorem:
(defthm hint-pair-list-fix-of-cons (equal (hint-pair-list-fix (cons a x)) (cons (hint-pair-fix a) (hint-pair-list-fix x))))
Theorem:
(defthm len-of-hint-pair-list-fix (equal (len (hint-pair-list-fix acl2::x)) (len acl2::x)))
Theorem:
(defthm hint-pair-list-fix-of-append (equal (hint-pair-list-fix (append std::a std::b)) (append (hint-pair-list-fix std::a) (hint-pair-list-fix std::b))))
Theorem:
(defthm hint-pair-list-fix-of-repeat (equal (hint-pair-list-fix (acl2::repeat acl2::n acl2::x)) (acl2::repeat acl2::n (hint-pair-fix acl2::x))))
Theorem:
(defthm list-equiv-refines-hint-pair-list-equiv (implies (acl2::list-equiv acl2::x acl2::y) (hint-pair-list-equiv acl2::x acl2::y)) :rule-classes :refinement)
Theorem:
(defthm nth-of-hint-pair-list-fix (equal (nth acl2::n (hint-pair-list-fix acl2::x)) (if (< (nfix acl2::n) (len acl2::x)) (hint-pair-fix (nth acl2::n acl2::x)) nil)))
Theorem:
(defthm hint-pair-list-equiv-implies-hint-pair-list-equiv-append-1 (implies (hint-pair-list-equiv acl2::x fty::x-equiv) (hint-pair-list-equiv (append acl2::x acl2::y) (append fty::x-equiv acl2::y))) :rule-classes (:congruence))
Theorem:
(defthm hint-pair-list-equiv-implies-hint-pair-list-equiv-append-2 (implies (hint-pair-list-equiv acl2::y fty::y-equiv) (hint-pair-list-equiv (append acl2::x acl2::y) (append acl2::x fty::y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm hint-pair-list-equiv-implies-hint-pair-list-equiv-nthcdr-2 (implies (hint-pair-list-equiv acl2::l l-equiv) (hint-pair-list-equiv (nthcdr acl2::n acl2::l) (nthcdr acl2::n l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm hint-pair-list-equiv-implies-hint-pair-list-equiv-take-2 (implies (hint-pair-list-equiv acl2::l l-equiv) (hint-pair-list-equiv (take acl2::n acl2::l) (take acl2::n l-equiv))) :rule-classes (:congruence))
Function:
(defun decl->type-reqfix (x) (declare (xargs :guard (hint-pair-p x))) (let ((acl2::__function__ 'decl->type-reqfix)) (declare (ignorable acl2::__function__)) (b* ((x (hint-pair-fix x)) (thm (hint-pair->thm x)) (hints (hint-pair->hints x))) (make-hint-pair :thm (if (symbolp thm) thm nil) :hints (true-list-fix hints)))))
Theorem:
(defthm hint-pair-p-of-decl->type-reqfix (b* ((fixed (decl->type-reqfix x))) (hint-pair-p fixed)) :rule-classes :rewrite)
Function:
(defun decl-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'decl-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(name type))) :exec (fty::alist-with-carsp x '(name type))) (b* ((name (cdr (std::da-nth 0 x))) (type (cdr (std::da-nth 1 x)))) (and (symbolp name) (hint-pair-p type) (symbolp (hint-pair->thm type)))))))
Theorem:
(defthm consp-when-decl-p (implies (decl-p x) (consp x)) :rule-classes :compound-recognizer)
Function:
(defun decl-fix$inline (x) (declare (xargs :guard (decl-p x))) (let ((acl2::__function__ 'decl-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((name (symbol-fix (cdr (std::da-nth 0 x)))) (type (hint-pair-fix (cdr (std::da-nth 1 x))))) (let ((type (decl->type-reqfix type))) (list (cons 'name name) (cons 'type type)))) :exec x)))
Theorem:
(defthm decl-p-of-decl-fix (b* ((new-x (decl-fix$inline x))) (decl-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm decl-fix-when-decl-p (implies (decl-p x) (equal (decl-fix x) x)))
Function:
(defun decl-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (decl-p acl2::x) (decl-p acl2::y)))) (equal (decl-fix acl2::x) (decl-fix acl2::y)))
Theorem:
(defthm decl-equiv-is-an-equivalence (and (booleanp (decl-equiv x y)) (decl-equiv x x) (implies (decl-equiv x y) (decl-equiv y x)) (implies (and (decl-equiv x y) (decl-equiv y z)) (decl-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm decl-equiv-implies-equal-decl-fix-1 (implies (decl-equiv acl2::x x-equiv) (equal (decl-fix acl2::x) (decl-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm decl-fix-under-decl-equiv (decl-equiv (decl-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-decl-fix-1-forward-to-decl-equiv (implies (equal (decl-fix acl2::x) acl2::y) (decl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-decl-fix-2-forward-to-decl-equiv (implies (equal acl2::x (decl-fix acl2::y)) (decl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm decl-equiv-of-decl-fix-1-forward (implies (decl-equiv (decl-fix acl2::x) acl2::y) (decl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm decl-equiv-of-decl-fix-2-forward (implies (decl-equiv acl2::x (decl-fix acl2::y)) (decl-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun decl->name$inline (x) (declare (xargs :guard (decl-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'decl->name)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-fix (cdr (std::da-nth 0 x)))) :exec (cdr (std::da-nth 0 x)))))
Theorem:
(defthm symbolp-of-decl->name (b* ((name (decl->name$inline x))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm decl->name$inline-of-decl-fix-x (equal (decl->name$inline (decl-fix x)) (decl->name$inline x)))
Theorem:
(defthm decl->name$inline-decl-equiv-congruence-on-x (implies (decl-equiv x x-equiv) (equal (decl->name$inline x) (decl->name$inline x-equiv))) :rule-classes :congruence)
Function:
(defun decl->type$inline (x) (declare (xargs :guard (decl-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'decl->type)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x)) (name (symbol-fix (cdr (std::da-nth 0 x)))) (type (hint-pair-fix (cdr (std::da-nth 1 x))))) (decl->type-reqfix type)) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm hint-pair-p-of-decl->type (b* ((type (decl->type$inline x))) (hint-pair-p type)) :rule-classes :rewrite)
Theorem:
(defthm decl->type$inline-of-decl-fix-x (equal (decl->type$inline (decl-fix x)) (decl->type$inline x)))
Theorem:
(defthm decl->type$inline-decl-equiv-congruence-on-x (implies (decl-equiv x x-equiv) (equal (decl->type$inline x) (decl->type$inline x-equiv))) :rule-classes :congruence)
Function:
(defun decl (name type) (declare (xargs :guard (and (symbolp name) (hint-pair-p type)))) (declare (xargs :guard (symbolp (hint-pair->thm type)))) (let ((acl2::__function__ 'decl)) (declare (ignorable acl2::__function__)) (b* ((name (mbe :logic (symbol-fix name) :exec name)) (type (mbe :logic (hint-pair-fix type) :exec type))) (let ((type (mbe :logic (decl->type-reqfix type) :exec type))) (list (cons 'name name) (cons 'type type))))))
Theorem:
(defthm decl-p-of-decl (b* ((x (decl name type))) (decl-p x)) :rule-classes :rewrite)
Theorem:
(defthm decl->name-of-decl (equal (decl->name (decl name type)) (symbol-fix name)))
Theorem:
(defthm decl->type-of-decl (equal (decl->type (decl name type)) (b* ((?name (symbol-fix name)) (common-lisp::?type (hint-pair-fix type))) (decl->type-reqfix type))))
Theorem:
(defthm decl-requirements (b* ((?name (decl->name x)) (common-lisp::?type (decl->type x))) (symbolp (hint-pair->thm type))))
Theorem:
(defthm decl-of-fields (equal (decl (decl->name x) (decl->type x)) (decl-fix x)))
Theorem:
(defthm decl-fix-when-decl (equal (decl-fix x) (decl (decl->name x) (decl->type x))))
Theorem:
(defthm equal-of-decl (equal (equal (decl name type) x) (and (decl-p x) (equal (decl->name x) (symbol-fix name)) (equal (decl->type x) (b* ((?name (symbol-fix name)) (common-lisp::?type (hint-pair-fix type))) (decl->type-reqfix type))))))
Theorem:
(defthm decl-of-symbol-fix-name (equal (decl (symbol-fix name) type) (decl name type)))
Theorem:
(defthm decl-symbol-equiv-congruence-on-name (implies (acl2::symbol-equiv name name-equiv) (equal (decl name type) (decl name-equiv type))) :rule-classes :congruence)
Theorem:
(defthm decl-of-hint-pair-fix-type (equal (decl name (hint-pair-fix type)) (decl name type)))
Theorem:
(defthm decl-hint-pair-equiv-congruence-on-type (implies (hint-pair-equiv type type-equiv) (equal (decl name type) (decl name type-equiv))) :rule-classes :congruence)
Theorem:
(defthm decl-fix-redef (equal (decl-fix x) (decl (decl->name x) (decl->type x))) :rule-classes :definition)
Function:
(defun decl-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'decl-listp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (decl-p (car x)) (decl-listp (cdr x))))))
Theorem:
(defthm decl-listp-of-cons (equal (decl-listp (cons acl2::a acl2::x)) (and (decl-p acl2::a) (decl-listp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-cdr-when-decl-listp (implies (decl-listp (double-rewrite acl2::x)) (decl-listp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-when-not-consp (implies (not (consp acl2::x)) (equal (decl-listp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-p-of-car-when-decl-listp (implies (decl-listp acl2::x) (iff (decl-p (car acl2::x)) (or (consp acl2::x) (decl-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-decl-listp-compound-recognizer (implies (decl-listp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm decl-listp-of-list-fix (implies (decl-listp acl2::x) (decl-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-sfix (iff (decl-listp (set::sfix acl2::x)) (or (decl-listp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-insert (iff (decl-listp (set::insert acl2::a acl2::x)) (and (decl-listp (set::sfix acl2::x)) (decl-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-delete (implies (decl-listp acl2::x) (decl-listp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-mergesort (iff (decl-listp (set::mergesort acl2::x)) (decl-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-union (iff (decl-listp (set::union acl2::x acl2::y)) (and (decl-listp (set::sfix acl2::x)) (decl-listp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-intersect-1 (implies (decl-listp acl2::x) (decl-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-intersect-2 (implies (decl-listp acl2::y) (decl-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-difference (implies (decl-listp acl2::x) (decl-listp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-duplicated-members (implies (decl-listp acl2::x) (decl-listp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-rev (equal (decl-listp (acl2::rev acl2::x)) (decl-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-append (equal (decl-listp (append acl2::a acl2::b)) (and (decl-listp (acl2::list-fix acl2::a)) (decl-listp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-rcons (iff (decl-listp (acl2::rcons acl2::a acl2::x)) (and (decl-p acl2::a) (decl-listp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-p-when-member-equal-of-decl-listp (and (implies (and (member-equal acl2::a acl2::x) (decl-listp acl2::x)) (decl-p acl2::a)) (implies (and (decl-listp acl2::x) (member-equal acl2::a acl2::x)) (decl-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (decl-listp acl2::y)) (equal (decl-listp acl2::x) (true-listp acl2::x))) (implies (and (decl-listp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (decl-listp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-set-difference-equal (implies (decl-listp acl2::x) (decl-listp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-intersection-equal-1 (implies (decl-listp (double-rewrite acl2::x)) (decl-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-intersection-equal-2 (implies (decl-listp (double-rewrite acl2::y)) (decl-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-union-equal (equal (decl-listp (union-equal acl2::x acl2::y)) (and (decl-listp (acl2::list-fix acl2::x)) (decl-listp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-take (implies (decl-listp (double-rewrite acl2::x)) (iff (decl-listp (take acl2::n acl2::x)) (or (decl-p nil) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-repeat (iff (decl-listp (acl2::repeat acl2::n acl2::x)) (or (decl-p acl2::x) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-p-of-nth-when-decl-listp (implies (and (decl-listp acl2::x) (< (nfix acl2::n) (len acl2::x))) (decl-p (nth acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-update-nth (implies (decl-listp (double-rewrite acl2::x)) (iff (decl-listp (update-nth acl2::n acl2::y acl2::x)) (and (decl-p acl2::y) (or (<= (nfix acl2::n) (len acl2::x)) (decl-p nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-butlast (implies (decl-listp (double-rewrite acl2::x)) (decl-listp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-nthcdr (implies (decl-listp (double-rewrite acl2::x)) (decl-listp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-last (implies (decl-listp (double-rewrite acl2::x)) (decl-listp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-remove (implies (decl-listp acl2::x) (decl-listp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm decl-listp-of-revappend (equal (decl-listp (revappend acl2::x acl2::y)) (and (decl-listp (acl2::list-fix acl2::x)) (decl-listp acl2::y))) :rule-classes ((:rewrite)))
Function:
(defun decl-list-fix$inline (x) (declare (xargs :guard (decl-listp x))) (let ((acl2::__function__ 'decl-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (cons (decl-fix (car x)) (decl-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm decl-listp-of-decl-list-fix (b* ((fty::newx (decl-list-fix$inline x))) (decl-listp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm decl-list-fix-when-decl-listp (implies (decl-listp x) (equal (decl-list-fix x) x)))
Function:
(defun decl-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (decl-listp acl2::x) (decl-listp acl2::y)))) (equal (decl-list-fix acl2::x) (decl-list-fix acl2::y)))
Theorem:
(defthm decl-list-equiv-is-an-equivalence (and (booleanp (decl-list-equiv x y)) (decl-list-equiv x x) (implies (decl-list-equiv x y) (decl-list-equiv y x)) (implies (and (decl-list-equiv x y) (decl-list-equiv y z)) (decl-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm decl-list-equiv-implies-equal-decl-list-fix-1 (implies (decl-list-equiv acl2::x x-equiv) (equal (decl-list-fix acl2::x) (decl-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm decl-list-fix-under-decl-list-equiv (decl-list-equiv (decl-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-decl-list-fix-1-forward-to-decl-list-equiv (implies (equal (decl-list-fix acl2::x) acl2::y) (decl-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-decl-list-fix-2-forward-to-decl-list-equiv (implies (equal acl2::x (decl-list-fix acl2::y)) (decl-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm decl-list-equiv-of-decl-list-fix-1-forward (implies (decl-list-equiv (decl-list-fix acl2::x) acl2::y) (decl-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm decl-list-equiv-of-decl-list-fix-2-forward (implies (decl-list-equiv acl2::x (decl-list-fix acl2::y)) (decl-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm car-of-decl-list-fix-x-under-decl-equiv (decl-equiv (car (decl-list-fix acl2::x)) (car acl2::x)))
Theorem:
(defthm car-decl-list-equiv-congruence-on-x-under-decl-equiv (implies (decl-list-equiv acl2::x x-equiv) (decl-equiv (car acl2::x) (car x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cdr-of-decl-list-fix-x-under-decl-list-equiv (decl-list-equiv (cdr (decl-list-fix acl2::x)) (cdr acl2::x)))
Theorem:
(defthm cdr-decl-list-equiv-congruence-on-x-under-decl-list-equiv (implies (decl-list-equiv acl2::x x-equiv) (decl-list-equiv (cdr acl2::x) (cdr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cons-of-decl-fix-x-under-decl-list-equiv (decl-list-equiv (cons (decl-fix acl2::x) acl2::y) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-decl-equiv-congruence-on-x-under-decl-list-equiv (implies (decl-equiv acl2::x x-equiv) (decl-list-equiv (cons acl2::x acl2::y) (cons x-equiv acl2::y))) :rule-classes :congruence)
Theorem:
(defthm cons-of-decl-list-fix-y-under-decl-list-equiv (decl-list-equiv (cons acl2::x (decl-list-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-decl-list-equiv-congruence-on-y-under-decl-list-equiv (implies (decl-list-equiv acl2::y y-equiv) (decl-list-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-decl-list-fix (equal (consp (decl-list-fix acl2::x)) (consp acl2::x)))
Theorem:
(defthm decl-list-fix-under-iff (iff (decl-list-fix acl2::x) (consp acl2::x)))
Theorem:
(defthm decl-list-fix-of-cons (equal (decl-list-fix (cons a x)) (cons (decl-fix a) (decl-list-fix x))))
Theorem:
(defthm len-of-decl-list-fix (equal (len (decl-list-fix acl2::x)) (len acl2::x)))
Theorem:
(defthm decl-list-fix-of-append (equal (decl-list-fix (append std::a std::b)) (append (decl-list-fix std::a) (decl-list-fix std::b))))
Theorem:
(defthm decl-list-fix-of-repeat (equal (decl-list-fix (acl2::repeat acl2::n acl2::x)) (acl2::repeat acl2::n (decl-fix acl2::x))))
Theorem:
(defthm list-equiv-refines-decl-list-equiv (implies (acl2::list-equiv acl2::x acl2::y) (decl-list-equiv acl2::x acl2::y)) :rule-classes :refinement)
Theorem:
(defthm nth-of-decl-list-fix (equal (nth acl2::n (decl-list-fix acl2::x)) (if (< (nfix acl2::n) (len acl2::x)) (decl-fix (nth acl2::n acl2::x)) nil)))
Theorem:
(defthm decl-list-equiv-implies-decl-list-equiv-append-1 (implies (decl-list-equiv acl2::x fty::x-equiv) (decl-list-equiv (append acl2::x acl2::y) (append fty::x-equiv acl2::y))) :rule-classes (:congruence))
Theorem:
(defthm decl-list-equiv-implies-decl-list-equiv-append-2 (implies (decl-list-equiv acl2::y fty::y-equiv) (decl-list-equiv (append acl2::x acl2::y) (append acl2::x fty::y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm decl-list-equiv-implies-decl-list-equiv-nthcdr-2 (implies (decl-list-equiv acl2::l l-equiv) (decl-list-equiv (nthcdr acl2::n acl2::l) (nthcdr acl2::n l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm decl-list-equiv-implies-decl-list-equiv-take-2 (implies (decl-list-equiv acl2::l l-equiv) (decl-list-equiv (take acl2::n acl2::l) (take acl2::n l-equiv))) :rule-classes (:congruence))
Function:
(defun func-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'func-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(name formals guard returns more-returns expansion-depth flattened-formals flattened-returns))) :exec (fty::alist-with-carsp x '(name formals guard returns more-returns expansion-depth flattened-formals flattened-returns))) (b* ((name (cdr (std::da-nth 0 x))) (formals (cdr (std::da-nth 1 x))) (guard (cdr (std::da-nth 2 x))) (returns (cdr (std::da-nth 3 x))) (more-returns (cdr (std::da-nth 4 x))) (expansion-depth (cdr (std::da-nth 5 x))) (flattened-formals (cdr (std::da-nth 6 x))) (flattened-returns (cdr (std::da-nth 7 x)))) (and (symbolp name) (decl-listp formals) (hint-pair-p guard) (decl-listp returns) (hint-pair-listp more-returns) (natp expansion-depth) (symbol-listp flattened-formals) (symbol-listp flattened-returns))))))
Theorem:
(defthm consp-when-func-p (implies (func-p x) (consp x)) :rule-classes :compound-recognizer)
Function:
(defun func-fix$inline (x) (declare (xargs :guard (func-p x))) (let ((acl2::__function__ 'func-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((name (symbol-fix (cdr (std::da-nth 0 x)))) (formals (decl-list-fix (cdr (std::da-nth 1 x)))) (guard (hint-pair-fix (cdr (std::da-nth 2 x)))) (returns (decl-list-fix (cdr (std::da-nth 3 x)))) (more-returns (hint-pair-list-fix (cdr (std::da-nth 4 x)))) (expansion-depth (nfix (cdr (std::da-nth 5 x)))) (flattened-formals (symbol-list-fix (cdr (std::da-nth 6 x)))) (flattened-returns (symbol-list-fix (cdr (std::da-nth 7 x))))) (list (cons 'name name) (cons 'formals formals) (cons 'guard guard) (cons 'returns returns) (cons 'more-returns more-returns) (cons 'expansion-depth expansion-depth) (cons 'flattened-formals flattened-formals) (cons 'flattened-returns flattened-returns))) :exec x)))
Theorem:
(defthm func-p-of-func-fix (b* ((new-x (func-fix$inline x))) (func-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm func-fix-when-func-p (implies (func-p x) (equal (func-fix x) x)))
Function:
(defun func-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (func-p acl2::x) (func-p acl2::y)))) (equal (func-fix acl2::x) (func-fix acl2::y)))
Theorem:
(defthm func-equiv-is-an-equivalence (and (booleanp (func-equiv x y)) (func-equiv x x) (implies (func-equiv x y) (func-equiv y x)) (implies (and (func-equiv x y) (func-equiv y z)) (func-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm func-equiv-implies-equal-func-fix-1 (implies (func-equiv acl2::x x-equiv) (equal (func-fix acl2::x) (func-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm func-fix-under-func-equiv (func-equiv (func-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-func-fix-1-forward-to-func-equiv (implies (equal (func-fix acl2::x) acl2::y) (func-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-func-fix-2-forward-to-func-equiv (implies (equal acl2::x (func-fix acl2::y)) (func-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm func-equiv-of-func-fix-1-forward (implies (func-equiv (func-fix acl2::x) acl2::y) (func-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm func-equiv-of-func-fix-2-forward (implies (func-equiv acl2::x (func-fix acl2::y)) (func-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun func->name$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->name)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-fix (cdr (std::da-nth 0 x)))) :exec (cdr (std::da-nth 0 x)))))
Theorem:
(defthm symbolp-of-func->name (b* ((name (func->name$inline x))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm func->name$inline-of-func-fix-x (equal (func->name$inline (func-fix x)) (func->name$inline x)))
Theorem:
(defthm func->name$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->name$inline x) (func->name$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->formals$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->formals)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (decl-list-fix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm decl-listp-of-func->formals (b* ((formals (func->formals$inline x))) (decl-listp formals)) :rule-classes :rewrite)
Theorem:
(defthm func->formals$inline-of-func-fix-x (equal (func->formals$inline (func-fix x)) (func->formals$inline x)))
Theorem:
(defthm func->formals$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->formals$inline x) (func->formals$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->guard$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->guard)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (hint-pair-fix (cdr (std::da-nth 2 x)))) :exec (cdr (std::da-nth 2 x)))))
Theorem:
(defthm hint-pair-p-of-func->guard (b* ((guard (func->guard$inline x))) (hint-pair-p guard)) :rule-classes :rewrite)
Theorem:
(defthm func->guard$inline-of-func-fix-x (equal (func->guard$inline (func-fix x)) (func->guard$inline x)))
Theorem:
(defthm func->guard$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->guard$inline x) (func->guard$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->returns$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->returns)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (decl-list-fix (cdr (std::da-nth 3 x)))) :exec (cdr (std::da-nth 3 x)))))
Theorem:
(defthm decl-listp-of-func->returns (b* ((returns (func->returns$inline x))) (decl-listp returns)) :rule-classes :rewrite)
Theorem:
(defthm func->returns$inline-of-func-fix-x (equal (func->returns$inline (func-fix x)) (func->returns$inline x)))
Theorem:
(defthm func->returns$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->returns$inline x) (func->returns$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->more-returns$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->more-returns)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (hint-pair-list-fix (cdr (std::da-nth 4 x)))) :exec (cdr (std::da-nth 4 x)))))
Theorem:
(defthm hint-pair-listp-of-func->more-returns (b* ((more-returns (func->more-returns$inline x))) (hint-pair-listp more-returns)) :rule-classes :rewrite)
Theorem:
(defthm func->more-returns$inline-of-func-fix-x (equal (func->more-returns$inline (func-fix x)) (func->more-returns$inline x)))
Theorem:
(defthm func->more-returns$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->more-returns$inline x) (func->more-returns$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->expansion-depth$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->expansion-depth)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (nfix (cdr (std::da-nth 5 x)))) :exec (cdr (std::da-nth 5 x)))))
Theorem:
(defthm natp-of-func->expansion-depth (b* ((expansion-depth (func->expansion-depth$inline x))) (natp expansion-depth)) :rule-classes :rewrite)
Theorem:
(defthm func->expansion-depth$inline-of-func-fix-x (equal (func->expansion-depth$inline (func-fix x)) (func->expansion-depth$inline x)))
Theorem:
(defthm func->expansion-depth$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->expansion-depth$inline x) (func->expansion-depth$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->flattened-formals$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->flattened-formals)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-list-fix (cdr (std::da-nth 6 x)))) :exec (cdr (std::da-nth 6 x)))))
Theorem:
(defthm symbol-listp-of-func->flattened-formals (b* ((flattened-formals (func->flattened-formals$inline x))) (symbol-listp flattened-formals)) :rule-classes :rewrite)
Theorem:
(defthm func->flattened-formals$inline-of-func-fix-x (equal (func->flattened-formals$inline (func-fix x)) (func->flattened-formals$inline x)))
Theorem:
(defthm func->flattened-formals$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->flattened-formals$inline x) (func->flattened-formals$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func->flattened-returns$inline (x) (declare (xargs :guard (func-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func->flattened-returns)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-list-fix (cdr (std::da-nth 7 x)))) :exec (cdr (std::da-nth 7 x)))))
Theorem:
(defthm symbol-listp-of-func->flattened-returns (b* ((flattened-returns (func->flattened-returns$inline x))) (symbol-listp flattened-returns)) :rule-classes :rewrite)
Theorem:
(defthm func->flattened-returns$inline-of-func-fix-x (equal (func->flattened-returns$inline (func-fix x)) (func->flattened-returns$inline x)))
Theorem:
(defthm func->flattened-returns$inline-func-equiv-congruence-on-x (implies (func-equiv x x-equiv) (equal (func->flattened-returns$inline x) (func->flattened-returns$inline x-equiv))) :rule-classes :congruence)
Function:
(defun func (name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (declare (xargs :guard (and (symbolp name) (decl-listp formals) (hint-pair-p guard) (decl-listp returns) (hint-pair-listp more-returns) (natp expansion-depth) (symbol-listp flattened-formals) (symbol-listp flattened-returns)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'func)) (declare (ignorable acl2::__function__)) (b* ((name (mbe :logic (symbol-fix name) :exec name)) (formals (mbe :logic (decl-list-fix formals) :exec formals)) (guard (mbe :logic (hint-pair-fix guard) :exec guard)) (returns (mbe :logic (decl-list-fix returns) :exec returns)) (more-returns (mbe :logic (hint-pair-list-fix more-returns) :exec more-returns)) (expansion-depth (mbe :logic (nfix expansion-depth) :exec expansion-depth)) (flattened-formals (mbe :logic (symbol-list-fix flattened-formals) :exec flattened-formals)) (flattened-returns (mbe :logic (symbol-list-fix flattened-returns) :exec flattened-returns))) (list (cons 'name name) (cons 'formals formals) (cons 'guard guard) (cons 'returns returns) (cons 'more-returns more-returns) (cons 'expansion-depth expansion-depth) (cons 'flattened-formals flattened-formals) (cons 'flattened-returns flattened-returns)))))
Theorem:
(defthm func-p-of-func (b* ((x (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns))) (func-p x)) :rule-classes :rewrite)
Theorem:
(defthm func->name-of-func (equal (func->name (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (symbol-fix name)))
Theorem:
(defthm func->formals-of-func (equal (func->formals (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (decl-list-fix formals)))
Theorem:
(defthm func->guard-of-func (equal (func->guard (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (hint-pair-fix guard)))
Theorem:
(defthm func->returns-of-func (equal (func->returns (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (decl-list-fix returns)))
Theorem:
(defthm func->more-returns-of-func (equal (func->more-returns (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (hint-pair-list-fix more-returns)))
Theorem:
(defthm func->expansion-depth-of-func (equal (func->expansion-depth (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (nfix expansion-depth)))
Theorem:
(defthm func->flattened-formals-of-func (equal (func->flattened-formals (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (symbol-list-fix flattened-formals)))
Theorem:
(defthm func->flattened-returns-of-func (equal (func->flattened-returns (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)) (symbol-list-fix flattened-returns)))
Theorem:
(defthm func-of-fields (equal (func (func->name x) (func->formals x) (func->guard x) (func->returns x) (func->more-returns x) (func->expansion-depth x) (func->flattened-formals x) (func->flattened-returns x)) (func-fix x)))
Theorem:
(defthm func-fix-when-func (equal (func-fix x) (func (func->name x) (func->formals x) (func->guard x) (func->returns x) (func->more-returns x) (func->expansion-depth x) (func->flattened-formals x) (func->flattened-returns x))))
Theorem:
(defthm equal-of-func (equal (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) x) (and (func-p x) (equal (func->name x) (symbol-fix name)) (equal (func->formals x) (decl-list-fix formals)) (equal (func->guard x) (hint-pair-fix guard)) (equal (func->returns x) (decl-list-fix returns)) (equal (func->more-returns x) (hint-pair-list-fix more-returns)) (equal (func->expansion-depth x) (nfix expansion-depth)) (equal (func->flattened-formals x) (symbol-list-fix flattened-formals)) (equal (func->flattened-returns x) (symbol-list-fix flattened-returns)))))
Theorem:
(defthm func-of-symbol-fix-name (equal (func (symbol-fix name) formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-symbol-equiv-congruence-on-name (implies (acl2::symbol-equiv name name-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name-equiv formals guard returns more-returns expansion-depth flattened-formals flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-decl-list-fix-formals (equal (func name (decl-list-fix formals) guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-decl-list-equiv-congruence-on-formals (implies (decl-list-equiv formals formals-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals-equiv guard returns more-returns expansion-depth flattened-formals flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-hint-pair-fix-guard (equal (func name formals (hint-pair-fix guard) returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-hint-pair-equiv-congruence-on-guard (implies (hint-pair-equiv guard guard-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard-equiv returns more-returns expansion-depth flattened-formals flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-decl-list-fix-returns (equal (func name formals guard (decl-list-fix returns) more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-decl-list-equiv-congruence-on-returns (implies (decl-list-equiv returns returns-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns-equiv more-returns expansion-depth flattened-formals flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-hint-pair-list-fix-more-returns (equal (func name formals guard returns (hint-pair-list-fix more-returns) expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-hint-pair-list-equiv-congruence-on-more-returns (implies (hint-pair-list-equiv more-returns more-returns-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns-equiv expansion-depth flattened-formals flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-nfix-expansion-depth (equal (func name formals guard returns more-returns (nfix expansion-depth) flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-nat-equiv-congruence-on-expansion-depth (implies (acl2::nat-equiv expansion-depth expansion-depth-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth-equiv flattened-formals flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-symbol-list-fix-flattened-formals (equal (func name formals guard returns more-returns expansion-depth (symbol-list-fix flattened-formals) flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-symbol-list-equiv-congruence-on-flattened-formals (implies (acl2::symbol-list-equiv flattened-formals flattened-formals-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals-equiv flattened-returns))) :rule-classes :congruence)
Theorem:
(defthm func-of-symbol-list-fix-flattened-returns (equal (func name formals guard returns more-returns expansion-depth flattened-formals (symbol-list-fix flattened-returns)) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns)))
Theorem:
(defthm func-symbol-list-equiv-congruence-on-flattened-returns (implies (acl2::symbol-list-equiv flattened-returns flattened-returns-equiv) (equal (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns) (func name formals guard returns more-returns expansion-depth flattened-formals flattened-returns-equiv))) :rule-classes :congruence)
Theorem:
(defthm func-fix-redef (equal (func-fix x) (func (func->name x) (func->formals x) (func->guard x) (func->returns x) (func->more-returns x) (func->expansion-depth x) (func->flattened-formals x) (func->flattened-returns x))) :rule-classes :definition)
Function:
(defun func-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'func-listp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (func-p (car x)) (func-listp (cdr x))))))
Theorem:
(defthm func-listp-of-cons (equal (func-listp (cons acl2::a acl2::x)) (and (func-p acl2::a) (func-listp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-cdr-when-func-listp (implies (func-listp (double-rewrite acl2::x)) (func-listp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-when-not-consp (implies (not (consp acl2::x)) (equal (func-listp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-p-of-car-when-func-listp (implies (func-listp acl2::x) (iff (func-p (car acl2::x)) (or (consp acl2::x) (func-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-func-listp-compound-recognizer (implies (func-listp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm func-listp-of-list-fix (implies (func-listp acl2::x) (func-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-sfix (iff (func-listp (set::sfix acl2::x)) (or (func-listp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-insert (iff (func-listp (set::insert acl2::a acl2::x)) (and (func-listp (set::sfix acl2::x)) (func-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-delete (implies (func-listp acl2::x) (func-listp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-mergesort (iff (func-listp (set::mergesort acl2::x)) (func-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-union (iff (func-listp (set::union acl2::x acl2::y)) (and (func-listp (set::sfix acl2::x)) (func-listp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-intersect-1 (implies (func-listp acl2::x) (func-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-intersect-2 (implies (func-listp acl2::y) (func-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-difference (implies (func-listp acl2::x) (func-listp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-duplicated-members (implies (func-listp acl2::x) (func-listp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-rev (equal (func-listp (acl2::rev acl2::x)) (func-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-append (equal (func-listp (append acl2::a acl2::b)) (and (func-listp (acl2::list-fix acl2::a)) (func-listp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-rcons (iff (func-listp (acl2::rcons acl2::a acl2::x)) (and (func-p acl2::a) (func-listp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-p-when-member-equal-of-func-listp (and (implies (and (member-equal acl2::a acl2::x) (func-listp acl2::x)) (func-p acl2::a)) (implies (and (func-listp acl2::x) (member-equal acl2::a acl2::x)) (func-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (func-listp acl2::y)) (equal (func-listp acl2::x) (true-listp acl2::x))) (implies (and (func-listp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (func-listp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-set-difference-equal (implies (func-listp acl2::x) (func-listp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-intersection-equal-1 (implies (func-listp (double-rewrite acl2::x)) (func-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-intersection-equal-2 (implies (func-listp (double-rewrite acl2::y)) (func-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-union-equal (equal (func-listp (union-equal acl2::x acl2::y)) (and (func-listp (acl2::list-fix acl2::x)) (func-listp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-take (implies (func-listp (double-rewrite acl2::x)) (iff (func-listp (take acl2::n acl2::x)) (or (func-p nil) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-repeat (iff (func-listp (acl2::repeat acl2::n acl2::x)) (or (func-p acl2::x) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-p-of-nth-when-func-listp (implies (and (func-listp acl2::x) (< (nfix acl2::n) (len acl2::x))) (func-p (nth acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-update-nth (implies (func-listp (double-rewrite acl2::x)) (iff (func-listp (update-nth acl2::n acl2::y acl2::x)) (and (func-p acl2::y) (or (<= (nfix acl2::n) (len acl2::x)) (func-p nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-butlast (implies (func-listp (double-rewrite acl2::x)) (func-listp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-nthcdr (implies (func-listp (double-rewrite acl2::x)) (func-listp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-last (implies (func-listp (double-rewrite acl2::x)) (func-listp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-remove (implies (func-listp acl2::x) (func-listp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-listp-of-revappend (equal (func-listp (revappend acl2::x acl2::y)) (and (func-listp (acl2::list-fix acl2::x)) (func-listp acl2::y))) :rule-classes ((:rewrite)))
Function:
(defun func-list-fix$inline (x) (declare (xargs :guard (func-listp x))) (let ((acl2::__function__ 'func-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (cons (func-fix (car x)) (func-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm func-listp-of-func-list-fix (b* ((fty::newx (func-list-fix$inline x))) (func-listp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm func-list-fix-when-func-listp (implies (func-listp x) (equal (func-list-fix x) x)))
Function:
(defun func-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (func-listp acl2::x) (func-listp acl2::y)))) (equal (func-list-fix acl2::x) (func-list-fix acl2::y)))
Theorem:
(defthm func-list-equiv-is-an-equivalence (and (booleanp (func-list-equiv x y)) (func-list-equiv x x) (implies (func-list-equiv x y) (func-list-equiv y x)) (implies (and (func-list-equiv x y) (func-list-equiv y z)) (func-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm func-list-equiv-implies-equal-func-list-fix-1 (implies (func-list-equiv acl2::x x-equiv) (equal (func-list-fix acl2::x) (func-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm func-list-fix-under-func-list-equiv (func-list-equiv (func-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-func-list-fix-1-forward-to-func-list-equiv (implies (equal (func-list-fix acl2::x) acl2::y) (func-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-func-list-fix-2-forward-to-func-list-equiv (implies (equal acl2::x (func-list-fix acl2::y)) (func-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm func-list-equiv-of-func-list-fix-1-forward (implies (func-list-equiv (func-list-fix acl2::x) acl2::y) (func-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm func-list-equiv-of-func-list-fix-2-forward (implies (func-list-equiv acl2::x (func-list-fix acl2::y)) (func-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm car-of-func-list-fix-x-under-func-equiv (func-equiv (car (func-list-fix acl2::x)) (car acl2::x)))
Theorem:
(defthm car-func-list-equiv-congruence-on-x-under-func-equiv (implies (func-list-equiv acl2::x x-equiv) (func-equiv (car acl2::x) (car x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cdr-of-func-list-fix-x-under-func-list-equiv (func-list-equiv (cdr (func-list-fix acl2::x)) (cdr acl2::x)))
Theorem:
(defthm cdr-func-list-equiv-congruence-on-x-under-func-list-equiv (implies (func-list-equiv acl2::x x-equiv) (func-list-equiv (cdr acl2::x) (cdr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cons-of-func-fix-x-under-func-list-equiv (func-list-equiv (cons (func-fix acl2::x) acl2::y) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-func-equiv-congruence-on-x-under-func-list-equiv (implies (func-equiv acl2::x x-equiv) (func-list-equiv (cons acl2::x acl2::y) (cons x-equiv acl2::y))) :rule-classes :congruence)
Theorem:
(defthm cons-of-func-list-fix-y-under-func-list-equiv (func-list-equiv (cons acl2::x (func-list-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-func-list-equiv-congruence-on-y-under-func-list-equiv (implies (func-list-equiv acl2::y y-equiv) (func-list-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-func-list-fix (equal (consp (func-list-fix acl2::x)) (consp acl2::x)))
Theorem:
(defthm func-list-fix-under-iff (iff (func-list-fix acl2::x) (consp acl2::x)))
Theorem:
(defthm func-list-fix-of-cons (equal (func-list-fix (cons a x)) (cons (func-fix a) (func-list-fix x))))
Theorem:
(defthm len-of-func-list-fix (equal (len (func-list-fix acl2::x)) (len acl2::x)))
Theorem:
(defthm func-list-fix-of-append (equal (func-list-fix (append std::a std::b)) (append (func-list-fix std::a) (func-list-fix std::b))))
Theorem:
(defthm func-list-fix-of-repeat (equal (func-list-fix (acl2::repeat acl2::n acl2::x)) (acl2::repeat acl2::n (func-fix acl2::x))))
Theorem:
(defthm list-equiv-refines-func-list-equiv (implies (acl2::list-equiv acl2::x acl2::y) (func-list-equiv acl2::x acl2::y)) :rule-classes :refinement)
Theorem:
(defthm nth-of-func-list-fix (equal (nth acl2::n (func-list-fix acl2::x)) (if (< (nfix acl2::n) (len acl2::x)) (func-fix (nth acl2::n acl2::x)) nil)))
Theorem:
(defthm func-list-equiv-implies-func-list-equiv-append-1 (implies (func-list-equiv acl2::x fty::x-equiv) (func-list-equiv (append acl2::x acl2::y) (append fty::x-equiv acl2::y))) :rule-classes (:congruence))
Theorem:
(defthm func-list-equiv-implies-func-list-equiv-append-2 (implies (func-list-equiv acl2::y fty::y-equiv) (func-list-equiv (append acl2::x acl2::y) (append acl2::x fty::y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm func-list-equiv-implies-func-list-equiv-nthcdr-2 (implies (func-list-equiv acl2::l l-equiv) (func-list-equiv (nthcdr acl2::n acl2::l) (nthcdr acl2::n l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm func-list-equiv-implies-func-list-equiv-take-2 (implies (func-list-equiv acl2::l l-equiv) (func-list-equiv (take acl2::n acl2::l) (take acl2::n l-equiv))) :rule-classes (:congruence))
Function:
(defun func-alistp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'func-alistp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (consp (car x)) (symbolp (caar x)) (func-p (cdar x)) (func-alistp (cdr x))))))
Theorem:
(defthm func-alistp-of-revappend (equal (func-alistp (revappend acl2::x acl2::y)) (and (func-alistp (acl2::list-fix acl2::x)) (func-alistp acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-remove (implies (func-alistp acl2::x) (func-alistp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-last (implies (func-alistp (double-rewrite acl2::x)) (func-alistp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-nthcdr (implies (func-alistp (double-rewrite acl2::x)) (func-alistp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-butlast (implies (func-alistp (double-rewrite acl2::x)) (func-alistp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-update-nth (implies (func-alistp (double-rewrite acl2::x)) (iff (func-alistp (update-nth acl2::n acl2::y acl2::x)) (and (and (consp acl2::y) (symbolp (car acl2::y)) (func-p (cdr acl2::y))) (or (<= (nfix acl2::n) (len acl2::x)) (and (consp nil) (symbolp (car nil)) (func-p (cdr nil))))))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-repeat (iff (func-alistp (acl2::repeat acl2::n acl2::x)) (or (and (consp acl2::x) (symbolp (car acl2::x)) (func-p (cdr acl2::x))) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-take (implies (func-alistp (double-rewrite acl2::x)) (iff (func-alistp (take acl2::n acl2::x)) (or (and (consp nil) (symbolp (car nil)) (func-p (cdr nil))) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-union-equal (equal (func-alistp (union-equal acl2::x acl2::y)) (and (func-alistp (acl2::list-fix acl2::x)) (func-alistp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-intersection-equal-2 (implies (func-alistp (double-rewrite acl2::y)) (func-alistp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-intersection-equal-1 (implies (func-alistp (double-rewrite acl2::x)) (func-alistp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-set-difference-equal (implies (func-alistp acl2::x) (func-alistp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (func-alistp acl2::y)) (equal (func-alistp acl2::x) (true-listp acl2::x))) (implies (and (func-alistp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (func-alistp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-rcons (iff (func-alistp (acl2::rcons acl2::a acl2::x)) (and (and (consp acl2::a) (symbolp (car acl2::a)) (func-p (cdr acl2::a))) (func-alistp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-append (equal (func-alistp (append acl2::a acl2::b)) (and (func-alistp (acl2::list-fix acl2::a)) (func-alistp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-rev (equal (func-alistp (acl2::rev acl2::x)) (func-alistp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-duplicated-members (implies (func-alistp acl2::x) (func-alistp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-difference (implies (func-alistp acl2::x) (func-alistp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-intersect-2 (implies (func-alistp acl2::y) (func-alistp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-intersect-1 (implies (func-alistp acl2::x) (func-alistp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-union (iff (func-alistp (set::union acl2::x acl2::y)) (and (func-alistp (set::sfix acl2::x)) (func-alistp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-mergesort (iff (func-alistp (set::mergesort acl2::x)) (func-alistp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-delete (implies (func-alistp acl2::x) (func-alistp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-insert (iff (func-alistp (set::insert acl2::a acl2::x)) (and (func-alistp (set::sfix acl2::x)) (and (consp acl2::a) (symbolp (car acl2::a)) (func-p (cdr acl2::a))))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-sfix (iff (func-alistp (set::sfix acl2::x)) (or (func-alistp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-list-fix (implies (func-alistp acl2::x) (func-alistp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-func-alistp-compound-recognizer (implies (func-alistp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm func-alistp-when-not-consp (implies (not (consp acl2::x)) (equal (func-alistp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-cdr-when-func-alistp (implies (func-alistp (double-rewrite acl2::x)) (func-alistp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-cons (equal (func-alistp (cons acl2::a acl2::x)) (and (and (consp acl2::a) (symbolp (car acl2::a)) (func-p (cdr acl2::a))) (func-alistp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-remove-assoc (implies (func-alistp acl2::x) (func-alistp (remove-assoc-equal acl2::name acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-put-assoc (implies (and (func-alistp acl2::x)) (iff (func-alistp (put-assoc-equal acl2::name acl2::val acl2::x)) (and (symbolp acl2::name) (func-p acl2::val)))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-fast-alist-clean (implies (func-alistp acl2::x) (func-alistp (fast-alist-clean acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-hons-shrink-alist (implies (and (func-alistp acl2::x) (func-alistp acl2::y)) (func-alistp (hons-shrink-alist acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-alistp-of-hons-acons (equal (func-alistp (hons-acons acl2::a acl2::n acl2::x)) (and (symbolp acl2::a) (func-p acl2::n) (func-alistp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm func-p-of-cdr-of-hons-assoc-equal-when-func-alistp (implies (func-alistp acl2::x) (iff (func-p (cdr (hons-assoc-equal acl2::k acl2::x))) (or (hons-assoc-equal acl2::k acl2::x) (func-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm alistp-when-func-alistp-rewrite (implies (func-alistp acl2::x) (alistp acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm alistp-when-func-alistp (implies (func-alistp acl2::x) (alistp acl2::x)) :rule-classes :tau-system)
Theorem:
(defthm func-p-of-cdar-when-func-alistp (implies (func-alistp acl2::x) (iff (func-p (cdar acl2::x)) (or (consp acl2::x) (func-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm symbolp-of-caar-when-func-alistp (implies (func-alistp acl2::x) (iff (symbolp (caar acl2::x)) (or (consp acl2::x) (symbolp nil)))) :rule-classes ((:rewrite)))
Function:
(defun func-alist-fix$inline (x) (declare (xargs :guard (func-alistp x))) (let ((acl2::__function__ 'func-alist-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (if (consp (car x)) (cons (cons (symbol-fix (caar x)) (func-fix (cdar x))) (func-alist-fix (cdr x))) (func-alist-fix (cdr x)))) :exec x)))
Theorem:
(defthm func-alistp-of-func-alist-fix (b* ((fty::newx (func-alist-fix$inline x))) (func-alistp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm func-alist-fix-when-func-alistp (implies (func-alistp x) (equal (func-alist-fix x) x)))
Function:
(defun func-alist-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (func-alistp acl2::x) (func-alistp acl2::y)))) (equal (func-alist-fix acl2::x) (func-alist-fix acl2::y)))
Theorem:
(defthm func-alist-equiv-is-an-equivalence (and (booleanp (func-alist-equiv x y)) (func-alist-equiv x x) (implies (func-alist-equiv x y) (func-alist-equiv y x)) (implies (and (func-alist-equiv x y) (func-alist-equiv y z)) (func-alist-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm func-alist-equiv-implies-equal-func-alist-fix-1 (implies (func-alist-equiv acl2::x x-equiv) (equal (func-alist-fix acl2::x) (func-alist-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm func-alist-fix-under-func-alist-equiv (func-alist-equiv (func-alist-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-func-alist-fix-1-forward-to-func-alist-equiv (implies (equal (func-alist-fix acl2::x) acl2::y) (func-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-func-alist-fix-2-forward-to-func-alist-equiv (implies (equal acl2::x (func-alist-fix acl2::y)) (func-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm func-alist-equiv-of-func-alist-fix-1-forward (implies (func-alist-equiv (func-alist-fix acl2::x) acl2::y) (func-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm func-alist-equiv-of-func-alist-fix-2-forward (implies (func-alist-equiv acl2::x (func-alist-fix acl2::y)) (func-alist-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm cons-of-symbol-fix-k-under-func-alist-equiv (func-alist-equiv (cons (cons (symbol-fix acl2::k) acl2::v) acl2::x) (cons (cons acl2::k acl2::v) acl2::x)))
Theorem:
(defthm cons-symbol-equiv-congruence-on-k-under-func-alist-equiv (implies (acl2::symbol-equiv acl2::k k-equiv) (func-alist-equiv (cons (cons acl2::k acl2::v) acl2::x) (cons (cons k-equiv acl2::v) acl2::x))) :rule-classes :congruence)
Theorem:
(defthm cons-of-func-fix-v-under-func-alist-equiv (func-alist-equiv (cons (cons acl2::k (func-fix acl2::v)) acl2::x) (cons (cons acl2::k acl2::v) acl2::x)))
Theorem:
(defthm cons-func-equiv-congruence-on-v-under-func-alist-equiv (implies (func-equiv acl2::v v-equiv) (func-alist-equiv (cons (cons acl2::k acl2::v) acl2::x) (cons (cons acl2::k v-equiv) acl2::x))) :rule-classes :congruence)
Theorem:
(defthm cons-of-func-alist-fix-y-under-func-alist-equiv (func-alist-equiv (cons acl2::x (func-alist-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-func-alist-equiv-congruence-on-y-under-func-alist-equiv (implies (func-alist-equiv acl2::y y-equiv) (func-alist-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm func-alist-fix-of-acons (equal (func-alist-fix (cons (cons acl2::a acl2::b) x)) (cons (cons (symbol-fix acl2::a) (func-fix acl2::b)) (func-alist-fix x))))
Theorem:
(defthm func-alist-fix-of-append (equal (func-alist-fix (append std::a std::b)) (append (func-alist-fix std::a) (func-alist-fix std::b))))
Theorem:
(defthm consp-car-of-func-alist-fix (equal (consp (car (func-alist-fix x))) (consp (func-alist-fix x))))
Function:
(defun binding-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'binding-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(var expr type))) :exec (fty::alist-with-carsp x '(var expr type))) (b* ((var (cdr (std::da-nth 0 x))) (expr (cdr (std::da-nth 1 x))) (type (cdr (std::da-nth 2 x)))) (and (symbolp var) (pseudo-termp expr) (symbolp type))))))
Theorem:
(defthm consp-when-binding-p (implies (binding-p x) (consp x)) :rule-classes :compound-recognizer)
Function:
(defun binding-fix$inline (x) (declare (xargs :guard (binding-p x))) (let ((acl2::__function__ 'binding-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((var (symbol-fix (cdr (std::da-nth 0 x)))) (expr (pseudo-term-fix (cdr (std::da-nth 1 x)))) (type (symbol-fix (cdr (std::da-nth 2 x))))) (list (cons 'var var) (cons 'expr expr) (cons 'type type))) :exec x)))
Theorem:
(defthm binding-p-of-binding-fix (b* ((new-x (binding-fix$inline x))) (binding-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm binding-fix-when-binding-p (implies (binding-p x) (equal (binding-fix x) x)))
Function:
(defun binding-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (binding-p acl2::x) (binding-p acl2::y)))) (equal (binding-fix acl2::x) (binding-fix acl2::y)))
Theorem:
(defthm binding-equiv-is-an-equivalence (and (booleanp (binding-equiv x y)) (binding-equiv x x) (implies (binding-equiv x y) (binding-equiv y x)) (implies (and (binding-equiv x y) (binding-equiv y z)) (binding-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm binding-equiv-implies-equal-binding-fix-1 (implies (binding-equiv acl2::x x-equiv) (equal (binding-fix acl2::x) (binding-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm binding-fix-under-binding-equiv (binding-equiv (binding-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-binding-fix-1-forward-to-binding-equiv (implies (equal (binding-fix acl2::x) acl2::y) (binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-binding-fix-2-forward-to-binding-equiv (implies (equal acl2::x (binding-fix acl2::y)) (binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm binding-equiv-of-binding-fix-1-forward (implies (binding-equiv (binding-fix acl2::x) acl2::y) (binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm binding-equiv-of-binding-fix-2-forward (implies (binding-equiv acl2::x (binding-fix acl2::y)) (binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun binding->var$inline (x) (declare (xargs :guard (binding-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'binding->var)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-fix (cdr (std::da-nth 0 x)))) :exec (cdr (std::da-nth 0 x)))))
Theorem:
(defthm symbolp-of-binding->var (b* ((var (binding->var$inline x))) (symbolp var)) :rule-classes :rewrite)
Theorem:
(defthm binding->var$inline-of-binding-fix-x (equal (binding->var$inline (binding-fix x)) (binding->var$inline x)))
Theorem:
(defthm binding->var$inline-binding-equiv-congruence-on-x (implies (binding-equiv x x-equiv) (equal (binding->var$inline x) (binding->var$inline x-equiv))) :rule-classes :congruence)
Function:
(defun binding->expr$inline (x) (declare (xargs :guard (binding-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'binding->expr)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (pseudo-term-fix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm pseudo-termp-of-binding->expr (b* ((expr (binding->expr$inline x))) (pseudo-termp expr)) :rule-classes :rewrite)
Theorem:
(defthm binding->expr$inline-of-binding-fix-x (equal (binding->expr$inline (binding-fix x)) (binding->expr$inline x)))
Theorem:
(defthm binding->expr$inline-binding-equiv-congruence-on-x (implies (binding-equiv x x-equiv) (equal (binding->expr$inline x) (binding->expr$inline x-equiv))) :rule-classes :congruence)
Function:
(defun binding->type$inline (x) (declare (xargs :guard (binding-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'binding->type)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-fix (cdr (std::da-nth 2 x)))) :exec (cdr (std::da-nth 2 x)))))
Theorem:
(defthm symbolp-of-binding->type (b* ((type (binding->type$inline x))) (symbolp type)) :rule-classes :rewrite)
Theorem:
(defthm binding->type$inline-of-binding-fix-x (equal (binding->type$inline (binding-fix x)) (binding->type$inline x)))
Theorem:
(defthm binding->type$inline-binding-equiv-congruence-on-x (implies (binding-equiv x x-equiv) (equal (binding->type$inline x) (binding->type$inline x-equiv))) :rule-classes :congruence)
Function:
(defun binding (var expr type) (declare (xargs :guard (and (symbolp var) (pseudo-termp expr) (symbolp type)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'binding)) (declare (ignorable acl2::__function__)) (b* ((var (mbe :logic (symbol-fix var) :exec var)) (expr (mbe :logic (pseudo-term-fix expr) :exec expr)) (type (mbe :logic (symbol-fix type) :exec type))) (list (cons 'var var) (cons 'expr expr) (cons 'type type)))))
Theorem:
(defthm binding-p-of-binding (b* ((x (binding var expr type))) (binding-p x)) :rule-classes :rewrite)
Theorem:
(defthm binding->var-of-binding (equal (binding->var (binding var expr type)) (symbol-fix var)))
Theorem:
(defthm binding->expr-of-binding (equal (binding->expr (binding var expr type)) (pseudo-term-fix expr)))
Theorem:
(defthm binding->type-of-binding (equal (binding->type (binding var expr type)) (symbol-fix type)))
Theorem:
(defthm binding-of-fields (equal (binding (binding->var x) (binding->expr x) (binding->type x)) (binding-fix x)))
Theorem:
(defthm binding-fix-when-binding (equal (binding-fix x) (binding (binding->var x) (binding->expr x) (binding->type x))))
Theorem:
(defthm equal-of-binding (equal (equal (binding var expr type) x) (and (binding-p x) (equal (binding->var x) (symbol-fix var)) (equal (binding->expr x) (pseudo-term-fix expr)) (equal (binding->type x) (symbol-fix type)))))
Theorem:
(defthm binding-of-symbol-fix-var (equal (binding (symbol-fix var) expr type) (binding var expr type)))
Theorem:
(defthm binding-symbol-equiv-congruence-on-var (implies (acl2::symbol-equiv var var-equiv) (equal (binding var expr type) (binding var-equiv expr type))) :rule-classes :congruence)
Theorem:
(defthm binding-of-pseudo-term-fix-expr (equal (binding var (pseudo-term-fix expr) type) (binding var expr type)))
Theorem:
(defthm binding-pseudo-term-equiv-congruence-on-expr (implies (pseudo-term-equiv expr expr-equiv) (equal (binding var expr type) (binding var expr-equiv type))) :rule-classes :congruence)
Theorem:
(defthm binding-of-symbol-fix-type (equal (binding var expr (symbol-fix type)) (binding var expr type)))
Theorem:
(defthm binding-symbol-equiv-congruence-on-type (implies (acl2::symbol-equiv type type-equiv) (equal (binding var expr type) (binding var expr type-equiv))) :rule-classes :congruence)
Theorem:
(defthm binding-fix-redef (equal (binding-fix x) (binding (binding->var x) (binding->expr x) (binding->type x))) :rule-classes :definition)
Function:
(defun binding-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'binding-listp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (binding-p (car x)) (binding-listp (cdr x))))))
Theorem:
(defthm binding-listp-of-cons (equal (binding-listp (cons acl2::a acl2::x)) (and (binding-p acl2::a) (binding-listp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-cdr-when-binding-listp (implies (binding-listp (double-rewrite acl2::x)) (binding-listp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-when-not-consp (implies (not (consp acl2::x)) (equal (binding-listp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-p-of-car-when-binding-listp (implies (binding-listp acl2::x) (iff (binding-p (car acl2::x)) (or (consp acl2::x) (binding-p nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-binding-listp-compound-recognizer (implies (binding-listp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm binding-listp-of-list-fix (implies (binding-listp acl2::x) (binding-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-sfix (iff (binding-listp (set::sfix acl2::x)) (or (binding-listp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-insert (iff (binding-listp (set::insert acl2::a acl2::x)) (and (binding-listp (set::sfix acl2::x)) (binding-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-delete (implies (binding-listp acl2::x) (binding-listp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-mergesort (iff (binding-listp (set::mergesort acl2::x)) (binding-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-union (iff (binding-listp (set::union acl2::x acl2::y)) (and (binding-listp (set::sfix acl2::x)) (binding-listp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-intersect-1 (implies (binding-listp acl2::x) (binding-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-intersect-2 (implies (binding-listp acl2::y) (binding-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-difference (implies (binding-listp acl2::x) (binding-listp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-duplicated-members (implies (binding-listp acl2::x) (binding-listp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-rev (equal (binding-listp (acl2::rev acl2::x)) (binding-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-append (equal (binding-listp (append acl2::a acl2::b)) (and (binding-listp (acl2::list-fix acl2::a)) (binding-listp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-rcons (iff (binding-listp (acl2::rcons acl2::a acl2::x)) (and (binding-p acl2::a) (binding-listp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-p-when-member-equal-of-binding-listp (and (implies (and (member-equal acl2::a acl2::x) (binding-listp acl2::x)) (binding-p acl2::a)) (implies (and (binding-listp acl2::x) (member-equal acl2::a acl2::x)) (binding-p acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (binding-listp acl2::y)) (equal (binding-listp acl2::x) (true-listp acl2::x))) (implies (and (binding-listp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (binding-listp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-set-difference-equal (implies (binding-listp acl2::x) (binding-listp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-intersection-equal-1 (implies (binding-listp (double-rewrite acl2::x)) (binding-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-intersection-equal-2 (implies (binding-listp (double-rewrite acl2::y)) (binding-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-union-equal (equal (binding-listp (union-equal acl2::x acl2::y)) (and (binding-listp (acl2::list-fix acl2::x)) (binding-listp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-take (implies (binding-listp (double-rewrite acl2::x)) (iff (binding-listp (take acl2::n acl2::x)) (or (binding-p nil) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-repeat (iff (binding-listp (acl2::repeat acl2::n acl2::x)) (or (binding-p acl2::x) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-p-of-nth-when-binding-listp (implies (and (binding-listp acl2::x) (< (nfix acl2::n) (len acl2::x))) (binding-p (nth acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-update-nth (implies (binding-listp (double-rewrite acl2::x)) (iff (binding-listp (update-nth acl2::n acl2::y acl2::x)) (and (binding-p acl2::y) (or (<= (nfix acl2::n) (len acl2::x)) (binding-p nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-butlast (implies (binding-listp (double-rewrite acl2::x)) (binding-listp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-nthcdr (implies (binding-listp (double-rewrite acl2::x)) (binding-listp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-last (implies (binding-listp (double-rewrite acl2::x)) (binding-listp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-remove (implies (binding-listp acl2::x) (binding-listp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm binding-listp-of-revappend (equal (binding-listp (revappend acl2::x acl2::y)) (and (binding-listp (acl2::list-fix acl2::x)) (binding-listp acl2::y))) :rule-classes ((:rewrite)))
Function:
(defun binding-list-fix$inline (x) (declare (xargs :guard (binding-listp x))) (let ((acl2::__function__ 'binding-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (cons (binding-fix (car x)) (binding-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm binding-listp-of-binding-list-fix (b* ((fty::newx (binding-list-fix$inline x))) (binding-listp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm binding-list-fix-when-binding-listp (implies (binding-listp x) (equal (binding-list-fix x) x)))
Function:
(defun binding-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (binding-listp acl2::x) (binding-listp acl2::y)))) (equal (binding-list-fix acl2::x) (binding-list-fix acl2::y)))
Theorem:
(defthm binding-list-equiv-is-an-equivalence (and (booleanp (binding-list-equiv x y)) (binding-list-equiv x x) (implies (binding-list-equiv x y) (binding-list-equiv y x)) (implies (and (binding-list-equiv x y) (binding-list-equiv y z)) (binding-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm binding-list-equiv-implies-equal-binding-list-fix-1 (implies (binding-list-equiv acl2::x x-equiv) (equal (binding-list-fix acl2::x) (binding-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm binding-list-fix-under-binding-list-equiv (binding-list-equiv (binding-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-binding-list-fix-1-forward-to-binding-list-equiv (implies (equal (binding-list-fix acl2::x) acl2::y) (binding-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-binding-list-fix-2-forward-to-binding-list-equiv (implies (equal acl2::x (binding-list-fix acl2::y)) (binding-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm binding-list-equiv-of-binding-list-fix-1-forward (implies (binding-list-equiv (binding-list-fix acl2::x) acl2::y) (binding-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm binding-list-equiv-of-binding-list-fix-2-forward (implies (binding-list-equiv acl2::x (binding-list-fix acl2::y)) (binding-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm car-of-binding-list-fix-x-under-binding-equiv (binding-equiv (car (binding-list-fix acl2::x)) (car acl2::x)))
Theorem:
(defthm car-binding-list-equiv-congruence-on-x-under-binding-equiv (implies (binding-list-equiv acl2::x x-equiv) (binding-equiv (car acl2::x) (car x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cdr-of-binding-list-fix-x-under-binding-list-equiv (binding-list-equiv (cdr (binding-list-fix acl2::x)) (cdr acl2::x)))
Theorem:
(defthm cdr-binding-list-equiv-congruence-on-x-under-binding-list-equiv (implies (binding-list-equiv acl2::x x-equiv) (binding-list-equiv (cdr acl2::x) (cdr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cons-of-binding-fix-x-under-binding-list-equiv (binding-list-equiv (cons (binding-fix acl2::x) acl2::y) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-binding-equiv-congruence-on-x-under-binding-list-equiv (implies (binding-equiv acl2::x x-equiv) (binding-list-equiv (cons acl2::x acl2::y) (cons x-equiv acl2::y))) :rule-classes :congruence)
Theorem:
(defthm cons-of-binding-list-fix-y-under-binding-list-equiv (binding-list-equiv (cons acl2::x (binding-list-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-binding-list-equiv-congruence-on-y-under-binding-list-equiv (implies (binding-list-equiv acl2::y y-equiv) (binding-list-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-binding-list-fix (equal (consp (binding-list-fix acl2::x)) (consp acl2::x)))
Theorem:
(defthm binding-list-fix-under-iff (iff (binding-list-fix acl2::x) (consp acl2::x)))
Theorem:
(defthm binding-list-fix-of-cons (equal (binding-list-fix (cons a x)) (cons (binding-fix a) (binding-list-fix x))))
Theorem:
(defthm len-of-binding-list-fix (equal (len (binding-list-fix acl2::x)) (len acl2::x)))
Theorem:
(defthm binding-list-fix-of-append (equal (binding-list-fix (append std::a std::b)) (append (binding-list-fix std::a) (binding-list-fix std::b))))
Theorem:
(defthm binding-list-fix-of-repeat (equal (binding-list-fix (acl2::repeat acl2::n acl2::x)) (acl2::repeat acl2::n (binding-fix acl2::x))))
Theorem:
(defthm list-equiv-refines-binding-list-equiv (implies (acl2::list-equiv acl2::x acl2::y) (binding-list-equiv acl2::x acl2::y)) :rule-classes :refinement)
Theorem:
(defthm nth-of-binding-list-fix (equal (nth acl2::n (binding-list-fix acl2::x)) (if (< (nfix acl2::n) (len acl2::x)) (binding-fix (nth acl2::n acl2::x)) nil)))
Theorem:
(defthm binding-list-equiv-implies-binding-list-equiv-append-1 (implies (binding-list-equiv acl2::x fty::x-equiv) (binding-list-equiv (append acl2::x acl2::y) (append fty::x-equiv acl2::y))) :rule-classes (:congruence))
Theorem:
(defthm binding-list-equiv-implies-binding-list-equiv-append-2 (implies (binding-list-equiv acl2::y fty::y-equiv) (binding-list-equiv (append acl2::x acl2::y) (append acl2::x fty::y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm binding-list-equiv-implies-binding-list-equiv-nthcdr-2 (implies (binding-list-equiv acl2::l l-equiv) (binding-list-equiv (nthcdr acl2::n acl2::l) (nthcdr acl2::n l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm binding-list-equiv-implies-binding-list-equiv-take-2 (implies (binding-list-equiv acl2::l l-equiv) (binding-list-equiv (take acl2::n acl2::l) (take acl2::n l-equiv))) :rule-classes (:congruence))
Function:
(defun let-binding-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'let-binding-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(bindings hypotheses))) :exec (fty::alist-with-carsp x '(bindings hypotheses))) (b* ((bindings (cdr (std::da-nth 0 x))) (hypotheses (cdr (std::da-nth 1 x)))) (and (binding-listp bindings) (hint-pair-listp hypotheses))))))
Theorem:
(defthm consp-when-let-binding-p (implies (let-binding-p x) (consp x)) :rule-classes :compound-recognizer)
Function:
(defun let-binding-fix$inline (x) (declare (xargs :guard (let-binding-p x))) (let ((acl2::__function__ 'let-binding-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((bindings (binding-list-fix (cdr (std::da-nth 0 x)))) (hypotheses (hint-pair-list-fix (cdr (std::da-nth 1 x))))) (list (cons 'bindings bindings) (cons 'hypotheses hypotheses))) :exec x)))
Theorem:
(defthm let-binding-p-of-let-binding-fix (b* ((new-x (let-binding-fix$inline x))) (let-binding-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm let-binding-fix-when-let-binding-p (implies (let-binding-p x) (equal (let-binding-fix x) x)))
Function:
(defun let-binding-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (let-binding-p acl2::x) (let-binding-p acl2::y)))) (equal (let-binding-fix acl2::x) (let-binding-fix acl2::y)))
Theorem:
(defthm let-binding-equiv-is-an-equivalence (and (booleanp (let-binding-equiv x y)) (let-binding-equiv x x) (implies (let-binding-equiv x y) (let-binding-equiv y x)) (implies (and (let-binding-equiv x y) (let-binding-equiv y z)) (let-binding-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm let-binding-equiv-implies-equal-let-binding-fix-1 (implies (let-binding-equiv acl2::x x-equiv) (equal (let-binding-fix acl2::x) (let-binding-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm let-binding-fix-under-let-binding-equiv (let-binding-equiv (let-binding-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-let-binding-fix-1-forward-to-let-binding-equiv (implies (equal (let-binding-fix acl2::x) acl2::y) (let-binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-let-binding-fix-2-forward-to-let-binding-equiv (implies (equal acl2::x (let-binding-fix acl2::y)) (let-binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm let-binding-equiv-of-let-binding-fix-1-forward (implies (let-binding-equiv (let-binding-fix acl2::x) acl2::y) (let-binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm let-binding-equiv-of-let-binding-fix-2-forward (implies (let-binding-equiv acl2::x (let-binding-fix acl2::y)) (let-binding-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun let-binding->bindings$inline (x) (declare (xargs :guard (let-binding-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'let-binding->bindings)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (binding-list-fix (cdr (std::da-nth 0 x)))) :exec (cdr (std::da-nth 0 x)))))
Theorem:
(defthm binding-listp-of-let-binding->bindings (b* ((bindings (let-binding->bindings$inline x))) (binding-listp bindings)) :rule-classes :rewrite)
Theorem:
(defthm let-binding->bindings$inline-of-let-binding-fix-x (equal (let-binding->bindings$inline (let-binding-fix x)) (let-binding->bindings$inline x)))
Theorem:
(defthm let-binding->bindings$inline-let-binding-equiv-congruence-on-x (implies (let-binding-equiv x x-equiv) (equal (let-binding->bindings$inline x) (let-binding->bindings$inline x-equiv))) :rule-classes :congruence)
Function:
(defun let-binding->hypotheses$inline (x) (declare (xargs :guard (let-binding-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'let-binding->hypotheses)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (hint-pair-list-fix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm hint-pair-listp-of-let-binding->hypotheses (b* ((hypotheses (let-binding->hypotheses$inline x))) (hint-pair-listp hypotheses)) :rule-classes :rewrite)
Theorem:
(defthm let-binding->hypotheses$inline-of-let-binding-fix-x (equal (let-binding->hypotheses$inline (let-binding-fix x)) (let-binding->hypotheses$inline x)))
Theorem:
(defthm let-binding->hypotheses$inline-let-binding-equiv-congruence-on-x (implies (let-binding-equiv x x-equiv) (equal (let-binding->hypotheses$inline x) (let-binding->hypotheses$inline x-equiv))) :rule-classes :congruence)
Function:
(defun let-binding (bindings hypotheses) (declare (xargs :guard (and (binding-listp bindings) (hint-pair-listp hypotheses)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'let-binding)) (declare (ignorable acl2::__function__)) (b* ((bindings (mbe :logic (binding-list-fix bindings) :exec bindings)) (hypotheses (mbe :logic (hint-pair-list-fix hypotheses) :exec hypotheses))) (list (cons 'bindings bindings) (cons 'hypotheses hypotheses)))))
Theorem:
(defthm let-binding-p-of-let-binding (b* ((x (let-binding bindings hypotheses))) (let-binding-p x)) :rule-classes :rewrite)
Theorem:
(defthm let-binding->bindings-of-let-binding (equal (let-binding->bindings (let-binding bindings hypotheses)) (binding-list-fix bindings)))
Theorem:
(defthm let-binding->hypotheses-of-let-binding (equal (let-binding->hypotheses (let-binding bindings hypotheses)) (hint-pair-list-fix hypotheses)))
Theorem:
(defthm let-binding-of-fields (equal (let-binding (let-binding->bindings x) (let-binding->hypotheses x)) (let-binding-fix x)))
Theorem:
(defthm let-binding-fix-when-let-binding (equal (let-binding-fix x) (let-binding (let-binding->bindings x) (let-binding->hypotheses x))))
Theorem:
(defthm equal-of-let-binding (equal (equal (let-binding bindings hypotheses) x) (and (let-binding-p x) (equal (let-binding->bindings x) (binding-list-fix bindings)) (equal (let-binding->hypotheses x) (hint-pair-list-fix hypotheses)))))
Theorem:
(defthm let-binding-of-binding-list-fix-bindings (equal (let-binding (binding-list-fix bindings) hypotheses) (let-binding bindings hypotheses)))
Theorem:
(defthm let-binding-binding-list-equiv-congruence-on-bindings (implies (binding-list-equiv bindings bindings-equiv) (equal (let-binding bindings hypotheses) (let-binding bindings-equiv hypotheses))) :rule-classes :congruence)
Theorem:
(defthm let-binding-of-hint-pair-list-fix-hypotheses (equal (let-binding bindings (hint-pair-list-fix hypotheses)) (let-binding bindings hypotheses)))
Theorem:
(defthm let-binding-hint-pair-list-equiv-congruence-on-hypotheses (implies (hint-pair-list-equiv hypotheses hypotheses-equiv) (equal (let-binding bindings hypotheses) (let-binding bindings hypotheses-equiv))) :rule-classes :congruence)
Theorem:
(defthm let-binding-fix-redef (equal (let-binding-fix x) (let-binding (let-binding->bindings x) (let-binding->hypotheses x))) :rule-classes :definition)
Function:
(defun smtlink-hint-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint-p)) (declare (ignorable acl2::__function__)) (and (mbe :logic (and (alistp x) (equal (strip-cars x) '(functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :exec (fty::alist-with-carsp x '(functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) (b* ((functions (cdr (std::da-nth 0 x))) (hypotheses (cdr (std::da-nth 1 x))) (main-hint (cdr (std::da-nth 2 x))) (let-binding (cdr (std::da-nth 3 x))) (symbols (cdr (std::da-nth 4 x))) (abs (cdr (std::da-nth 5 x))) (fty (cdr (std::da-nth 6 x))) (fty-info (cdr (std::da-nth 7 x))) (fty-types (cdr (std::da-nth 8 x))) (int-to-rat (cdr (std::da-nth 9 x))) (smt-dir (cdr (std::da-nth 10 x))) (rm-file (cdr (std::da-nth 11 x))) (smt-fname (cdr (std::da-nth 12 x))) (smt-params (cdr (std::da-nth 13 x))) (fast-functions (cdr (std::da-nth 14 x))) (type-decl-list (cdr (std::da-nth 15 x))) (expanded-clause-w/-hint (cdr (std::da-nth 16 x))) (expanded-g/type (cdr (std::da-nth 17 x))) (smt-cnf (cdr (std::da-nth 18 x))) (wrld-fn-len (cdr (std::da-nth 19 x))) (custom-p (cdr (std::da-nth 20 x)))) (and (func-listp functions) (hint-pair-listp hypotheses) (true-listp main-hint) (let-binding-p let-binding) (symbol-listp symbols) (symbol-listp abs) (symbol-listp fty) (fty-info-alist-p fty-info) (fty-types-p fty-types) (booleanp int-to-rat) (stringp smt-dir) (booleanp rm-file) (stringp smt-fname) (true-listp smt-params) (func-alistp fast-functions) (pseudo-termp type-decl-list) (hint-pair-p expanded-clause-w/-hint) (pseudo-termp expanded-g/type) (smtlink-config-p smt-cnf) (natp wrld-fn-len) (booleanp custom-p))))))
Theorem:
(defthm consp-when-smtlink-hint-p (implies (smtlink-hint-p x) (consp x)) :rule-classes :compound-recognizer)
Function:
(defun smtlink-hint-fix$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (let ((acl2::__function__ 'smtlink-hint-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((functions (func-list-fix (cdr (std::da-nth 0 x)))) (hypotheses (hint-pair-list-fix (cdr (std::da-nth 1 x)))) (main-hint (true-list-fix (cdr (std::da-nth 2 x)))) (let-binding (let-binding-fix (cdr (std::da-nth 3 x)))) (symbols (symbol-list-fix (cdr (std::da-nth 4 x)))) (abs (symbol-list-fix (cdr (std::da-nth 5 x)))) (fty (symbol-list-fix (cdr (std::da-nth 6 x)))) (fty-info (fty-info-alist-fix (cdr (std::da-nth 7 x)))) (fty-types (fty-types-fix (cdr (std::da-nth 8 x)))) (int-to-rat (acl2::bool-fix (cdr (std::da-nth 9 x)))) (smt-dir (str-fix (cdr (std::da-nth 10 x)))) (rm-file (acl2::bool-fix (cdr (std::da-nth 11 x)))) (smt-fname (str-fix (cdr (std::da-nth 12 x)))) (smt-params (true-list-fix (cdr (std::da-nth 13 x)))) (fast-functions (func-alist-fix (cdr (std::da-nth 14 x)))) (type-decl-list (pseudo-term-fix (cdr (std::da-nth 15 x)))) (expanded-clause-w/-hint (hint-pair-fix (cdr (std::da-nth 16 x)))) (expanded-g/type (pseudo-term-fix (cdr (std::da-nth 17 x)))) (smt-cnf (smtlink-config-fix (cdr (std::da-nth 18 x)))) (wrld-fn-len (nfix (cdr (std::da-nth 19 x)))) (custom-p (acl2::bool-fix (cdr (std::da-nth 20 x))))) (list (cons 'functions functions) (cons 'hypotheses hypotheses) (cons 'main-hint main-hint) (cons 'let-binding let-binding) (cons 'symbols symbols) (cons 'abs abs) (cons 'fty fty) (cons 'fty-info fty-info) (cons 'fty-types fty-types) (cons 'int-to-rat int-to-rat) (cons 'smt-dir smt-dir) (cons 'rm-file rm-file) (cons 'smt-fname smt-fname) (cons 'smt-params smt-params) (cons 'fast-functions fast-functions) (cons 'type-decl-list type-decl-list) (cons 'expanded-clause-w/-hint expanded-clause-w/-hint) (cons 'expanded-g/type expanded-g/type) (cons 'smt-cnf smt-cnf) (cons 'wrld-fn-len wrld-fn-len) (cons 'custom-p custom-p))) :exec x)))
Theorem:
(defthm smtlink-hint-p-of-smtlink-hint-fix (b* ((new-x (smtlink-hint-fix$inline x))) (smtlink-hint-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint-fix-when-smtlink-hint-p (implies (smtlink-hint-p x) (equal (smtlink-hint-fix x) x)))
Function:
(defun smtlink-hint-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (smtlink-hint-p acl2::x) (smtlink-hint-p acl2::y)))) (equal (smtlink-hint-fix acl2::x) (smtlink-hint-fix acl2::y)))
Theorem:
(defthm smtlink-hint-equiv-is-an-equivalence (and (booleanp (smtlink-hint-equiv x y)) (smtlink-hint-equiv x x) (implies (smtlink-hint-equiv x y) (smtlink-hint-equiv y x)) (implies (and (smtlink-hint-equiv x y) (smtlink-hint-equiv y z)) (smtlink-hint-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm smtlink-hint-equiv-implies-equal-smtlink-hint-fix-1 (implies (smtlink-hint-equiv acl2::x x-equiv) (equal (smtlink-hint-fix acl2::x) (smtlink-hint-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm smtlink-hint-fix-under-smtlink-hint-equiv (smtlink-hint-equiv (smtlink-hint-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-smtlink-hint-fix-1-forward-to-smtlink-hint-equiv (implies (equal (smtlink-hint-fix acl2::x) acl2::y) (smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-smtlink-hint-fix-2-forward-to-smtlink-hint-equiv (implies (equal acl2::x (smtlink-hint-fix acl2::y)) (smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm smtlink-hint-equiv-of-smtlink-hint-fix-1-forward (implies (smtlink-hint-equiv (smtlink-hint-fix acl2::x) acl2::y) (smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm smtlink-hint-equiv-of-smtlink-hint-fix-2-forward (implies (smtlink-hint-equiv acl2::x (smtlink-hint-fix acl2::y)) (smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Function:
(defun smtlink-hint->functions$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->functions)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (func-list-fix (cdr (std::da-nth 0 x)))) :exec (cdr (std::da-nth 0 x)))))
Theorem:
(defthm func-listp-of-smtlink-hint->functions (b* ((functions (smtlink-hint->functions$inline x))) (func-listp functions)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->functions$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->functions$inline (smtlink-hint-fix x)) (smtlink-hint->functions$inline x)))
Theorem:
(defthm smtlink-hint->functions$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->functions$inline x) (smtlink-hint->functions$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->hypotheses$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->hypotheses)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (hint-pair-list-fix (cdr (std::da-nth 1 x)))) :exec (cdr (std::da-nth 1 x)))))
Theorem:
(defthm hint-pair-listp-of-smtlink-hint->hypotheses (b* ((hypotheses (smtlink-hint->hypotheses$inline x))) (hint-pair-listp hypotheses)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->hypotheses$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->hypotheses$inline (smtlink-hint-fix x)) (smtlink-hint->hypotheses$inline x)))
Theorem:
(defthm smtlink-hint->hypotheses$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->hypotheses$inline x) (smtlink-hint->hypotheses$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->main-hint$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->main-hint)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (true-list-fix (cdr (std::da-nth 2 x)))) :exec (cdr (std::da-nth 2 x)))))
Theorem:
(defthm true-listp-of-smtlink-hint->main-hint (b* ((main-hint (smtlink-hint->main-hint$inline x))) (true-listp main-hint)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->main-hint$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->main-hint$inline (smtlink-hint-fix x)) (smtlink-hint->main-hint$inline x)))
Theorem:
(defthm smtlink-hint->main-hint$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->main-hint$inline x) (smtlink-hint->main-hint$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->let-binding$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->let-binding)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (let-binding-fix (cdr (std::da-nth 3 x)))) :exec (cdr (std::da-nth 3 x)))))
Theorem:
(defthm let-binding-p-of-smtlink-hint->let-binding (b* ((let-binding (smtlink-hint->let-binding$inline x))) (let-binding-p let-binding)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->let-binding$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->let-binding$inline (smtlink-hint-fix x)) (smtlink-hint->let-binding$inline x)))
Theorem:
(defthm smtlink-hint->let-binding$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->let-binding$inline x) (smtlink-hint->let-binding$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->symbols$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->symbols)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-list-fix (cdr (std::da-nth 4 x)))) :exec (cdr (std::da-nth 4 x)))))
Theorem:
(defthm symbol-listp-of-smtlink-hint->symbols (b* ((symbols (smtlink-hint->symbols$inline x))) (symbol-listp symbols)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->symbols$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->symbols$inline (smtlink-hint-fix x)) (smtlink-hint->symbols$inline x)))
Theorem:
(defthm smtlink-hint->symbols$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->symbols$inline x) (smtlink-hint->symbols$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->abs$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->abs)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-list-fix (cdr (std::da-nth 5 x)))) :exec (cdr (std::da-nth 5 x)))))
Theorem:
(defthm symbol-listp-of-smtlink-hint->abs (b* ((abs (smtlink-hint->abs$inline x))) (symbol-listp abs)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->abs$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->abs$inline (smtlink-hint-fix x)) (smtlink-hint->abs$inline x)))
Theorem:
(defthm smtlink-hint->abs$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->abs$inline x) (smtlink-hint->abs$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->fty$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->fty)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (symbol-list-fix (cdr (std::da-nth 6 x)))) :exec (cdr (std::da-nth 6 x)))))
Theorem:
(defthm symbol-listp-of-smtlink-hint->fty (b* ((fty (smtlink-hint->fty$inline x))) (symbol-listp fty)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->fty$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->fty$inline (smtlink-hint-fix x)) (smtlink-hint->fty$inline x)))
Theorem:
(defthm smtlink-hint->fty$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->fty$inline x) (smtlink-hint->fty$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->fty-info$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->fty-info)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (fty-info-alist-fix (cdr (std::da-nth 7 x)))) :exec (cdr (std::da-nth 7 x)))))
Theorem:
(defthm fty-info-alist-p-of-smtlink-hint->fty-info (b* ((fty-info (smtlink-hint->fty-info$inline x))) (fty-info-alist-p fty-info)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->fty-info$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->fty-info$inline (smtlink-hint-fix x)) (smtlink-hint->fty-info$inline x)))
Theorem:
(defthm smtlink-hint->fty-info$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->fty-info$inline x) (smtlink-hint->fty-info$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->fty-types$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->fty-types)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (fty-types-fix (cdr (std::da-nth 8 x)))) :exec (cdr (std::da-nth 8 x)))))
Theorem:
(defthm fty-types-p-of-smtlink-hint->fty-types (b* ((fty-types (smtlink-hint->fty-types$inline x))) (fty-types-p fty-types)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->fty-types$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->fty-types$inline (smtlink-hint-fix x)) (smtlink-hint->fty-types$inline x)))
Theorem:
(defthm smtlink-hint->fty-types$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->fty-types$inline x) (smtlink-hint->fty-types$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->int-to-rat$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->int-to-rat)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (acl2::bool-fix (cdr (std::da-nth 9 x)))) :exec (cdr (std::da-nth 9 x)))))
Theorem:
(defthm booleanp-of-smtlink-hint->int-to-rat (b* ((int-to-rat (smtlink-hint->int-to-rat$inline x))) (booleanp int-to-rat)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->int-to-rat$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->int-to-rat$inline (smtlink-hint-fix x)) (smtlink-hint->int-to-rat$inline x)))
Theorem:
(defthm smtlink-hint->int-to-rat$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->int-to-rat$inline x) (smtlink-hint->int-to-rat$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->smt-dir$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->smt-dir)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (str-fix (cdr (std::da-nth 10 x)))) :exec (cdr (std::da-nth 10 x)))))
Theorem:
(defthm stringp-of-smtlink-hint->smt-dir (b* ((smt-dir (smtlink-hint->smt-dir$inline x))) (stringp smt-dir)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->smt-dir$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->smt-dir$inline (smtlink-hint-fix x)) (smtlink-hint->smt-dir$inline x)))
Theorem:
(defthm smtlink-hint->smt-dir$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->smt-dir$inline x) (smtlink-hint->smt-dir$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->rm-file$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->rm-file)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (acl2::bool-fix (cdr (std::da-nth 11 x)))) :exec (cdr (std::da-nth 11 x)))))
Theorem:
(defthm booleanp-of-smtlink-hint->rm-file (b* ((rm-file (smtlink-hint->rm-file$inline x))) (booleanp rm-file)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->rm-file$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->rm-file$inline (smtlink-hint-fix x)) (smtlink-hint->rm-file$inline x)))
Theorem:
(defthm smtlink-hint->rm-file$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->rm-file$inline x) (smtlink-hint->rm-file$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->smt-fname$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->smt-fname)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (str-fix (cdr (std::da-nth 12 x)))) :exec (cdr (std::da-nth 12 x)))))
Theorem:
(defthm stringp-of-smtlink-hint->smt-fname (b* ((smt-fname (smtlink-hint->smt-fname$inline x))) (stringp smt-fname)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->smt-fname$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->smt-fname$inline (smtlink-hint-fix x)) (smtlink-hint->smt-fname$inline x)))
Theorem:
(defthm smtlink-hint->smt-fname$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->smt-fname$inline x) (smtlink-hint->smt-fname$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->smt-params$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->smt-params)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (true-list-fix (cdr (std::da-nth 13 x)))) :exec (cdr (std::da-nth 13 x)))))
Theorem:
(defthm true-listp-of-smtlink-hint->smt-params (b* ((smt-params (smtlink-hint->smt-params$inline x))) (true-listp smt-params)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->smt-params$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->smt-params$inline (smtlink-hint-fix x)) (smtlink-hint->smt-params$inline x)))
Theorem:
(defthm smtlink-hint->smt-params$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->smt-params$inline x) (smtlink-hint->smt-params$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->fast-functions$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->fast-functions)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (func-alist-fix (cdr (std::da-nth 14 x)))) :exec (cdr (std::da-nth 14 x)))))
Theorem:
(defthm func-alistp-of-smtlink-hint->fast-functions (b* ((fast-functions (smtlink-hint->fast-functions$inline x))) (func-alistp fast-functions)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->fast-functions$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->fast-functions$inline (smtlink-hint-fix x)) (smtlink-hint->fast-functions$inline x)))
Theorem:
(defthm smtlink-hint->fast-functions$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->fast-functions$inline x) (smtlink-hint->fast-functions$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->type-decl-list$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->type-decl-list)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (pseudo-term-fix (cdr (std::da-nth 15 x)))) :exec (cdr (std::da-nth 15 x)))))
Theorem:
(defthm pseudo-termp-of-smtlink-hint->type-decl-list (b* ((type-decl-list (smtlink-hint->type-decl-list$inline x))) (pseudo-termp type-decl-list)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->type-decl-list$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->type-decl-list$inline (smtlink-hint-fix x)) (smtlink-hint->type-decl-list$inline x)))
Theorem:
(defthm smtlink-hint->type-decl-list$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->type-decl-list$inline x) (smtlink-hint->type-decl-list$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->expanded-clause-w/-hint$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->expanded-clause-w/-hint)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (hint-pair-fix (cdr (std::da-nth 16 x)))) :exec (cdr (std::da-nth 16 x)))))
Theorem:
(defthm hint-pair-p-of-smtlink-hint->expanded-clause-w/-hint (b* ((expanded-clause-w/-hint (smtlink-hint->expanded-clause-w/-hint$inline x))) (hint-pair-p expanded-clause-w/-hint)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->expanded-clause-w/-hint$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->expanded-clause-w/-hint$inline (smtlink-hint-fix x)) (smtlink-hint->expanded-clause-w/-hint$inline x)))
Theorem:
(defthm smtlink-hint->expanded-clause-w/-hint$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->expanded-clause-w/-hint$inline x) (smtlink-hint->expanded-clause-w/-hint$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->expanded-g/type$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->expanded-g/type)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (pseudo-term-fix (cdr (std::da-nth 17 x)))) :exec (cdr (std::da-nth 17 x)))))
Theorem:
(defthm pseudo-termp-of-smtlink-hint->expanded-g/type (b* ((expanded-g/type (smtlink-hint->expanded-g/type$inline x))) (pseudo-termp expanded-g/type)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->expanded-g/type$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->expanded-g/type$inline (smtlink-hint-fix x)) (smtlink-hint->expanded-g/type$inline x)))
Theorem:
(defthm smtlink-hint->expanded-g/type$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->expanded-g/type$inline x) (smtlink-hint->expanded-g/type$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->smt-cnf$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->smt-cnf)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (smtlink-config-fix (cdr (std::da-nth 18 x)))) :exec (cdr (std::da-nth 18 x)))))
Theorem:
(defthm smtlink-config-p-of-smtlink-hint->smt-cnf (b* ((smt-cnf (smtlink-hint->smt-cnf$inline x))) (smtlink-config-p smt-cnf)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->smt-cnf$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->smt-cnf$inline (smtlink-hint-fix x)) (smtlink-hint->smt-cnf$inline x)))
Theorem:
(defthm smtlink-hint->smt-cnf$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->smt-cnf$inline x) (smtlink-hint->smt-cnf$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->wrld-fn-len$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->wrld-fn-len)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (nfix (cdr (std::da-nth 19 x)))) :exec (cdr (std::da-nth 19 x)))))
Theorem:
(defthm natp-of-smtlink-hint->wrld-fn-len (b* ((wrld-fn-len (smtlink-hint->wrld-fn-len$inline x))) (natp wrld-fn-len)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->wrld-fn-len$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->wrld-fn-len$inline (smtlink-hint-fix x)) (smtlink-hint->wrld-fn-len$inline x)))
Theorem:
(defthm smtlink-hint->wrld-fn-len$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->wrld-fn-len$inline x) (smtlink-hint->wrld-fn-len$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint->custom-p$inline (x) (declare (xargs :guard (smtlink-hint-p x))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint->custom-p)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and t x))) (acl2::bool-fix (cdr (std::da-nth 20 x)))) :exec (cdr (std::da-nth 20 x)))))
Theorem:
(defthm booleanp-of-smtlink-hint->custom-p (b* ((custom-p (smtlink-hint->custom-p$inline x))) (booleanp custom-p)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->custom-p$inline-of-smtlink-hint-fix-x (equal (smtlink-hint->custom-p$inline (smtlink-hint-fix x)) (smtlink-hint->custom-p$inline x)))
Theorem:
(defthm smtlink-hint->custom-p$inline-smtlink-hint-equiv-congruence-on-x (implies (smtlink-hint-equiv x x-equiv) (equal (smtlink-hint->custom-p$inline x) (smtlink-hint->custom-p$inline x-equiv))) :rule-classes :congruence)
Function:
(defun smtlink-hint (functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (declare (xargs :guard (and (func-listp functions) (hint-pair-listp hypotheses) (true-listp main-hint) (let-binding-p let-binding) (symbol-listp symbols) (symbol-listp abs) (symbol-listp fty) (fty-info-alist-p fty-info) (fty-types-p fty-types) (booleanp int-to-rat) (stringp smt-dir) (booleanp rm-file) (stringp smt-fname) (true-listp smt-params) (func-alistp fast-functions) (pseudo-termp type-decl-list) (hint-pair-p expanded-clause-w/-hint) (pseudo-termp expanded-g/type) (smtlink-config-p smt-cnf) (natp wrld-fn-len) (booleanp custom-p)))) (declare (xargs :guard t)) (let ((acl2::__function__ 'smtlink-hint)) (declare (ignorable acl2::__function__)) (b* ((functions (mbe :logic (func-list-fix functions) :exec functions)) (hypotheses (mbe :logic (hint-pair-list-fix hypotheses) :exec hypotheses)) (main-hint (mbe :logic (true-list-fix main-hint) :exec main-hint)) (let-binding (mbe :logic (let-binding-fix let-binding) :exec let-binding)) (symbols (mbe :logic (symbol-list-fix symbols) :exec symbols)) (abs (mbe :logic (symbol-list-fix abs) :exec abs)) (fty (mbe :logic (symbol-list-fix fty) :exec fty)) (fty-info (mbe :logic (fty-info-alist-fix fty-info) :exec fty-info)) (fty-types (mbe :logic (fty-types-fix fty-types) :exec fty-types)) (int-to-rat (mbe :logic (acl2::bool-fix int-to-rat) :exec int-to-rat)) (smt-dir (mbe :logic (str-fix smt-dir) :exec smt-dir)) (rm-file (mbe :logic (acl2::bool-fix rm-file) :exec rm-file)) (smt-fname (mbe :logic (str-fix smt-fname) :exec smt-fname)) (smt-params (mbe :logic (true-list-fix smt-params) :exec smt-params)) (fast-functions (mbe :logic (func-alist-fix fast-functions) :exec fast-functions)) (type-decl-list (mbe :logic (pseudo-term-fix type-decl-list) :exec type-decl-list)) (expanded-clause-w/-hint (mbe :logic (hint-pair-fix expanded-clause-w/-hint) :exec expanded-clause-w/-hint)) (expanded-g/type (mbe :logic (pseudo-term-fix expanded-g/type) :exec expanded-g/type)) (smt-cnf (mbe :logic (smtlink-config-fix smt-cnf) :exec smt-cnf)) (wrld-fn-len (mbe :logic (nfix wrld-fn-len) :exec wrld-fn-len)) (custom-p (mbe :logic (acl2::bool-fix custom-p) :exec custom-p))) (list (cons 'functions functions) (cons 'hypotheses hypotheses) (cons 'main-hint main-hint) (cons 'let-binding let-binding) (cons 'symbols symbols) (cons 'abs abs) (cons 'fty fty) (cons 'fty-info fty-info) (cons 'fty-types fty-types) (cons 'int-to-rat int-to-rat) (cons 'smt-dir smt-dir) (cons 'rm-file rm-file) (cons 'smt-fname smt-fname) (cons 'smt-params smt-params) (cons 'fast-functions fast-functions) (cons 'type-decl-list type-decl-list) (cons 'expanded-clause-w/-hint expanded-clause-w/-hint) (cons 'expanded-g/type expanded-g/type) (cons 'smt-cnf smt-cnf) (cons 'wrld-fn-len wrld-fn-len) (cons 'custom-p custom-p)))))
Theorem:
(defthm smtlink-hint-p-of-smtlink-hint (b* ((x (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) (smtlink-hint-p x)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-hint->functions-of-smtlink-hint (equal (smtlink-hint->functions (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (func-list-fix functions)))
Theorem:
(defthm smtlink-hint->hypotheses-of-smtlink-hint (equal (smtlink-hint->hypotheses (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (hint-pair-list-fix hypotheses)))
Theorem:
(defthm smtlink-hint->main-hint-of-smtlink-hint (equal (smtlink-hint->main-hint (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (true-list-fix main-hint)))
Theorem:
(defthm smtlink-hint->let-binding-of-smtlink-hint (equal (smtlink-hint->let-binding (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (let-binding-fix let-binding)))
Theorem:
(defthm smtlink-hint->symbols-of-smtlink-hint (equal (smtlink-hint->symbols (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (symbol-list-fix symbols)))
Theorem:
(defthm smtlink-hint->abs-of-smtlink-hint (equal (smtlink-hint->abs (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (symbol-list-fix abs)))
Theorem:
(defthm smtlink-hint->fty-of-smtlink-hint (equal (smtlink-hint->fty (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (symbol-list-fix fty)))
Theorem:
(defthm smtlink-hint->fty-info-of-smtlink-hint (equal (smtlink-hint->fty-info (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (fty-info-alist-fix fty-info)))
Theorem:
(defthm smtlink-hint->fty-types-of-smtlink-hint (equal (smtlink-hint->fty-types (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (fty-types-fix fty-types)))
Theorem:
(defthm smtlink-hint->int-to-rat-of-smtlink-hint (equal (smtlink-hint->int-to-rat (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (acl2::bool-fix int-to-rat)))
Theorem:
(defthm smtlink-hint->smt-dir-of-smtlink-hint (equal (smtlink-hint->smt-dir (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (str-fix smt-dir)))
Theorem:
(defthm smtlink-hint->rm-file-of-smtlink-hint (equal (smtlink-hint->rm-file (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (acl2::bool-fix rm-file)))
Theorem:
(defthm smtlink-hint->smt-fname-of-smtlink-hint (equal (smtlink-hint->smt-fname (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (str-fix smt-fname)))
Theorem:
(defthm smtlink-hint->smt-params-of-smtlink-hint (equal (smtlink-hint->smt-params (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (true-list-fix smt-params)))
Theorem:
(defthm smtlink-hint->fast-functions-of-smtlink-hint (equal (smtlink-hint->fast-functions (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (func-alist-fix fast-functions)))
Theorem:
(defthm smtlink-hint->type-decl-list-of-smtlink-hint (equal (smtlink-hint->type-decl-list (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (pseudo-term-fix type-decl-list)))
Theorem:
(defthm smtlink-hint->expanded-clause-w/-hint-of-smtlink-hint (equal (smtlink-hint->expanded-clause-w/-hint (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (hint-pair-fix expanded-clause-w/-hint)))
Theorem:
(defthm smtlink-hint->expanded-g/type-of-smtlink-hint (equal (smtlink-hint->expanded-g/type (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (pseudo-term-fix expanded-g/type)))
Theorem:
(defthm smtlink-hint->smt-cnf-of-smtlink-hint (equal (smtlink-hint->smt-cnf (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (smtlink-config-fix smt-cnf)))
Theorem:
(defthm smtlink-hint->wrld-fn-len-of-smtlink-hint (equal (smtlink-hint->wrld-fn-len (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (nfix wrld-fn-len)))
Theorem:
(defthm smtlink-hint->custom-p-of-smtlink-hint (equal (smtlink-hint->custom-p (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)) (acl2::bool-fix custom-p)))
Theorem:
(defthm smtlink-hint-of-fields (equal (smtlink-hint (smtlink-hint->functions x) (smtlink-hint->hypotheses x) (smtlink-hint->main-hint x) (smtlink-hint->let-binding x) (smtlink-hint->symbols x) (smtlink-hint->abs x) (smtlink-hint->fty x) (smtlink-hint->fty-info x) (smtlink-hint->fty-types x) (smtlink-hint->int-to-rat x) (smtlink-hint->smt-dir x) (smtlink-hint->rm-file x) (smtlink-hint->smt-fname x) (smtlink-hint->smt-params x) (smtlink-hint->fast-functions x) (smtlink-hint->type-decl-list x) (smtlink-hint->expanded-clause-w/-hint x) (smtlink-hint->expanded-g/type x) (smtlink-hint->smt-cnf x) (smtlink-hint->wrld-fn-len x) (smtlink-hint->custom-p x)) (smtlink-hint-fix x)))
Theorem:
(defthm smtlink-hint-fix-when-smtlink-hint (equal (smtlink-hint-fix x) (smtlink-hint (smtlink-hint->functions x) (smtlink-hint->hypotheses x) (smtlink-hint->main-hint x) (smtlink-hint->let-binding x) (smtlink-hint->symbols x) (smtlink-hint->abs x) (smtlink-hint->fty x) (smtlink-hint->fty-info x) (smtlink-hint->fty-types x) (smtlink-hint->int-to-rat x) (smtlink-hint->smt-dir x) (smtlink-hint->rm-file x) (smtlink-hint->smt-fname x) (smtlink-hint->smt-params x) (smtlink-hint->fast-functions x) (smtlink-hint->type-decl-list x) (smtlink-hint->expanded-clause-w/-hint x) (smtlink-hint->expanded-g/type x) (smtlink-hint->smt-cnf x) (smtlink-hint->wrld-fn-len x) (smtlink-hint->custom-p x))))
Theorem:
(defthm equal-of-smtlink-hint (equal (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) x) (and (smtlink-hint-p x) (equal (smtlink-hint->functions x) (func-list-fix functions)) (equal (smtlink-hint->hypotheses x) (hint-pair-list-fix hypotheses)) (equal (smtlink-hint->main-hint x) (true-list-fix main-hint)) (equal (smtlink-hint->let-binding x) (let-binding-fix let-binding)) (equal (smtlink-hint->symbols x) (symbol-list-fix symbols)) (equal (smtlink-hint->abs x) (symbol-list-fix abs)) (equal (smtlink-hint->fty x) (symbol-list-fix fty)) (equal (smtlink-hint->fty-info x) (fty-info-alist-fix fty-info)) (equal (smtlink-hint->fty-types x) (fty-types-fix fty-types)) (equal (smtlink-hint->int-to-rat x) (acl2::bool-fix int-to-rat)) (equal (smtlink-hint->smt-dir x) (str-fix smt-dir)) (equal (smtlink-hint->rm-file x) (acl2::bool-fix rm-file)) (equal (smtlink-hint->smt-fname x) (str-fix smt-fname)) (equal (smtlink-hint->smt-params x) (true-list-fix smt-params)) (equal (smtlink-hint->fast-functions x) (func-alist-fix fast-functions)) (equal (smtlink-hint->type-decl-list x) (pseudo-term-fix type-decl-list)) (equal (smtlink-hint->expanded-clause-w/-hint x) (hint-pair-fix expanded-clause-w/-hint)) (equal (smtlink-hint->expanded-g/type x) (pseudo-term-fix expanded-g/type)) (equal (smtlink-hint->smt-cnf x) (smtlink-config-fix smt-cnf)) (equal (smtlink-hint->wrld-fn-len x) (nfix wrld-fn-len)) (equal (smtlink-hint->custom-p x) (acl2::bool-fix custom-p)))))
Theorem:
(defthm smtlink-hint-of-func-list-fix-functions (equal (smtlink-hint (func-list-fix functions) hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-func-list-equiv-congruence-on-functions (implies (func-list-equiv functions functions-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions-equiv hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-hint-pair-list-fix-hypotheses (equal (smtlink-hint functions (hint-pair-list-fix hypotheses) main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-hint-pair-list-equiv-congruence-on-hypotheses (implies (hint-pair-list-equiv hypotheses hypotheses-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses-equiv main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-true-list-fix-main-hint (equal (smtlink-hint functions hypotheses (true-list-fix main-hint) let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-true-list-equiv-congruence-on-main-hint (implies (true-list-equiv main-hint main-hint-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint-equiv let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-let-binding-fix-let-binding (equal (smtlink-hint functions hypotheses main-hint (let-binding-fix let-binding) symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-let-binding-equiv-congruence-on-let-binding (implies (let-binding-equiv let-binding let-binding-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding-equiv symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-symbol-list-fix-symbols (equal (smtlink-hint functions hypotheses main-hint let-binding (symbol-list-fix symbols) abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-symbol-list-equiv-congruence-on-symbols (implies (acl2::symbol-list-equiv symbols symbols-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols-equiv abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-symbol-list-fix-abs (equal (smtlink-hint functions hypotheses main-hint let-binding symbols (symbol-list-fix abs) fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-symbol-list-equiv-congruence-on-abs (implies (acl2::symbol-list-equiv abs abs-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs-equiv fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-symbol-list-fix-fty (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs (symbol-list-fix fty) fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-symbol-list-equiv-congruence-on-fty (implies (acl2::symbol-list-equiv fty fty-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty-equiv fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-fty-info-alist-fix-fty-info (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty (fty-info-alist-fix fty-info) fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-fty-info-alist-equiv-congruence-on-fty-info (implies (fty-info-alist-equiv fty-info fty-info-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info-equiv fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-fty-types-fix-fty-types (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info (fty-types-fix fty-types) int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-fty-types-equiv-congruence-on-fty-types (implies (fty-types-equiv fty-types fty-types-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types-equiv int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-bool-fix-int-to-rat (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types (acl2::bool-fix int-to-rat) smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-iff-congruence-on-int-to-rat (implies (iff int-to-rat int-to-rat-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat-equiv smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-str-fix-smt-dir (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat (str-fix smt-dir) rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-streqv-congruence-on-smt-dir (implies (acl2::streqv smt-dir smt-dir-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir-equiv rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-bool-fix-rm-file (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir (acl2::bool-fix rm-file) smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-iff-congruence-on-rm-file (implies (iff rm-file rm-file-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file-equiv smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-str-fix-smt-fname (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file (str-fix smt-fname) smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-streqv-congruence-on-smt-fname (implies (acl2::streqv smt-fname smt-fname-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname-equiv smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-true-list-fix-smt-params (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname (true-list-fix smt-params) fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-true-list-equiv-congruence-on-smt-params (implies (true-list-equiv smt-params smt-params-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params-equiv fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-func-alist-fix-fast-functions (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params (func-alist-fix fast-functions) type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-func-alist-equiv-congruence-on-fast-functions (implies (func-alist-equiv fast-functions fast-functions-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions-equiv type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-pseudo-term-fix-type-decl-list (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions (pseudo-term-fix type-decl-list) expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-pseudo-term-equiv-congruence-on-type-decl-list (implies (pseudo-term-equiv type-decl-list type-decl-list-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list-equiv expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-hint-pair-fix-expanded-clause-w/-hint (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list (hint-pair-fix expanded-clause-w/-hint) expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-hint-pair-equiv-congruence-on-expanded-clause-w/-hint (implies (hint-pair-equiv expanded-clause-w/-hint expanded-clause-w/-hint-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint-equiv expanded-g/type smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-pseudo-term-fix-expanded-g/type (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint (pseudo-term-fix expanded-g/type) smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-pseudo-term-equiv-congruence-on-expanded-g/type (implies (pseudo-term-equiv expanded-g/type expanded-g/type-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type-equiv smt-cnf wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-smtlink-config-fix-smt-cnf (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type (smtlink-config-fix smt-cnf) wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-smtlink-config-equiv-congruence-on-smt-cnf (implies (smtlink-config-equiv smt-cnf smt-cnf-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf-equiv wrld-fn-len custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-nfix-wrld-fn-len (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf (nfix wrld-fn-len) custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-nat-equiv-congruence-on-wrld-fn-len (implies (acl2::nat-equiv wrld-fn-len wrld-fn-len-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len-equiv custom-p))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-of-bool-fix-custom-p (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len (acl2::bool-fix custom-p)) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p)))
Theorem:
(defthm smtlink-hint-iff-congruence-on-custom-p (implies (iff custom-p custom-p-equiv) (equal (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p) (smtlink-hint functions hypotheses main-hint let-binding symbols abs fty fty-info fty-types int-to-rat smt-dir rm-file smt-fname smt-params fast-functions type-decl-list expanded-clause-w/-hint expanded-g/type smt-cnf wrld-fn-len custom-p-equiv))) :rule-classes :congruence)
Theorem:
(defthm smtlink-hint-fix-redef (equal (smtlink-hint-fix x) (smtlink-hint (smtlink-hint->functions x) (smtlink-hint->hypotheses x) (smtlink-hint->main-hint x) (smtlink-hint->let-binding x) (smtlink-hint->symbols x) (smtlink-hint->abs x) (smtlink-hint->fty x) (smtlink-hint->fty-info x) (smtlink-hint->fty-types x) (smtlink-hint->int-to-rat x) (smtlink-hint->smt-dir x) (smtlink-hint->rm-file x) (smtlink-hint->smt-fname x) (smtlink-hint->smt-params x) (smtlink-hint->fast-functions x) (smtlink-hint->type-decl-list x) (smtlink-hint->expanded-clause-w/-hint x) (smtlink-hint->expanded-g/type x) (smtlink-hint->smt-cnf x) (smtlink-hint->wrld-fn-len x) (smtlink-hint->custom-p x))) :rule-classes :definition)
Function:
(defun maybe-smtlink-hint-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'maybe-smtlink-hint-p)) (declare (ignorable acl2::__function__)) (cond ((not x) (b* nil t)) (t (b* ((fty::val x)) (smtlink-hint-p fty::val))))))
Theorem:
(defthm maybe-smtlink-hint-p-when-smtlink-hint-p (implies (smtlink-hint-p x) (maybe-smtlink-hint-p x)))
Theorem:
(defthm smtlink-hint-p-when-maybe-smtlink-hint-p (implies (and (maybe-smtlink-hint-p x) (double-rewrite x)) (smtlink-hint-p x)))
Function:
(defun maybe-smtlink-hint-fix$inline (x) (declare (xargs :guard (maybe-smtlink-hint-p x))) (let ((acl2::__function__ 'maybe-smtlink-hint-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (cond ((not x) nil) (t (b* ((fty::val (smtlink-hint-fix x))) fty::val))) :exec x)))
Theorem:
(defthm maybe-smtlink-hint-p-of-maybe-smtlink-hint-fix (b* ((new-x (maybe-smtlink-hint-fix$inline x))) (maybe-smtlink-hint-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm maybe-smtlink-hint-fix-when-maybe-smtlink-hint-p (implies (maybe-smtlink-hint-p x) (equal (maybe-smtlink-hint-fix x) x)))
Function:
(defun maybe-smtlink-hint-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (maybe-smtlink-hint-p acl2::x) (maybe-smtlink-hint-p acl2::y)))) (equal (maybe-smtlink-hint-fix acl2::x) (maybe-smtlink-hint-fix acl2::y)))
Theorem:
(defthm maybe-smtlink-hint-equiv-is-an-equivalence (and (booleanp (maybe-smtlink-hint-equiv x y)) (maybe-smtlink-hint-equiv x x) (implies (maybe-smtlink-hint-equiv x y) (maybe-smtlink-hint-equiv y x)) (implies (and (maybe-smtlink-hint-equiv x y) (maybe-smtlink-hint-equiv y z)) (maybe-smtlink-hint-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm maybe-smtlink-hint-equiv-implies-equal-maybe-smtlink-hint-fix-1 (implies (maybe-smtlink-hint-equiv acl2::x x-equiv) (equal (maybe-smtlink-hint-fix acl2::x) (maybe-smtlink-hint-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm maybe-smtlink-hint-fix-under-maybe-smtlink-hint-equiv (maybe-smtlink-hint-equiv (maybe-smtlink-hint-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-maybe-smtlink-hint-fix-1-forward-to-maybe-smtlink-hint-equiv (implies (equal (maybe-smtlink-hint-fix acl2::x) acl2::y) (maybe-smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-maybe-smtlink-hint-fix-2-forward-to-maybe-smtlink-hint-equiv (implies (equal acl2::x (maybe-smtlink-hint-fix acl2::y)) (maybe-smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm maybe-smtlink-hint-equiv-of-maybe-smtlink-hint-fix-1-forward (implies (maybe-smtlink-hint-equiv (maybe-smtlink-hint-fix acl2::x) acl2::y) (maybe-smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm maybe-smtlink-hint-equiv-of-maybe-smtlink-hint-fix-2-forward (implies (maybe-smtlink-hint-equiv acl2::x (maybe-smtlink-hint-fix acl2::y)) (maybe-smtlink-hint-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm maybe-smtlink-hint-fix-under-iff (iff (maybe-smtlink-hint-fix x) x))
Theorem:
(defthm maybe-smtlink-hint-equiv-refines-smtlink-hint-equiv (implies (maybe-smtlink-hint-equiv x y) (smtlink-hint-equiv x y)) :rule-classes (:refinement))
Function:
(defun maybe-smtlink-hint-none nil (declare (xargs :guard t)) (let ((acl2::__function__ 'maybe-smtlink-hint-none)) (declare (ignorable acl2::__function__)) nil))
Theorem:
(defthm return-type-of-maybe-smtlink-hint-none (b* ((x (maybe-smtlink-hint-none))) (and (maybe-smtlink-hint-p x) (not x))) :rule-classes :rewrite)
Theorem:
(defthm maybe-smtlink-hint-fix-when-none (implies (not x) (equal (maybe-smtlink-hint-fix x) (maybe-smtlink-hint-none))) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm equal-of-maybe-smtlink-hint-none (equal (equal (maybe-smtlink-hint-none) x) (and (maybe-smtlink-hint-p x) (not x))))
Function:
(defun maybe-smtlink-hint-some->val$inline (x) (declare (xargs :guard (maybe-smtlink-hint-p x))) (declare (xargs :guard x)) (let ((acl2::__function__ 'maybe-smtlink-hint-some->val)) (declare (ignorable acl2::__function__)) (mbe :logic (b* ((x (and x x))) (smtlink-hint-fix x)) :exec x)))
Theorem:
(defthm smtlink-hint-p-of-maybe-smtlink-hint-some->val (b* ((fty::val (maybe-smtlink-hint-some->val$inline x))) (smtlink-hint-p fty::val)) :rule-classes :rewrite)
Theorem:
(defthm maybe-smtlink-hint-some->val$inline-of-maybe-smtlink-hint-fix-x (equal (maybe-smtlink-hint-some->val$inline (maybe-smtlink-hint-fix x)) (maybe-smtlink-hint-some->val$inline x)))
Theorem:
(defthm maybe-smtlink-hint-some->val$inline-maybe-smtlink-hint-equiv-congruence-on-x (implies (maybe-smtlink-hint-equiv x x-equiv) (equal (maybe-smtlink-hint-some->val$inline x) (maybe-smtlink-hint-some->val$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm maybe-smtlink-hint-some->val-when-wrong-kind (implies (not x) (equal (maybe-smtlink-hint-some->val x) (smtlink-hint-fix nil))))
Function:
(defun maybe-smtlink-hint-some (fty::val) (declare (xargs :guard (smtlink-hint-p fty::val))) (declare (xargs :guard t)) (let ((acl2::__function__ 'maybe-smtlink-hint-some)) (declare (ignorable acl2::__function__)) (b* ((fty::val (mbe :logic (smtlink-hint-fix fty::val) :exec fty::val))) fty::val)))
Theorem:
(defthm return-type-of-maybe-smtlink-hint-some (b* ((x (maybe-smtlink-hint-some fty::val))) (and (maybe-smtlink-hint-p x) x)) :rule-classes :rewrite)
Theorem:
(defthm maybe-smtlink-hint-some->val-of-maybe-smtlink-hint-some (equal (maybe-smtlink-hint-some->val (maybe-smtlink-hint-some fty::val)) (smtlink-hint-fix fty::val)))
Theorem:
(defthm maybe-smtlink-hint-some-of-fields (implies x (equal (maybe-smtlink-hint-some (maybe-smtlink-hint-some->val x)) (maybe-smtlink-hint-fix x))))
Theorem:
(defthm maybe-smtlink-hint-fix-when-some (implies x (equal (maybe-smtlink-hint-fix x) (maybe-smtlink-hint-some (maybe-smtlink-hint-some->val x)))) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm equal-of-maybe-smtlink-hint-some (equal (equal (maybe-smtlink-hint-some fty::val) x) (and (maybe-smtlink-hint-p x) x (equal (maybe-smtlink-hint-some->val x) (smtlink-hint-fix fty::val)))))
Theorem:
(defthm maybe-smtlink-hint-some-of-smtlink-hint-fix-val (equal (maybe-smtlink-hint-some (smtlink-hint-fix fty::val)) (maybe-smtlink-hint-some fty::val)))
Theorem:
(defthm maybe-smtlink-hint-some-smtlink-hint-equiv-congruence-on-val (implies (smtlink-hint-equiv fty::val val-equiv) (equal (maybe-smtlink-hint-some fty::val) (maybe-smtlink-hint-some val-equiv))) :rule-classes :congruence)
Theorem:
(defthm maybe-smtlink-hint-fix-redef (equal (maybe-smtlink-hint-fix x) (cond ((not x) (maybe-smtlink-hint-none)) (t (maybe-smtlink-hint-some (maybe-smtlink-hint-some->val x))))) :rule-classes :definition)
Function:
(defun flatten-formals/returns (formal/return-lst) (declare (xargs :guard (decl-listp formal/return-lst))) (let ((acl2::__function__ 'flatten-formals/returns)) (declare (ignorable acl2::__function__)) (b* ((formal/return-lst (decl-list-fix formal/return-lst)) ((if (endp formal/return-lst)) nil) ((cons first rest) formal/return-lst) ((decl d) first)) (cons d.name (flatten-formals/returns rest)))))
Theorem:
(defthm symbol-listp-of-flatten-formals/returns (b* ((flattened-lst (flatten-formals/returns formal/return-lst))) (symbol-listp flattened-lst)) :rule-classes :rewrite)
Function:
(defun make-alist-fn-lst (fn-lst) (declare (xargs :guard (func-listp fn-lst))) (let ((acl2::__function__ 'make-alist-fn-lst)) (declare (ignorable acl2::__function__)) (b* ((fn-lst (func-list-fix fn-lst)) ((unless (consp fn-lst)) nil) ((cons first rest) fn-lst) ((func f) first) (new-f (change-func f :flattened-formals (flatten-formals/returns f.formals) :flattened-returns (flatten-formals/returns f.returns)))) (cons (cons f.name new-f) (make-alist-fn-lst rest)))))
Theorem:
(defthm func-alistp-of-make-alist-fn-lst (b* ((fast-fn-lst (make-alist-fn-lst fn-lst))) (func-alistp fast-fn-lst)) :rule-classes :rewrite)
Theorem:
(defthm smtlink-p-of-smt-hint (smtlink-hint-p (smt-hint)))
Function:
(defun default-smtlink-hint nil (declare (xargs :guard t)) (let ((acl2::__function__ 'default-smtlink-hint)) (declare (ignorable acl2::__function__)) (change-smtlink-hint *default-smtlink-hint*)))