		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-algo-divconq-oset-0-1

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

Signature
(schemalg-gen-algo-divconq-oset-0-1 algo algo-enable x-z1...zm x ?g ?h verify-guards) → (mv local-event exported-event)
Arguments: algo — Guard (symbolp algo).; algo-enable — Guard (booleanp algo-enable).; x-z1...zm — Guard (symbol-listp x-z1...zm).; x — Guard (symbolp x).; ?g — Guard (symbolp ?g).; ?h — Guard (symbolp ?h).; verify-guards — Guard (booleanp verify-guards).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

Definitions and Theorems

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

(defun schemalg-gen-algo-divconq-oset-0-1
       (algo algo-enable
             x-z1...zm x ?g ?h verify-guards)
 (declare (xargs :guard (and (symbolp algo)
                             (booleanp algo-enable)
                             (symbol-listp x-z1...zm)
                             (symbolp x)
                             (symbolp ?g)
                             (symbolp ?h)
                             (booleanp verify-guards))))
 (let ((__function__ 'schemalg-gen-algo-divconq-oset-0-1))
  (declare (ignorable __function__))
  (b*
    ((head-x-z1...zm (loop$ for
                            var of-type symbol in x-z1...zm collect
                            (if (eq var x) (list 'head var) var)))
     (tail-x-z1...zm (loop$ for
                            var of-type symbol in x-z1...zm collect
                            (if (eq var x) (list 'tail var) var))))
   (evmac-generate-soft-defun2
    algo
    :formals x-z1...zm
    :body
    (cons
     'cond
     (cons
      (cons
           (cons 'or
                 (cons (cons 'not
                             (cons (cons 'setp (cons x 'nil)) 'nil))
                       (cons (cons 'emptyp (cons x 'nil))
                             'nil)))
           (cons (cons ?g x-z1...zm) 'nil))
      (cons
       (cons
        't
        (cons (cons ?h
                    (append head-x-z1...zm
                            (cons (cons algo tail-x-z1...zm) 'nil)))
              'nil))
       'nil)))
    :verify-guards verify-guards
    :enable algo-enable
    :measure (cons 'acl2-count (cons x 'nil))
    :hints '(("Goal" :in-theory '(set::tail-count-built-in)))
    :guard-hints '(("Goal" :in-theory nil))))))

Theorem: pseudo-event-formp-of-schemalg-gen-algo-divconq-oset-0-1.local-event

(defthm
 pseudo-event-formp-of-schemalg-gen-algo-divconq-oset-0-1.local-event
 (b* (((mv ?local-event ?exported-event)
       (schemalg-gen-algo-divconq-oset-0-1
            algo algo-enable
            x-z1...zm x ?g ?h verify-guards)))
   (pseudo-event-formp local-event))
 :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-schemalg-gen-algo-divconq-oset-0-1.exported-event

(defthm
 pseudo-event-formp-of-schemalg-gen-algo-divconq-oset-0-1.exported-event
 (b* (((mv ?local-event ?exported-event)
       (schemalg-gen-algo-divconq-oset-0-1
            algo algo-enable
            x-z1...zm x ?g ?h verify-guards)))
   (pseudo-event-formp exported-event))
 :rule-classes :rewrite)