Process some of the schema-specific inputs
when the schema is
(schemalg-process-divconq-list-0-1-inputs list-input list-input? cdr-output cdr-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-list-0-1-inputs (list-input list-input? cdr-output cdr-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 list-input?) (booleanp cdr-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-list-0-1-inputs)) (declare (ignorable __function__)) (b* ((schema :divconq-list-0-1) ((er x) (schemalg-process-list-input list-input list-input? schema old ?f x-x1...xn x-a1...am ctx state)) ((er y) (schemalg-process-cdr-output cdr-output cdr-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)))))