Process some of the schema-specific inputs
when the schema is
(schemalg-process-divconq-oset-0-1-inputs oset-input oset-input? tail-output tail-output? fvar-0-name fvar-1-name spec-0-name spec-1-name old ?f x-x1...xn x-a1...am names-to-avoid ctx state) → (mv erp result state)
Function:
(defun schemalg-process-divconq-oset-0-1-inputs (oset-input oset-input? tail-output tail-output? fvar-0-name fvar-1-name spec-0-name spec-1-name old ?f x-x1...xn x-a1...am names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp oset-input?) (booleanp tail-output?) (symbolp old) (symbolp ?f) (symbol-listp x-x1...xn) (pseudo-term-listp x-a1...am) (symbol-listp names-to-avoid)))) (let ((__function__ 'schemalg-process-divconq-oset-0-1-inputs)) (declare (ignorable __function__)) (b* ((schema :divconq-oset-0-1) ((er x) (schemalg-process-oset-input oset-input oset-input? schema old ?f x-x1...xn x-a1...am ctx state)) ((er y) (schemalg-process-tail-output tail-output tail-output? schema old x-x1...xn ctx state)) ((er (list ??g names-to-avoid)) (schemalg-process-fvar-0-name fvar-0-name ?f names-to-avoid ctx state)) ((er (list ??h names-to-avoid)) (schemalg-process-fvar-1-name fvar-1-name ?f names-to-avoid ctx state)) ((er (list spec-0 names-to-avoid)) (schemalg-process-spec-0-name spec-0-name old ?g names-to-avoid ctx state)) ((er (list spec-1 names-to-avoid)) (schemalg-process-spec-1-name spec-1-name old ?h names-to-avoid ctx state))) (value (list x y ?g ?h spec-0 spec-1 names-to-avoid)))))