		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-divconq-oset-0-1-inputs

Process some of the schema-specific inputs when the schema is :divconq-oset-0-1.

Signature
(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)
Arguments: oset-input? — Guard (booleanp oset-input?).; tail-output? — Guard (booleanp tail-output?).; old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A (tuple (x symbolp) (y symbolp) (?g symbolp) (?h symbolp) (spec-0 symbolp) (spec-1 symbolp) (updated-names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: schemalg-process-divconq-oset-0-1-inputs

(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)))))