		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-?f1...?fp

Generate the function variables ?f1, ..., ?fp.

Signature
(schemalg-gen-?f1...?fp schema ?g ?g0 ?g1 ?h x-a1...am) → events
Arguments: schema — Guard (keywordp schema).; ?g — Guard (symbolp ?g).; ?g0 — Guard (symbolp ?g0).; ?g1 — Guard (symbolp ?g1).; ?h — Guard (symbolp ?h).; x-a1...am — Guard (pseudo-term-listp x-a1...am).
Returns: events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: schemalg-gen-?f1...?fp

(defun schemalg-gen-?f1...?fp (schema ?g ?g0 ?g1 ?h x-a1...am)
 (declare (xargs :guard (and (keywordp schema)
                             (symbolp ?g)
                             (symbolp ?g0)
                             (symbolp ?g1)
                             (symbolp ?h)
                             (pseudo-term-listp x-a1...am))))
 (let ((__function__ 'schemalg-gen-?f1...?fp))
  (declare (ignorable __function__))
  (case schema
   ((:divconq-list-0-1 :divconq-oset-0-1)
    (list (evmac-generate-soft-defunvar ?g (len x-a1...am))
          (evmac-generate-soft-defunvar ?h (1+ (len x-a1...am)))))
   (:divconq-list-0-1-2
      (list (evmac-generate-soft-defunvar ?g0 (len x-a1...am))
            (evmac-generate-soft-defunvar ?g1 (1+ (len x-a1...am)))
            (evmac-generate-soft-defunvar ?h (1+ (len x-a1...am)))))
   (t (raise "Internal error: unknown schema ~x0."
             schema)))))

Theorem: pseudo-event-form-listp-of-schemalg-gen-?f1...?fp

(defthm pseudo-event-form-listp-of-schemalg-gen-?f1...?fp
 (b*
  ((events (schemalg-gen-?f1...?fp schema ?g ?g0 ?g1 ?h x-a1...am)))
  (pseudo-event-form-listp events))
 :rule-classes :rewrite)