Process the inputs and generate the events.
(deftreeops-process-inputs-and-gen-everything args call wrld) → (mv erp event)
Function:
(defun deftreeops-process-inputs-and-gen-everything (args call wrld) (declare (xargs :guard (and (true-listp args) (pseudo-event-formp call) (plist-worldp wrld)))) (let ((__function__ 'deftreeops-process-inputs-and-gen-everything)) (declare (ignorable __function__)) (b* (((reterr) '(_)) ((when (deftreeops-table-lookup call wrld)) (retok '(value-triple :redundant))) ((erp grammar rules prefix) (deftreeops-process-inputs args wrld))) (retok (deftreeops-gen-everything grammar rules prefix call)))))
Theorem:
(defthm pseudo-event-formp-of-deftreeops-process-inputs-and-gen-everything.event (b* (((mv acl2::?erp acl2::?event) (deftreeops-process-inputs-and-gen-everything args call wrld))) (pseudo-event-formp event)) :rule-classes :rewrite)