(aig-scons-with-hint b v hint) → ans
Function:
(defun aig-scons-with-hint$inline (b v hint) (declare (xargs :guard (and (true-listp v) (true-listp hint)))) (let ((__function__ 'aig-scons-with-hint)) (declare (ignorable __function__)) (if (atom v) (if b (cons-with-hint b (let ((ans '(nil))) (mbe :logic ans :exec (if (equal ans (cdr hint)) (cdr hint) ans))) hint) (let ((ans '(nil))) (mbe :logic ans :exec (if (equal hint ans) hint ans)))) (if (and (atom (cdr v)) (hons-equal (car v) b)) (llist-fix v) (cons-with-hint b (llist-fix v) hint)))))
Theorem:
(defthm return-type-of-aig-scons-with-hint (b* ((ans (aig-scons-with-hint$inline b v hint))) (equal ans (aig-scons b v))) :rule-classes :rewrite)
Theorem:
(defthm aig-scons-with-hint$inline-of-list-fix-v (equal (aig-scons-with-hint$inline b (list-fix v) hint) (aig-scons-with-hint$inline b v hint)))
Theorem:
(defthm aig-scons-with-hint$inline-list-equiv-congruence-on-v (implies (list-equiv v v-equiv) (equal (aig-scons-with-hint$inline b v hint) (aig-scons-with-hint$inline b v-equiv hint))) :rule-classes :congruence)
Theorem:
(defthm aig-scons-with-hint$inline-of-list-fix-hint (equal (aig-scons-with-hint$inline b v (list-fix hint)) (aig-scons-with-hint$inline b v hint)))
Theorem:
(defthm aig-scons-with-hint$inline-list-equiv-congruence-on-hint (implies (list-equiv hint hint-equiv) (equal (aig-scons-with-hint$inline b v hint) (aig-scons-with-hint$inline b v hint-equiv))) :rule-classes :congruence)