(svex-alist-merge-branches key-alist cond then-st else-st st-acc) → merged-st
Function:
(defun svex-alist-merge-branches (key-alist cond then-st else-st st-acc) (declare (xargs :guard (and (svex-alist-p key-alist) (svex-p cond) (svex-alist-p then-st) (svex-alist-p else-st) (svex-alist-p st-acc)))) (let ((__function__ 'svex-alist-merge-branches)) (declare (ignorable __function__)) (b* (((when (atom key-alist)) (svex-alist-fix st-acc)) ((unless (mbt (and (consp (car key-alist)) (svar-p (caar key-alist))))) (svex-alist-merge-branches (cdr key-alist) cond then-st else-st st-acc)) (key (caar key-alist)) ((when (svex-fastlookup key st-acc)) (svex-alist-merge-branches (cdr key-alist) cond then-st else-st st-acc)) (then-val (or (svex-fastlookup key then-st) (make-svex-var :name key))) (else-val (or (svex-fastlookup key else-st) (make-svex-var :name key))) (val (svex-svstmt-ite cond then-val else-val)) (st-acc (hons-acons key val st-acc))) (svex-alist-merge-branches (cdr key-alist) cond then-st else-st st-acc))))
Theorem:
(defthm svex-alist-p-of-svex-alist-merge-branches (b* ((merged-st (svex-alist-merge-branches key-alist cond then-st else-st st-acc))) (svex-alist-p merged-st)) :rule-classes :rewrite)
Theorem:
(defthm svex-alist-merge-branches-lookup-under-iff (iff (svex-lookup k (svex-alist-merge-branches key-alist cond then-st else-st st-acc)) (or (svex-lookup k st-acc) (svex-lookup k key-alist))))
Theorem:
(defthm svex-alist-merge-branches-when-cond-true-lookup (implies (equal (4vec-reduction-or (svex-eval cond env)) -1) (equal (svex-eval (svex-lookup k (svex-alist-merge-branches key-alist cond then-st else-st st-acc)) env) (if (svex-lookup k st-acc) (svex-eval (svex-lookup k st-acc) env) (if (svex-lookup k key-alist) (if (svex-lookup k then-st) (svex-eval (svex-lookup k then-st) env) (svex-env-lookup k env)) (4vec-x))))))
Theorem:
(defthm svex-alist-merge-branches-when-cond-false-lookup (implies (equal (4vec-reduction-or (svex-eval cond env)) 0) (equal (svex-eval (svex-lookup k (svex-alist-merge-branches key-alist cond then-st else-st st-acc)) env) (if (svex-lookup k st-acc) (svex-eval (svex-lookup k st-acc) env) (if (svex-lookup k key-alist) (if (svex-lookup k else-st) (svex-eval (svex-lookup k else-st) env) (svex-env-lookup k env)) (4vec-x))))))
Theorem:
(defthm keys-of-svex-alist-merge-branches (implies (and (not (member v (svex-alist-keys then-st))) (not (member v (svex-alist-keys else-st))) (not (member v (svex-alist-keys st-acc))) (not (member v (svex-alist-keys key-alist)))) (not (member v (svex-alist-keys (svex-alist-merge-branches key-alist cond then-st else-st st-acc))))))
Theorem:
(defthm svex-lookup-of-svex-alist-merge-branches (implies (and (not (member v (svex-alist-keys then-st))) (not (member v (svex-alist-keys else-st))) (not (member v (svex-alist-keys st-acc))) (not (member v (svex-alist-keys key-alist))) (svar-p v)) (not (svex-lookup v (svex-alist-merge-branches key-alist cond then-st else-st st-acc)))))
Theorem:
(defthm vars-of-svex-alist-merge-branches (implies (and (not (member v (svex-vars cond))) (not (member v (svex-alist-vars then-st))) (not (member v (svex-alist-vars else-st))) (not (member v (svex-alist-vars st-acc))) (not (member v (svex-alist-keys key-alist)))) (not (member v (svex-alist-vars (svex-alist-merge-branches key-alist cond then-st else-st st-acc))))))
Theorem:
(defthm svex-alist-merge-branches-of-svex-alist-fix-key-alist (equal (svex-alist-merge-branches (svex-alist-fix key-alist) cond then-st else-st st-acc) (svex-alist-merge-branches key-alist cond then-st else-st st-acc)))
Theorem:
(defthm svex-alist-merge-branches-svex-alist-equiv-congruence-on-key-alist (implies (svex-alist-equiv key-alist key-alist-equiv) (equal (svex-alist-merge-branches key-alist cond then-st else-st st-acc) (svex-alist-merge-branches key-alist-equiv cond then-st else-st st-acc))) :rule-classes :congruence)
Theorem:
(defthm svex-alist-merge-branches-of-svex-fix-cond (equal (svex-alist-merge-branches key-alist (svex-fix cond) then-st else-st st-acc) (svex-alist-merge-branches key-alist cond then-st else-st st-acc)))
Theorem:
(defthm svex-alist-merge-branches-svex-equiv-congruence-on-cond (implies (svex-equiv cond cond-equiv) (equal (svex-alist-merge-branches key-alist cond then-st else-st st-acc) (svex-alist-merge-branches key-alist cond-equiv then-st else-st st-acc))) :rule-classes :congruence)
Theorem:
(defthm svex-alist-merge-branches-of-svex-alist-fix-then-st (equal (svex-alist-merge-branches key-alist cond (svex-alist-fix then-st) else-st st-acc) (svex-alist-merge-branches key-alist cond then-st else-st st-acc)))
Theorem:
(defthm svex-alist-merge-branches-svex-alist-equiv-congruence-on-then-st (implies (svex-alist-equiv then-st then-st-equiv) (equal (svex-alist-merge-branches key-alist cond then-st else-st st-acc) (svex-alist-merge-branches key-alist cond then-st-equiv else-st st-acc))) :rule-classes :congruence)
Theorem:
(defthm svex-alist-merge-branches-of-svex-alist-fix-else-st (equal (svex-alist-merge-branches key-alist cond then-st (svex-alist-fix else-st) st-acc) (svex-alist-merge-branches key-alist cond then-st else-st st-acc)))
Theorem:
(defthm svex-alist-merge-branches-svex-alist-equiv-congruence-on-else-st (implies (svex-alist-equiv else-st else-st-equiv) (equal (svex-alist-merge-branches key-alist cond then-st else-st st-acc) (svex-alist-merge-branches key-alist cond then-st else-st-equiv st-acc))) :rule-classes :congruence)
Theorem:
(defthm svex-alist-merge-branches-of-svex-alist-fix-st-acc (equal (svex-alist-merge-branches key-alist cond then-st else-st (svex-alist-fix st-acc)) (svex-alist-merge-branches key-alist cond then-st else-st st-acc)))
Theorem:
(defthm svex-alist-merge-branches-svex-alist-equiv-congruence-on-st-acc (implies (svex-alist-equiv st-acc st-acc-equiv) (equal (svex-alist-merge-branches key-alist cond then-st else-st st-acc) (svex-alist-merge-branches key-alist cond then-st else-st st-acc-equiv))) :rule-classes :congruence)