Generate a local theorem asserting
the correctness of
(schemalg-gen-algo-correct schema x-x1...xn x-a1...am x y iorel algo spec-0 spec-1 spec-2 names-to-avoid wrld) → (mv event name updated-names-to-avoid)
This is the theorem
Function:
(defun schemalg-gen-algo-correct (schema x-x1...xn x-a1...am x y iorel algo spec-0 spec-1 spec-2 names-to-avoid wrld) (declare (xargs :guard (and (keywordp schema) (symbol-listp x-x1...xn) (symbol-listp x-a1...am) (symbolp x) (symbolp y) (pseudo-lambdap iorel) (symbolp algo) (symbolp spec-0) (symbolp spec-1) (symbolp spec-2) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'schemalg-gen-algo-correct)) (declare (ignorable __function__)) (case schema (:divconq-list-0-1 (schemalg-gen-algo-correct-divconq-list-0-1 x-x1...xn x-a1...am x y iorel algo spec-0 spec-1 names-to-avoid wrld)) (:divconq-list-0-1-2 (schemalg-gen-algo-correct-divconq-list-0-1-2 x-x1...xn x-a1...am x y iorel algo spec-0 spec-1 spec-2 names-to-avoid wrld)) (:divconq-oset-0-1 (schemalg-gen-algo-correct-divconq-oset-0-1 x-x1...xn x-a1...am x y iorel algo spec-0 spec-1 names-to-avoid wrld)) (t (prog2$ (raise "Internal error: unknown schema ~x0." schema) (mv '(irrelevant) nil names-to-avoid))))))