(moddb-clear moddb) → moddb1
Function:
(defun moddb-clear (moddb) (declare (xargs :stobjs (moddb))) (declare (xargs :guard t)) (let ((__function__ 'moddb-clear)) (declare (ignorable __function__)) (b* ((moddb (moddb->modname-idxes-clear moddb)) (moddb (update-moddb->nmods 0 moddb))) (resize-moddb->mods 0 moddb))))
Theorem:
(defthm return-type-of-moddb-clear (b* ((moddb1 (moddb-clear moddb))) (and (moddb-mods-ok moddb1) (moddb-basics-ok moddb1))) :rule-classes :rewrite)
Theorem:
(defthm moddb-clear-normalize (implies (syntaxp (not (equal moddb ''nil))) (equal (moddb-clear moddb) (moddb-clear nil))))
Theorem:
(defthm moddb-clear-of-moddb-fix-moddb (equal (moddb-clear (moddb-fix moddb)) (moddb-clear moddb)))
Theorem:
(defthm moddb-clear-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (moddb-clear moddb) (moddb-clear moddb-equiv))) :rule-classes :congruence)