		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-block-item-list-empty

Equality lifting transformation of the empty list of block items.

Signature
(xeq-block-item-list-empty gin) → gout
Arguments: gin — Guard (ginp gin).
Returns: gout — Type (goutp gout).

This is introduced mainly for uniformity. It actually takes and returns no block item list, because there is only one empty block item list.

Definitions and Theorems

Function: xeq-block-item-list-empty

(defun xeq-block-item-list-empty (gin)
 (declare (xargs :guard (ginp gin)))
 (let ((__function__ 'xeq-block-item-list-empty))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (items nil)
    (hints
       '(("Goal" :in-theory '((:e insert)
                              block-item-list-empty-compustate-vars)
                 :use (block-item-list-empty-congruence))))
    ((mv thm-event thm-name thm-index)
     (gen-block-item-list-thm items items gin.vartys
                              gin.const-new gin.thm-index hints)))
   (make-gout :events (cons thm-event gin.events)
              :thm-index thm-index
              :thm-name thm-name
              :vartys gin.vartys))))

Theorem: goutp-of-xeq-block-item-list-empty

(defthm goutp-of-xeq-block-item-list-empty
  (b* ((gout (xeq-block-item-list-empty gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: xeq-block-item-list-empty-of-gin-fix-gin

(defthm xeq-block-item-list-empty-of-gin-fix-gin
  (equal (xeq-block-item-list-empty (gin-fix gin))
         (xeq-block-item-list-empty gin)))

Theorem: xeq-block-item-list-empty-gin-equiv-congruence-on-gin

(defthm xeq-block-item-list-empty-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (xeq-block-item-list-empty gin)
                  (xeq-block-item-list-empty gin-equiv)))
  :rule-classes :congruence)