Generate the function
(schemalg-gen-spec-1-divconq-list-0-1-2 spec-1 spec-1-enable old x-x1...xn x-a1...am x iorel ?g1 verify-guards wrld) → (mv local-event exported-event)
Function:
(defun schemalg-gen-spec-1-divconq-list-0-1-2 (spec-1 spec-1-enable old x-x1...xn x-a1...am x iorel ?g1 verify-guards wrld) (declare (xargs :guard (and (symbolp spec-1) (booleanp spec-1-enable) (symbolp old) (symbol-listp x-x1...xn) (pseudo-term-listp x-a1...am) (symbolp x) (pseudo-lambdap iorel) (symbolp ?g1) (booleanp verify-guards) (plist-worldp wrld)))) (let ((__function__ 'schemalg-gen-spec-1-divconq-list-0-1-2)) (declare (ignorable __function__)) (b* ((car/cdr-x-a1...am (loop$ for term in x-a1...am append (if (eq term x) (list (list 'car term) (list 'cdr term)) (list term)))) (iorel-term (apply-term iorel (append x-x1...xn (list (cons ?g1 car/cdr-x-a1...am))))) (iorel-term (untranslate iorel-term t wrld))) (evmac-generate-soft-defun-sk2 spec-1 :formals nil :guard t :body (cons 'forall (cons x-x1...xn (cons (cons 'impliez (cons (cons 'and (cons (cons 'consp (cons x 'nil)) (cons (cons 'atom (cons (cons 'cdr (cons x 'nil)) 'nil)) 'nil))) (cons iorel-term 'nil))) 'nil))) :verify-guards verify-guards :enable spec-1-enable :guard-hints (cons (cons '"Goal" (cons ':use (cons (cons ':guard-theorem (cons old 'nil)) 'nil))) 'nil)))))