		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-algo-divconq-list-0-1-2

Generate the function algo[?g0][?g1][?h] for the :divconq-list-0-1-2 schema.

Signature
(schemalg-gen-algo-divconq-list-0-1-2 algo algo-enable x-z1...zm x ?g0 ?g1 ?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).; ?g0 — Guard (symbolp ?g0).; ?g1 — Guard (symbolp ?g1).; ?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-list-0-1-2

(defun schemalg-gen-algo-divconq-list-0-1-2
       (algo algo-enable
             x-z1...zm x ?g0 ?g1 ?h verify-guards)
 (declare (xargs :guard (and (symbolp algo)
                             (booleanp algo-enable)
                             (symbol-listp x-z1...zm)
                             (symbolp x)
                             (symbolp ?g0)
                             (symbolp ?g1)
                             (symbolp ?h)
                             (booleanp verify-guards))))
 (let ((__function__ 'schemalg-gen-algo-divconq-list-0-1-2))
  (declare (ignorable __function__))
  (b* ((car/cdr-x-z1...zm
            (loop$ for
                   var of-type symbol in x-z1...zm append
                   (if (eq var x)
                       (list (list 'car var) (list 'cdr var))
                     (list var))))
       (car-x-z1...zm (loop$ for
                             var of-type symbol in x-z1...zm collect
                             (if (eq var x) (list 'car var) var)))
       (cdr-x-z1...zm (loop$ for
                             var of-type symbol in x-z1...zm collect
                             (if (eq var x) (list 'cdr var) var))))
   (evmac-generate-soft-defun2
    algo
    :formals x-z1...zm
    :body
    (cons
     'cond
     (cons
      (cons (cons 'atom (cons x 'nil))
            (cons (cons ?g0 x-z1...zm) 'nil))
      (cons
       (cons (cons 'atom
                   (cons (cons 'cdr (cons x 'nil)) 'nil))
             (cons (cons ?g1 car/cdr-x-z1...zm)
                   'nil))
       (cons
        (cons
         't
         (cons (cons ?h
                     (append car-x-z1...zm
                             (cons (cons algo cdr-x-z1...zm) 'nil)))
               'nil))
        'nil))))
    :verify-guards verify-guards
    :enable algo-enable
    :measure (cons 'acl2-count (cons x 'nil))
    :hints
    (cons
     (cons
      '"Goal"
      (cons
       ':expand
       (cons
           (cons (cons 'acl2-count (cons x 'nil))
                 'nil)
           '(:in-theory
                 '(acl2-count o-finp o< car-cdr-elim
                              car-cons cdr-cons (:t acl2-count))))))
     'nil)
    :guard-hints '(("Goal" :in-theory nil))))))

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

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

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

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