Generate the function
(schemalg-gen-spec-1-divconq-list-0-1 spec-1 spec-1-enable old x-x1...xn x-a1...am x y iorel ?h verify-guards wrld) → (mv local-event exported-event)
Function:
(defun schemalg-gen-spec-1-divconq-list-0-1 (spec-1 spec-1-enable old x-x1...xn x-a1...am x y iorel ?h 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) (symbolp y) (pseudo-lambdap iorel) (symbolp ?h) (booleanp verify-guards) (plist-worldp wrld)))) (let ((__function__ 'schemalg-gen-spec-1-divconq-list-0-1)) (declare (ignorable __function__)) (b* ((cdr-x-x1...xn (loop$ for var in x-x1...xn collect (if (eq var x) (list 'cdr var) var))) (car-x-a1...am (loop$ for term in x-a1...am collect (if (eq term x) (list 'car term) term))) (iorel-term1 (apply-term iorel (append cdr-x-x1...xn (list y)))) (iorel-term2 (apply-term iorel (append x-x1...xn (list (cons ?h (append car-x-a1...am (cons y 'nil))))))) (iorel-term1 (untranslate iorel-term1 t wrld)) (iorel-term2 (untranslate iorel-term2 t wrld))) (evmac-generate-soft-defun-sk2 spec-1 :formals nil :guard t :body (cons 'forall (cons (append x-x1...xn (cons y 'nil)) (cons (cons 'impliez (cons (cons 'and (cons (cons 'consp (cons x 'nil)) (cons iorel-term1 'nil))) (cons iorel-term2 '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)))))