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