Generate the theorem for a character value notation.
(deftreeops-gen-charval-events charval info prefix) → (mv leafterm-thm-event event-alist)
Function:
(defun deftreeops-gen-charval-events (charval info prefix) (declare (xargs :guard (and (char-val-p charval) (deftreeops-charval-infop info) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-charval-events)) (declare (ignorable __function__)) (b* (((deftreeops-charval-info info) info) (matchp (deftreeops-match-pred prefix)) (matchp$ (packn-pos (list matchp "$") matchp)) (charval-desc (pretty-print-char-val charval)) (leafterm-thm-event (cons 'defruled (cons info.leafterm-thm (cons (cons 'implies (cons (cons matchp (cons 'cst (cons charval-desc 'nil))) '((equal (tree-kind cst) :leafterm)))) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons matchp$ '(tree-leafterm-when-match-numval/charval (:e element-kind) (:e member-equal))) 'nil)) 'nil))) 'nil) 'nil))))))) (mv leafterm-thm-event (list (cons info.leafterm-thm leafterm-thm-event))))))
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-charval-events.leafterm-thm-event (b* (((mv ?leafterm-thm-event ?event-alist) (deftreeops-gen-charval-events charval info prefix))) (pseudo-event-formp leafterm-thm-event)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-charval-events.event-alist (b* (((mv ?leafterm-thm-event ?event-alist) (deftreeops-gen-charval-events charval info prefix))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)