Process the
(schemalg-process-oset-input oset-input oset-input? schema old ?f x-x1...xn x-a1...am ctx state) → (mv erp x state)
Function:
(defun schemalg-process-oset-input (oset-input oset-input? schema old ?f x-x1...xn x-a1...am ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp oset-input?) (keywordp schema) (symbolp old) (symbolp ?f) (symbol-listp x-x1...xn) (pseudo-term-listp x-a1...am)))) (let ((__function__ 'schemalg-process-oset-input)) (declare (ignorable __function__)) (b* ((schemas-allowed (list :divconq-oset-0-1)) ((when (and oset-input? (not (member-eq schema schemas-allowed)))) (er-soft+ ctx t nil "The :OSET-INPUT input can be present only if ~ the :SCHEMA input is ~v0, but that input is ~x1 instead." schemas-allowed schema))) (process-input-select-old-soft-io oset-input :oset-input old ?f x-x1...xn x-a1...am ctx state))))
Theorem:
(defthm symbolp-of-schemalg-process-oset-input.x (b* (((mv ?erp ?x acl2::?state) (schemalg-process-oset-input oset-input oset-input? schema old ?f x-x1...xn x-a1...am ctx state))) (symbolp x)) :rule-classes :rewrite)