other
(in-package "GL")
other
(include-book "glcp-geval")
other
(include-book "rewrite-tables")
other
(def-unify glcp-generic-geval-ev glcp-generic-geval-ev-alist)
other
(def-meta-extract glcp-generic-geval-ev glcp-generic-geval-ev-lst)
other
(define good-rewrite-rulesp (rules) (if (atom rules) t (and (glcp-generic-geval-ev-theoremp (rewrite-rule-term (car rules))) (good-rewrite-rulesp (cdr rules)))))
other
(def-functional-instance good-rewrite-rulesp-of-fn-branch-merge-rules
mextract-good-rewrite-rulesp-of-fn-branch-merge-rules
((mextract-ev glcp-generic-geval-ev) (mextract-ev-lst glcp-generic-geval-ev-lst)
(mextract-ev-falsify glcp-generic-geval-ev-falsify)
(mextract-global-badguy glcp-generic-geval-ev-meta-extract-global-badguy)
(mextract-good-rewrite-rulesp good-rewrite-rulesp))
:hints ((and stable-under-simplificationp
'(:in-theory (enable glcp-generic-geval-ev-of-fncall-args
glcp-generic-geval-ev-of-nonsymbol-atom
good-rewrite-rulesp)))))
other
(def-functional-instance good-rewrite-rulesp-of-fn-rewrite-rules
mextract-good-rewrite-rulesp-of-fn-rewrite-rules
((mextract-ev glcp-generic-geval-ev) (mextract-ev-lst glcp-generic-geval-ev-lst)
(mextract-ev-falsify glcp-generic-geval-ev-falsify)
(mextract-global-badguy glcp-generic-geval-ev-meta-extract-global-badguy)
(mextract-good-rewrite-rulesp good-rewrite-rulesp))
:hints ((and stable-under-simplificationp
'(:in-theory (enable glcp-generic-geval-ev-of-fncall-args
glcp-generic-geval-ev-of-nonsymbol-atom
good-rewrite-rulesp)))))