(max-supertypes types tops) → super?
Function:
(defun max-supertypes (types tops) (declare (xargs :guard (and (type-listp types) (toplevel-listp tops)))) (let ((__function__ 'max-supertypes)) (declare (ignorable __function__)) (if (endp types) nil (cons (or (max-supertype (car types) tops) (type-fix (car types))) (max-supertypes (cdr types) tops)))))
Theorem:
(defthm type-listp-of-max-supertypes (b* ((super? (max-supertypes types tops))) (type-listp super?)) :rule-classes :rewrite)
Theorem:
(defthm max-supertypes-of-type-list-fix-types (equal (max-supertypes (type-list-fix types) tops) (max-supertypes types tops)))
Theorem:
(defthm max-supertypes-type-list-equiv-congruence-on-types (implies (type-list-equiv types types-equiv) (equal (max-supertypes types tops) (max-supertypes types-equiv tops))) :rule-classes :congruence)
Theorem:
(defthm max-supertypes-of-toplevel-list-fix-tops (equal (max-supertypes types (toplevel-list-fix tops)) (max-supertypes types tops)))
Theorem:
(defthm max-supertypes-toplevel-list-equiv-congruence-on-tops (implies (toplevel-list-equiv tops tops-equiv) (equal (max-supertypes types tops) (max-supertypes types tops-equiv))) :rule-classes :congruence)