		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Gout-no-thm

Build a gout without a theorem name.

Signature
(gout-no-thm gin) → gout
Arguments: gin — Guard (ginp gin).
Returns: gout — Type (goutp gout).

This is used for constructs for which we do not generate proofs yet. The events, theorem index, and variable-type map are taken from a gin, as they result from previous transformations.

Definitions and Theorems

Function: gout-no-thm

(defun gout-no-thm (gin)
  (declare (xargs :guard (ginp gin)))
  (let ((__function__ 'gout-no-thm))
    (declare (ignorable __function__))
    (b* (((gin gin) gin))
      (make-gout :events gin.events
                 :thm-index gin.thm-index
                 :thm-name nil
                 :vartys gin.vartys))))

Theorem: goutp-of-gout-no-thm

(defthm goutp-of-gout-no-thm
  (b* ((gout (gout-no-thm gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: gout-no-thm-of-gin-fix-gin

(defthm gout-no-thm-of-gin-fix-gin
  (equal (gout-no-thm (gin-fix gin))
         (gout-no-thm gin)))

Theorem: gout-no-thm-gin-equiv-congruence-on-gin

(defthm gout-no-thm-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (gout-no-thm gin)
                  (gout-no-thm gin-equiv)))
  :rule-classes :congruence)