Disambiguate a list of external declarations.
(dimb-extdecl-list edecls table) → (mv erp new-edecls new-table)
Function:
(defun dimb-extdecl-list (edecls table) (declare (xargs :guard (and (extdecl-listp edecls) (dimb-tablep table)))) (let ((__function__ 'dimb-extdecl-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp edecls)) (retok nil (dimb-table-fix table))) ((erp new-edecl table) (dimb-extdecl (car edecls) table)) ((erp new-edecls table) (dimb-extdecl-list (cdr edecls) table))) (retok (cons new-edecl new-edecls) table))))
Theorem:
(defthm extdecl-listp-of-dimb-extdecl-list.new-edecls (b* (((mv acl2::?erp ?new-edecls ?new-table) (dimb-extdecl-list edecls table))) (extdecl-listp new-edecls)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-extdecl-list.new-table (b* (((mv acl2::?erp ?new-edecls ?new-table) (dimb-extdecl-list edecls table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm extdecl-list-unambp-of-dimb-extdecl-list (b* (((mv acl2::?erp ?new-edecls ?new-table) (dimb-extdecl-list edecls table))) (implies (not erp) (extdecl-list-unambp new-edecls))))
Theorem:
(defthm dimb-extdecl-list-of-extdecl-list-fix-edecls (equal (dimb-extdecl-list (extdecl-list-fix edecls) table) (dimb-extdecl-list edecls table)))
Theorem:
(defthm dimb-extdecl-list-extdecl-list-equiv-congruence-on-edecls (implies (extdecl-list-equiv edecls edecls-equiv) (equal (dimb-extdecl-list edecls table) (dimb-extdecl-list edecls-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-extdecl-list-of-dimb-table-fix-table (equal (dimb-extdecl-list edecls (dimb-table-fix table)) (dimb-extdecl-list edecls table)))
Theorem:
(defthm dimb-extdecl-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-extdecl-list edecls table) (dimb-extdecl-list edecls table-equiv))) :rule-classes :congruence)