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 event-alist)
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 nil)) ((cons range info) (car range-infos)) ((mv get-nat-fn-event bounds-thm-event event-alist) (deftreeops-gen-numrange-events range info prefix)) ((mv more-get-nat-fn-events more-bounds-thm-events more-event-alist) (deftreeops-gen-numrange-alist-events (cdr range-infos) prefix))) (mv (cons get-nat-fn-event more-get-nat-fn-events) (cons bounds-thm-event more-bounds-thm-events) (append event-alist more-event-alist)))))
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 ?event-alist) (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 ?event-alist) (deftreeops-gen-numrange-alist-events range-infos prefix))) (pseudo-event-form-listp bounds-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-numrange-alist-events.event-alist (b* (((mv ?get-nat-fn-events ?bounds-thm-events ?event-alist) (deftreeops-gen-numrange-alist-events range-infos prefix))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)