Generate the events for all the numeric ranges in the alist.
(deftreeops-gen-numrange-alist-events range-infos prefix) → (mv get-nat-fn-events bounds-thm-events)
Function:
(defun deftreeops-gen-numrange-alist-events (range-infos prefix) (declare (xargs :guard (and (deftreeops-numrange-info-alistp range-infos) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-numrange-alist-events)) (declare (ignorable __function__)) (b* (((when (endp range-infos)) (mv nil nil)) ((cons range info) (car range-infos)) ((mv get-nat-fn-event bounds-thm-event) (deftreeops-gen-numrange-events range info prefix)) ((mv get-nat-fn-more-events bounds-thm-more-events) (deftreeops-gen-numrange-alist-events (cdr range-infos) prefix))) (mv (cons get-nat-fn-event get-nat-fn-more-events) (cons bounds-thm-event bounds-thm-more-events)))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-numrange-alist-events.get-nat-fn-events (b* (((mv ?get-nat-fn-events ?bounds-thm-events) (deftreeops-gen-numrange-alist-events range-infos prefix))) (pseudo-event-form-listp get-nat-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-numrange-alist-events.bounds-thm-events (b* (((mv ?get-nat-fn-events ?bounds-thm-events) (deftreeops-gen-numrange-alist-events range-infos prefix))) (pseudo-event-form-listp bounds-thm-events)) :rule-classes :rewrite)