|
|
|---|
|
|
|
|---|
Concatenate 32 16-bit numbers together to form an 512-bit result.
(merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
→
resultFunction:
(defun merge-32-u16s (a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (declare (type (unsigned-byte 16) a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)) (declare (xargs :guard t)) (let ((__function__ 'merge-32-u16s)) (declare (ignorable __function__)) (mbe :logic (logapp* 16 (nfix a0) (nfix a1) (nfix a2) (nfix a3) (nfix a4) (nfix a5) (nfix a6) (nfix a7) (nfix a8) (nfix a9) (nfix a10) (nfix a11) (nfix a12) (nfix a13) (nfix a14) (nfix a15) (nfix a16) (nfix a17) (nfix a18) (nfix a19) (nfix a20) (nfix a21) (nfix a22) (nfix a23) (nfix a24) (nfix a25) (nfix a26) (nfix a27) (nfix a28) (nfix a29) (nfix a30) (nfix a31) 0) :exec (merge-2-u256s (the (unsigned-byte 256) (merge-16-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16)) (the (unsigned-byte 256) (merge-16-u16s a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))))))
Theorem:
(defthm acl2::natp-of-merge-32-u16s (b* ((result (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) (natp result)) :rule-classes :type-prescription)
Theorem:
(defthm unsigned-byte-p-512-of-merge-32-u16s (unsigned-byte-p 512 (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)) :rule-classes ((:rewrite :corollary (implies (>= (nfix n) 512) (unsigned-byte-p n (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :hints (("Goal" :in-theory (disable unsigned-byte-p))))))
Theorem:
(defthm merge-32-u16s-is-merge-unsigneds (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-unsigneds 16 (list (nfix a31) (nfix a30) (nfix a29) (nfix a28) (nfix a27) (nfix a26) (nfix a25) (nfix a24) (nfix a23) (nfix a22) (nfix a21) (nfix a20) (nfix a19) (nfix a18) (nfix a17) (nfix a16) (nfix a15) (nfix a14) (nfix a13) (nfix a12) (nfix a11) (nfix a10) (nfix a9) (nfix a8) (nfix a7) (nfix a6) (nfix a5) (nfix a4) (nfix a3) (nfix a2) (nfix a1) (nfix a0)))))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-32 (implies (nat-equiv a0 a0-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0-equiv))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-31 (implies (nat-equiv a1 a1-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1-equiv a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-30 (implies (nat-equiv a2 a2-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2-equiv a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-29 (implies (nat-equiv a3 a3-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3-equiv a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-28 (implies (nat-equiv a4 a4-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4-equiv a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-27 (implies (nat-equiv a5 a5-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5-equiv a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-26 (implies (nat-equiv a6 a6-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6-equiv a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-25 (implies (nat-equiv a7 a7-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7-equiv a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-24 (implies (nat-equiv a8 a8-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8-equiv a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-23 (implies (nat-equiv a9 a9-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9-equiv a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-22 (implies (nat-equiv a10 a10-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10-equiv a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-21 (implies (nat-equiv a11 a11-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11-equiv a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-20 (implies (nat-equiv a12 a12-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12-equiv a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-19 (implies (nat-equiv a13 a13-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13-equiv a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-18 (implies (nat-equiv a14 a14-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14-equiv a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-17 (implies (nat-equiv a15 a15-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15-equiv a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-16 (implies (nat-equiv a16 a16-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16-equiv a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-15 (implies (nat-equiv a17 a17-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17-equiv a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-14 (implies (nat-equiv a18 a18-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18-equiv a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-13 (implies (nat-equiv a19 a19-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19-equiv a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-12 (implies (nat-equiv a20 a20-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20-equiv a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-11 (implies (nat-equiv a21 a21-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21-equiv a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-10 (implies (nat-equiv a22 a22-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22-equiv a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-9 (implies (nat-equiv a23 a23-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23-equiv a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-8 (implies (nat-equiv a24 a24-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24-equiv a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-7 (implies (nat-equiv a25 a25-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26 a25-equiv a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-6 (implies (nat-equiv a26 a26-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27 a26-equiv a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-5 (implies (nat-equiv a27 a27-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28 a27-equiv a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-4 (implies (nat-equiv a28 a28-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29 a28-equiv a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-3 (implies (nat-equiv a29 a29-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30 a29-equiv a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-2 (implies (nat-equiv a30 a30-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31 a30-equiv a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))
Theorem:
(defthm nat-equiv-implies-equal-merge-32-u16s-1 (implies (nat-equiv a31 a31-equiv) (equal (merge-32-u16s a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) (merge-32-u16s a31-equiv a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))) :rule-classes (:congruence))