Combine a direct abstract declarator into another.
(combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2) → dirabsdeclor
A direct abstract declarator has, except for the base case(s),
a slot
This function stores
Function:
(defun combine-dirabsdeclor-into-dirabsdeclor (dirabsdeclor1 dirabsdeclor2) (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor1) (dirabsdeclorp dirabsdeclor2)))) (declare (xargs :guard (dirabsdeclor-decl?-nil-p dirabsdeclor2))) (let ((__function__ 'combine-dirabsdeclor-into-dirabsdeclor)) (declare (ignorable __function__)) (b* ((dirabsdeclor1 (dirabsdeclor-fix dirabsdeclor1))) (dirabsdeclor-case dirabsdeclor2 :dummy-base (prog2$ (impossible) (irr-dirabsdeclor)) :paren (prog2$ (impossible) (irr-dirabsdeclor)) :array (change-dirabsdeclor-array dirabsdeclor2 :decl? (dirabsdeclor-fix dirabsdeclor1)) :array-static1 (change-dirabsdeclor-array-static1 dirabsdeclor2 :decl? dirabsdeclor1) :array-static2 (change-dirabsdeclor-array-static2 dirabsdeclor2 :decl? dirabsdeclor1) :array-star (change-dirabsdeclor-array-star dirabsdeclor2 :decl? dirabsdeclor1) :function (change-dirabsdeclor-function dirabsdeclor2 :decl? dirabsdeclor1)))))
Theorem:
(defthm dirabsdeclorp-of-combine-dirabsdeclor-into-dirabsdeclor (b* ((dirabsdeclor (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm combine-dirabsdeclor-into-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor1 (equal (combine-dirabsdeclor-into-dirabsdeclor (dirabsdeclor-fix dirabsdeclor1) dirabsdeclor2) (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2)))
Theorem:
(defthm combine-dirabsdeclor-into-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor1 (implies (dirabsdeclor-equiv dirabsdeclor1 dirabsdeclor1-equiv) (equal (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2) (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1-equiv dirabsdeclor2))) :rule-classes :congruence)
Theorem:
(defthm combine-dirabsdeclor-into-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor2 (equal (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 (dirabsdeclor-fix dirabsdeclor2)) (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2)))
Theorem:
(defthm combine-dirabsdeclor-into-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor2 (implies (dirabsdeclor-equiv dirabsdeclor2 dirabsdeclor2-equiv) (equal (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2) (combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2-equiv))) :rule-classes :congruence)