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