#|
 Copyright (C) 1993 by Matt Wilding.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Matt Wilding PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Matt Wilding BE LIABLE TO YOU FOR ANY DAMAGES,
 ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
(note-lib "piton" t)
;; NIM Piton proof
;; Matt Wilding 4-15-92

;; modified 7-92 to work on Piton library

;; This script takes 10 hours to run on a 64 meg Sparc2

;; This work is described in Technical Report #78.  A presentation
;; about this work was made at the CLI research review in April 92.

#|
Nim is a game played with piles of matches.  Two opponents alternate
taking at least one match from exactly one pile until there are no
matches left.  The player who takes the last match loses.

Piton is an assembly-level language with a formal semantics and a
verified compiler.  Piton is described in CLI tech report #22.  One of
the machines to which Piton is targeted is FM9001, a microprocessor
that has a formal semantics and that has been fabricated.

This proof script leads NQTHM to a proof that a Piton program that
"plays" Nim does so optimally.  Informally, this means

  a) A Piton program (see function CM-PROG) when run on the Piton
  interpreter and given as input a reasonable Nim state yields a new
  Nim state equal to what is calculated by function COMPUTER-MOVE.  
  (See event COMPUTER-MOVE-IMPLEMENTED.)

  b) COMPUTER-MOVE generates valid moves.  That is, it removes at
  least one match from exactly one pile.  (VALID-MOVEP-COMPUTER-MOVE)

  c) Depth-first search of the state space of all possible moves is
  used to define what is meant by optimal Nim play.  Exhaustive search
  is used to find if there is a strategy for a Nim player to ensures
  eventual victory from the current Nim state.  An optimal strategy
  transforms any state for which there exists such a winning strategy
  into a state from which exhaustive search can find no winning
  strategy.  
     Exhaustive search of all possible moves from a NIM state is 
  formalized in the function WSP.  The optimalilty of the strategy
  COMPUTER-MOVE is proved in the event COMPUTER-MOVE-WORKS.

  d) The FM9001 Piton compiler correctness theorem assumes that the 
  Piton state that is to be run contains valid Piton code, fit into 
  an FM9001's memory, and use constants of word size 32.  A Piton 
  state (used in the Indiana test described below) was constructed
  that contains the Nim program, and is proved to meet the compiler
  correctness constraints (CM-PROG-FM9001-LOADABLE)

The algorithm used by the program is non-obvious and very efficient,
avoiding the need to search.  (I invented the programming trick only
to subsequently discover that it has been known since the beginning
of the century.)  See tech report #78 for a description.

(Constant bounds on the number of Piton instructions executed while
running this program have been proved using PC-NQTHM.  These events
are not included in this NQTHM-processable script, but the theorem is
included in comments later in this file for completeness.)

This script was developed using only those events from the Piton
library necessary to define the interpreter and the naturals library.
In July 92 it was modified somewhat to "fit" onto the Piton library
that sits on top of the FM9001 library.  The immediate motivation was
to make it easier to include in the upcoming NQTHM-1992 proveall
release being put together by Boyer.  The Piton library contains the
events of the FM9001 library.  The FM9001 library contains an older
version of the naturals library (though not explicitly with a
note-lib).  Thus, this script requires only the Piton library.

In May 92, in consultation with researchers at Indiana University, I
compiled the Nim Piton program for the FM9001 and sent the image to
Indiana.  They ran the image and generated an optimal NIM move on a
fabricated FM9001 they had wired up.  The intial image and part of the
resulting image is included in a comment at the end of this script.  A
non-trivial program compiled using a reasonably-complex compiler for a
small microprocessor worked without any conventional testing done on
any of the components, and everyone was pleased but not surprised.

|#



(set-status addition-on addition ((otherwise enable)))
(set-status multiplication-on multiplication ((otherwise enable)))
(set-status remainders-on remainders ((otherwise enable)))
(set-status quotients-on quotients ((otherwise enable)))
(set-status exponentiation-on exponentiation ((otherwise enable)))
(set-status logs-on logs ((otherwise enable)))
(set-status gcds-on gcds ((otherwise enable)))

(defn clock-plus (x y)
  (plus x y))

(prove-lemma p-add1 (rewrite)
	     (equal
	      (p p0 (add1 n))
	      (p (p-step p0) n))
	     ((disable p-step)))

(prove-lemma p-0 (rewrite)
	     (implies
	      (zerop n)
	      (equal (p p0 n) p0)))

(prove-lemma clock-plus-function (rewrite)
	     (equal 
	      (p p0 (clock-plus x y))
	      (p (p p0 x) y))
	     ((induct (p p0 x))
	      (disable p p-step)))

(disable p-add1)

(prove-lemma clock-plus-add1 (rewrite)
	     (equal
	      (p p0 (clock-plus (add1 x) y))
	      (p p0 (add1 (clock-plus x y)))))

(disable clock-plus)

(prove-lemma clock-plus-0 (rewrite)
	     (implies
	      (zerop x)
	     (equal
	      (clock-plus x y)
	      (fix y)))
	     ((enable clock-plus)))

(prove-lemma fix-clock-plus (rewrite)
	     (equal
	      (fix (clock-plus x y))
	      (clock-plus x y))
	     ((enable clock-plus)))

(prove-lemma p-step1-opener (rewrite)
  (equal (p-step1 (cons opcode operands) p)
	 (if (p-ins-okp (cons opcode operands) p)
	     (p-ins-step (cons opcode operands) p)
	     (p-halt p (x-y-error-msg 'p opcode))))

  ((disable p-ins-okp p-ins-step)))

(disable p-step1)

(prove-lemma p-opener (rewrite)
  (and (equal (p s 0) s)
       (equal (p (p-state pc ctrl temp prog data max-ctrl max-temp word-size 
			  psw)
		 (add1 n))
	      (p (p-step (p-state pc ctrl temp prog data max-ctrl max-temp 
				  word-size psw))
		 n)))
  ((disable p-step)))

(disable p)

(defn at-least-morep (base delta value)
  (not (lessp value (plus base delta))))

(prove-lemma at-least-morep-normalize (rewrite)
	     (and
	      (equal
	       (at-least-morep (add1 base) delta value)
	       (at-least-morep base (add1 delta) value))
	      (equal
	       (at-least-morep base (add1 delta) (add1 value))
	       (at-least-morep base delta value))))

(prove-lemma at-least-morep-linear (rewrite)
	     (implies
	      (and
	       (at-least-morep base d1 value)
	       (not (lessp d1 d2)))
	      (at-least-morep base d2 value)))

(prove-lemma lessp-as-at-least-morep (rewrite)
	     (implies
	      (at-least-morep base delta value)
	      (and
	       (equal
		(lessp value x)
		(not (at-least-morep x 0 value)))
	       (equal
		(lessp x value)
		(at-least-morep x 1 value)))))

(disable at-least-morep)

(defn nat-to-bv (nat size)
  (if (zerop size)
      nil
    (if (lessp nat (exp 2 (sub1 size)))
	(cons 0 (nat-to-bv nat (sub1 size)))
      (cons 1 (nat-to-bv (difference nat (exp 2 (sub1 size))) 
			 (sub1 size))))))

(defn nat-to-bv-state (state size)
  (if (listp state)
      (cons (nat-to-bv (car state) size)
	    (nat-to-bv-state (cdr state) size))
    nil))

;; a more elegant way to write this program would be to use the
;; bit-vector of all 0's initially, then xor all the elements of
;; the array.  But we don't want a pointer to memory to
;; ever have an improper value, so we write things this way

(defn xor-bvs-program nil
  '(xor-bvs (vecs-addr numvecs)
	      nil
	      (push-local vecs-addr)
	      (fetch)
	      (push-local numvecs)
	      (sub1-nat)
	      (pop-local numvecs)
      (dl loop ()
	      (push-local numvecs))
	      (test-nat-and-jump zero done)
	      (push-local numvecs)
	      (sub1-nat)
	      (pop-local numvecs)
	      (push-local vecs-addr)
	      (push-constant (nat 1))
	      (add-addr)
	      (set-local vecs-addr)
	      (fetch)
	      (xor-bitv)
	      (jump loop)
     (dl done () 
	      (ret))))

(defn bit-vectors-piton (array size)
  (if (listp array)
      (and
       (listp (car array))
       (equal (caar array) 'bitv)
       (bit-vectorp (cadar array) size)
       (equal (cddar array) nil)
       (bit-vectors-piton (cdr array) size))
    (equal array nil)))

(defn array (name segment) 
  (cdr (assoc name segment)))

;; vecs is name of state
(defn xor-bvs-input-conditionp (p0)
  (and
   (equal (car (top (p-temp-stk p0))) 'nat)
   (equal (car (top (cdr (p-temp-stk p0)))) 'addr)
   (equal (cdadr (top (cdr (p-temp-stk p0)))) 0)
   (listp (cadr (top (cdr (p-temp-stk p0)))))
   (equal (cddr (top (p-temp-stk p0))) nil)
   (equal (cddr (top (cdr (p-temp-stk p0)))) nil)
   (definedp (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0))
   (bit-vectors-piton (array (caadr (top (cdr (p-temp-stk p0))))
			     (p-data-segment p0))
		      (p-word-size p0))
   (equal (cadr (top (p-temp-stk p0)))
	  (length (array (caadr (top (cdr (p-temp-stk p0))))
			 (p-data-segment p0))))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   4 (p-max-ctrl-stk-size p0))
   (at-least-morep (length (p-temp-stk p0)) 
		   2 (p-max-temp-stk-size p0))
   (not (zerop (untag (top (p-temp-stk p0)))))
   (lessp (untag (top (p-temp-stk p0))) (exp 2 (p-word-size p0)))
   (listp (p-ctrl-stk p0))))

; time to run loop
(defn xor-bvs-clock-loop (numvecs)
  (if (zerop numvecs)
      3
    (plus 12 (xor-bvs-clock-loop (sub1 numvecs)))))

; time to run xor-bvs, including call and ret

(defn xor-bvs-clock (numvecs)
  (plus 6 (xor-bvs-clock-loop (sub1 numvecs))))

(defn xor-bvs-array (current array n array-size)
  (if (zerop n)
      current
    (xor-bvs-array
     (xor-bitv current (untag (get (difference array-size n) array)))
     array (sub1 n) array-size)))
     
(prove-lemma lessp-1-exp (rewrite)
	     (equal
	      (lessp 1 (exp a b))
	      (and (lessp 1 a) (not (zerop b))))
	     ((enable exp)))

(prove-lemma bit-vectors-piton-means (rewrite)
	     (implies
	      (and
	       (bit-vectors-piton state size)
	       (lessp p (length state)))
	      (and
	       (equal (car (get p state)) 'bitv)
	       (listp (get p state))
	       (bit-vectorp (cadr (get p state)) size)
	       (equal (cddr (get p state)) nil))))

(defn xor-bvs-loop-correctness-general-induct (i current n s data-segment)
  (if (zerop i) t
    (xor-bvs-loop-correctness-general-induct
     (sub1 i)
     (xor-bitv 
      current 
      (cadr (get (difference n i) (array s data-segment))))
     n s data-segment)))


;; in Piton library
;(prove-lemma bit-vectorp-xor-bitv (rewrite)
;	     (implies
;	      (and
;	       (bit-vectorp x size)
;	       (bit-vectorp y size))
;	      (bit-vectorp (xor-bitv x y) size)))

(enable bit-vectorp-xor-bitv)

(prove-lemma xor-bvs-loop-correctness-general nil
	     (implies
	      (and
	       (lessp (length (array s data-segment)) 
		      (exp 2 word-size))
	       (not (zerop word-size))
	       (listp ctrl-stk)
	       (bit-vectors-piton (array s data-segment) word-size)
	       (at-least-morep (length temp-stk) 3 max-temp-stk-size)
	       (equal (definition 'xor-bvs prog-segment)
		      (xor-bvs-program))
	       (definedp s data-segment)
	       (numberp i)
	       (lessp i n)
	       (bit-vectorp current word-size)
	       (equal n (length (array s data-segment))))
	      (equal
	       (p (p-state '(pc (xor-bvs . 5))
			   (cons (list
				  (list 
				   (cons 'vecs-addr 
					 (list 'addr 
					       (cons 
						s 
						(sub1
						 (difference n i)))))
				   (cons 'numvecs (list 'nat i)))
				  ret-pc)
				 ctrl-stk)
			   (cons (list 'bitv current)
				 temp-stk)
			   prog-segment
			   data-segment
			   max-ctrl-stk-size
			   max-temp-stk-size
			   word-size
			   'run)
		  (xor-bvs-clock-loop i))
	       (p-state ret-pc
			ctrl-stk
			(cons (list 'bitv (xor-bvs-array 
					   current 
					   (array s data-segment)
					   i n))
				    temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((induct (xor-bvs-loop-correctness-general-induct 
		       i current n s data-segment))))

(prove-lemma difference-x-sub1-x-better (rewrite)
	     (equal (difference x (sub1 x))
		    (if (lessp 0 x) 1 0)))

(prove-lemma xor-bvs-loop-correctness nil
	     (implies
	      (and
	       (lessp (length (array s data-segment)) 
		      (exp 2 word-size))
	       (not (zerop word-size))
	       (listp ctrl-stk)
	       (bit-vectors-piton (array s data-segment) word-size)
	       (at-least-morep (length temp-stk) 3 max-temp-stk-size)
	       (equal (definition 'xor-bvs prog-segment)
		      (xor-bvs-program))
	       (definedp s data-segment)
	       (lessp 0 n)
	       (bit-vectorp current word-size)
	       (equal n (length (array s data-segment))))
	      (equal
	       (p (p-state '(pc (xor-bvs . 5))
			   (cons (list
				  (list 
				   (cons 'vecs-addr 
					 (list 'addr (cons s 0)))
				   (cons 'numvecs 
					 (list 'nat (sub1 n))))
				  ret-pc)
				 ctrl-stk)
			   (cons (list 'bitv current) temp-stk)
			   prog-segment
			   data-segment
			   max-ctrl-stk-size
			   max-temp-stk-size
			   word-size
			   'run)
		  (xor-bvs-clock-loop (sub1 n)))
	       (p-state ret-pc
			ctrl-stk
			(cons (list 'bitv (xor-bvs-array 
					   current 
					   (array s data-segment)
					   (sub1 n) n))
				    temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((use (xor-bvs-loop-correctness-general (i (sub1 n))))))

(prove-lemma exp-0 (rewrite)
	     (implies
	      (zerop x)
	      (and (equal (exp x y) (if (zerop y) 1 0))
		   (equal (exp y x) 1)))
	     ((enable exp)))

(prove-lemma bit-vectors-piton-means-more (rewrite)
	     (implies
	      (and
	       (listp x)
	       (bit-vectors-piton x size))
	      (equal
	       (LIST 'BITV (CADAR x))
	       (car x))))

;; xor-bvs of an array of at least one bit vector
(defn xor-bvs (array)
  (if (listp array)
      (xor-bitv (car array) (xor-bvs (cdr array)))
    nil))


(defn untag-array (array)
  (if (listp array)
      (cons (untag (car array))
	    (untag-array (cdr array)))
    nil))

(prove-lemma bit-vectorp-get (rewrite)
	     (implies
	      (bit-vectors-piton array size)
	      (equal
	       (bit-vectorp (untag (get n array)) size)
	       (lessp n (length array)))))

;(prove-lemma difference-sub1-arg2 (rewrite)
;	     (equal
;	      (difference a (sub1 n))
;	      (if (zerop n) (fix a)
;		(if (lessp a n) 0 (add1 (difference a n))))))
(enable difference-sub1-arg2)

(prove-lemma xor-bitv-commutative (rewrite)
	     (implies
	      (equal (length a) (length b))
	      (equal (xor-bitv a b) (xor-bitv b a))))

(prove-lemma xor-bitv-commutative2 (rewrite)
	     (implies
	      (equal (length a) (length b))
	      (equal (xor-bitv a (xor-bitv b c))
		     (xor-bitv b (xor-bitv a c)))))

(prove-lemma xor-bitv-associative (rewrite)
	     (implies
	      (equal (length a) (length b))
	      (equal (xor-bitv (xor-bitv a b) c)
		     (xor-bitv a (xor-bitv b c)))))


(prove-lemma length-from-bit-vectorp (rewrite)
	     (implies
	      (bit-vectorp x s)
	      (equal (length x) (fix s))))

(prove-lemma length-xor-bitv (rewrite)
	     (equal
	      (length (xor-bitv a b))
	      (length a)))

(prove-lemma length-cadr-get-bit-vectors-piton (rewrite)
	     (implies
	      (and
	       (bit-vectors-piton x l)
	       (lessp i (length x)))
	      (equal (length (cadr (get i x))) (fix l))))

(prove-lemma equal-xor-bitv-x-x (rewrite)
	     (implies
	      (and 
	       (bit-vectorp b (length a))
	       (bit-vectorp c (length a)))
	      (equal
	       (equal (xor-bitv a b) (xor-bitv a c))
	       (equal b c))))

(defn bit-vectorp-induct (size a b)
  (if (zerop size) t
    (bit-vectorp-induct (sub1 size) (cdr a) (cdr b))))

(prove-lemma bit-vectorp-xor-bitv2 (rewrite)
	     (equal 
	      (bit-vectorp (xor-bitv a b) size)
	      (equal (length a) (fix size)))
	     ((induct (bit-vectorp-induct size a b))))

	      
(defn bit-vectorsp (bvs size)
  (if (listp bvs)
      (and
       (bit-vectorp (car bvs) size)
       (bit-vectorsp (cdr bvs) size))
    (equal bvs nil)))

(prove-lemma length-xor-bvs (rewrite)
	     (implies
	      (bit-vectorsp bvs (length (car bvs)))
	      (equal (length (xor-bvs bvs)) (length (car bvs)))))

(prove-lemma bit-vectorsp-untag (rewrite)
	     (implies
	      (bit-vectors-piton x s)
	      (bit-vectorsp (untag-array x) s)))

(prove-lemma bit-vectorsp-cdr-untag (rewrite)
	     (implies
	      (bit-vectors-piton (cdr x) s)
	      (bit-vectorsp (cdr (untag-array x)) s)))

;; actually part of npiton-defs, but not supporter of p
;;
;(DEFN NTHCDR
;      (N L)
;      (IF (ZEROP N)
;          L
;          (NTHCDR (SUB1 N) (CDR L))))
(enable nthcdr)

(prove-lemma bit-vectorsp-nthcdr (rewrite)
	     (implies
	      (and
	       (bit-vectorsp x s)
	       (lessp n (length x)))
	      (bit-vectorsp (nthcdr n x) s))
	     ((enable nthcdr)))

(prove-lemma bit-vectorp-xor-bvs (rewrite)
	     (implies
	      (and
	       (bit-vectorsp x size)
	       (listp x))
	      (bit-vectorp (xor-bvs x) size)))

(prove-lemma length-untag-array (rewrite)
	     (equal (length (untag-array x)) (length x)))

;(prove-lemma listp-nthcdr (rewrite)
;	     (equal
;	      (listp (nthcdr n x))
;	      (lessp n (length x)))
;	     ((enable nthcdr)))
(enable listp-nthcdr)

(prove-lemma nthcdr-open (rewrite)
	     (implies
	      (lessp n (length x))
	      (equal
	       (nthcdr n x)
	       (cons (get n x) (nthcdr (add1 n) x))))
	     ((enable nthcdr)))

(prove-lemma get-untag-array (rewrite)
	     (implies
	      (lessp n (length x))
	      (equal
	       (get n (untag-array x))
	       (cadr (get n x)))))


(prove-lemma equal-xor-bitv-x-x-special (rewrite)
	     (implies
	      (and 
	       (bit-vectorp b (length a))
	       (bit-vectorp (xor-bitv z c) (length a)))
	      (equal
	       (equal (xor-bitv a b) (xor-bitv z (xor-bitv a c)))
	       (equal b (xor-bitv z c)))))

(defn fix-bit (b)
  (if (equal b 0) 0 1))

(prove-lemma xor-bitv-0 (rewrite)
	     (and
	      (equal (xor-bit x 0) (fix-bit x))
	      (equal (xor-bit 0 x) (fix-bit x))))

(prove-lemma xor-bitv-nlistp (rewrite)
	     (implies
	      (not (listp c))
	      (equal (xor-bitv a (xor-bitv b c))
		     (xor-bitv a b))))

(prove-lemma xor-bitv-nlistp2 (rewrite)
	     (implies
	      (and
	       (bit-vectorp a b)
	       (not (listp c)))
	      (equal (xor-bitv a c) a)))

(prove-lemma xor-bvs-array-rewrite (rewrite)
	     (implies
	      (and
	       (bit-vectors-piton array (length current))
	       (bit-vectorp current (length current))
	       (lessp n (length array))
	       (equal (length array) as))
	     (equal
	      (xor-bvs-array current array n as)
	      (xor-bitv current 
			(xor-bvs 
			 (nthcdr (difference as n) 
				 (untag-array array))))))
	     ((induct (xor-bvs-array current array n as))
	      (enable nthcdr)))

;; in npiton-defs but not a supporter of p
;(PROVE-LEMMA EQUAL-LENGTH-0
;             (REWRITE)
;             (EQUAL (EQUAL (LENGTH X) '0)
;                    (NLISTP X)))
(enable equal-length-0)

(prove-lemma correctness-of-xor-bvs-helper
 (rewrite)
 (implies
  (and (equal p0
              (p-state pc ctrl-stk
                       (append (list (tag 'nat numvecs)
                                     (tag 'addr (cons state 0)))
                               temp-stk)
                       prog-segment data-segment max-ctrl-stk-size
                       max-temp-stk-size word-size 'run))
       (equal (p-current-instruction p0)
              '(call xor-bvs))
       (equal (definition 'xor-bvs prog-segment)
              (xor-bvs-program))
       (xor-bvs-input-conditionp p0))
  (equal
   (p p0 (xor-bvs-clock numvecs))
   (p-state (add1-addr pc)
            ctrl-stk
            (cons (list 'bitv
                        (xor-bvs-array (untag (car (array state data-segment)))
                                       (array state data-segment)
                                       (sub1 numvecs)
                                       numvecs))
                  temp-stk)
            prog-segment data-segment max-ctrl-stk-size max-temp-stk-size
            word-size 'run)))
 ((use
   (xor-bvs-loop-correctness (current (untag (car (array state data-segment))))
                             (s state)
                             (n numvecs)
                             (ret-pc (add-addr pc 1))))))

(prove-lemma length-cadar-bvs (rewrite)
	     (implies
	      (and
	       (bit-vectors-piton x s)
	       (listp x))
	      (equal (length (cadar x)) (fix s))))

(prove-lemma bit-vectorp-from-bit-vectors-piton (rewrite)
	     (implies
	      (bit-vectors-piton x s)
	      (and
	       (equal
		(bit-vectorp (cadar x) s)
		(listp x))
	       (equal
		(bit-vectorp (cadr (get n x)) s)
		(lessp n (length x))))))

(prove-lemma nthcdr-1 (rewrite)
	     (equal 
	      (nthcdr 1 a)
	      (cdr a))
	     ((enable nthcdr)))

(prove-lemma listp-untag-array (rewrite)
	     (equal
	      (listp (untag-array x))
	      (listp x)))

(prove-lemma xor-bvs-input-conditionp-means-xor-bvs-hack (rewrite)
	     (implies
	      (and
	       (xor-bvs-input-conditionp 
			  (p-state 
			  pc
			  ctrl-stk
			  (cons (list 'nat numvecs)
				(cons (list 'addr (cons state 0))
				      temp-stk))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (lessp 0 word-size))
	      (equal
	       (xor-bvs-array 
		(untag 
		 (car (array state data-segment)))
		(array state data-segment)
		(sub1 numvecs) numvecs)
	       (xor-bvs (untag-array (array state data-segment)))))
	     ((enable nthcdr)))

(prove-lemma correctness-of-xor-bvs (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons n (cons s temp-stk))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (lessp 0 word-size)
	       (equal (p-current-instruction p0) '(call xor-bvs))
	       (equal (definition 'xor-bvs prog-segment)
		      (xor-bvs-program))
	       (xor-bvs-input-conditionp p0))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons n (cons s temp-stk))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (xor-bvs-clock (cadr n)))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'bitv 
				    (xor-bvs (untag-array 
					      (array (caadr s) data-segment))))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((disable xor-bvs-clock)
	      (use (correctness-of-xor-bvs-helper 
		    (state (caadr s)) (numvecs (cadr n)))
		   (xor-bvs-input-conditionp-means-xor-bvs-hack
		    (state (caadr s)) (numvecs (cadr n))))))

(defn example-xor-bvs-p-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (arr . 0)))
			(push-constant (nat 3))
			(call xor-bvs)
			(ret))
		 (xor-bvs-program))
	   '((arr (bitv (0 1 0 1 1 0 0 1))
		  (bitv (0 0 0 0 0 0 0 1))
		  (bitv (0 1 1 0 1 0 0 1))))
	   10
	   8
	   8
	   'run))

;;;; push-1-vector 
;; Piton currently does not provide any mechanism for creating a
;; bit vector except as an operation on other bit vectors.  Until
;; this apparent flaw is fixed, we'll write our program as a
;; function of the word size.

(defn one-bit-vector (wordsize)
  (if (lessp wordsize 2)
      (list 1)
    (cons 0 (one-bit-vector (sub1 wordsize)))))

(defn push-1-vector-program (wordsize)
  (list 'push-1-vector nil nil
	(list 'push-constant (list 'bitv (one-bit-vector wordsize)))
	(list 'ret)))
   

(defn example-push-1-vector-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(call push-1-vector)
			(ret))
		 (push-1-vector-program 8))
	   nil
	   10
	   8
	   8
	   'run))

(defn push-1-vector-input-conditionp (p0)
  (and
   (not (lessp (p-max-ctrl-stk-size p0)
	       (plus 2 (p-ctrl-stk-size (p-ctrl-stk p0)))))
   (not (lessp (p-max-temp-stk-size p0) 
	       (plus 1 (length (p-temp-stk p0)))))
   (listp (p-ctrl-stk p0))))

;(prove-lemma length-append (rewrite)
;	     (equal
;	      (length (append a b))
;	      (plus (length a) (length b))))
(enable length-append)

(prove-lemma equal-assoc-cons (rewrite)
	     (implies
	      (equal (assoc k a) (cons x y))
	      (and
	       (equal (car (assoc k a)) x)
	       (equal (cdr (assoc k a)) y))))

(prove-lemma correctness-of-push-1-vector (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  temp-stk
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) 
		      '(call push-1-vector))
	       (equal (definition 'push-1-vector prog-segment)
		      (push-1-vector-program word-size))
	       (push-1-vector-input-conditionp p0))
	      (equal
	       (p p0 3)
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'bitv (one-bit-vector word-size))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run))))

;;;; nat-to-bv

(defn nat-to-bv-program nil
  '(nat-to-bv (value)
	      ((current-bit (nat 0)) (temp (nat 0)))
	      (call push-1-vector)
	      (pop-local current-bit)
	      (call push-1-vector)
	      (rsh-bitv)
	 (dl loop ()
	      (push-local value))
	      (test-nat-and-jump zero done)
	      (push-local value)
	      (div2-nat)
	      (pop-local temp)
	      (pop-local value)
	      (push-local temp)
	      (test-nat-and-jump zero lab)
	      (push-local current-bit)
	      (xor-bitv)
	 (dl lab ()
	      (push-local current-bit))
	      (lsh-bitv)
	      (pop-local current-bit)
	      (jump loop)
         (dl done ()
	      (ret))))

(defn example-nat-to-bv-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (nat 86))
			(call nat-to-bv)
			(ret))
		 (push-1-vector-program 8)
		 (nat-to-bv-program))
	   nil
	   10
	   8
	   8
	   'run))

(defn zero-bit-vector (size)
  (if (zerop size) nil
    (cons 0 (zero-bit-vector (sub1 size)))))


(defn nat-to-bv2-helper (value current-bit bit-vector)
  (if (zerop value)
      bit-vector
    (nat-to-bv2-helper (quotient value 2) 
		       (append (cdr current-bit) (list 0))
		       (if (equal (remainder value 2) 1) 
			   (xor-bitv current-bit bit-vector)
			 bit-vector))))

(defn nat-to-bv2 (value size)
  (nat-to-bv2-helper value (one-bit-vector size) 
		     (zero-bit-vector size)))

(defn nat-to-bv-loop-clock (value)
  (if (zerop value)
      3
    (plus
     (if (equal (remainder value 2) 0) 12 14)
     (nat-to-bv-loop-clock (quotient value 2)))))
	 
(defn correctness-of-nat-to-bv-general-induct (value cb temp bv)
  (if (zerop value) t
    (correctness-of-nat-to-bv-general-induct
     (quotient value 2) 
     (append (cdr cb) (list 0))
     (list 'nat (remainder value 2))
     (if (equal (remainder value 2) 0) bv (xor-bitv bv cb)))))

(prove-lemma lessp-remainder-simple (rewrite)
	     (implies
	      (not (zerop y))
	      (lessp (remainder x y) y)))

(prove-lemma lessp-exp-simple (rewrite)
	     (implies
	      (and
	       (lessp x y)
	       (not (zerop z)))
	      (lessp x (exp y z)))
	     ((enable exp)))

(prove-lemma lessp-1 (rewrite)
	     (equal
	      (lessp x 1)
	      (zerop x)))

(prove-lemma lessp-remainder-x-exp-x (rewrite)
	     (equal
	      (lessp (remainder x y) (exp y z))
	      (or
	       (and
		(zerop z)
		(equal (remainder x y) 0))
	       (and
		(not (zerop z))
		(not (zerop y)))))
	     ((enable exp)))

(prove-lemma bit-vectorp-append (rewrite)
	     (implies
	      (bit-vectorp x x-size)
	      (equal
	       (bit-vectorp (append x y) size)
	       (and
		(bit-vectorp y (difference size x-size))
		(not (lessp size x-size))))))

(prove-lemma correctness-of-nat-to-bv-general (rewrite)
	     (implies
	      (and
	       (listp ctrl-stk)
	       (at-least-morep (length temp-stk)
			       3 max-temp-stk-size)
	       (equal (definition 'nat-to-bv prog-segment)
		      (nat-to-bv-program))
	       (numberp value)
	       (lessp 0 word-size)
	       (lessp value (exp 2 word-size))
	       (bit-vectorp bv word-size)
	       (bit-vectorp cb word-size))
	      (equal
	       (p (p-state '(pc (nat-to-bv . 4))
			   (cons (list
				  (list
				   (cons 'value (list 'nat value))
				   (cons 'current-bit (list 'bitv cb))
				   (cons 'temp temp))
				  ret-pc)
				 ctrl-stk)
			   (cons (list 'bitv bv) 
				 temp-stk)
			   prog-segment
			   data-segment
			   max-ctrl-stk-size
			   max-temp-stk-size
			   word-size
			   'run)
		  (nat-to-bv-loop-clock value))
	       (p-state ret-pc
			ctrl-stk
			(cons (list 'bitv (nat-to-bv2-helper 
					   value cb bv))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	      ((induct (correctness-of-nat-to-bv-general-induct 
			value cb temp bv))))

(defn nat-to-bv-clock (value)
  (plus 9 (nat-to-bv-loop-clock value)))

(defn nat-to-bv-input-conditionp (p0)
  (and
   (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0)))
   (numberp (cadr (top (p-temp-stk p0))))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   7 (p-max-ctrl-stk-size p0))
   (lessp 0 (p-word-size p0))
   (at-least-morep (length (p-temp-stk p0))
		   2 (p-max-temp-stk-size p0))
   (listp (p-ctrl-stk p0))))
	 
(prove-lemma bit-vectorp-one-bit-vector (rewrite)
	     (equal
	      (bit-vectorp (one-bit-vector s) s)
	      (lessp 0 s)))

(prove-lemma bit-vectorp-zero-bit-vector (rewrite)
	     (bit-vectorp (zero-bit-vector s) s))

(prove-lemma all-but-last-one-bit-vector (rewrite)
	     (equal
	      (all-but-last (one-bit-vector s))
	      (zero-bit-vector (sub1 s))))

(prove-lemma correctness-of-nat-to-bv-helper nil
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons (list 'nat value) temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) '(call nat-to-bv))
	       (equal (definition 'nat-to-bv prog-segment)
		      (nat-to-bv-program))
	       (equal (definition 'push-1-vector prog-segment)
		      (push-1-vector-program word-size))
	       (nat-to-bv-input-conditionp p0))
	      (equal
	       (p p0 (nat-to-bv-clock value))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'bitv 
				    (nat-to-bv2 value word-size))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run))))

(defn bv-to-nat (bv)
  (if (listp bv)
      (plus (times (fix-bit (car bv)) (exp 2 (length (cdr bv)))) 
	    (bv-to-nat (cdr bv)))
    0))

(prove-lemma length-nat-to-bv (rewrite)
	     (equal (length (nat-to-bv nat size)) (fix size)))


(prove-lemma bv-to-nat-nat-to-bv (rewrite)
	      (equal (bv-to-nat (nat-to-bv nat size)) 
		     (if (lessp nat (exp 2 size))
			 (fix nat)
		       (sub1 (exp 2 size))))
	      ((enable exp)))

(enable exp)

(prove-lemma nat-to-bv-simple (rewrite)
	     (implies
	      (zerop x)
	      (and
	       (equal (nat-to-bv x y) (zero-bit-vector y))
	       (equal (nat-to-bv y x) nil))))

(prove-lemma nat-to-bv-bv-to-nat (rewrite)
	     (implies
	      (bit-vectorp bv size)
	      (equal (nat-to-bv (bv-to-nat bv) size) bv)))

(prove-lemma bv-to-nat-append (rewrite)
	     (equal
	      (bv-to-nat (append x y))
	      (plus
	       (bv-to-nat y)
	       (times (exp 2 (length y)) (bv-to-nat x)))))

(prove-lemma lessp-plus-hacks (rewrite)
	     (and
	     (equal
	      (lessp
	       (plus a (plus b (plus c (plus (times d e) (times d e)))))
	       (plus e e))
	      (and
	       (zerop d)
	       (lessp (plus a (plus b c)) (plus e e))))
	     (equal
	      (lessp
	       (plus a (plus b (plus c (plus e (plus (times d g) h)))))
	       g)
	      (and
	       (zerop d)
	       (lessp (plus a (plus b (plus c (plus e h)))) g)))))

(prove-lemma bv-to-nat-xor-bitv (rewrite)
	     (implies
	      (and
	       (bit-vectorp x size)
	       (bit-vectorp y size)
	       (equal (and-bitv x y) (zero-bit-vector size)))
	      (equal 
	       (bv-to-nat (xor-bitv x y))
	       (plus (bv-to-nat x) (bv-to-nat y)))))

(prove-lemma lessp-bv-to-nat-exp-2 (rewrite)
	     (implies
	      (bit-vectorp x size)
	      (equal (lessp (bv-to-nat x) (exp 2 size)) t)))

(prove-lemma equal-nat-to-bv (rewrite)
	     (implies
	      (and
	       (bit-vectorp bv size)
	       (lessp y (exp 2 size)))
	      (and
	       (equal
		(equal (nat-to-bv y size) bv)
		(equal (bv-to-nat bv) (fix y)))
	       (equal
		(equal bv (nat-to-bv y size))
		(equal (fix y) (bv-to-nat bv))))))

(defn least-bit-higher-than-high-bit (x y)
  (if (listp x)
      (and
       (equal (length x) (length y))
       (if (not (equal (car y) 0))
	   (all-zero-bitvp x)
	 (least-bit-higher-than-high-bit (cdr x) (cdr y))))
    (nlistp y)))

(prove-lemma least-bit-higher-means-and-0 (rewrite)
	     (implies
	      (and
	       (bit-vectorp x size)
	       (bit-vectorp y size)
	       (least-bit-higher-than-high-bit x y))
	      (and
	       (equal (and-bitv x y) (zero-bit-vector size))
	       (equal (and-bitv y x) (zero-bit-vector size)))))

(prove-lemma all-zero-bitvp-zero-bit-vector (rewrite)
	     (all-zero-bitvp (zero-bit-vector size)))

(prove-lemma bv-to-nat-one-bit-vector (rewrite)
	     (equal (bv-to-nat (one-bit-vector size)) 1))

;; renamed from firstn to avoid conflict with similar but different
;; definition in piton library
(defn make-list-from (n list)
  (if (zerop n)
      nil
    (cons (car list) (make-list-from (sub1 n) (cdr list)))))

(prove-lemma length-make-list-from (rewrite)
	     (equal (length (make-list-from n list)) (fix n)))

(prove-lemma make-list-from-1 (rewrite)
	     (equal
	      (make-list-from 1 x)
	      (list (car x))))

(prove-lemma listp-make-list-from (rewrite)
	     (equal
	      (listp (make-list-from n x))
	      (not (zerop n))))
			   
(defn double-cdr-induct (x z)
  (if (listp x)
      (double-cdr-induct (cdr x) (cdr z))
    t))


(prove-lemma all-zero-bitvp-append (rewrite)
	     (equal
	      (all-zero-bitvp (append x y))
	      (and
	       (all-zero-bitvp x)
	       (all-zero-bitvp y))))


(prove-lemma least-bit-higher-than-high-bit-append-0s (rewrite)
	     (implies
	      (and
	       (all-zero-bitvp y)
	       (equal (length z) (length (append x y))))
	     (equal
	      (least-bit-higher-than-high-bit (append x y) z)
	      (least-bit-higher-than-high-bit 
	       x (make-list-from (length x) z))))
	     ((induct (double-cdr-induct x z))))

(prove-lemma equal-xor-bitv-x-y-1 (rewrite)
	     (equal
	      (equal (xor-bitv a b) b)
	      (and
	       (bit-vectorp b (length a))
	       (all-zero-bitvp a))))

(prove-lemma equal-xor-bitv-x-y-2 (rewrite)
	     (equal
	      (equal (xor-bitv a b) a)
	      (and
	       (all-zero-bitvp (make-list-from (length a) b))
	       (bit-vectorp a (length a)))))

(prove-lemma least-bit-higher-than-high-bit-simple (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (equal 
	       (least-bit-higher-than-high-bit x y)
	       (equal (length x) (length y)))))

(prove-lemma make-list-from-is-all-but-last (rewrite)
	     (implies
	      (equal (length x) (add1 n))
	      (equal
	       (make-list-from n x)
	       (all-but-last x))))

(prove-lemma least-bit-higher-all-but-last (rewrite)
	     (implies
	      (least-bit-higher-than-high-bit a b)
	      (equal
	       (least-bit-higher-than-high-bit 
		a (cons 0 (all-but-last b)))
	       (listp a))))

(defn at-most-one-bit-on (bv)
  (if (listp bv)
      (if (equal (car bv) 0)
	  (at-most-one-bit-on (cdr bv))
	(all-zero-bitvp (cdr bv)))
    t))

;
;(prove-lemma length-all-but-last (rewrite)
;	     (equal
;	      (length (all-but-last x))
;	      (if (listp x) (sub1 (length x)) 0)))
(enable length-all-but-last)

(prove-lemma listp-xor-bitv (rewrite)
	     (equal
	      (listp (xor-bitv a b))
	      (listp a)))

(prove-lemma all-zero-bitvp-means-at-most-one-bit-on (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (at-most-one-bit-on x)))

(prove-lemma at-most-one-bit-on-append (rewrite)
	     (equal
	      (at-most-one-bit-on (append a b))
	      (or
	       (and
		(all-zero-bitvp a)
		(at-most-one-bit-on b))
	       (and
		(at-most-one-bit-on a)
		(all-zero-bitvp b)))))

(defn fix-bitv (list)
  (if (listp list)
      (cons (if (equal (car list) 0) 0 1) (fix-bitv (cdr list)))
    nil))

(prove-lemma xor-bitv-nlistp3 (rewrite)
	     (implies
	      (not (listp x))
	      (and
	       (equal (xor-bitv x y) nil)
	       (equal (xor-bitv y x) (fix-bitv y)))))

(disable xor-bitv-nlistp)
(disable xor-bitv-nlistp2)

(prove-lemma fix-bitv-all-but-last (rewrite)
	     (equal
	      (fix-bitv (all-but-last x))
	      (all-but-last (fix-bitv x))))

(prove-lemma all-but-last-xor-bitv (rewrite)
	     (equal
	      (all-but-last (xor-bitv a b))
	      (if (lessp (length b) (length a))
		  (xor-bitv (all-but-last a) b)
		(xor-bitv (all-but-last a) (all-but-last b)))))

(prove-lemma least-bit-higher-cons-xor-bitv-hack (rewrite)
	     (implies
	      (and
	       (least-bit-higher-than-high-bit (cdr x) a)
	       (least-bit-higher-than-high-bit (cdr x) b))
	      (equal
	       (least-bit-higher-than-high-bit 
		x (cons 0 (xor-bitv a b)))
	       (listp x))))

(prove-lemma least-bit-higher-cdr-all-but-last (rewrite)
	     (implies
	      (least-bit-higher-than-high-bit a b)
	      (least-bit-higher-than-high-bit (cdr a) (all-but-last b))))

(prove-lemma least-bit-higher-x-all-but-last-x (rewrite)
	     (implies
	      (at-most-one-bit-on x)
	      (least-bit-higher-than-high-bit 
	       (cdr x) (all-but-last x))))

(prove-lemma nat-to-bv-equiv-helper nil
	     (implies
	      (and
	       (bit-vectorp cb size)
	       (bit-vectorp bv size)
	       (lessp 0 size)
	       (lessp (plus (bv-to-nat bv) 
			    (times (bv-to-nat cb) value))
		      (exp 2 size))
	       (at-most-one-bit-on cb)
	       (least-bit-higher-than-high-bit cb bv))
	     (equal
	      (nat-to-bv2-helper value cb bv)
	      (nat-to-bv (plus (times (bv-to-nat cb) value) 
			       (bv-to-nat bv))
			 size)))
	     ((induct (nat-to-bv2-helper value cb bv))))

(prove-lemma at-most-one-bit-on-one-bit-vector (rewrite)
	     (at-most-one-bit-on (one-bit-vector size)))

(prove-lemma bv-to-nat-all-zero-bitvp (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (equal (bv-to-nat x) 0)))


(prove-lemma least-bit-higher-than-high-bit-simple2 (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (equal 
	       (least-bit-higher-than-high-bit y x)
	       (equal (length x) (length y)))))

(prove-lemma length-zero-bit-vector (rewrite)
	     (equal (length (zero-bit-vector size)) (fix size)))

(prove-lemma length-one-bit-vector (rewrite)
	     (equal (length (one-bit-vector size)) 
		    (if (zerop size) 1 size)))

(prove-lemma nat-to-bv-equivalence (rewrite)
	     (implies
	      (and
	       (lessp value (exp 2 size))
	       (lessp 0 size))
	     (equal
	      (nat-to-bv2 value size)
	      (nat-to-bv value size)))
	     ((use (nat-to-bv-equiv-helper
		    (cb (one-bit-vector size))
		    (bv (zero-bit-vector size))))))

(prove-lemma correctness-of-nat-to-bv (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons v temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (car v) 'nat)
	       (equal (cddr v) nil)
	       (equal (p-current-instruction p0) '(call nat-to-bv))
	       (equal (definition 'nat-to-bv prog-segment)
		      (nat-to-bv-program))
	       (equal (definition 'push-1-vector prog-segment)
		      (push-1-vector-program word-size))
	       (equal num (cadr v))
	       (nat-to-bv-input-conditionp p0))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons v temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (nat-to-bv-clock num))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'bitv 
				    (nat-to-bv (cadr v) word-size))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((disable-theory t)
	      (enable nat-to-bv-input-conditionp p-state
		      p-word-size-p-state p-temp-stk-p-state top)
	      (enable-theory ground-zero)
	      (use (correctness-of-nat-to-bv-helper (value (cadr v)))
		   (nat-to-bv-equivalence (size word-size)
					  (value (cadr v))))))

;;;; bv-to-nat

(defn bv-to-nat-program nil
  '(bv-to-nat (bv)
	      ((current-bit (nat 0)) (current-2power (nat 0)))
	      (push-constant (nat 1))
	      (pop-local current-2power)
	      (call push-1-vector)
	      (pop-local current-bit)
	      (push-constant (nat 0))
           (dl loop ()
	      (push-local bv))
	      (push-local current-bit)
	      (and-bitv)
	      (test-bitv-and-jump all-zero lab)
	      (push-local current-2power)
	      (add-nat)
	   (dl lab ()
	      (push-local current-bit))
	      (lsh-bitv)
	      (set-local current-bit)
	      (test-bitv-and-jump all-zero done)
	      (push-local current-2power)
	      (mult2-nat)
	      (pop-local current-2power)
	      (jump loop)
	   (dl done ()
	      (ret))))

(defn example-bv-to-nat-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (bitv (1 0 1 1 0 0 0 1)))
			(call bv-to-nat)
			(ret))
		 (push-1-vector-program 8)
		 (bv-to-nat-program))
	   nil
	   10
	   8
	   8
	   'run))

(defn trailing-zeros-helper (list acc)
  (if (listp list)
      (trailing-zeros-helper 
       (cdr list) (if (equal (car list) 0) (add1 acc) 0))
    (fix acc)))

(defn trailing-zeros (list)
  (trailing-zeros-helper list 0))

(prove-lemma trailing-zeros-of-all-zero-bitvp (rewrite)
	     (implies
	      (all-zero-bitvp bv)
	      (equal (trailing-zeros-helper bv n) 
		     (plus (length bv) n))))

(prove-lemma non-zero-means-acc-irrelevant-spec (rewrite)
	     (implies
	      (not (all-zero-bitvp bv))
	      (equal (trailing-zeros-helper bv (add1 x))
		     (trailing-zeros-helper bv x))))

(prove-lemma non-zero-means-acc-irrelevant (rewrite)
	     (implies
	      (and
	       (not (all-zero-bitvp bv))
	       (not (equal x 0)))
	      (equal (trailing-zeros-helper bv x)
		     (trailing-zeros-helper bv 0))))

(prove-lemma trailing-zeros-helper-append (rewrite)
	     (equal
	      (trailing-zeros-helper (append x y) acc)
	      (if (all-zero-bitvp y)
		  (plus (trailing-zeros-helper x acc) (length y))
		(trailing-zeros-helper y acc))))

(prove-lemma trailing-zeros-append (rewrite)
	     (equal
	      (trailing-zeros (append x y))
	      (if (all-zero-bitvp y)
		  (plus (trailing-zeros x) (length y))
		(trailing-zeros y))))

(prove-lemma lessp-trailing-zeros-helper (rewrite)
	     (implies
	      (not (lessp n (plus acc (length x))))
	      (equal (lessp n (trailing-zeros-helper x acc)) f)))

(defn last (list)
  (if (listp list)
      (if (listp (cdr list))
	  (last (cdr list))
	(car list))
    0))

(prove-lemma equal-trailing-zeros-helper-0 (rewrite)
	     (equal
	      (equal (trailing-zeros-helper x acc) 0)
	      (or (and (zerop acc) (nlistp x))
		  (not (equal (last x) 0)))))

(prove-lemma lessp-length-cdr-trailing (rewrite)
	     (implies
	      (and
	       (lessp (length (cdr x)) (trailing-zeros-helper x acc))
	       (listp x))
	      (and
	       (all-zero-bitvp x)
	       (all-zero-bitvp (cdr x)))))

(prove-lemma not-all-zero-bitvp-cdr-means (rewrite)
	     (implies
	      (not (all-zero-bitvp (cdr x)))
	      (equal
	       (trailing-zeros-helper x acc)
	       (trailing-zeros-helper (cdr x) 0))))

(defn bv-to-nat2-helper (bv cb current-2power)
  (if (all-zero-bitvp cb)
      0
    (plus
     (if (all-zero-bitvp (and-bitv bv cb)) 0 current-2power)
     (bv-to-nat2-helper 
      bv (append (cdr cb) (list 0)) (times 2 current-2power))))
  ((lessp (difference (length cb) (trailing-zeros cb)))))
			   
(defn bv-to-nat2 (bv)
  (bv-to-nat2-helper bv (one-bit-vector (length bv)) 1))

(prove-lemma lessp-length-trailing-zeros-hack (rewrite)
	     (implies
	      (zerop acc)
	      (not (lessp (length x) (trailing-zeros-helper x acc)))))

(defn bv-to-nat-loop-clock (cb bv)
  (if (all-zero-bitvp (cdr cb))
      (if (or (equal (car cb) 0) (equal (car bv) 0)) 9 11)
    (plus (if (all-zero-bitvp (and-bitv cb bv)) 12 14)
	  (bv-to-nat-loop-clock (append (cdr cb) '(0)) bv)))
  ((lessp (difference (length cb) (trailing-zeros cb)))))

(defn bv-to-nat-induct (value bv cb current-2power)
  (if (all-zero-bitvp cb)
      0
     (bv-to-nat-induct
      (plus (if (all-zero-bitvp (and-bitv bv cb)) 0 current-2power)
	    value)
      bv (append (cdr cb) (list 0)) (times 2 current-2power)))
  ((lessp (difference (length cb) (trailing-zeros cb)))))

(defn double-cdr-with-sub1-induct (x y n)
  (if (listp x)
      (double-cdr-with-sub1-induct (cdr x) (cdr y) (sub1 n))
    t))

(prove-lemma bit-vectorp-and-bitv-better (rewrite)
	     (equal
	      (bit-vectorp (and-bitv x y) size)
	      (equal (length x) (fix size)))
	     ((induct (double-cdr-with-sub1-induct x y size))))

(prove-lemma lessp-bv-to-nat-exp (rewrite)
	     (implies
	      (bit-vectorp x size)
	      (lessp (bv-to-nat x) (exp 2 size))))

(prove-lemma equal-bv-to-nat-0 (rewrite)
	     (implies
	      (bit-vectorp x size)
	     (equal
	      (equal (bv-to-nat x) 0)
	      (all-zero-bitvp x))))

;(prove-lemma commutativity-of-and-bitv (rewrite)
;	     (implies
;	      (equal (length x) (length y))
;	      (equal (and-bitv x y) (and-bitv y x))))
(enable commutativity-of-and-bitv)

(prove-lemma commutativity2-of-and-bitv (rewrite)
	     (implies
	      (equal (length x) (length y))
	      (equal (and-bitv x (and-bitv y z)) 
		     (and-bitv y (and-bitv x z)))))

(prove-lemma associativity-of-and-bitv (rewrite)
	     (implies
	      (equal (length x) (length y))
	     (equal (and-bitv (and-bitv x y) z)
		    (and-bitv x (and-bitv y z)))))

(prove-lemma all-zero-bitvp-and-bitv (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (and
	       (all-zero-bitvp (and-bitv x y))
	       (all-zero-bitvp (and-bitv y x)))))

(prove-lemma bv-to-nat-loop-clock-open (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (equal (bv-to-nat-loop-clock x y) 9)))

(prove-lemma bv-to-nat2-helper-hack (rewrite)
	     (implies
	      (and
	       (all-zero-bitvp z)
	       (equal (length d) (length z)))
	      (equal (bv-to-nat2-helper (cons 1 d) (cons 1 z) v)
		     (fix v)))
	     ((expand (bv-to-nat2-helper (cons 1 d) (cons 1 z) v))))

(prove-lemma bv-to-nat2-helper-hack2 (rewrite)
	     (implies
	      (and
	       (all-zero-bitvp z)
	       (equal (length d) (length z)))
	      (equal (bv-to-nat2-helper (cons 0 d) (cons 1 z) v) 0))
	     ((expand (bv-to-nat2-helper (cons 0 d) (cons 1 z) v))))

(prove-lemma correctness-of-bv-to-nat-general (rewrite)
	     (implies
	      (and
	       (listp ctrl-stk)
	       (at-least-morep (length temp-stk) 
			       3 max-temp-stk-size)
	       (equal (definition 'bv-to-nat prog-segment)
		      (bv-to-nat-program))
	       (numberp c2p)
	       (lessp 0 word-size)
	       (at-most-one-bit-on cb)
	       (equal c2p (bv-to-nat cb))
	       (bit-vectorp bv word-size)
	       (bit-vectorp cb word-size)
	       (numberp value)
	       (lessp value c2p))
	      (equal
	       (p (p-state '(pc (bv-to-nat . 5))
			   (cons (list
				  (list
				   (cons 'bv (list 'bitv bv))
				   (cons 'current-bit (list 'bitv cb))
				   (cons 'current-2power 
					 (list 'nat c2p)))
				  ret-pc)
				 ctrl-stk)
			   (cons (list 'nat value) 
				 temp-stk)
			   prog-segment
			   data-segment
			   max-ctrl-stk-size
			   max-temp-stk-size
			   word-size
			   'run)
		  (bv-to-nat-loop-clock cb bv))
	       (p-state ret-pc
			ctrl-stk
			(cons 
			 (list 'nat 
			       (plus (bv-to-nat2-helper bv cb c2p)
				     value))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	      ((induct (bv-to-nat-induct value bv cb c2p))))


(defn bv-to-nat-clock (word-size bv)
  (plus 8 (bv-to-nat-loop-clock (one-bit-vector word-size) bv)))

(defn bv-to-nat-input-conditionp (p0)
  (and
   (equal (car (top (p-temp-stk p0))) 'bitv)
   (equal (cddr (top (p-temp-stk p0))) nil)
   (bit-vectorp (cadr (top (p-temp-stk p0))) (p-word-size p0))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   7 (p-max-ctrl-stk-size p0))
   (lessp 0 (p-word-size p0))
   (at-least-morep (length (p-temp-stk p0)) 
		   2 (p-max-temp-stk-size p0))
   (listp (p-ctrl-stk p0))))

(prove-lemma correctness-of-bv-to-nat-helper nil
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons (list 'bitv bv) temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) '(call bv-to-nat))
	       (equal (definition 'bv-to-nat prog-segment)
		      (bv-to-nat-program))
	       (equal (definition 'push-1-vector prog-segment)
		      (push-1-vector-program word-size))
	       (bv-to-nat-input-conditionp p0))
	      (equal
	       (p p0 (bv-to-nat-clock word-size bv))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'nat (bv-to-nat2 bv)) temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run))))

(prove-lemma bit-vectorp-append-better (rewrite)
	     (implies
	      (bit-vectorp x (length x))
	      (equal (bit-vectorp (append x y) size)
		     (and
		      (bit-vectorp y (length y))
		      (equal (fix size) 
			     (plus (length x) (length y))))))
	      ((induct (make-list-from size x))))

(prove-lemma bit-vectorp-hack (rewrite)
	     (equal
	      (bit-vectorp x (plus a (length (cdr x))))
	      (and
	       (if (listp x) (equal a 1) (zerop a))
	       (bit-vectorp x (length x))))
	     ((use (length-from-bit-vectorp 
		    (x x) (s (plus a (length (cdr x))))))
	      (disable length-from-bit-vectorp)))

(prove-lemma bv-to-nat-one-bit (rewrite)
	     (implies
	      (and
	       (not (all-zero-bitvp x))
	       (at-most-one-bit-on x)
	       (bit-vectorp x size))
	      (equal (bv-to-nat x) (exp 2 (trailing-zeros x)))))

(prove-lemma lessp-sub1-plus-hack (rewrite)
	     (equal
	      (lessp (sub1 x) (plus y x))
	      (or (not (zerop x)) (not (zerop y)))))

(prove-lemma quotient-plus-hack (rewrite)
	     (equal
	      (quotient (plus a b b) 2)
	      (plus (quotient a 2) b)))

(prove-lemma bv-to-nat-all-but-last (rewrite)
	     (implies
	      (bit-vectorp x size)
	     (equal
	      (bv-to-nat (all-but-last x))
	      (quotient (bv-to-nat x) 2))))

(prove-lemma make-list-from-cons (rewrite)
	     (equal
	      (make-list-from n (cons a b))
	      (if (zerop n) nil (cons a (make-list-from (sub1 n) b)))))

(prove-lemma equal-plus-times-hack (rewrite)
	     (equal
	      (equal (plus a (times a b) (times a c)) (times a d))
	      (or (zerop a) (equal (plus 1 b c) d)))
	     ((use (equal-times-arg1 (a a) (x (plus 1 b c)) (y d)))))

;(defn nth (n list)
;  (if (zerop n)
;      (car list)
;    (nth (sub1 n) (cdr list))))
(enable nth)

(prove-lemma last-make-list-from (rewrite)
	     (equal (last (make-list-from n x)) 
		    (if (zerop n) 0 (nth (sub1 n) x))))

(prove-lemma make-list-from-nlistp (rewrite)
	     (implies
	      (nlistp x)
	      (equal (make-list-from n x) (zero-bit-vector n))))

(prove-lemma nth-nlistp (rewrite)
	     (implies
	      (nlistp x)
	      (equal (nth n x) 0)))

(prove-lemma bit-vectorp-make-list-from (rewrite)
	     (implies
	      (bit-vectorp x size)
	      (bit-vectorp (make-list-from n x) n)))

(prove-lemma equal-bv-to-nat-0-2 (rewrite)
	     (implies
	      (bit-vectorp x (length x))
	      (equal 
	       (equal (bv-to-nat x) 0)
	       (all-zero-bitvp x))))

(prove-lemma bv-to-nat-make-list-from-from-sub1-make-list-from (rewrite)
	     (implies
	      (equal (bv-to-nat (make-list-from (sub1 n) v)) 0)
	      (equal (bv-to-nat (make-list-from n v))
		     (if (zerop n) 0 (fix-bit (nth (sub1 n) v))))))

(prove-lemma plus-bv-to-nat-make-list-from (rewrite)
	     (equal
	      (plus (bv-to-nat (make-list-from (sub1 z) v))
		    (bv-to-nat (make-list-from (sub1 z) v)))
	      (difference (bv-to-nat (make-list-from z v))
			  (fix-bit (last (make-list-from z v)))))
	     ((induct (make-list-from z v))))

(prove-lemma equal-bv-to-nat-1 (rewrite)
	     (implies
	      (bit-vectorp x (length x))
	     (equal
	      (equal (bv-to-nat x) 1)
	      (and
	       (all-zero-bitvp (all-but-last x))
	       (equal (last x) 1))))
	     ((induct (all-but-last x))))

(prove-lemma lessp-1-hack (rewrite)
	     (equal
	      (lessp 1 a)
	      (and
	       (not (zerop a))
	       (not (equal a 1)))))

(prove-lemma not-equal-nth-0-means (rewrite)
	     (implies
	      (and
	       (not (equal (nth n v) 0))
	       (lessp n s))
	      (not (all-zero-bitvp (make-list-from s v)))))

(prove-lemma all-zero-bitvp-all-but-last-means nil
	     (implies
	      (and
	       (all-zero-bitvp (all-but-last x))
	       (equal (length x) (length y))
	       (lessp 0 (trailing-zeros-helper y acc)))
	      (all-zero-bitvp (and-bitv x y))))

(prove-lemma all-zero-bitvp-all-but-last-means-spec (rewrite)
	     (implies
	      (and
	       (all-zero-bitvp (all-but-last x))
	       (equal (length x) (length y))
	       (lessp 0 (trailing-zeros-helper y 0)))
	      (all-zero-bitvp (and-bitv x y)))
	     ((use (all-zero-bitvp-all-but-last-means (acc 0)))))

(prove-lemma all-zero-means-to-and-bitv (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (and 
	       (equal (and-bitv x y) (zero-bit-vector (length x)))
	       (equal (and-bitv y x) (zero-bit-vector (length y))))))

(prove-lemma trailing-zeros-nth-proof nil
	     (implies
	      (and
	       (equal n 
		      (sub1 (difference (length x) 
					(trailing-zeros-helper x acc))))
	       (not (all-zero-bitvp x)))
	      (not (equal (nth n x) 0))))


(prove-lemma trailing-zeros-nth-spec (rewrite)
	     (implies
	      (and
	       (equal n 
		      (sub1 (difference (length x) 
					(trailing-zeros-helper x 0))))
	       (not (all-zero-bitvp x)))
	      (not (equal (nth n x) 0)))
	     ((use (trailing-zeros-nth-proof (acc 0)))))

(prove-lemma and-bitv-special (rewrite)
	     (implies
	      (and
	       (equal (nth n w) 0)
	       (not (equal (nth n x) 0))
	       (equal (length x) (length x))
	       (at-most-one-bit-on x))
	      (equal (and-bitv w x) (zero-bit-vector (length w)))))


(prove-lemma equal-trailing-zeros-length-spec nil
	     (equal
	      (equal (trailing-zeros-helper x acc) (plus acc (length x)))
	      (all-zero-bitvp x)))

(prove-lemma equal-trailing-zeros-length (rewrite)
	     (implies
	      (zerop acc)
	     (equal
	      (equal (trailing-zeros-helper x acc) (length x))
	      (all-zero-bitvp x)))
	     ((use (equal-trailing-zeros-length-spec))))

(prove-lemma bit-vectorp-trailing-zeros (rewrite)
	     (equal
	      (bit-vectorp x (trailing-zeros-helper x acc))
	      (and
	       (all-zero-bitvp x)
	       (bit-vectorp x (length x))
	       (zerop acc)))
	     ((use (equal-trailing-zeros-length-spec)
		   (length-from-bit-vectorp 
		    (s (trailing-zeros-helper x acc))))
	      (disable length-from-bit-vectorp)))


(prove-lemma quotient-exp-hack (rewrite)
	     (implies
	      (not (zerop b))
	     (equal (quotient (plus x (exp b y)) b)
		    (if (zerop y)
			(quotient (add1 x) b)
		      (plus (exp b (sub1 y)) (quotient x b))))))

;(defn properp (list)
;  (if (listp list)
;      (properp (cdr list))
;    (equal list nil)))

(prove-lemma bit-vectorp-means-properp (rewrite)
	     (implies
	      (bit-vectorp x (length x))
	      (properp x)))

(prove-lemma make-list-from-simplify (rewrite)
	     (implies
	      (and
	       (equal n (length x))
	       (properp x))
	      (equal (make-list-from n x) x)))

(prove-lemma equal-add1-plus-hack (rewrite)
	     (and
	      (equal 
	       (equal (add1 (plus a b)) (plus c (plus d a)))
	       (equal (add1 b) (plus c d)))
	      (equal 
	       (equal (add1 (plus a b)) (plus c a))
	       (equal (add1 b) (fix c)))
	      (equal
	       (equal (add1 a) (plus b a))
	       (equal 1 (fix b)))))

(prove-lemma plus-quotient-bv-to-nat (rewrite)
	     (equal
	      (plus (quotient (bv-to-nat x) 2)
		    (quotient (bv-to-nat x) 2))
	      (difference (bv-to-nat x) (fix-bit (last x)))))

(prove-lemma equal-plus-times-hack2 (rewrite)
	     (equal
	      (equal (plus (times a b) (times a c)) (times a d))
	      (or (zerop a)
		  (equal (plus b c) (fix d))))
	     ((use (equal-times-arg1 (a a) (x (plus b c)) (y d)))))

(prove-lemma and-bitv-special-special (rewrite)
	     (implies
	      (and
	       (equal (last w) 0)
	       (not (equal (last x) 0))
	       (equal (length x) (length w))
	       (at-most-one-bit-on x))
	      (equal (and-bitv w x) (zero-bit-vector (length w)))))

(prove-lemma and-bitv-special-3 (rewrite)
	     (implies
	      (and
	       (equal (length x) (length y))
	       (not (equal (last x) 0))
	       (not (equal (last y) 0)))
	      (not (all-zero-bitvp (and-bitv x y)))))

(prove-lemma and-bitv-special-4 (rewrite)
	     (implies
	      (and
	       (not (equal (nth n w) 0))
	       (not (equal (nth n x) 0))
	       (equal (length x) (length x)))
	       (not (all-zero-bitvp (and-bitv w x)))))

(prove-lemma and-bitv-special-5 (rewrite)
	     (implies
	      (and
	       (equal (last w) 0)
	       (not (equal (last x) 0))
	       (equal (add1 (length x)) (length w))
	       (at-most-one-bit-on x))
	      (equal (and-bitv w (cons 0 x)) 
		     (zero-bit-vector (length w)))))

(prove-lemma and-bitv-special-6 (rewrite)
	     (implies
	      (and
	       (not (equal (last w) 0))
	       (not (equal (last x) 0))
	       (equal (add1 (length x)) (length w)))
	      (not (all-zero-bitvp (and-bitv w (cons 0 x))))))

(prove-lemma not-last-0-means-not-all-0 (rewrite)
	     (implies
	      (not (equal (last x) 0))
	      (not (all-zero-bitvp x))))

(prove-lemma bit-vectorp-plus-length-hack (rewrite)
	     (and
	     (equal
	      (bit-vectorp x (plus z (length x)))
	      (and
	       (bit-vectorp x (length x))
	       (zerop z)))
	     (equal
	      (bit-vectorp x (plus (add1 z) (length (cdr x))))
	      (and
	       (bit-vectorp x (length x))
	       (listp x)
	       (zerop z)))))

(prove-lemma last-append (rewrite)
	     (equal
	      (last (append x y))
	      (if (listp y) (last y) (last x))))

(prove-lemma bv-to-nat2-helper-bv-to-nat (rewrite)
	     (implies
	      (and
	       (at-most-one-bit-on cb)
	       (bit-vectorp cb size)
	       (bit-vectorp bv size)
	       (equal c2 (bv-to-nat cb)))
	      (equal
	       (bv-to-nat2-helper bv cb c2)
	       (bv-to-nat (append 
			   (make-list-from (difference (length bv)
					       (trailing-zeros cb))
				   bv)
			   (zero-bit-vector (trailing-zeros cb)))))))

(prove-lemma bv-to-nat2-helper-bv-to-nat-better (rewrite)
	     (implies
	      (and
	       (at-most-one-bit-on cb)
	       (bit-vectorp cb (length cb))
	       (bit-vectorp bv (length cb))
	       (equal c2 (bv-to-nat cb)))
	      (equal
	       (bv-to-nat2-helper bv cb c2)
	       (bv-to-nat (append 
			   (make-list-from (difference (length bv)
					       (trailing-zeros cb))
				   bv)
			   (zero-bit-vector (trailing-zeros cb)))))))

(prove-lemma nlistp-bv-to-nat2 (rewrite)
	     (implies
	      (not (listp x))
	      (equal (bv-to-nat2-helper x a b) 0)))

(prove-lemma bv-to-nat2-bv-to-nat-helper nil
	     (implies (nlistp x)
		      (equal (bv-to-nat2 x) (bv-to-nat x))))

(prove-lemma bit-vectorp-one-bit-vector-rewrite (rewrite)
	     (equal
	      (bit-vectorp (one-bit-vector s) n)
	      (if (zerop s) (equal n 1) (equal (fix s) (fix n))))
	     ((induct (lessp s n))))

(prove-lemma trailing-zeros-helper-one-bit-vector (rewrite)
	     (equal
	      (trailing-zeros-helper (one-bit-vector n) acc)
	      0))

(prove-lemma bv-to-nat2-bv-to-nat (rewrite)
	     (implies
	      (bit-vectorp x (length x))
	      (equal (bv-to-nat2 x) (bv-to-nat x)))
	     ((use (bv-to-nat2-bv-to-nat-helper))))

(prove-lemma bv-length-weaker (rewrite)
	     (implies
	      (bit-vectorp x s)
	      (bit-vectorp x (length x))))

(prove-lemma correctness-of-bv-to-nat (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons b temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) '(call bv-to-nat))
	       (equal (definition 'bv-to-nat prog-segment)
		      (bv-to-nat-program))
	       (equal (definition 'push-1-vector prog-segment)
		      (push-1-vector-program word-size))
	       (equal bv (cadr b))
	       (bv-to-nat-input-conditionp p0))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons b temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (bv-to-nat-clock word-size bv))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'nat (bv-to-nat bv)) temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((use (correctness-of-bv-to-nat-helper)
		   (bv-to-nat2-bv-to-nat (x bv)))
	      (disable-theory t)
	      (enable bv-to-nat-input-conditionp p-state
		      p-word-size-p-state bv-length-weaker
		      top p-temp-stk-p-state)
	      (enable-theory ground-zero)))

;;;; number-with-at-least


(defn number-with-at-least-program nil
  '(number-with-at-least (nums-addr numnums min) ((i (nat 0)))
	    (push-constant (nat 0))
	    (set-local i)
     (dl loop ()
	    (push-local nums-addr))
            (fetch)
            (push-local min)
            (lt-nat)
	    (test-bool-and-jump t lab)
            (add1-nat)
      (dl lab ()
	    (push-local numnums))
            (push-local i)
	    (add1-nat)
	    (set-local i)
	    (sub-nat)
	    (test-nat-and-jump zero done)
            (push-local nums-addr)
            (push-constant (nat 1))
	    (add-addr)
	    (pop-local nums-addr)
	    (jump loop)
       (dl done ()
	   (ret))))

(defn example-number-with-at-least-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (nums . 0)))
			(push-constant (nat 5))
			(push-constant (nat 3))
			(call number-with-at-least)
			(ret))
		 (number-with-at-least-program))
	   '((nums (nat 3) (nat 8) (nat 9) (nat 2) (nat 100)))
	   10
	   8
	   8
	   'run))

(defn number-with-at-least (numlist min)
  (if (listp numlist)
      (if (lessp (car numlist) min)
	  (number-with-at-least (cdr numlist) min)
	(add1 (number-with-at-least (cdr numlist) min)))
    0))

(defn nat-list-piton (array word-size)
  (if (listp array)
      (and
       (listp (car array))
       (equal (caar array) 'nat)
       (numberp (cadar array))
       (equal (cddar array) nil)
       (lessp (cadar array) (exp 2 word-size))
       (nat-list-piton (cdr array) word-size))
    (equal array nil)))

(defn number-with-at-least-general-induct (i current n s min data-segment)
  (if (lessp i n)
      (number-with-at-least-general-induct
       (add1 i) 
       (if (lessp (cadr (get i (array s data-segment))) min) 
	   current (add1 current))
       n s min data-segment)
    t)
  ((lessp (difference n i))))

(defn number-with-at-least-clock-loop (i min array)
  (if (not (lessp i (length array))) 0
    (plus
     (if (lessp (cadr (get i array)) min) 0 1)
     (if (equal (add1 i) (length array))
	 12
       (plus 16 (number-with-at-least-clock-loop (add1 i) min array)))))
  ((lessp (difference (length array) i))))

(prove-lemma equal-difference-1 (rewrite)
	     (equal
	      (equal (difference x y) 1)
	      (equal x (add1 y))))


(prove-lemma nat-list-piton-means (rewrite)
	     (implies
	      (and
	       (nat-list-piton state size)
	       (lessp p (length state)))
	      (and
	       (equal (car (get p state)) 'nat)
	       (listp (get p state))
	       (numberp (cadr (get p state)))
	       (lessp (cadr (get p state)) (exp 2 size))
	       (equal (cddr (get p state)) nil))))

(prove-lemma number-with-at-least-nlistp (rewrite)
	     (implies 
	      (not (listp x))
	      (equal (number-with-at-least x min) 0)))

(prove-lemma equal-add1-length (rewrite)
	     (equal 
	      (equal (add1 x) (length y))
	      (and
	       (listp y)
	       (equal (fix x) (length (cdr y))))))

(disable number-with-at-least-clock-loop)


(prove-lemma length-cdr-untag-array (rewrite)
	     (equal
	      (length (cdr (untag-array x)))
	      (length (cdr x))))

(prove-lemma number-with-at-least-correctness-general nil
	     (implies
	      (and
	       (lessp (length (array s data-segment)) 
		      (exp 2 word-size))
	       (not (zerop word-size))
	       (listp ctrl-stk)
	       (nat-list-piton (array s data-segment) word-size)
	       (at-least-morep (length temp-stk)
			       3 max-temp-stk-size)
	       (equal (definition 'number-with-at-least prog-segment)
		      (number-with-at-least-program))
	       (definedp s data-segment)
	       (lessp min (exp 2 word-size))
	       (numberp min)
	       (lessp i n)
	       (numberp i)
	       (lessp n (exp 2 word-size))
	       (numberp current)
	       (not (lessp i current))
	       (equal n (length (array s data-segment))))
	      (equal
	       (p (p-state '(pc (number-with-at-least . 2))
			   (cons (list
				  (list 
				   (cons 'nums-addr 
					 (list 'addr (cons s i)))
				   (cons 'numnums (list 'nat n))
				   (cons 'min (list 'nat min))
				   (cons 'i (list 'nat i)))
				  ret-pc)
				 ctrl-stk)
			   (cons (list 'nat current)
				 temp-stk)
			   prog-segment
			   data-segment
			   max-ctrl-stk-size
			   max-temp-stk-size
			   word-size
			   'run)
		  (number-with-at-least-clock-loop 
		   i min (array s data-segment)))
	       (p-state ret-pc
			ctrl-stk
			(cons 
			 (list 'nat 
			       (plus current
			       (number-with-at-least
				(nthcdr i (untag-array 
					   (array s data-segment)))
				min)))
			 temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((induct (number-with-at-least-general-induct
		       i current n s min data-segment))
	      (expand (NUMBER-WITH-AT-LEAST-CLOCK-LOOP 
		       I MIN (CDR (ASSOC S DATA-SEGMENT))))))

(defn number-with-at-least-clock (min array)
  (plus 3 (number-with-at-least-clock-loop 0 min array)))

(defn number-with-at-least-input-conditionp (p0)
  (and
   (equal (car (car (p-temp-stk p0))) 'nat)
   (equal (cddr (car (p-temp-stk p0))) nil)
   (equal (car (cadr (p-temp-stk p0))) 'nat)
   (equal (cddr (cadr (p-temp-stk p0))) nil)
   (equal (car (caddr (p-temp-stk p0))) 'addr)
   (equal (cdadr (caddr (p-temp-stk p0))) 0)
   (equal (cddr (caddr (p-temp-stk p0))) nil)
   (listp (cadr (caddr (p-temp-stk p0))))
   (lessp (length (array (car (cadr (caddr (p-temp-stk p0)))) 
			 (p-data-segment p0)))
	  (exp 2 (p-word-size p0)))
   (not (zerop (p-word-size p0)))
   (listp (p-ctrl-stk p0))
   (nat-list-piton (array (car (cadr (caddr (p-temp-stk p0)))) 
			  (p-data-segment p0)) 
		   (p-word-size p0))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   6 (p-max-ctrl-stk-size p0))
   (at-least-morep (length (p-temp-stk p0))
		   0 (p-max-temp-stk-size p0))
   (equal (definition 'number-with-at-least (p-prog-segment p0))
	  (number-with-at-least-program))
   (definedp (car (cadr (caddr (p-temp-stk p0)))) (p-data-segment p0))
   (lessp (cadr (car (p-temp-stk p0))) (exp 2 (p-word-size p0)))
   (numberp (cadr (car (p-temp-stk p0))))
   (lessp 0 (cadr (cadr (p-temp-stk p0))))
   (equal (cadr (cadr (p-temp-stk p0))) 
	  (length (array (car (cadr (caddr (p-temp-stk p0)))) 
			 (p-data-segment p0))))))

(prove-lemma correctness-of-number-with-at-least (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons m (cons n (cons s temp-stk)))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) 
		      '(call number-with-at-least))
	       (number-with-at-least-input-conditionp p0)
	       (equal minc (cadr m))
	       (equal arrayc (array (car (cadr s)) data-segment)))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons m (cons n (cons s temp-stk)))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (number-with-at-least-clock minc arrayc))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'nat
				    (number-with-at-least 
				     (untag-array 
				      (array (car (cadr s)) 
					     data-segment))
				     (cadr m)))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	      ((use (number-with-at-least-correctness-general 
		     (i 0) (current 0) (s (car (cadr s)))
		    (ret-pc (add1-addr pc))
		    (n (cadr n)) (min (cadr m))))
	       (disable number-with-at-least-clock-loop)))

;; highest-bit


(defn highest-bit-program nil
  '(highest-bit (bv) ((cb (nat 0)))
	    (call push-1-vector)
	    (set-local cb)
	    (rsh-bitv)
     (dl loop ()
	    (push-local cb))
	    (test-bitv-and-jump all-zero done)
	    (push-local bv)
	    (push-local cb)
	    (and-bitv)
	    (test-bitv-and-jump all-zero lab)
	    (pop)
	    (push-local cb)
       (dl lab ()
	    (push-local cb))
	    (lsh-bitv)
	    (pop-local cb)
	    (jump loop)
       (dl done ()
 	    (ret))))

(defn example-highest-bit-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (bitv (0 0 0 0 0 0 0 0)))
			(call highest-bit)
			(push-constant (bitv (0 0 1 1 0 1 0 0)))
			(call highest-bit)
			(push-constant (bitv (1 0 1 1 0 1 0 0)))
			(call highest-bit)
			(ret))
		  (highest-bit-program)
		  (push-1-vector-program 8))
	   nil
	   10
	   8
	   8
	   'run))

(defn highest-bit (x)
  (if (listp x)
      (if (equal (car x) 0)
	  (cons 0 (highest-bit (cdr x)))
	(cons 1 (zero-bit-vector (length (cdr x)))))
    nil))

(prove-lemma listp-highest-bit (rewrite)
	     (equal (listp (highest-bit x)) (listp x)))

(prove-lemma length-highest-bit (rewrite)
	     (equal (length (highest-bit x)) (length x)))

(defn highest-bit-loop-clock (cb bv)
  (if (all-zero-bitvp cb)
      3
    (plus
     10 (if (all-zero-bitvp (and-bitv cb bv)) 0 2)
     (highest-bit-loop-clock (append (cdr cb) '(0)) bv)))
  ((lessp (difference (length cb) (trailing-zeros cb)))))

(defn highest-bit-induct (current bv cb)
  (if (all-zero-bitvp cb)
      t
    (highest-bit-induct 
     (if (all-zero-bitvp (and-bitv cb bv)) current cb)
     bv
     (append (cdr cb) '(0))))
  ((lessp (difference (length cb) (trailing-zeros cb)))))

(prove-lemma bit-vectorp-simple-not (rewrite)
	     (implies
	      (not (equal (length x) (fix y)))
	      (not (bit-vectorp x y))))

(prove-lemma at-most-one-bit-on-cdr (rewrite)
	     (implies
	      (at-most-one-bit-on x)
	      (at-most-one-bit-on (cdr x))))


(prove-lemma equal-one-bit-vector (rewrite)
	     (equal
	      (equal x (one-bit-vector z))
	      (or
	       (and
		(zerop z)
		(equal x '(1)))
	       (and
		(bit-vectorp x z)
		(all-zero-bitvp (all-but-last x))
		(not (equal (last x) 0))))))

(prove-lemma at-most-one-bit-is-all-zeros (rewrite)
	     (implies
	      (not (equal (last x) 0))
	      (equal
	       (at-most-one-bit-on x)
	       (all-zero-bitvp (all-but-last x)))))

(defn highest-bit2-helper (current cb bv)
  (if (all-zero-bitvp cb)
      current
    (highest-bit2-helper
     (if (all-zero-bitvp (and-bitv bv cb)) current cb)
     (append (cdr cb) '(0))
     bv))
  ((lessp (difference (length cb) (trailing-zeros cb)))))

(prove-lemma equal-x-zero-bit-vector (rewrite)
	     (equal
	      (equal x (zero-bit-vector y))
	      (and
	       (all-zero-bitvp x)
	       (bit-vectorp x y))))

(prove-lemma all-zero-bitvp-all-but-last-simple (rewrite)
	     (implies
	      (all-zero-bitvp x)
	      (all-zero-bitvp (all-but-last x))))

(prove-lemma equal-trailing-zeros-acc-irrelevant (rewrite)
	     (equal
	      (equal (trailing-zeros-helper x acc1)
		     (trailing-zeros-helper x acc2))
	      (or
	       (equal (fix acc1) (fix acc2))
	       (not (all-zero-bitvp x)))))

(prove-lemma lessp-trailing-zeros (rewrite)
	     (implies
	      (not (all-zero-bitvp z))
	      (lessp (trailing-zeros-helper z acc)
		     (length z))))

(prove-lemma nthcdr-append (rewrite)
	     (equal (nthcdr n (append x y))
		    (if (lessp (length x) n)
			(nthcdr (difference n (length x)) y)
		      (append (nthcdr n x) y))))

(prove-lemma listp-zero-bit-vector (rewrite)
	     (equal
	      (listp (zero-bit-vector x))
	      (not (zerop x))))

(prove-lemma and-bitv-append (rewrite)
	     (equal
	      (and-bitv (append x y) z)
	      (append 
	       (and-bitv x (make-list-from (length x) z))
	       (and-bitv y (nthcdr (length x) z))))
	     ((induct (double-cdr-induct x z))))

(prove-lemma and-bitv-append2 (rewrite)
	     (implies
	      (equal (length (append x y)) (length z))
	     (equal
	      (and-bitv z (append x y))
	      (append 
	       (and-bitv x (make-list-from (length x) z))
	       (and-bitv y (nthcdr (length x) z)))))
	     ((induct (double-cdr-induct x z))))

(prove-lemma all-zero-bitvp-and-bitv-append (rewrite)
	     (equal
	      (all-zero-bitvp (and-bitv z (append x y)))
	      (and
	       (all-zero-bitvp (and-bitv (make-list-from (length x) z) x))
	       (all-zero-bitvp (and-bitv (nthcdr (length x) z) y))))
	     ((induct (double-cdr-induct x z))))

(prove-lemma length-cdr-zero-bit-vector (rewrite)
	     (equal
	      (length (cdr (zero-bit-vector x)))
	      (sub1 x)))

(prove-lemma length-nthcdr (rewrite)
	     (equal
	      (length (nthcdr n x))
	      (difference (length x) n)))

(disable and-bitv-special)
(disable and-bitv-special-special)
(disable and-bitv-special-3)
(disable and-bitv-special-4)
(disable and-bitv-special-5)
(disable and-bitv-special-6)


(prove-lemma bit-vectorp-zero-bit-vector-better (rewrite)
	     (equal
	      (bit-vectorp (zero-bit-vector x) size)
	      (equal (fix x) (fix size))))

(prove-lemma highest-bit-correctness-general nil
	     (implies
	      (and
	       (not (zerop word-size))
	       (at-most-one-bit-on cb)
	       (listp ctrl-stk)
	       (at-least-morep (length temp-stk)
			       3 max-temp-stk-size)
	       (equal (definition 'highest-bit prog-segment)
		      (highest-bit-program))
	       (bit-vectorp bv word-size)
	       (bit-vectorp cb word-size)
	       (bit-vectorp current word-size))
	      (equal
	       (p (p-state '(pc (highest-bit . 3))
			   (cons (list
				  (list 
				   (cons 'bv (list 'bitv bv))
				   (cons 'cb (list 'bitv cb)))
				  ret-pc)
				 ctrl-stk)
			   (cons (list 'bitv current) temp-stk)
			   prog-segment
			   data-segment
			   max-ctrl-stk-size
			   max-temp-stk-size
			   word-size
			   'run)
		  (highest-bit-loop-clock cb bv))
	       (p-state ret-pc
			ctrl-stk
			(cons 
			 (list 'bitv
			       (highest-bit2-helper current cb bv))
			 temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((induct (highest-bit-induct current bv cb))))

(prove-lemma make-list-from-simple (rewrite)
	     (implies
	      (zerop n)
	      (equal (make-list-from n x) nil)))

(prove-lemma not-all-zero-bitvp-make-list-from (rewrite)
	     (implies
	      (and
	       (all-zero-bitvp (make-list-from n1 x))
	       (not (lessp n1 n2)))
	      (all-zero-bitvp (make-list-from n2 x))))

(disable nthcdr-open)

;(prove-lemma listp-append (rewrite)
;	     (equal
;	      (listp (append x y))
;	      (or (listp x) (listp y))))
(enable listp-append)

(prove-lemma highest-bit2-helper-cons-1 (rewrite)
	     (implies
	      (and
	       (not (all-zero-bitvp cb))
	       (at-most-one-bit-on cb)
	       (equal (length cb) (length bv))
	       (bit-vectorp cb (length cb))
	       (equal (car bv) 1))
	     (equal
	      (highest-bit2-helper current cb bv)
	      (cons 1 (zero-bit-vector (length (cdr bv)))))))

(prove-lemma bit-vectorp-append-cdr-hack (rewrite)
	     (implies
	      (bit-vectorp x n)
	      (equal (bit-vectorp (append (cdr x) '(0)) n)
		     (listp x))))

(defn triple-cdr-with-sub1-induct (x y z n)
  (if (zerop n) t
    (triple-cdr-with-sub1-induct (cdr x) (cdr y) (cdr z) (sub1 n))))


(prove-lemma car-append-better (rewrite)
	     (equal
	      (car (append x y))
	      (if (listp x) 
		  (car x)
		(car y))))

(prove-lemma open-highest-when-and-not-0 (rewrite)
	     (implies
	      (and
	       (not (all-zero-bitvp (and-bitv x y)))
	       (equal (length x) (length y)))
	      (equal (highest-bit2-helper c x y)
		     (highest-bit2-helper x (append (cdr x) '(0)) y))))

;(prove-lemma cdr-append (rewrite)
;	     (equal
;	      (cdr (append x y))
;	      (if (listp x)
;		  (append (cdr x) y)
;		(cdr y))))
(enable cdr-append)

(prove-lemma highest-bit2-helper-cons-0 (rewrite)
	     (implies
	      (and
	       (not (all-zero-bitvp cb))
	       (at-most-one-bit-on cb)
	       (bit-vectorp cb size)
	       (bit-vectorp bv size)
	       (bit-vectorp current size)
	       (equal (car bv) 0)
	       (equal (car current) 0))
	     (equal
	      (highest-bit2-helper current cb bv)
	      (cons 0 (highest-bit2-helper 
		       (cdr current) (cdr cb) (cdr bv)))))
	     ((expand (highest-bit2-helper z x v))))

(prove-lemma highest-bit2-helper-cons-0-rewrite (rewrite)
	     (implies
	      (and
	       (not (all-zero-bitvp cb))
	       (at-most-one-bit-on cb)
	       (bit-vectorp cb (length cb))
	       (bit-vectorp bv (length cb))
	       (bit-vectorp current (length cb))
	       (equal (car bv) 0)
	       (equal (car current) 0))
	     (equal
	      (highest-bit2-helper current cb bv)
	      (cons 0 (highest-bit2-helper 
		       (cdr current) (cdr cb) (cdr bv)))))
	     ((use (highest-bit2-helper-cons-0 (size (length cb))))))

(prove-lemma append-zeros-0 (rewrite)
	     (implies
	      (and
	       (all-zero-bitvp x)
	       (properp x))
	      (equal (append x '(0)) (cons 0 x))))

(prove-lemma highest-bit2-helper-cons-helper nil
	     (implies
	      (and
	       (bit-vectorp bv size)
	       (bit-vectorp cb size)
	       (at-most-one-bit-on cb)
	       (at-most-one-bit-on current)
	       (not (all-zero-bitvp cb))
	       (or
		(all-zero-bitvp current)
		(lessp (trailing-zeros current) (trailing-zeros cb)))
	       (bit-vectorp current size)
	       (not (zerop size)))
	       (equal
		(highest-bit2-helper current cb bv)
		(if (equal (car bv) 0)
		    (cons 0 (highest-bit2-helper (cdr current)
						 (cdr cb) (cdr bv)))
		  (cons 1 (zero-bit-vector (sub1 size))))))
	     ((induct (triple-cdr-with-sub1-induct
		       bv cb current size))))

(prove-lemma highest-bit2-helper-cons-helper-rewrite (rewrite)
	     (implies
	      (and
	       (bit-vectorp bv (length bv))
	       (bit-vectorp cb (length bv))
	       (at-most-one-bit-on cb)
	       (at-most-one-bit-on current)
	       (not (all-zero-bitvp cb))
	       (or
		(all-zero-bitvp current)
		(lessp (trailing-zeros current) (trailing-zeros cb)))
	       (bit-vectorp current (length bv))
	       (listp bv))
	       (equal
		(highest-bit2-helper current cb bv)
		(if (equal (car bv) 0)
		    (cons 0 (highest-bit2-helper (cdr current)
						 (cdr cb) (cdr bv)))
		  (cons 1 (zero-bit-vector (sub1 (length bv)))))))
	     ((use (highest-bit2-helper-cons-helper (size (length bv))))
	      (disable-theory t)
	      (enable equal-length-0)
	      (enable-theory ground-zero)))

(prove-lemma bit-vectorp-cdr-from-free (rewrite)
	     (implies
	      (bit-vectorp x n)
	      (equal (bit-vectorp (cdr x) s)
		     (equal (add1 s) n))))

(prove-lemma all-zero-bitvp-one-bit-vector (rewrite)
	     (not (all-zero-bitvp (one-bit-vector x))))

(prove-lemma trailing-zeros-one-bit-vector (rewrite)
	     (equal (trailing-zeros (one-bit-vector n)) 0))

(prove-lemma cdr-zero-one-bit-vector (rewrite)
	     (and
	      (equal (cdr (one-bit-vector x))
		     (if (lessp x 2) nil (one-bit-vector (sub1 x))))
	      (equal (cdr (zero-bit-vector x))
		     (if (zerop x) 0 (zero-bit-vector (sub1 x))))))

(prove-lemma highest-bit2-helper-highest-bit (rewrite)
	     (implies
	      (and
	       (bit-vectorp bv word-size)
	       (not (zerop word-size)))
	     (equal
	      (highest-bit2-helper (zero-bit-vector word-size) 
				   (one-bit-vector word-size) bv)
	      (highest-bit bv)))
	     ((induct (bit-vectorp bv word-size))
	      (disable-theory t)
	      (enable-theory ground-zero naturals)
	      (enable highest-bit2-helper-cons-helper-rewrite
		      bv-length-weaker LENGTH-FROM-BIT-VECTORP 
		      at-most-one-bit-on-one-bit-vector 
		      *1*zero-bit-vector *1*one-bit-vector
		      *1*highest-bit2-helper bitp
		      bit-vectorp cdr-zero-one-bit-vector
		      ALL-ZERO-BITVP-ZERO-BIT-VECTOR
		      bit-vectorp-simple-not length highest-bit
		      TRAILING-ZEROS-OF-ALL-ZERO-BITVP
		      bit-vectorp-zero-bit-vector-better
		      length-zero-bit-vector
		      trailing-zeros-one-bit-vector
		      all-zero-bitvp-one-bit-vector
		      ALL-ZERO-BITVP-MEANS-AT-MOST-ONE-BIT-ON
		      bit-vectorp-one-bit-vector-rewrite)))


(defn highest-bit-input-conditionp (p0)
  (and
   (equal (car (top (p-temp-stk p0))) 'bitv)
   (equal (cddr (top (p-temp-stk p0))) nil)
   (not (zerop (p-word-size p0)))
   (listp (p-ctrl-stk p0))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   6 (p-max-ctrl-stk-size p0))
   (at-least-morep (length (p-temp-stk p0))
		   2 (p-max-temp-stk-size p0))
   (equal (definition 'highest-bit (p-prog-segment p0))
	  (highest-bit-program))
   (equal (definition 'push-1-vector (p-prog-segment p0))
	  (push-1-vector-program (p-word-size p0)))
   (bit-vectorp (cadr (top (p-temp-stk p0))) (p-word-size p0))))

(defn highest-bit-clock (bv)
  (plus 6 (highest-bit-loop-clock (one-bit-vector (length bv)) bv)))

(prove-lemma cons-0-zero-bit-vector (rewrite)
	     (equal
	      (cons 0 (zero-bit-vector x))
	      (zero-bit-vector (add1 x))))

(disable cons-0-zero-bit-vector)

(prove-lemma correctness-of-highest-bit (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons b temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) 
		      '(call highest-bit))
	       (equal bc (cadr b))
	       (highest-bit-input-conditionp p0))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons b temp-stk)
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (highest-bit-clock bc))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons (list 'bitv (highest-bit (cadr b)))
			      temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((use (highest-bit-correctness-general 
		    (ret-pc (add1-addr pc))
		    (current (zero-bit-vector word-size))
		    (cb (one-bit-vector word-size))
		    (bv (cadr b))))
	      (expand (highest-bit-clock (cadr b)))
	      (enable cons-0-zero-bit-vector)
	      (disable highest-bit-loop-clock zero-bit-vector)))
	



;; match-and-xor

(defn match-and-xor-program ()
  '(match-and-xor (vecs numvecs match xor-vector) ((i (nat 0)))
		   (push-constant (nat 0))
		   (pop-local i)
	     (dl loop ()
		   (push-local vecs))
		   (fetch)
		   (push-local match)
		   (and-bitv)
		   (test-bitv-and-jump not-all-zeros found)
		   (push-local i)
		   (add1-nat)
		   (set-local i)
		   (push-local numvecs)
		   (lt-nat)
		   (test-bool-and-jump f done)
		   (push-local vecs)
		   (push-constant (nat 1))
		   (add-addr)
		   (pop-local vecs)
		   (jump loop)
	     (dl found ()
		   (push-local vecs))
		   (fetch)
		   (push-local xor-vector)
		   (xor-bitv)
		   (push-local vecs)
		   (deposit)
	      (dl done ()
		   (ret))))


(defn example-match-and-xor-p-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (arr . 0)))
			(push-constant (nat 6))
			(push-constant (bitv (0 0 0 1 0 0 0 0)))
			(push-constant (bitv (1 1 1 1 1 1 1 1)))
			(call match-and-xor)
			(ret))
		 (match-and-xor-program))
	   '((arr (bitv (0 1 0 0 1 0 0 1))
		  (bitv (0 0 0 0 0 0 0 1))
		  (bitv (0 0 0 1 0 0 0 1))
		  (bitv (0 0 0 0 0 0 0 1))
		  (bitv (0 0 0 1 0 0 0 1))
		  (bitv (0 1 1 0 1 0 0 1))))
	   10
	   8
	   8
	   'run))

(defn match-and-xor (bvs match xor-vector)
  (if (listp bvs)
      (if (all-zero-bitvp (and-bitv (car bvs) match))
	  (cons (car bvs) (match-and-xor (cdr bvs) match xor-vector))
	(cons (xor-bitv (car bvs) xor-vector) (cdr bvs)))
    nil))

(defn match-and-xor-loop-clock (bvs match)
  (if (listp bvs)
      (if (all-zero-bitvp (and-bitv (car bvs) match))
	  (if (listp (cdr bvs)) 
	    (plus 16 (match-and-xor-loop-clock (cdr bvs) match))
	    12)
	12)
    0))

(defn tag-array (tag array)
  (if (listp array)
      (cons (tag tag (car array))
	    (tag-array tag (cdr array)))
    nil))


(defn match-and-xor-general-induct (numvecs i)
  (if (lessp i numvecs)
      (match-and-xor-general-induct numvecs (add1 i))
    t)
  ((lessp (difference numvecs i))))

(prove-lemma tag-array-untag-array (rewrite)
  (implies
   (bit-vectors-piton x (length (untag (car x))))
   (equal (tag-array 'bitv (untag-array x)) x)))

(prove-lemma bit-vectors-piton-free-means (rewrite)
	     (implies
	      (bit-vectors-piton x size)
	      (and
	       (bit-vectors-piton x (length (cadr (car x))))
	       (equal
		(bit-vectors-piton (cdr x) (length (cadr (cadr x))))
		(listp x)))))

(prove-lemma listp-cdr-nthcdr (rewrite)
	     (equal
	      (listp (cdr (nthcdr i x)))
	      (lessp i (length (cdr x)))))

(prove-lemma nthcdr-untag-array (rewrite)
	      (equal
	       (nthcdr i (untag-array x))
	       (if (lessp i (length x))
		   (untag-array (nthcdr i x))
		 (if (equal (fix i) (length x)) nil 0))))

(prove-lemma put-length-cdr (rewrite)
	     (implies
	      (properp x)
	     (equal
	      (put val (length (cdr x)) x)
	      (append (all-but-last x) (list val)))))

(prove-lemma nthcdr-length-cdr (rewrite)
	     (implies
	      (properp x)
	     (equal
	      (nthcdr (length (cdr x)) x)
	      (if (listp x) (list (last x)) nil))))

(prove-lemma get-length-cdr (rewrite)
	     (equal
	      (get (length (cdr x)) x)
	      (if (listp x) (last x) 0)))

(prove-lemma append-all-but-last-last (rewrite)
	     (implies
	      (properp x)
	      (equal
	       (append (all-but-last x) (list (last x)))
	       (if (nlistp x) (list (last x)) x))))

(prove-lemma listp-cdr-untag-array (rewrite)
	     (equal
	      (listp (cdr (untag-array x)))
	      (listp (cdr x))))

(prove-lemma bit-vectorp-last (rewrite)
	     (implies
	      (bit-vectors-piton bvs s)
	      (equal (bit-vectorp (cadr (last bvs)) s) (listp bvs))))

(prove-lemma bit-vectors-piton-means-properp (rewrite)
	     (implies
	      (bit-vectors-piton x s)
	      (properp x)))

(prove-lemma bit-vectors-piton-means-last (rewrite)
	     (implies
	      (and
	       (bit-vectors-piton state size)
	       (listp state))
	      (and
	       (equal (car (last state)) 'bitv)
	       (listp (last state))
	       (bit-vectorp (cadr (last state)) size)
	       (equal (cddr (last state)) nil)
	       (equal (length (cadr (last state))) (fix size))))
	     ((disable bit-vectorp-last)))

(prove-lemma list-bitv-cadr-bitvp (rewrite)
	     (implies
	      (and
	       (equal (car x) 'bitv)
	       (equal (cddr x) nil))
	      (equal (list 'bitv (cadr x)) x)))

(prove-lemma equal-x-put-assoc-x (rewrite)
	     (equal
	      (equal x (put-assoc val name  x))
	      (or
	       (not (definedp name x))
	       (equal (assoc name x) (cons name val)))))

(prove-lemma cons-n-assoc-n (rewrite)
	     (implies
	      (listp (assoc n d))
	      (equal (cons n (cdr (assoc n d)))
		     (if (definedp n d)
			 (assoc n d)
		       (cons n 0)))))

(prove-lemma cons-n-cadr-list-assoc-n (rewrite)
	     (implies
	       (equal (cddr (assoc n d)) nil)
	      (equal (list n (cadr (assoc n d)))
		     (if (definedp n d)
			 (assoc n d)
		       (cons n 0)))))

(prove-lemma cons-n-assoc-n-hack (rewrite)
         (implies
         (listp (cdr (assoc n d)))
         (equal (cons n (cdr (assoc n d)))
              (if (definedp n d)
                  (assoc n d)
                   (cons n 0)))))

(prove-lemma car-untag-array (rewrite)
	     (equal
	      (car (untag-array x))
	      (untag (car x))))

(prove-lemma car-nthcdr (rewrite)
	     (equal
	      (car (nthcdr i x))
	      (get i x)))


(prove-lemma tag-array-cdr-untag-array-hack (rewrite)
	     (implies
	      (bit-vectors-piton x (length (untag (car x))))
	     (equal
	      (tag-array 'bitv (cdr (untag-array x)))
	      (if (listp x) (cdr x) nil))))
		
(prove-lemma bit-vectors-piton-means-car (rewrite)
	     (implies
	      (and
	       (bit-vectors-piton state size)
	       (listp state))
	      (and
	       (equal (caar state) 'bitv)
	       (listp (car state))
	       (bit-vectorp (cadr (car state)) size)
	       (equal (cddr (car state)) nil)
	       (equal (length (cadr (car state))) (fix size)))))

(prove-lemma equal-put-assoc (rewrite)
	     (equal
	      (equal (put-assoc v1 n s) (put-assoc v2 n s))
	      (or
	       (not (definedp n s))
	       (equal v1 v2))))

(prove-lemma get-nlistp-better (rewrite)
	     (implies
	      (not (lessp i (length x)))
	      (equal (get i x) 0)))

(prove-lemma equal-append-zero-bit-vector-zero-bit-vector (rewrite)
	     (equal
	      (equal (append (zero-bit-vector n1) x)
		     (append (zero-bit-vector n2) y))
	      (if (lessp n1 n2)
		  (equal  
		   x (append (zero-bit-vector (difference n2 n1)) y))
		(equal 
		 y (append (zero-bit-vector (difference n1 n2)) x)))))
		
(prove-lemma append-make-list-from-cons-get-hack (rewrite)
	     (equal
	      (append (make-list-from i x) (cons (get i x) y))
	      (append (make-list-from (add1 i) x) y)))

(prove-lemma cdr-untag-array-nthcdr (rewrite)
	     (implies
	      (lessp i (length x))
	      (equal
	       (cdr (untag-array (nthcdr i x)))
	       (untag-array (nthcdr i (cdr x))))))

(prove-lemma equal-nil-nthcdr-length (rewrite)
	     (equal
	      (equal nil (nthcdr (length x) x))
	      (properp x)))

(prove-lemma lessp-0-length-better (rewrite)
	     (implies
	      (zerop x)
	      (equal (lessp x (length y)) (listp y))))

(prove-lemma bit-vectors-piton-means-get-cdr (rewrite)
	     (implies
	      (bit-vectors-piton state size)
	      (and
	       (equal (car (get i (cdr state))) 
		      (if (lessp i (length (cdr state))) 'bitv 0))
	       (equal (listp (get i (cdr state)))
		      (lessp i (length (cdr state))))
	       (equal (bit-vectorp (cadr (get i (cdr state))) size)
		      (lessp i (length (cdr state))))
	       (equal (cddr (get i (cdr state))) 
		      (if (lessp i (length (cdr state))) nil 0))
	       (equal (length (cadr (get i (cdr state)))) 
		      (if (lessp i (length (cdr state))) (fix size) 0))))
	     ((induct (get i state))))

(prove-lemma bit-vectors-piton-nthcdr (rewrite)
	     (implies
	      (bit-vectors-piton x s1)
	      (and
	       (equal (bit-vectors-piton (nthcdr i x) s)
		      (or
		       (and
			(lessp i (length x))
			(equal (fix s1) (fix s)))
		       (equal (fix i) (length x))))
	       (equal (bit-vectors-piton (nthcdr i (cdr x)) s)
		      (and
		       (lessp i (length x))
		       (or (equal (fix s) (fix s1))
			   (equal (fix i) (length (cdr x)))))))))

(prove-lemma tag-array-untag-array-nthcdr-cddr-hack (rewrite)
	     (implies
	      (and
	       (lessp i (length x))
	       (bit-vectors-piton x s))
	      (equal
	       (tag-array 'bitv (untag-array (nthcdr i (cdr x))))
	       (nthcdr i (cdr x))))
	     ((use (tag-array-untag-array (x (nthcdr i (cdr x)))))))

(prove-lemma append-make-list-from-put-hack (rewrite)
	     (implies
	      (lessp i (length x))
	     (equal
	      (append
	       (make-list-from i x)
	       (cons v (nthcdr i (cdr x))))
	      (put v i x))))

(enable lessp-sub1-x-x)
(enable lessp-x-x)

(prove-lemma correctness-of-match-and-xor-general nil
	     (implies
	      (and
	          (listp ctrl-stk)
		  (at-least-morep (p-ctrl-stk-size ctrl-stk)
				  7 max-ctrl-stk-size)
		  (at-least-morep (length temp-stk)
				  4 max-temp-stk-size)
		  (equal (definition 'match-and-xor prog-segment) (match-and-xor-program))
		  (bit-vectorp match word-size)
		  (bit-vectorp xor-vector word-size)
		  (equal numvecs (length (array vecs data-segment)))
		  (bit-vectors-piton (array vecs data-segment) word-size)
		  (definedp vecs data-segment)
		  (numberp i)
		  (lessp i numvecs)
		  (lessp (length (array vecs data-segment)) (exp 2 word-size)))
	      (equal
	       (p 
		(p-state '(pc (match-and-xor . 2))
			 (cons (list
				(list
				 (cons 'vecs (list 'addr (cons vecs i)))
				 (cons 'numvecs (list 'nat numvecs))
				 (cons 'match (list 'bitv match))
				 (cons 'xor-vector (list 'bitv xor-vector))
				 (cons 'i (list 'nat i)))
				ret-pc)
			       ctrl-stk)
			 temp-stk
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run)
		(match-and-xor-loop-clock 
		 (nthcdr i (untag-array (array vecs data-segment))) match))
	       (p-state
		ret-pc
		ctrl-stk
		temp-stk
		prog-segment
		(put-assoc
		 (append (make-list-from i (array vecs data-segment))
			 (tag-array 'bitv
				    (match-and-xor
				     (untag-array (nthcdr i (array vecs data-segment)))
				     match xor-vector)))
		 vecs data-segment)
		max-ctrl-stk-size
		max-temp-stk-size
		word-size
		'run)))
	     ((induct (match-and-xor-general-induct numvecs i))
	      (disable bit-vectors-piton)
	      (expand      
	       (match-and-xor-loop-clock
		(untag-array (nthcdr i (cdr (assoc vecs data-segment))))
		match)
	       (match-and-xor-loop-clock
		(untag-array (nthcdr (length (cddr (assoc vecs data-segment)))
				     (cdr (assoc vecs data-segment))))
		match))))

(defn match-and-xor-clock (bvs match)
  (plus 3 (match-and-xor-loop-clock bvs match)))


(defn match-and-xor-input-conditionp (p0)
  (and
   (equal (car (top (p-temp-stk p0))) 'bitv)
   (equal (cddr (top (p-temp-stk p0))) nil)
   (equal (car (top (cdr (p-temp-stk p0)))) 'bitv)
   (equal (cddr (top (cdr (p-temp-stk p0)))) nil)
   (equal (car (top (cddr (p-temp-stk p0)))) 'nat)
   (equal (cddr (top (cddr (p-temp-stk p0)))) nil)
   (equal (car (top (cdddr (p-temp-stk p0)))) 'addr)
   (equal (cdr (cadr (top (cdddr (p-temp-stk p0))))) 0)
   (listp (cadr (top (cdddr (p-temp-stk p0)))))
   (equal (cddr (top (cdddr (p-temp-stk p0)))) nil)
   (not (zerop (cadr (top (cddr (p-temp-stk p0))))))
   (listp (p-ctrl-stk p0))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   7 (p-max-ctrl-stk-size p0))
   (at-least-morep (length (p-temp-stk p0))
		   0 (p-max-temp-stk-size p0))
   (equal (definition 'match-and-xor (p-prog-segment p0))
	  (match-and-xor-program))
   (bit-vectorp (cadr (top (cdr (p-temp-stk p0)))) (p-word-size p0))
   (bit-vectorp (cadr (top (p-temp-stk p0))) (p-word-size p0))
   (equal (cadr (top (cddr (p-temp-stk p0)))) 
	  (length (array (car (cadr (top (cdddr (p-temp-stk p0)))))
			 (p-data-segment p0))))
   (definedp (car (cadr (top (cdddr (p-temp-stk p0)))))
     (p-data-segment p0))
   (lessp (length (array (car (cadr (top (cdddr (p-temp-stk p0)))))
			 (p-data-segment p0))) 
	  (exp 2 (p-word-size p0)))
   (bit-vectors-piton 
    (array (car (cadr (top (cdddr (p-temp-stk p0)))))
	   (p-data-segment p0)) 
    (p-word-size p0))))

(prove-lemma correctness-of-match-and-xor (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons x (cons m (cons n (cons v temp-stk))))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) '(call match-and-xor))
	       (match-and-xor-input-conditionp p0)
	       (equal match (cadr m))
	       (equal vecs-to-match 
		      (untag-array (array (caadr v) data-segment))))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons x (cons m (cons n (cons v temp-stk))))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (match-and-xor-clock vecs-to-match match))
	       (p-state (add1-addr pc)
			ctrl-stk
			temp-stk
			prog-segment
			(put-assoc 
			 (tag-array 'bitv 
			  (match-and-xor  
			   (untag-array 
			    (array (caadr v) data-segment)) 
			   (cadr m) (cadr x)))
			  (caadr v) data-segment)
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	     ((disable match-and-xor-loop-clock)
	      (use (correctness-of-match-and-xor-general
		    (ret-pc (add1-addr pc)) (i 0)
		    (xor-vector (cadr x)) (match (cadr m))
		    (numvecs (cadr n)) (vecs (caadr v))))))

;;; nat-to-bv-list

(defn nat-to-bv-list-program ()
  '(nat-to-bv-list (nat-list bv-list length) ((i (nat 0)))
              (dl loop ()
		    (push-local nat-list))
		    (fetch)
		    (call nat-to-bv)
		    (push-local bv-list)
		    (deposit)
		    (push-local i)
		    (add1-nat)
		    (set-local i)
		    (push-local length)
		    (eq)
		    (test-bool-and-jump t done)
		    (push-local nat-list)
		    (push-constant (nat 1))
		    (add-addr)
		    (pop-local nat-list)
		    (push-local bv-list)
		    (push-constant (nat 1))
		    (add-addr)
		    (pop-local bv-list)
		    (jump loop)
		(dl done () (ret))))

(defn example-nat-to-bv-list-p-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (arr . 0)))
			(push-constant (addr (arr2 . 0)))
			(push-constant (nat 6))
			(call nat-to-bv-list)
			(ret))
		 (nat-to-bv-list-program)
		 (nat-to-bv-program)
		 (push-1-vector-program 8))
	   '((arr (nat 3)
		  (nat 5)
		  (nat 8)
		  (nat 0)
		  (nat 23)
		  (nat 9))
	     (arr2 nil nil nil nil nil nil))
	   100
	   80
	   8
	   'run))

(defn nat-to-bv-list (nat-list size)
  (if (listp nat-list)
      (cons
       (nat-to-bv (car nat-list) size)
       (nat-to-bv-list (cdr nat-list) size))
    nil))

(defn nat-to-bv-list-loop-clock (i nats)
       (if (lessp i (length nats))
           (clock-plus '2
               (clock-plus (nat-to-bv-clock (untag (get i nats)))
                   (if (lessp i (length (cdr nats)))
                       (clock-plus '17
                           (nat-to-bv-list-loop-clock (add1 i) nats))
                       '9)))
           '0)
       ((lessp (difference (length nats) i))))

(defn nat-to-bv-list-loop-induct (i nats bvs-name word-size data-segment)
  (if (and (lessp i (length nats))
	   (lessp i (length (cdr nats))))
      (nat-to-bv-list-loop-induct
       (add1 i) nats bvs-name word-size
       (put-assoc (append 
		   (make-list-from i (cdr (assoc bvs-name data-segment)))
		   (cons 
		    (list 'bitv (nat-to-bv (untag (get i nats)) word-size))
		    (nthcdr (add1 i) (cdr (assoc bvs-name data-segment)))))
		  bvs-name data-segment))
    t)
  ((lessp (difference (length nats) i))))



(prove-lemma nat-list-piton-means-car (rewrite)
	     (implies
	      (and
	       (nat-list-piton state size)
	       (listp state))
	      (and
	       (equal (caar state) 'nat)
	       (listp (car state))
	       (numberp (cadr (car state)))
	       (lessp (cadr (car state)) (exp 2 size))
	       (equal (lessp (cadr (car state)) (exp 2 size)) t)
	       (equal (cddr (car state)) nil))))

(defn array-pitonp (array length)
  (if (listp array)
      (and
       (not (zerop length))
       (array-pitonp (cdr array) (sub1 length)))
    (and
     (equal array nil)
     (zerop length))))


(prove-lemma nat-list-piton-means-last (rewrite)
	     (implies
	      (nat-list-piton state size)
	      (and
	       (equal (car (last state)) (if (listp state) 'nat 0))
	       (equal (listp (last state)) (listp state))
	       (numberp (cadr (last state)))
	       (equal (lessp (cadr (last state)) (exp 2 size)) t)
	       (equal (cddr (last state)) (if (listp state) nil 0)))))

(prove-lemma nat-list-piton-means-last-cdr (rewrite)
	     (implies
	      (and
	       (nat-list-piton state size)
	       (listp state))
	      (and
	       (equal (car (last (cdr state))) 
		      (if (listp (cdr state)) 'nat 0))
	       (equal (listp (last (cdr state))) (listp (cdr state)))
	       (numberp (cadr (last (cdr state))))
	       (equal (lessp (cadr (last (cdr state))) (exp 2 size)) t)
	       (equal (cddr (last (cdr state))) 
		      (if (listp (cdr state)) nil 0)))))

;(prove-lemma definedp-put-assoc (rewrite)
;	     (equal
;	      (definedp n (put-assoc v n1 a))
;	      (definedp n a)))
(enable definedp-put-assoc)

(prove-lemma assoc-put-assoc-better (rewrite)
	     (equal (assoc n1 (put-assoc v n2 a))
		    (if (definedp n1 a)
			(if (equal n1 n2)
			    (cons n1 v)
			  (assoc n1 a))
		      f)))

(disable nat-to-bv-list-loop-clock)

(prove-lemma get-add1 (rewrite)
	     (implies
	      (lessp n 4)
	      (equal (get (add1 n) x) (get n (cdr x)))))

(prove-lemma get-0-better (rewrite)
	     (implies
	      (zerop n)
	      (equal (get n x) (car x))))

(prove-lemma length-cdr-tag-array (rewrite)
	     (equal
	      (length (cdr (tag-array l x)))
	      (length (cdr x))))

(prove-lemma length-nat-to-bv-list (rewrite)
	     (equal
	      (length (nat-to-bv-list x s))
	      (length x)))

(prove-lemma length-cdr-nat-to-bv-list (rewrite)
	     (equal
	      (length (cdr (nat-to-bv-list x s)))
	      (length (cdr x))))

(prove-lemma length-tag-array (rewrite)
	     (equal
	      (length (tag-array l x))
	      (length x)))

(prove-lemma listp-tag-array (rewrite)
	     (equal
	      (listp (tag-array l x))
	      (listp x)))

(prove-lemma listp-nat-to-bv-list (rewrite)
	     (equal
	      (listp (nat-to-bv-list x s))
	      (listp x)))

(prove-lemma array-pitonp-tag-array (rewrite)
	     (equal
	      (array-pitonp (tag-array l x) length)
	      (equal (length x) (fix length)))
	     ((induct (array-pitonp x length))))

(prove-lemma array-pitonp-append (rewrite)
	     (equal
	      (array-pitonp (append x y) size)
	      (and
	       (not (lessp size (length x)))
	       (array-pitonp y (difference size (length x)))))
	     ((induct (get size x))))

(prove-lemma nat-list-piton-means-cadr (rewrite)
	     (implies
	      (and
	       (nat-list-piton state size)
	       (listp (cdr state)))
	      (and
	       (equal (caadr state) 'nat)
	       (listp (cadr state))
	       (numberp (cadr (cadr state)))
	       (lessp (cadr (cadr state)) (exp 2 size))
	       (equal (lessp (cadr (cadr state)) (exp 2 size)) t)
	       (equal (cddr (cadr state)) nil))))

(prove-lemma array-pitonp-add1 (rewrite)
	     (equal
	      (array-pitonp x (add1 n))
	      (and
	       (listp x)
	       (array-pitonp (cdr x) n))))

;(prove-lemma put-assoc-put-assoc (rewrite)
;	     (equal
;	      (put-assoc v n (put-assoc v2 n a))
;	      (put-assoc v n a)))
(enable put-assoc-put-assoc)

(prove-lemma length-cdr-nlistp (rewrite)
	     (implies
	      (not (listp (cdr x)))
	      (equal (length x) (if (listp x) 1 0))))

(prove-lemma equal-nil-cdr-tag-array-hack (rewrite)
	     (equal
	      (equal nil (cdr (tag-array l x)))
	      (equal (length x) 1)))

(prove-lemma length-from-array-pitonp (rewrite)
	     (implies
	      (array-pitonp x s)
	      (equal (length x) (fix s))))

(disable nat-to-bv-clock)

(disable nat-to-bv-list-loop-clock)

(prove-lemma nat-list-piton-means-get (rewrite)
	     (implies
	      (nat-list-piton state size)
	      (and
	       (equal (car (get p state)) 
		      (if (lessp p (length state)) 'nat 0))
	       (equal (listp (get p state)) (lessp p (length state)))
	       (numberp (cadr (get p state)))
	       (equal (lessp (cadr (get p state)) (exp 2 size)) t)
	       (equal (cddr (get p state)) 
		      (if (lessp p (length state)) nil 0)))))

(prove-lemma nat-list-piton-means-get-cdr (rewrite)
	     (implies
	      (and
	       (nat-list-piton state size)
	       (listp state))
	      (and
	       (equal (car (get p (cdr state)) )
		      (if (lessp p (length (cdr state))) 'nat 0))
	       (equal (listp (get p (cdr state))) (lessp p (length (cdr state))))
	       (numberp (cadr (get p (cdr state))))
	       (equal (lessp (cadr (get p (cdr state))) (exp 2 size)) t)
	       (equal (cddr (get p (cdr state))) 
		      (if (lessp p (length (cdr state))) nil 0)))))

(disable nat-list-piton-means)

(prove-lemma length-put-better (rewrite)
	     (equal (length (put v n a))
		    (if (lessp n (length a)) (length a) (add1 n))))

(prove-lemma cons-car-x-put-append-make-list-from-hack (rewrite)
	     (equal
	      (cons (car (put v x b)) 
		    (append (make-list-from x (cdr (put v x b))) y))
	      (append (make-list-from x b) (cons v y))))

(prove-lemma array-pitonp-put (rewrite)
	     (implies
	      (and
	       (array-pitonp a l)
	       (equal (fix l) (fix length)))
	      (equal
	       (array-pitonp (put v n a) length)
	       (lessp n (length a)))))


(prove-lemma array-pitonp-means-properp (rewrite)
	     (and
	      (implies (array-pitonp x s) (properp x))
	      (implies (array-pitonp (cdr x) s) (properp x))))

(prove-lemma put-length-cdr-general (rewrite)
	     (implies
	      (and
	       (properp x)
	       (equal (length x) (length y)))
	     (equal
	      (put val (length (cdr y)) x)
	      (append (all-but-last x) (list val)))))

(prove-lemma nthcdr-x-cdr-put-x (rewrite)
	     (implies
	      (properp a)
	     (equal
	      (nthcdr x (cdr (put val x a)))
	      (if (lessp x (length a))
		  (nthcdr x (cdr a))
		nil))))

(prove-lemma equal-append-a-append-a (rewrite)
	     (equal
	      (equal (append a b) (append a c))
	      (equal b c)))

;The correctness lemma of nat-to-bv-list could be more general - 
;the proof assumes the data areas are distinct, though the program
;works when they're not.  I did it this way because I had assumed
;I'd need distinct arrays in NIM, and designed the proof accordingly.
;This is a weakness I should correct in this proof as it will lead
;to sloppy use of memory in the program, but it takes so long
;to do these proofs I'll wait.


(prove-lemma correctness-of-nat-to-bv-list-general nil
	     (implies
	      (and
	          (listp ctrl-stk)
		  (at-least-morep (p-ctrl-stk-size ctrl-stk)
				  13 max-ctrl-stk-size)
		  (at-least-morep (length temp-stk) 
				  3 max-temp-stk-size)
		  (equal (definition 'nat-to-bv-list prog-segment)
			 (nat-to-bv-list-program))
		  (equal (definition 'nat-to-bv prog-segment)
			 (nat-to-bv-program))
		  (equal (definition 'push-1-vector prog-segment)
			 (push-1-vector-program word-size))
		  (equal length (length (array nats data-segment)))
		  (array-pitonp (array bvs data-segment) length)
		  (nat-list-piton (array nats data-segment) word-size)
		  (definedp nats data-segment)
		  (definedp bvs data-segment)
		  (not (zerop word-size))
		  (numberp i)
		  (lessp i length)
		  (lessp length (exp 2 word-size))
		  (not (equal nats bvs))
		  (equal natlist (array nats data-segment)))
	      (equal
	       (p 
		(p-state '(pc (nat-to-bv-list . 0))
			 (cons (list
				(list
				 (cons 'nat-list 
				       (list 'addr (cons nats i)))
				 (cons 'bv-list 
				       (list 'addr (cons bvs i)))
				 (cons 'length (list 'nat length))
				 (cons 'i (list 'nat i)))
				ret-pc)
			       ctrl-stk)
			 temp-stk
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run)
		(nat-to-bv-list-loop-clock i natlist))
	       (p-state
		ret-pc
		ctrl-stk
		temp-stk
		prog-segment
		(put-assoc
		 (append (make-list-from i (array bvs data-segment))
			 (tag-array 'bitv
				    (nat-to-bv-list 
				     (untag-array 
				      (nthcdr i (array nats data-segment)))
				     word-size)))
		 bvs data-segment)
		max-ctrl-stk-size
		max-temp-stk-size
		word-size
		'run)))
	     ((induct (nat-to-bv-list-loop-induct
		       i natlist bvs word-size data-segment))
	      (disable nat-list-piton)
	      (expand (ARRAY-PITONP (CDR (ASSOC BVS DATA-SEGMENT)) 1)
		      (UNTAG-ARRAY (CDR (ASSOC NATS DATA-SEGMENT)))
		      (UNTAG-ARRAY (CDR (ASSOC BVS DATA-SEGMENT)))
		      (NAT-TO-BV-LIST-LOOP-CLOCK 0
		       (CDR (ASSOC NATS DATA-SEGMENT)))
		      (nat-to-bv-list-loop-clock i natlist)
		      (NAT-TO-BV-LIST-LOOP-CLOCK i
		       (CDR (ASSOC NATS DATA-SEGMENT))))))

(defn nat-to-bv-list-clock (natlist)
  (clock-plus 1 (nat-to-bv-list-loop-clock 0 natlist)))

(defn nat-to-bv-list-input-conditionp (p0)
	      (and
	          (listp (p-ctrl-stk p0))
		  (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
				  13 (p-max-ctrl-stk-size p0))
		  (at-least-morep (length (p-temp-stk p0))
				  0 (p-max-temp-stk-size p0))
		  (equal (definition 'nat-to-bv-list (p-prog-segment p0))
			 (nat-to-bv-list-program))
		  (equal (definition 'nat-to-bv (p-prog-segment p0))
			 (nat-to-bv-program))
		  (equal (definition 'push-1-vector (p-prog-segment p0))
			 (push-1-vector-program (p-word-size p0)))
		  (equal (cadr (top (p-temp-stk p0))) (length (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0))))
		  (array-pitonp (array (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (cadr (top (p-temp-stk p0))))
		  (nat-list-piton (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)) (p-word-size p0))
		  (definedp (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0))
		  (definedp (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0))
		  (equal (p-current-instruction p0)
			 '(call nat-to-bv-list))
		  (not (zerop (p-word-size p0)))
		  (not (equal (caadr (top (cddr (p-temp-stk p0)))) (caadr (top (cdr (p-temp-stk p0))))))
		  (equal (car (top (p-temp-stk p0))) 'nat)
		  (not (zerop (cadr (top (p-temp-stk p0)))))
		  (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0)))
		  (equal (cddr (top (p-temp-stk p0))) nil)
		  (equal (car (top (cdr (p-temp-stk p0)))) 'addr)
		  (listp (cadr (top (cdr (p-temp-stk p0)))))
		  (equal (cdadr (top (cdr (p-temp-stk p0)))) 0)
		  (equal (cddr (top (cdr (p-temp-stk p0)))) nil)
		  (equal (car (top (cddr (p-temp-stk p0)))) 'addr)
		  (listp (cadr (top (cddr (p-temp-stk p0)))))
		  (equal (cdadr (top (cddr (p-temp-stk p0)))) 0)
		  (equal (cddr (top (cddr (p-temp-stk p0)))) nil)))

  
(prove-lemma correctness-of-nat-to-bv-list (rewrite)
	     (implies
	      (and
	       (equal p0
		      (p-state pc
			 ctrl-stk
			 (cons l (cons b (cons n temp-stk)))
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run))
	       (nat-to-bv-list-input-conditionp p0)
	       (equal natlist (array (caadr n) data-segment)))
	      (equal
	       (p 
		(p-state pc
			 ctrl-stk
			 (cons l (cons b (cons n temp-stk)))
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run)
		(nat-to-bv-list-clock natlist))
	       (p-state
		(add1-addr pc)
		ctrl-stk
		temp-stk
		prog-segment
		(put-assoc
		 (tag-array 'bitv
			    (nat-to-bv-list 
			     (untag-array 
			      (array (caadr n) data-segment))
			     word-size))
		 (caadr b) data-segment)
		max-ctrl-stk-size
		max-temp-stk-size
		word-size
		'run)))
	      ((use (correctness-of-nat-to-bv-list-general
		     (i 0) 
		     (ret-pc (LIST (CAR PC) (CONS (CAADR PC) (ADD1 (CDADR PC)))))
		     (nats (caadr n))
		     (bvs (caadr b))
		     (length (cadr l))))))


(disable nat-to-bv-list-program)
(disable match-and-xor-program)
(disable highest-bit-program)
(disable number-with-at-least-program)
(disable bv-to-nat-program)
(disable nat-to-bv-program)
(disable push-1-vector-program)
(disable xor-bvs-program)


;; bv-to-nat-list

(defn bv-to-nat-list-program ()
  '(bv-to-nat-list (bv-list nat-list length) ((i (nat 0)))
              (dl loop ()
		    (push-local bv-list))
		    (fetch)
		    (call bv-to-nat)
		    (push-local nat-list)
		    (deposit)
		    (push-local i)
		    (add1-nat)
		    (set-local i)
		    (push-local length)
		    (eq)
		    (test-bool-and-jump t done)
		    (push-local nat-list)
		    (push-constant (nat 1))
		    (add-addr)
		    (pop-local nat-list)
		    (push-local bv-list)
		    (push-constant (nat 1))
		    (add-addr)
		    (pop-local bv-list)
		    (jump loop)
		(dl done () (ret))))

(defn example-bv-to-nat-list-p-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (arr . 0)))
			(push-constant (addr (arr2 . 0)))
			(push-constant (nat 6))
			(call bv-to-nat-list)
			(ret))
		 (bv-to-nat-list-program)
		 (bv-to-nat-program)
		 (push-1-vector-program 8))
	   '((arr (bitv (0 1 0 1 0 1 0 0))
		  (bitv (1 1 1 1 1 1 1 1))
		  (bitv (0 1 0 1 0 1 0 0))
		  (bitv (0 1 0 1 0 1 0 0))
		  (bitv (0 0 0 0 0 0 0 0))
		  (bitv (0 1 0 1 0 1 0 0)))
      	     (arr2 nil nil nil nil nil nil))
	   100
	   80
	   8
	   'run))


(defn bv-to-nat-list-input-conditionp (p0)
	      (and
	          (listp (p-ctrl-stk p0))
		  (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
				  13 (p-max-ctrl-stk-size p0))
		  (at-least-morep (length (p-temp-stk p0))
				  0 (p-max-temp-stk-size p0))
		  (equal (definition 'bv-to-nat-list (p-prog-segment p0))
			 (bv-to-nat-list-program))
		  (equal (definition 'bv-to-nat (p-prog-segment p0))
			 (bv-to-nat-program))
		  (equal (definition 'push-1-vector (p-prog-segment p0))
			 (push-1-vector-program (p-word-size p0)))
		  (equal (cadr (top (p-temp-stk p0))) (length (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0))))
		  (array-pitonp (array (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0)) (cadr (top (p-temp-stk p0))))
		  (bit-vectors-piton (array (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0)) (p-word-size p0))
		  (definedp (caadr (top (cddr (p-temp-stk p0)))) (p-data-segment p0))
		  (definedp (caadr (top (cdr (p-temp-stk p0)))) (p-data-segment p0))
		  (equal (p-current-instruction p0)
			 '(call bv-to-nat-list))
		  (not (zerop (p-word-size p0)))
		  (not (equal (caadr (top (cddr (p-temp-stk p0)))) (caadr (top (cdr (p-temp-stk p0))))))
		  (equal (car (top (p-temp-stk p0))) 'nat)
		  (not (zerop (cadr (top (p-temp-stk p0)))))
		  (lessp (cadr (top (p-temp-stk p0))) (exp 2 (p-word-size p0)))
		  (equal (cddr (top (p-temp-stk p0))) nil)
		  (equal (car (top (cdr (p-temp-stk p0)))) 'addr)
		  (listp (cadr (top (cdr (p-temp-stk p0)))))
		  (equal (cdadr (top (cdr (p-temp-stk p0)))) 0)
		  (equal (cddr (top (cdr (p-temp-stk p0)))) nil)
		  (equal (car (top (cddr (p-temp-stk p0)))) 'addr)
		  (listp (cadr (top (cddr (p-temp-stk p0)))))
		  (equal (cdadr (top (cddr (p-temp-stk p0)))) 0)
		  (equal (cddr (top (cddr (p-temp-stk p0)))) nil)))

(defn bv-to-nat-list-loop-clock (wordsize i bvs)
       (if (lessp i (length bvs))
           (clock-plus '2
               (clock-plus (bv-to-nat-clock wordsize (untag (get i bvs)))
                   (if (lessp i (length (cdr bvs)))
                       (clock-plus '17
                           (bv-to-nat-list-loop-clock 
			    wordsize (add1 i) bvs))
                       '9)))
           '0)
       ((lessp (difference (length bvs) i))))

(defn bv-to-nat-list (bv-list)
  (if (listp bv-list)
      (cons
       (bv-to-nat (car bv-list))
       (bv-to-nat-list (cdr bv-list)))
    nil))

(defn bv-to-nat-list-loop-induct (i bvs nats-name data-segment)
  (if (and (lessp i (length bvs))
	   (lessp i (length (cdr bvs))))
      (bv-to-nat-list-loop-induct
       (add1 i) bvs nats-name
       (put-assoc (append 
		   (make-list-from i (cdr (assoc nats-name data-segment)))
		   (cons 
		    (list 'nat (bv-to-nat (untag (get i bvs))))
		    (nthcdr (add1 i) (cdr (assoc nats-name data-segment)))))
		  nats-name data-segment))
    t)
  ((lessp (difference (length bvs) i))))

(disable bv-to-nat-clock)

(prove-lemma correctness-of-bv-to-nat-list-general nil
	     (implies
	      (and
	          (listp ctrl-stk)
		  (at-least-morep (p-ctrl-stk-size ctrl-stk)
				  13 max-ctrl-stk-size)
		  (at-least-morep (length temp-stk) 
				  3 max-temp-stk-size)
		  (equal (definition 'bv-to-nat-list prog-segment)
			 (bv-to-nat-list-program))
		  (equal (definition 'bv-to-nat prog-segment)
			 (bv-to-nat-program))
		  (equal (definition 'push-1-vector prog-segment)
			 (push-1-vector-program word-size))
		  (equal length (length (array bvs data-segment)))
		  (bit-vectors-piton (array bvs data-segment) 
				      word-size)
		  (array-pitonp (array nats data-segment) length)
		  (definedp nats data-segment)
		  (definedp bvs data-segment)
		  (not (zerop word-size))
		  (numberp i)
		  (lessp i length)
		  (lessp length (exp 2 word-size))
		  (not (equal nats bvs))
		  (equal bvlist (array bvs data-segment)))
	      (equal
	       (p 
		(p-state '(pc (bv-to-nat-list . 0))
			 (cons (list
				(list
				 (cons 'bv-list 
				       (list 'addr (cons bvs i)))
				 (cons 'nat-list 
				       (list 'addr (cons nats i)))
				 (cons 'length (list 'nat length))
				 (cons 'i (list 'nat i)))
				ret-pc)
			       ctrl-stk)
			 temp-stk
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run)
		(bv-to-nat-list-loop-clock word-size i bvlist))
	       (p-state
		ret-pc
		ctrl-stk
		temp-stk
		prog-segment
		(put-assoc
		 (append (make-list-from i (array nats data-segment))
			 (tag-array 'nat
				    (bv-to-nat-list 
				     (untag-array 
				      (nthcdr i (array bvs data-segment))))))
		 nats data-segment)
		max-ctrl-stk-size
		max-temp-stk-size
		word-size
		'run)))
	     ((induct (bv-to-nat-list-loop-induct
		       i bvlist nats data-segment))
	      (disable bit-vectors-piton)
	      (expand (ARRAY-PITONP (CDR (ASSOC BVS DATA-SEGMENT)) 1)
		      (UNTAG-ARRAY (CDR (ASSOC NATS DATA-SEGMENT)))
		      (UNTAG-ARRAY (CDR (ASSOC BVS DATA-SEGMENT)))
		      (BV-TO-NAT-LIST-LOOP-CLOCK wordsize 0
		       (CDR (ASSOC NATS DATA-SEGMENT)))
		      (bv-to-nat-list-loop-clock wordsize i bvlist)
		      (BV-TO-NAT-LIST-LOOP-CLOCK wordsize i
		       (CDR (ASSOC NATS DATA-SEGMENT))))))


(defn bv-to-nat-list-clock (word-size natlist)
  (clock-plus 1 (bv-to-nat-list-loop-clock word-size 0 natlist)))

(disable bv-to-nat-list-loop-clock)

(disable bv-to-nat-list-program)

(prove-lemma correctness-of-bv-to-nat-list (rewrite)
	     (implies
	      (and
	       (equal p0
		      (p-state pc
			 ctrl-stk
			 (cons l (cons n (cons b temp-stk)))
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run))
	       (bv-to-nat-list-input-conditionp p0)
	       (equal bvlist (array (caadr b) data-segment)))
	      (equal
	       (p 
		(p-state pc
			 ctrl-stk
			 (cons l (cons n (cons b temp-stk)))
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run)
		(bv-to-nat-list-clock word-size bvlist))
	       (p-state
		(add1-addr pc)
		ctrl-stk
		temp-stk
		prog-segment
		(put-assoc
		 (tag-array 'nat
			    (bv-to-nat-list 
			     (untag-array 
			      (array (caadr b) data-segment))))
		 (caadr n) data-segment)
		max-ctrl-stk-size
		max-temp-stk-size
		word-size
		'run)))
	      ((use (correctness-of-bv-to-nat-list-general
		     (i 0) 
		     (ret-pc (LIST (CAR PC) (CONS (CAADR PC) (ADD1 (CDADR PC)))))
		     (nats (caadr n))
		     (bvs (caadr b))
		     (length (cadr l))))))

;; max-nat


(defn max-nat-program ()
  '(max-nat (nat-list length)  ((i (nat 0)) (j (nat 0)))
	            (push-constant (nat 0))
              (dl loop ()
		    (set-local j))
		    (push-local j)
		    (push-local nat-list)
		    (fetch)
		    (set-local j)
		    (lt-nat)
		    (test-bool-and-jump f lab)
		    (pop)
		    (push-local j)
	       (dl lab ()
		    (push-local i))
		    (add1-nat)
		    (set-local i)
		    (push-local length)
		    (eq)
		    (test-bool-and-jump t done)
		    (push-local nat-list)
		    (push-constant (nat 1))
		    (add-addr)
		    (pop-local nat-list)
		    (jump loop)
	       (dl done () (ret))))
		    

(defn example-max-nat-p-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (arr . 0)))
			(push-constant (nat 6))
			(call max-nat)
			(ret))
		 (max-nat-program))
	   '((arr (nat 3) (nat 10) (nat 3) (nat 6) (nat 9) (nat 0))
      	     (arr2 nil nil nil nil nil nil))
	   100
	   80
	   8
	   'run))

(defn max-list-helper (val x)
  (if (listp x)
      (if (lessp val (car x))
	  (max-list-helper (car x) (cdr x))
	(max-list-helper val (cdr x)))
    (fix val)))

(defn max-list (x)
  (if (listp x)
      (if (lessp (max-list (cdr x)) (car x))
	  (car x)
	(max-list (cdr x)))
    0))

(prove-lemma max-list-helper-max-list (rewrite)
	     (equal (max-list-helper val x)
		    (if (lessp (max-list x) val)
			val
		      (max-list x))))

(prove-lemma max-list-helper-max-list-0 (rewrite)
	     (equal (max-list-helper 0 x)
		    (max-list x)))

(disable max-list-helper-max-list)

(defn max-nat-loop-clock (val i nats)
  (if (lessp i (length nats))
       (if (lessp val (untag (get i nats)))
	   (if (lessp i (length (cdr nats)))
	       (clock-plus 20 
		(max-nat-loop-clock 
		 (untag (get i nats)) (add1 i) nats))
	     16)
	   (if (lessp i (length (cdr nats)))
	       (clock-plus 18 (max-nat-loop-clock val (add1 i) nats))
	     14))
    0)
  ((lessp (difference (length nats) i))))
	
(defn max-nat-loop-induct (i j x natlist length)
  (if (lessp i length)
      (max-nat-loop-induct 
       (add1 i) (get i natlist) 
       (if (lessp (untag (get i natlist)) (untag x)) 
	   (list 'nat (untag x)) (list 'nat (untag (get i natlist))))
       natlist length)
    t)
  ((lessp (difference length i))))


(prove-lemma list-nat-from-assoc-nat-list-piton-hack (rewrite)
	     (implies
	      (nat-list-piton nl s)
	      (and
	       (implies
		(lessp z (length (cdr nl)))
		(equal (list 'nat (cadr (get z (cdr nl)))) 
		       (get z (cdr nl))))
	       (implies
		(listp nl)
		(and
		 (equal 
		  (list 'nat (cadr (last nl)))
		  (last nl))
		(equal
		 (list 'nat (cadr (car nl)))
		 (car nl))))))
	     ((induct (get z nl))))

(prove-lemma correctness-of-max-nat-general nil
	     (implies
	      (and
	          (listp ctrl-stk)
		  (at-least-morep (p-ctrl-stk-size ctrl-stk)
				  4 max-ctrl-stk-size)
		  (at-least-morep (length temp-stk) 
				  4 max-temp-stk-size)
		  (equal (definition 'max-nat prog-segment)
			 (max-nat-program))
		  (equal length (length (array nats data-segment)))
		  (nat-list-piton (array nats data-segment) word-size)
		  (definedp nats data-segment)
		  (not (zerop word-size))
		  (numberp i)
		  (lessp i length)
		  (numberp (untag x))
		  (lessp (untag x) (exp 2 word-size))
		  (equal (car x) 'nat)
		  (equal (cddr x) nil)
		  (lessp length (exp 2 word-size))
		  (equal natlist (array nats data-segment)))
	      (equal
	       (p 
		(p-state '(pc (max-nat . 1))
			 (cons (list
				(list
				 (cons 'nat-list 
				       (list 'addr (cons nats i)))
				 (cons 'length (list 'nat length))
				 (cons 'i (list 'nat i))
				 (cons 'j j))
				ret-pc)
			       ctrl-stk)
			 (cons x
			  temp-stk)
			 prog-segment
			 data-segment
			 max-ctrl-stk-size
			 max-temp-stk-size
			 word-size
			 'run)
		(max-nat-loop-clock (untag x) i (array nats data-segment)))
	       (p-state
		ret-pc
		ctrl-stk
		(cons 
		 (list 'nat 
		       (max-list-helper (untag x)
			 (untag-array 
			  (nthcdr i (array nats data-segment)))))
		 temp-stk)
		prog-segment
		data-segment
		max-ctrl-stk-size
		max-temp-stk-size
		word-size
		'run)))
	      ((expand (MAX-NAT-LOOP-CLOCK 
			(cadr X) I (CDR (ASSOC NATS DATA-SEGMENT))))
	       (induct (max-nat-loop-induct i j x natlist length))))

(defn max-nat-clock (natlist)
  (clock-plus 2 (max-nat-loop-clock 0 0 natlist)))

(defn max-nat-input-conditionp (p0)
  (and
   (listp (p-ctrl-stk p0))
   (at-least-morep (p-ctrl-stk-size (p-ctrl-stk p0))
		   6 (p-max-ctrl-stk-size p0))
   (at-least-morep (length (p-temp-stk p0)) 
		   2 (p-max-temp-stk-size p0))
   (equal (definition 'max-nat (p-prog-segment p0))
	  (max-nat-program))
   (equal (untag (top (p-temp-stk p0)))
	 (length (array (car (untag (top (cdr (p-temp-stk p0)))))
			(p-data-segment p0))))
  (nat-list-piton (array (car (untag (top (cdr (p-temp-stk p0)))))
			 (p-data-segment p0))
		  (p-word-size p0))
  (definedp (car (untag (top (cdr (p-temp-stk p0)))))
    (p-data-segment p0))
  (not (zerop (p-word-size p0)))
  (not (zerop (untag (top (p-temp-stk p0)))))
  (equal (car (top (p-temp-stk p0))) 'nat)
  (equal (car (top (cdr (p-temp-stk p0)))) 'addr)
  (listp (untag (top (cdr (p-temp-stk p0)))))
  (lessp (untag (top (p-temp-stk p0))) (exp 2 (p-word-size p0)))
  (equal (cddr (top (cdr (p-temp-stk p0)))) nil)
  (equal (cddr (top (p-temp-stk p0))) nil)
  (equal (cdr (untag (top (cdr (p-temp-stk p0))))) 0)))

(prove-lemma correctness-of-max-nat (rewrite)
	     (implies
	      (and
	       (equal p0 (p-state 
			  pc
			  ctrl-stk
			  (cons n (cons s temp-stk))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run))
	       (equal (p-current-instruction p0) 
		      '(call max-nat))
	       (max-nat-input-conditionp p0)
	       (equal natlist (array (car (untag s)) data-segment)))
	      (equal
	       (p (p-state 
			  pc
			  ctrl-stk
			  (cons n (cons s temp-stk))
			  prog-segment
			  data-segment
			  max-ctrl-stk-size
			  max-temp-stk-size
			  word-size
			  'run)
		  (max-nat-clock natlist))
	       (p-state (add1-addr pc)
			ctrl-stk
			(cons 
			 (list 'nat (max-list (untag-array natlist)))
			 temp-stk)
			prog-segment
			data-segment
			max-ctrl-stk-size
			max-temp-stk-size
			word-size
			'run)))
	      ((use (correctness-of-max-nat-general 
		     (i 0) (j '(nat 0)) (x (list 'nat 0))
		     (nats (caadr s))
		    (ret-pc (add1-addr pc))
		    (length (cadr n))))))

(disable max-nat-program)

;; replace-value

;; replace the first occurrence of oldval by newval in list
;; of naturals (assumes oldval occurs in list)

(defn replace-value-program ()
  '(replace-value (list oldval newval) ()
              (dl loop ()
		  (push-local list))
		  (fetch)
		  (push-local oldval)
		  (eq)
		  (test-bool-and-jump t done)
		  (push-local list)
		  (push-constant (nat 1))
		  (add-addr)
		  (pop-local list)
		  (jump loop)
	       (dl done () 
		  (push-local newval))
	          (push-local list)
		  (deposit)
		  (ret)))

(defn example-replace-value-p-state ()
  (p-state '(pc (main . 0))
	   '((nil (pc (main . 0))))
	   nil
	   (list '(main nil nil
			(push-constant (addr (arr . 0)))
			(push-constant (nat 3))
			(push-constant (nat 4))
			(call replace-value)
			(ret))
		 (replace-value-program))
	   '((arr (nat 9) (nat 10) (nat 3) (nat 6) (nat 9) (nat 0)))
	   100
	   80
	   8
	   'run))

(defn replace-value-loop-clock (i list oldvalue)
  (if (lessp i (length list))
      (if (equal (get i list) oldvalue)
	  9
	(clock-plus 
	 10 (replace-value-loop-clock (add1 i) list oldvalue)))
    0)
  ((lessp (difference (length list) i))))

(defn replace-value-loop-induct (i list list-addr)
  (if (lessp i (length list))
      (replace-value-loop-induct (add1 i) list (add1-addr list-addr))
    t)
  ((lessp (difference (length list) i))))

(defn replace-value (list oldvalue newvalue)
  (if (listp list)
      (if (equal (car list) oldvalue)
	  (cons newvalue (cdr list))
	(cons (car list) (replace-value (cdr list) oldvalue newvalue)))
    nil))

(prove-lemma member-nthcdr-means (rewrite)
	     (implies
	      (member x (nthcdr i y))
	      (member x y)))

(prove-lemma member-of-natlist-means (rewrite)
	     (implies
	      (and
	       (nat-list-piton y s)
	       (member x y))
	      (and
	       (listp x)
	       (equal (car x) 'nat)
	       (numberp (cadr x))
	       (lessp (cadr x) (exp 2 s))
	       (equal (cddr x) nil))))

(prove-lemma replace-value-nthcdr-open (rewrite)
	     (implies
	      (and
	       (not (equal (get x a) old))
	       (lessp x (length a)))
	      (equal
	       (replace-value (nthcdr x a) old new)
	       (cons (get x a) 
		     (replace-value (nthcdr x (cdr a)) old new)))))

(prove-lemma list-nat-cadr-get-hack (rewrite)
	     (implies
	      (and
	       (nat-list-piton y s)
	       (lessp x (length y)))
	      (equal
	       (list 'nat (cadr (get x y)))
	       (get x y))))

(prove-lemma member-nthcdr-simplify (rewrite)
	     (implies
	      (and
	       (lessp i (length x))
	       (not (member a (nthcdr i (cdr x)))))
	      (equal
	       (member a (nthcdr i x))
	       (equal a (get i x)))))

(PROVE-LEMMA APPEND-MAKE-LIST-FROM-CONS-CDR
             (REWRITE)
             (IMPLIES (LESSP I (LENGTH Y))
                      (EQUAL (APPEND (MAKE-LIST-FROM I Y)
                                     (CONS V (CDR (NTHCDR I Y))))
                             (PUT V I Y))))

(prove-lemma correctness-of-replace-value-general nil
	     (implies
	      (and
	          (listp ctrl-stk)
		  (at-least-morep (length temp-stk) 
				  2 max-temp-stk-size)
		  (equal (definition 'replace-value prog-segment)
			 (replace-value-program))
		  (nat-list-piton (array list data-segment) word-size)
		  (definedp list data-segment)
		  (not (zerop word-size))
		  (numberp i)
		  (equal vallist (array list data-segment))
		  (equal (car list-addr) 'addr)
		  (equal (cddr list-addr) nil)
		  (listp (untag list-addr))
		  (equal (car (untag list-addr)) list)
		  (equal (cdr (untag list-addr)) i)
		  (equal (car newvalue) 'nat)