Generate a local theorem asserting
the correctness of
(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) → (mv event name updated-names-to-avoid)
Function:
(defun 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) (declare (xargs :guard (and (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-divconq-list-0-1-2)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'algo-correct nil names-to-avoid wrld)) (iorel-term (apply-term iorel (append x-x1...xn (list (cons algo x-a1...am))))) (spec-0-necc (add-suffix spec-0 "-NECC")) (spec-1-necc (add-suffix spec-1 "-NECC")) (spec-2-necc (add-suffix spec-2 "-NECC")) (cdr-x-a1...am (loop$ for term in x-a1...am collect (if (eq term x) (list 'cdr term) term))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons algo 'nil) 'nil)) (cons ':induct (cons (cons algo x-a1...am) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons spec-0-necc (cons spec-1-necc (cons (cons ':instance (cons spec-2-necc (cons (cons y (cons (cons algo cdr-x-a1...am) 'nil)) 'nil))) 'nil))) 'nil)) 'nil)) 'nil))) (event (cons 'local (cons (cons 'defthm (cons name (cons (cons 'implies (cons (cons 'and (cons (cons spec-0 'nil) (cons (cons spec-1 'nil) (cons (cons spec-2 'nil) 'nil)))) (cons iorel-term 'nil))) (cons ':rule-classes (cons 'nil (cons ':hints (cons hints 'nil))))))) 'nil)))) (mv event name names-to-avoid))))