Generate the event that extends the defmapping table.
(defmapping-gen-ext-table name$ doma$ domb$ alpha$ beta$ unconditional$ thm-names$ call$ expansion) → event
Function:
(defun defmapping-gen-ext-table (name$ doma$ domb$ alpha$ beta$ unconditional$ thm-names$ call$ expansion) (declare (xargs :guard (and (symbolp name$) (pseudo-termfnp doma$) (pseudo-termfnp domb$) (pseudo-termfnp alpha$) (pseudo-termfnp beta$) (booleanp unconditional$) (symbol-symbol-alistp thm-names$) (pseudo-event-formp call$) (pseudo-event-formp expansion)))) (let ((__function__ 'defmapping-gen-ext-table)) (declare (ignorable __function__)) (b* ((alpha-image (cdr (assoc-eq :alpha-image thm-names$))) (beta-image (cdr (assoc-eq :beta-image thm-names$))) (beta-of-alpha (cdr (assoc-eq :beta-of-alpha thm-names$))) (alpha-of-beta (cdr (assoc-eq :alpha-of-beta thm-names$))) (alpha-injective (cdr (assoc-eq :alpha-injective thm-names$))) (beta-injective (cdr (assoc-eq :beta-injective thm-names$))) (doma-guard (cdr (assoc-eq :doma-guard thm-names$))) (domb-guard (cdr (assoc-eq :domb-guard thm-names$))) (alpha-guard (cdr (assoc-eq :alpha-guard thm-names$))) (beta-guard (cdr (assoc-eq :beta-guard thm-names$))) (info (make-defmapping-info :call$ call$ :expansion expansion :doma doma$ :domb domb$ :alpha alpha$ :beta beta$ :alpha-image alpha-image :beta-image beta-image :beta-of-alpha beta-of-alpha :alpha-of-beta alpha-of-beta :alpha-injective alpha-injective :beta-injective beta-injective :doma-guard doma-guard :domb-guard domb-guard :alpha-guard alpha-guard :beta-guard beta-guard :unconditional unconditional$))) (cons 'table (cons *defmapping-table-name* (cons (cons 'quote (cons name$ 'nil)) (cons (cons 'quote (cons info 'nil)) 'nil)))))))
Theorem:
(defthm pseudo-event-formp-of-defmapping-gen-ext-table (b* ((event (defmapping-gen-ext-table name$ doma$ domb$ alpha$ beta$ unconditional$ thm-names$ call$ expansion))) (pseudo-event-formp event)) :rule-classes :rewrite)