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) '(_)) ((erp redundantp grammar rules prefix) (deftreeops-process-inputs args call wrld)) ((when redundantp) (retok '(value-triple :redundant)))) (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)