		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-input-processing

Simpadd0-process-inputs

Process all the inputs.

Signature
(simpadd0-process-inputs const-old const-old-present const-new const-new-present wrld) → (mv erp code-old const-new$)
Arguments: const-old-present — Guard (booleanp const-old-present).; const-new-present — Guard (booleanp const-new-present).; wrld — Guard (plist-worldp wrld).
Returns: code-old — Type (code-ensemblep code-old).; const-new$ — Type (symbolp const-new$).

Definitions and Theorems

Function: simpadd0-process-inputs

(defun simpadd0-process-inputs
       (const-old const-old-present
                  const-new const-new-present wrld)
  (declare (xargs :guard (and (booleanp const-old-present)
                              (booleanp const-new-present)
                              (plist-worldp wrld))))
  (let ((__function__ 'simpadd0-process-inputs))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-code-ensemble) nil)
         ((erp code-old)
          (process-const-old const-old const-old-present wrld))
         ((erp const-new)
          (process-const-new const-new const-new-present)))
      (retok code-old const-new))))

Theorem: code-ensemblep-of-simpadd0-process-inputs.code-old

(defthm code-ensemblep-of-simpadd0-process-inputs.code-old
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-old-present
                                 const-new const-new-present wrld)))
    (code-ensemblep code-old))
  :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-process-inputs.const-new$

(defthm symbolp-of-simpadd0-process-inputs.const-new$
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-old-present
                                 const-new const-new-present wrld)))
    (symbolp const-new$))
  :rule-classes :rewrite)

Theorem: code-ensemble-unambp-of-simpadd0-process-inputs

(defthm code-ensemble-unambp-of-simpadd0-process-inputs
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-old-present
                                 const-new const-new-present wrld)))
    (implies (not erp)
             (code-ensemble-unambp code-old))))

Theorem: code-ensemble-annop-of-simpadd0-process-inputs

(defthm code-ensemble-annop-of-simpadd0-process-inputs
  (b* (((mv acl2::?erp ?code-old ?const-new$)
        (simpadd0-process-inputs const-old const-old-present
                                 const-new const-new-present wrld)))
    (implies (not erp)
             (code-ensemble-annop code-old))))