(in-package "ACL2")

(include-book "model") ; ACL2 model

(defun input-assumptions (n)
  (and (not (zp n))

; "Long op" is initiated at n and asserted at n+2.
       
       (equal (longop n) 1)
       (equal (longop (+ 1 n)) 1)))