		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-spec-1-divconq-oset-0-1

Generate the function spec-1[?h] for the :divconq-oset-0-1 schema.

Signature
(schemalg-gen-spec-1-divconq-oset-0-1 spec-1 spec-1-enable old x-x1...xn x-a1...am x y iorel ?h verify-guards wrld) → (mv local-event exported-event)
Arguments: spec-1 — Guard (symbolp spec-1).; spec-1-enable — Guard (booleanp spec-1-enable).; old — Guard (symbolp old).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).; x — Guard (symbolp x).; y — Guard (symbolp y).; iorel — Guard (pseudo-lambdap iorel).; ?h — Guard (symbolp ?h).; verify-guards — Guard (booleanp verify-guards).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

Definitions and Theorems

Function: schemalg-gen-spec-1-divconq-oset-0-1

(defun schemalg-gen-spec-1-divconq-oset-0-1
       (spec-1 spec-1-enable old x-x1...xn x-a1...am
               x y iorel ?h verify-guards wrld)
 (declare (xargs :guard (and (symbolp spec-1)
                             (booleanp spec-1-enable)
                             (symbolp old)
                             (symbol-listp x-x1...xn)
                             (pseudo-term-listp x-a1...am)
                             (symbolp x)
                             (symbolp y)
                             (pseudo-lambdap iorel)
                             (symbolp ?h)
                             (booleanp verify-guards)
                             (plist-worldp wrld))))
 (let ((__function__ 'schemalg-gen-spec-1-divconq-oset-0-1))
  (declare (ignorable __function__))
  (b*
   ((tail-x-x1...xn (loop$ for var in x-x1...xn collect
                           (if (eq var x) (list 'tail var) var)))
    (head-x-a1...am (loop$ for var in x-a1...am collect
                           (if (eq var x) (list 'head var) var)))
    (iorel-term1
         (apply-term iorel (append tail-x-x1...xn (list y))))
    (iorel-term2
     (apply-term
      iorel
      (append x-x1...xn
              (list (cons ?h
                          (append head-x-a1...am (cons y 'nil)))))))
    (iorel-term1 (untranslate iorel-term1 t wrld))
    (iorel-term2 (untranslate iorel-term2 t wrld)))
   (evmac-generate-soft-defun-sk2
    spec-1
    :formals nil
    :guard t
    :body
    (cons
     'forall
     (cons
      (append x-x1...xn (cons y 'nil))
      (cons
       (cons
        'impliez
        (cons
          (cons 'and
                (cons (cons 'setp (cons x 'nil))
                      (cons (cons 'not
                                  (cons (cons 'emptyp (cons x 'nil))
                                        'nil))
                            (cons iorel-term1 'nil))))
          (cons iorel-term2 'nil)))
       'nil)))
    :verify-guards verify-guards
    :enable spec-1-enable
    :guard-hints
    (cons (cons '"Goal"
                (cons ':use
                      (cons (cons ':guard-theorem (cons old 'nil))
                            'nil)))
          'nil)))))