(acl2-number-list-fix x) is a usual fty list fixing function.
(acl2-number-list-fix x) → fty::newx
In the logic, we apply fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.
Function:
(defun acl2-number-list-fix$inline (x) (declare (xargs :guard (acl2-number-listp x))) (let ((__function__ 'acl2-number-list-fix)) (declare (ignorable __function__)) (mbe :logic (if (atom x) nil (cons (fix (car x)) (acl2-number-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm acl2-number-listp-of-acl2-number-list-fix (b* ((fty::newx (acl2-number-list-fix$inline x))) (acl2-number-listp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm acl2-number-list-fix-when-acl2-number-listp (implies (acl2-number-listp x) (equal (acl2-number-list-fix x) x)))
Function:
(defun acl2-number-list-equiv$inline (x y) (declare (xargs :guard (and (acl2-number-listp x) (acl2-number-listp y)))) (equal (acl2-number-list-fix x) (acl2-number-list-fix y)))
Theorem:
(defthm acl2-number-list-equiv-is-an-equivalence (and (booleanp (acl2-number-list-equiv x y)) (acl2-number-list-equiv x x) (implies (acl2-number-list-equiv x y) (acl2-number-list-equiv y x)) (implies (and (acl2-number-list-equiv x y) (acl2-number-list-equiv y z)) (acl2-number-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm acl2-number-list-equiv-implies-equal-acl2-number-list-fix-1 (implies (acl2-number-list-equiv x x-equiv) (equal (acl2-number-list-fix x) (acl2-number-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm acl2-number-list-fix-under-acl2-number-list-equiv (acl2-number-list-equiv (acl2-number-list-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-acl2-number-list-fix-1-forward-to-acl2-number-list-equiv (implies (equal (acl2-number-list-fix x) y) (acl2-number-list-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-acl2-number-list-fix-2-forward-to-acl2-number-list-equiv (implies (equal x (acl2-number-list-fix y)) (acl2-number-list-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm acl2-number-list-equiv-of-acl2-number-list-fix-1-forward (implies (acl2-number-list-equiv (acl2-number-list-fix x) y) (acl2-number-list-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm acl2-number-list-equiv-of-acl2-number-list-fix-2-forward (implies (acl2-number-list-equiv x (acl2-number-list-fix y)) (acl2-number-list-equiv x y)) :rule-classes :forward-chaining)
Theorem:
(defthm car-of-acl2-number-list-fix-x-under-number-equiv (number-equiv (car (acl2-number-list-fix x)) (car x)))
Theorem:
(defthm car-acl2-number-list-equiv-congruence-on-x-under-number-equiv (implies (acl2-number-list-equiv x x-equiv) (number-equiv (car x) (car x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cdr-of-acl2-number-list-fix-x-under-acl2-number-list-equiv (acl2-number-list-equiv (cdr (acl2-number-list-fix x)) (cdr x)))
Theorem:
(defthm cdr-acl2-number-list-equiv-congruence-on-x-under-acl2-number-list-equiv (implies (acl2-number-list-equiv x x-equiv) (acl2-number-list-equiv (cdr x) (cdr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cons-of-fix-x-under-acl2-number-list-equiv (acl2-number-list-equiv (cons (fix x) y) (cons x y)))
Theorem:
(defthm cons-number-equiv-congruence-on-x-under-acl2-number-list-equiv (implies (number-equiv x x-equiv) (acl2-number-list-equiv (cons x y) (cons x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm cons-of-acl2-number-list-fix-y-under-acl2-number-list-equiv (acl2-number-list-equiv (cons x (acl2-number-list-fix y)) (cons x y)))
Theorem:
(defthm cons-acl2-number-list-equiv-congruence-on-y-under-acl2-number-list-equiv (implies (acl2-number-list-equiv y y-equiv) (acl2-number-list-equiv (cons x y) (cons x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-acl2-number-list-fix (equal (consp (acl2-number-list-fix x)) (consp x)))
Theorem:
(defthm acl2-number-list-fix-under-iff (iff (acl2-number-list-fix x) (consp x)))
Theorem:
(defthm acl2-number-list-fix-of-cons (equal (acl2-number-list-fix (cons a x)) (cons (fix a) (acl2-number-list-fix x))))
Theorem:
(defthm len-of-acl2-number-list-fix (equal (len (acl2-number-list-fix x)) (len x)))
Theorem:
(defthm acl2-number-list-fix-of-append (equal (acl2-number-list-fix (append std::a std::b)) (append (acl2-number-list-fix std::a) (acl2-number-list-fix std::b))))
Theorem:
(defthm acl2-number-list-fix-of-repeat (equal (acl2-number-list-fix (repeat n x)) (repeat n (fix x))))
Theorem:
(defthm list-equiv-refines-acl2-number-list-equiv (implies (list-equiv x y) (acl2-number-list-equiv x y)) :rule-classes :refinement)
Theorem:
(defthm nth-of-acl2-number-list-fix (equal (nth n (acl2-number-list-fix x)) (if (< (nfix n) (len x)) (fix (nth n x)) nil)))
Theorem:
(defthm acl2-number-list-equiv-implies-acl2-number-list-equiv-append-1 (implies (acl2-number-list-equiv x fty::x-equiv) (acl2-number-list-equiv (append x y) (append fty::x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm acl2-number-list-equiv-implies-acl2-number-list-equiv-append-2 (implies (acl2-number-list-equiv y fty::y-equiv) (acl2-number-list-equiv (append x y) (append x fty::y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm acl2-number-list-equiv-implies-acl2-number-list-equiv-nthcdr-2 (implies (acl2-number-list-equiv l l-equiv) (acl2-number-list-equiv (nthcdr n l) (nthcdr n l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm acl2-number-list-equiv-implies-acl2-number-list-equiv-take-2 (implies (acl2-number-list-equiv l l-equiv) (acl2-number-list-equiv (take n l) (take n l-equiv))) :rule-classes (:congruence))