Generate the function
(schemalg-gen-spec-0-divconq-oset-0-1 spec-0 spec-0-enable old x-x1...xn x-a1...am x iorel ?g verify-guards wrld) → (mv local-event exported-event)
Function:
(defun schemalg-gen-spec-0-divconq-oset-0-1 (spec-0 spec-0-enable old x-x1...xn x-a1...am x iorel ?g verify-guards wrld) (declare (xargs :guard (and (symbolp spec-0) (booleanp spec-0-enable) (symbolp old) (symbol-listp x-x1...xn) (pseudo-term-listp x-a1...am) (symbolp x) (pseudo-lambdap iorel) (symbolp ?g) (booleanp verify-guards) (plist-worldp wrld)))) (let ((__function__ 'schemalg-gen-spec-0-divconq-oset-0-1)) (declare (ignorable __function__)) (b* ((iorel-term (apply-term iorel (append x-x1...xn (list (cons ?g x-a1...am))))) (iorel-term (untranslate iorel-term t wrld))) (evmac-generate-soft-defun-sk2 spec-0 :formals nil :guard t :body (cons 'forall (cons x-x1...xn (cons (cons 'impliez (cons (cons 'or (cons (cons 'not (cons (cons 'setp (cons x 'nil)) 'nil)) (cons (cons 'emptyp (cons x 'nil)) 'nil))) (cons iorel-term 'nil))) 'nil))) :verify-guards verify-guards :enable spec-0-enable :guard-hints (cons (cons '"Goal" (cons ':use (cons (cons ':guard-theorem (cons old 'nil)) 'nil))) 'nil)))))