(aabf-+-ss c v1 v2 man) → (mv sum new-man)
Function:
(defun aabf-+-ss (c v1 v2 man) (declare (xargs :guard (and (true-listp v1) (true-listp v2)))) (declare (xargs :guard (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v2 man)))) (let ((__function__ 'aabf-+-ss)) (declare (ignorable __function__)) (b* (((mv head1 tail1 end1) (aabf-first/rest/end v1)) ((mv head2 tail2 end2) (aabf-first/rest/end v2)) ((mv axorb man) (aabf-xor head1 head2 man)) ((mv s man) (aabf-xor c axorb man)) ((when (and end1 end2)) (b* (((mv last man) (aabf-ite axorb (aabf-not c man) head1 man))) (mv (aabf-scons s (list last)) man))) ((mv c man) (aabf-nest (or (and c axorb) (and head1 head2)) man)) ((mv rst man) (aabf-+-ss c tail1 tail2 man))) (mv (aabf-scons s rst) man))))
Theorem:
(defthm trivial-theorem-about-aabf-+-ss (b* nil (b* ((?ignore (aabf-+-ss c v1 v2 man))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-aabf-+-ss.sum (b* (((mv ?sum ?new-man) (aabf-+-ss c v1 v2 man))) (true-listp sum)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-extension-p-of-aabf-+-ss (b* (((mv ?sum ?new-man) (aabf-+-ss c v1 v2 man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-+-ss (b* (((mv sum new-man) (aabf-+-ss c v1 v2 man))) (implies (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v2 man)) (and (aabflist-p sum new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-+-ss (b* (((mv sum new-man) (aabf-+-ss c v1 v2 man))) (implies (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v2 man)) (and (equal (bools->int (aabflist-eval sum env new-man)) (+ (bool->bit (aabf-eval c env man)) (bools->int (aabflist-eval v1 env man)) (bools->int (aabflist-eval v2 env man))))))))
Theorem:
(defthm aabf-pred-of-aabf-+-ss (b* (((mv sum new-man) (aabf-+-ss c v1 v2 man))) (implies (and (aabf-p c man) (aabflist-p v1 man) (aabflist-p v2 man) (aabf-pred c man) (aabflist-pred v1 man) (aabflist-pred v2 man)) (and (aabflist-pred sum new-man)))))