Generate the function
(schemalg-gen-algo-divconq-oset-0-1 algo algo-enable x-z1...zm x ?g ?h verify-guards) → (mv local-event exported-event)
Function:
(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:
(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:
(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)