3
(set-enforce-redundancy t)
5
(local (include-book "../support/support/rom-helpers"))
8
(declare (xargs :guard (integerp k)))
12
(local (in-theory (enable bvecp)))
15
(declare (xargs :guard t))
19
(defun check-array (name a dim1 dim2)
22
(and (bvecp (aref1 name a (1- dim1)) dim2)
23
(check-array name a (1- dim1) dim2))))
25
(defthm check-array-lemma-1
26
(implies (and (not (zp dim1))
27
(check-array name a dim1 dim2)
30
(bvecp (aref1 name a i) dim2))
33
(defthm check-array-lemma
34
(implies (and (bvecp i n)
36
(check-array name a (expt 2 n) dim2))
37
(bvecp (aref1 name a i) dim2))