		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-nonappcond-thms

Generate the theorems that are not applicability conditions.

Signature
(defmapping-gen-nonappcond-thms doma$ domb$ alpha$ beta$ a1...an b1...bm beta-of-alpha-thm$ alpha-of-beta-thm$ unconditional$ thm-names$ thm-enable$ appcond-thm-names wrld) → (mv local-events exported-events)
Arguments: doma$ — Guard (pseudo-termfnp doma$).; domb$ — Guard (pseudo-termfnp domb$).; alpha$ — Guard (pseudo-termfnp alpha$).; beta$ — Guard (pseudo-termfnp beta$).; a1...an — Guard (symbol-listp a1...an).; b1...bm — Guard (symbol-listp b1...bm).; beta-of-alpha-thm$ — Guard (booleanp beta-of-alpha-thm$).; alpha-of-beta-thm$ — Guard (booleanp alpha-of-beta-thm$).; unconditional$ — Guard (booleanp unconditional$).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; thm-enable$ — Guard (keyword-listp thm-enable$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; wrld — Guard (plist-worldp wrld).
Returns: local-events — A pseudo-event-form-listp.; exported-events — A pseudo-event-form-listp.

These can be no, one, or two injectivity theorems, based on the :beta-of-alpha-thm and :alpha-of-beta-thm inputs.

Definitions and Theorems

Function: defmapping-gen-nonappcond-thms

(defun defmapping-gen-nonappcond-thms
       (doma$ domb$ alpha$ beta$ a1...an b1...bm
              beta-of-alpha-thm$ alpha-of-beta-thm$
              unconditional$ thm-names$
              thm-enable$ appcond-thm-names wrld)
  (declare
       (xargs :guard (and (pseudo-termfnp doma$)
                          (pseudo-termfnp domb$)
                          (pseudo-termfnp alpha$)
                          (pseudo-termfnp beta$)
                          (symbol-listp a1...an)
                          (symbol-listp b1...bm)
                          (booleanp beta-of-alpha-thm$)
                          (booleanp alpha-of-beta-thm$)
                          (booleanp unconditional$)
                          (symbol-symbol-alistp thm-names$)
                          (keyword-listp thm-enable$)
                          (symbol-symbol-alistp appcond-thm-names)
                          (plist-worldp wrld))))
  (let ((__function__ 'defmapping-gen-nonappcond-thms))
    (declare (ignorable __function__))
    (b* (((mv alpha-inj-local-event-singleton-list-or-nil
              alpha-inj-exported-event-singleton-list-or-nil)
          (if beta-of-alpha-thm$
              (b* (((mv local-event exported-event)
                    (defmapping-gen-alpha-injective
                         doma$ alpha$ beta$ a1...an
                         b1...bm unconditional$ thm-names$
                         thm-enable$ appcond-thm-names wrld)))
                (mv (list local-event)
                    (list exported-event)))
            (mv nil nil)))
         ((mv beta-inj-local-event-singleton-list-or-nil
              beta-inj-exported-event-singleton-list-or-nil)
          (if alpha-of-beta-thm$
              (b* (((mv local-event exported-event)
                    (defmapping-gen-beta-injective
                         domb$ alpha$ beta$ a1...an
                         b1...bm unconditional$ thm-names$
                         thm-enable$ appcond-thm-names wrld)))
                (mv (list local-event)
                    (list exported-event)))
            (mv nil nil))))
      (mv (append alpha-inj-local-event-singleton-list-or-nil
                  beta-inj-local-event-singleton-list-or-nil)
          (append alpha-inj-exported-event-singleton-list-or-nil
                  beta-inj-exported-event-singleton-list-or-nil)))))