draft.lisp

(in-package :pvs)

(defun f_7 ()
  #'(lambda (x)
      (pvs__+ (pvs__+ (the integer x) (the integer x))
              (the integer
                   (let ((x#0 2))
                     (declare (type nil x#0))
                     (the integer x#0))))))
(defun _f_7 (x)
  (declare (type integer x))
  (pvs__+ (pvs__+ (the integer x) (the integer x))
          (the integer
               (let ((x#0 2))
                 (declare (type nil x#0))
                 (the integer x#0)))))
(defun f!_7 (x)
  (declare (type integer x))
  (pvs__+ (pvs__+ (the integer x) (the integer x))
          (the integer
               (let ((x#0 2))
                 (declare (type nil x#0))
                 (the integer x#0)))))
(defun incr_2 () #'(lambda (x) (pvs__+ (the integer x) 1)))
(defun _incr_2 (x)
  (declare (type integer x))
  (pvs__+ (the integer x) 1))
(defun incr!_2 (x)
  (declare (type integer x))
  (pvs__+ (the integer x) 1))
(defun a_2 () (the integer (_incr_2 10)))
(defun _a_2 () (the integer (_incr_2 10)))
(defun a!_2 () (the integer (incr!_2 10)))
(defun f_8 ()
  #'(lambda (t56504)
      (let ((A285 0))
        (let ((N284 0) (E283 t56504))
          (pvs-outer-array-update E283 A285 N284 10)))))
(defun _f_8 (t268)
  (let ((A271 0))
    (let ((N270 0) (E269 t268))
      (pvs-outer-array-update E269 A271 N270 10))))
(defun f!_8 (t268)
  (let ((LHS278 0))
    (let ((RHS276 0) (E277 (mk-fun-array t268 10)))
      (pvs-setf E277 LHS278 RHS276)
      E277)))
(defun e_0 () #'(lambda (x) (the fixnum x)))
(defun _e_0 (x) (declare (type fixnum x)) (the fixnum x))
(defun e!_0 (x) (declare (type fixnum x)) (the fixnum x))
(defun g () (_f_8 (_f_8 (e_0))))
(defun _g () (_f_8 (_f_8 (e_0))))
(defun g! () (f!_8 (f!_8 (e_0))))