		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-implementation

Simpadd0-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(simpadd0-process-inputs-and-gen-everything const-old const-old-present const-new const-new-present state) → (mv erp event)
Arguments: const-old-present — Guard (booleanp const-old-present).; const-new-present — Guard (booleanp const-new-present).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: simpadd0-process-inputs-and-gen-everything

(defun simpadd0-process-inputs-and-gen-everything
       (const-old const-old-present
                  const-new const-new-present state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp const-old-present)
                              (booleanp const-new-present))))
  (let ((__function__ 'simpadd0-process-inputs-and-gen-everything))
    (declare (ignorable __function__))
    (b* (((reterr) '(_))
         ((erp code-old const-new)
          (simpadd0-process-inputs
               const-old const-old-present
               const-new const-new-present (w state))))
      (simpadd0-gen-everything code-old const-new))))

Theorem: pseudo-event-formp-of-simpadd0-process-inputs-and-gen-everything.event

(defthm
 pseudo-event-formp-of-simpadd0-process-inputs-and-gen-everything.event
 (b* (((mv acl2::?erp acl2::?event)
       (simpadd0-process-inputs-and-gen-everything
            const-old const-old-present
            const-new const-new-present state)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)