(value :q)

(lp)

(ld "packages.lisp")

;; Replace ... by the path to your ACL2 directory below:
(include-book ".../books/rtl/lib3/top")

(encapsulate ((unknown (key size n) t))
	     (local (defun unknown (key size n) (declare (ignore key size n)) 0))
	     (defthm bvecp-unknown (bvecp (unknown key size n) size)
	       :hints (("Goal" :in-theory (enable bvecp)))
	       :rule-classes (:type-prescription 
			      :rewrite
			      (:forward-chaining :trigger-terms ((unknown key size n))))))

(certify-book "model" 9)
:u

(certify-book "exec" 9)
:u

(certify-book "declarations" 9)
:u

(certify-book "constants" 9)
:u

(certify-book "inputs" 9)
:u

#| ; Doesn't help, even after including model, constants, inputs.
(defthm n-positive-lemma
  (implies (input-assumptions n)
           (not (zp n))))
|# ; |

(certify-book "pipe" 9)
:u

(certify-book "main" 9)