(sv::constraintlist-maybe-rewrite-fixpoint acl2::x sv::do-rewrite &key (count '4) (sv::verbosep 'nil)) → sv::new-x
Function:
(defun sv::constraintlist-maybe-rewrite-fixpoint-fn (acl2::x sv::do-rewrite count sv::verbosep) (declare (xargs :guard (and (sv::constraintlist-p acl2::x) (natp count)))) (let ((__function__ 'sv::constraintlist-maybe-rewrite-fixpoint)) (declare (ignorable __function__)) (if sv::do-rewrite (sv::constraintlist-update-conds acl2::x (sv::svexlist-rewrite-fixpoint (sv::constraintlist->conds acl2::x) :count count :verbosep sv::verbosep)) (sv::constraintlist-fix acl2::x))))
Theorem:
(defthm sv::constraintlist-p-of-constraintlist-maybe-rewrite-fixpoint (b* ((sv::new-x (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite count sv::verbosep))) (sv::constraintlist-p sv::new-x)) :rule-classes :rewrite)
Theorem:
(defthm sv::vars-of-constraintlist-maybe-rewrite-fixpoint (b* ((sv::?new-x (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite count sv::verbosep))) (implies (not (member sv::v (sv::constraintlist-vars acl2::x))) (not (member sv::v (sv::constraintlist-vars sv::new-x))))))
Theorem:
(defthm sv::constraintlist-maybe-rewrite-fixpoint-fn-of-constraintlist-fix-x (equal (sv::constraintlist-maybe-rewrite-fixpoint-fn (sv::constraintlist-fix acl2::x) sv::do-rewrite count sv::verbosep) (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite count sv::verbosep)))
Theorem:
(defthm sv::constraintlist-maybe-rewrite-fixpoint-fn-constraintlist-equiv-congruence-on-x (implies (sv::constraintlist-equiv acl2::x sv::x-equiv) (equal (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite count sv::verbosep) (sv::constraintlist-maybe-rewrite-fixpoint-fn sv::x-equiv sv::do-rewrite count sv::verbosep))) :rule-classes :congruence)
Theorem:
(defthm sv::constraintlist-maybe-rewrite-fixpoint-fn-of-nfix-count (equal (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite (nfix count) sv::verbosep) (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite count sv::verbosep)))
Theorem:
(defthm sv::constraintlist-maybe-rewrite-fixpoint-fn-nat-equiv-congruence-on-count (implies (acl2::nat-equiv count sv::count-equiv) (equal (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite count sv::verbosep) (sv::constraintlist-maybe-rewrite-fixpoint-fn acl2::x sv::do-rewrite sv::count-equiv sv::verbosep))) :rule-classes :congruence)