(atj-function-type-of-min-input-types-aux in-types fn-types current-min-in-types current-fn-type?) → fn-type?
Function:
(defun atj-function-type-of-min-input-types-aux (in-types fn-types current-min-in-types current-fn-type?) (declare (xargs :guard (and (atj-type-listp in-types) (atj-function-type-listp fn-types) (atj-type-listp current-min-in-types) (atj-maybe-function-type-p current-fn-type?)))) (let ((__function__ 'atj-function-type-of-min-input-types-aux)) (declare (ignorable __function__)) (b* (((when (endp fn-types)) current-fn-type?) (fn-type (car fn-types)) (fn-in-types (atj-function-type->inputs fn-type)) ((mv current-min-in-types current-fn-type?) (if (and (atj-type-list-<= in-types fn-in-types) (or (null current-fn-type?) (atj-type-list-< fn-in-types current-min-in-types))) (mv fn-in-types fn-type) (mv current-min-in-types current-fn-type?)))) (atj-function-type-of-min-input-types-aux in-types (cdr fn-types) current-min-in-types current-fn-type?))))
Theorem:
(defthm atj-maybe-function-type-p-of-atj-function-type-of-min-input-types-aux (implies (and (atj-function-type-listp fn-types) (atj-maybe-function-type-p current-fn-type?)) (b* ((fn-type? (atj-function-type-of-min-input-types-aux in-types fn-types current-min-in-types current-fn-type?))) (atj-maybe-function-type-p fn-type?))) :rule-classes :rewrite)