Transform a label.
Function:
(defun simpadd0-label (label) (declare (xargs :guard (labelp label))) (let ((__function__ 'simpadd0-label)) (declare (ignorable __function__)) (label-case label :name (label-fix label) :const (label-const (simpadd0-const-expr label.unwrap)) :default (label-fix label))))
Theorem:
(defthm labelp-of-simpadd0-label (b* ((new-label (simpadd0-label label))) (labelp new-label)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-label-of-label-fix-label (equal (simpadd0-label (label-fix label)) (simpadd0-label label)))
Theorem:
(defthm simpadd0-label-label-equiv-congruence-on-label (implies (c$::label-equiv label label-equiv) (equal (simpadd0-label label) (simpadd0-label label-equiv))) :rule-classes :congruence)