(bfr-+-ss c v1 v2) → sum
Function:
(defun bfr-+-ss (c v1 v2) (declare (xargs :guard (and (true-listp v1) (true-listp v2)))) (let ((__function__ 'bfr-+-ss)) (declare (ignorable __function__)) (b* (((mv head1 tail1 end1) (first/rest/end v1)) ((mv head2 tail2 end2) (first/rest/end v2)) (axorb (bfr-xor head1 head2)) (s (bfr-xor c axorb)) ((when (and end1 end2)) (let ((last (bfr-ite axorb (bfr-not c) head1))) (bfr-scons s (bfr-sterm last)))) (c (bfr-or (bfr-and c axorb) (bfr-and head1 head2))) (rst (bfr-+-ss c tail1 tail2))) (bfr-scons s rst))))
Theorem:
(defthm true-listp-of-bfr-+-ss (b* ((sum (bfr-+-ss c v1 v2))) (true-listp sum)) :rule-classes :type-prescription)
Theorem:
(defthm bfr-+-ss-correct (b* ((sum (bfr-+-ss c v1 v2))) (and (equal (bfr-list->s sum env) (+ (bool->bit (bfr-eval c env)) (bfr-list->s v1 env) (bfr-list->s v2 env))))))
Theorem:
(defthm bfr-+-ss-deps (b* ((sum (bfr-+-ss c v1 v2))) (implies (and (not (pbfr-depends-on varname param c)) (not (pbfr-list-depends-on varname param v1)) (not (pbfr-list-depends-on varname param v2))) (and (not (pbfr-list-depends-on varname param sum))))))