#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. 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 Computational Logic, Inc. 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.

|#

; ------------------------------------------------------------
; was lr-eval5-1.events
; ------------------------------------------------------------

(note-lib "app-c-d-e" t)

(prove-lemma axiom-53 (rewrite)
  (implies (subrp fn) (equal (formals fn) f)))

(disable proper-p-statep-restructuring)

;; Function for testing s->r
(defn CHANGE-ELEMENTS (list)
  (if (listp list)
      (if (truep (car list))
	  (cons (false) (change-elements (cdr list)))
	  (cons (true) (change-elements (cdr list))))
      (if (truep list) (false) (true))))

(disable deposit)
(disable fetch)

(disable add-addr)
(disable sub-addr)
(disable offset)
(disable area-name)

(disable errorp)

(disable p-current-program)

;; The following is inspired by the lemma length-put of Piton.
;; Now in Piton-basis  A. Flatau  8-Oct-1990
;(prove-lemma MY-LENGTH-PUT (rewrite)
;  (equal (length (put val n lst))
;	 (if (lessp n (length lst))
;	     (length lst)
;	     (add1 n)))
;  ((enable put)))
;
;(disable my-length-put)

;; This is similar to the lemma GET-PUT from Piton, but for the commented
;; out hypothesis.
(prove-lemma MY-GET-PUT (rewrite)
  (implies (and (numberp k)
		(numberp n)
		;(lessp n (length lst))
		)
	   (equal (get k (put val n lst))
		  (if (equal k n) val (get k lst))))
  ((enable get-cons get put get-anything-nil)))

(disable my-get-put)

(prove-lemma LISTP-CDR-P-FRAME (rewrite)
  (listp (cdr (p-frame bindings ret-pc)))
  ((enable p-frame)))

(prove-lemma EQUAL-CDDR-P-FRAME-NIL (rewrite)
  (equal (cddr (p-frame bindings ret-pc)) nil)
  ((enable p-frame)))

#||
;; The following is used to test handling of temp variables
(defn FOO (state name)
  (let ((prog (app name state)))
    (cons state (cons (car prog) (cons (cadr prog) (caddr prog))))))

;(setq ss
;      (logic->s '(change-elements (cons '*1*true (app x y)))
;		 '((x . (*1*true *1*true . *1*false))
;		   (y . (*1*true . *1*false)))
;		  '(change-elements app)))
;(setq lrs (s->lr ss 'main 50 50 50 32))
;(setq foop
;      '(FOO (STATE NAME)
;	    ((APP NAME STATE)
;	     (CDR ((TEMP-FETCH) (APP NAME STATE))))
;	    (CONS STATE
;		  (CONS (CAR ((TEMP-EVAL) (APP NAME STATE)))
;			(CONS (CAR ((TEMP-EVAL)
;				    (CDR ((TEMP-FETCH) (APP NAME STATE)))))
;			      (CAR (CDR ((TEMP-FETCH)
;					 (CDR ((temp-fetch)
;					       (APP NAME STATE)))))))))))
;
;(setq ss1 (s-state (s-expr ss)
;		   (s-params ss)
;		   (s-temps ss)
;		   (s-consts ss)
;		   (put-assoc (cdr foop) 'foo (s-progs ss))
;		   'run))
;
;(setq ss2 (s-state '(FOO (CHANGE-ELEMENTS (CONS '(ADDR (heap . 4))
;						(APP ((temp-eval) X) Y)))
;			 ((temp-fetch) X))
;		   (s-params ss1)
;		   (make-temps-entries '(x))
;		   (s-consts ss1)
;		   (s-progs ss1)
;		   'run))
||#

(defn S-L-EVAL-EQUIV-HYPS (flag s c)
  (and (s-good-statep s c)
       (good-posp flag (s-pos s) (s-body (s-prog s)))
       (equal (s-err-flag (s-eval flag s c)) 'run)))

(defn S-L-EVAL-FLAG-RUN-HYPS (flag s c)
  (and (s-good-statep s c)
       (s-all-temps-setp flag
			 (if (equal flag 'list)
			     (s-expr-list s)
			     (s-expr s))
			 (temp-alist-to-set (s-temps s)))
       (s-all-progs-temps-setp (s-progs s))
       (if (equal flag 'list)
	   (not (member f (l-eval flag
				  (s-expand-temps flag (s-expr-list s))
				  (s-params s)
				  c)))
	   (l-eval flag
		   (s-expand-temps flag (s-expr s))
		   (s-params s)
		   c))
       (s-check-temps-setp (s-temps s))))


;; ***** The LR-level (R for Resource, L for logic).  *****
;; We used to have an LR-STATE shell.  Now we just use a P-STATE shell.
;; However we refer to LR-STATES which are P-STATEs with LR level programs.
;; The function LR->P compiles an LR-STATE to a Piton state, by compiling
;; the programs and converting the P-PC to a Piton PC.
;; We use P-STATE shells instead of LR-STATE shell because we used to have
;; define functions analogous to P-OBJECTP (and functions that called
;; P-OBJECTP) that took LR-STATES or parts thereof.

;; We use the Piton notion of a PROPER state.  It should be the case that
;; all the LR-STATEs we are interested in are PROPER-P-STATEPs after we
;; apply LR->P to them.

;; An LR PC object is a combination of a Piton PC object and an S level
;; S-PNAME and S-POS.  The translation of (s-pname s) and (s-pos s) from
;; the S level is: (TAG 'PC (CONS (S-PNAME S) (S-POS S)))

;; Each element of P-PROG-SEGMENT is a program.  A program is a list
;; of the form:
;;
;; (name (formal1 formal2 ... formaln)
;;       ((temp1 init1)
;;        ...
;;        (tempk initk))
;;       body)
;;
;; The name and each formal and temp is a symbol.  The initial values
;; of the temps are tagged values.  Body is a form similar to that for
;; the S level, but temporary expressions have been replaced the name of
;; a temporary variable added to them
;; e.g. ((S-TEMP-EVAL) <expr>) -> ((S-TEMP-EVAL) <expr> <var>).
;; In the case of (S-TEMP-FETCH) <expr> is never used but we put it
;; in for consistency and so it is easier to convert back to s-states.
;; Also the numbers in the S level quote constructs have been replaced
;; by data-addresses that should contain pointers to the appropriate
;; structure in the heap.

;; Roughly speaking, a function application of FUN binds the formals to
;; the top n elements of the temp-stk (removing them from that stack and
;; building a ctrl-stk frame), binds the temps to the corresponding tagged
;; values (also in the ctrl-stk frame), and executes each instruction.

;; Producing LR-code from S-code.

(defn LR-UNDEFINED-TAG () 0)		; Used in node to indicate
					; uninitialized temporary variable
(defn LR-INIT-TAG () 1)			; Used in initial nodes that have
					; not been used
(defn LR-FALSE-TAG () 2)
(defn LR-TRUE-TAG  () 3)
(defn LR-ADD1-TAG  () 4)
(defn LR-CONS-TAG  () 5)
(defn LR-PACK-TAG  () 6)
(defn LR-MINUS-TAG  () 7)

(defn LR-HEAP-NAME () 'heap)

(defn LR-NODE-SIZE () 4)

(defn LR-UNDEF-ADDR () (tag 'addr '(heap . 0)))
(defn LR-F-ADDR () (add-addr (lr-undef-addr) (lr-node-size)))
(defn LR-T-ADDR () (add-addr (lr-F-addr) (lr-node-size)))
(defn LR-0-ADDR () (add-addr (lr-T-addr) (lr-node-size)))

(defn LR-FP-ADDR () (tag 'addr '(free-ptr . 0)))
(defn LR-ANSWER-ADDR () (tag 'addr '(answer . 0)))

(defn LR-FETCH-FP (data-seg)
  (fetch (lr-FP-addr) data-seg))

(defn LR-MINIMUM-HEAP-SIZE ()
  (offset (add-addr (lr-0-addr) (lr-node-size))))

;; The heap is a (presumably large) Piton data area.  It contains Nodes
;; which are four words.  One word is for the tag, one for the reference
;; count, and two for the contents.  Some data-types only require one word
;; for the contents (e.g. NUMBERPs) in that case one word is wasted.  Some
;; (user-defined) data-types require more than two words. In this case the
;; second word is a pointer to another node.  This contains up to three
;; words of data, the fourth word (if the data type needs more that four
;; words) is used to link another node with the same format.  The heap is
;; the Piton data area named HEAP.

;; LR-NEW-NODE returns another node to be stuck in memory
(defn LR-NEW-NODE (tag ref-count value1 value2)
  (list tag ref-count value1 value2))

(defn LR-REF-COUNT-OFFSET () 1)

(defn LR-CAR-OFFSET () 2)
(defn LR-CDR-OFFSET () 3)
(defn LR-UNPACK-OFFSET () 2)
(defn LR-UNBOX-NAT-OFFSET () 2)
(defn LR-NEGATIVE-GUTS-OFFSET () 2)

(defn LR-BOUNDARY-OFFSETP (offset)
  (equal (remainder offset (lr-node-size)) 0))

(defn LR-BOUNDARY-NODEP (node)
  (lr-boundary-offsetp (offset node)))

(defn LR-NODEP (addr data-seg)
  (and (equal (type addr) 'addr)
       (equal (cddr addr) nil)
       (listp addr)
       (adpp (untag addr) data-seg)
       (lr-boundary-nodep addr)
       (equal (area-name addr) (lr-heap-name))))

;; LR-GOOD-POINTERP checks that an addr is a node and its ref count field
;; is a natural.
(defn LR-GOOD-POINTERP (addr data-seg)
  (and (lr-nodep addr data-seg)
       (equal (type (fetch (add-addr addr (lr-ref-count-offset))
			   data-seg))
	      'nat)))

(defn LR-EXPR (p)
  (cur-expr (offset (p-pc p)) (program-body (p-current-program p))))

(disable lr-expr)

(defn LR-EXPR-LIST (p)
  (restn (car (last (offset (p-pc p))))
	 (cur-expr (butlast (offset (p-pc p)))
		   (program-body (p-current-program p)))))

(disable lr-expr-list)

;;; Debugging Stuff.
(defn MARK-INSTR (instruction-list n)
  (if (zerop n)
      (cons (list 'pc-> (car instruction-list)) (cdr instruction-list))
      (cons (car instruction-list)
	    (mark-instr (cdr instruction-list) (sub1 n)))))

(defn FIX-PROGRAM-SEGMENT (programs pc)
  (if (listp programs)
      (let ((prog (car programs)))
	(if (equal (car prog) (area-name pc))
	    (cons (append (list (car prog)
				(cadr prog)
				(caddr prog))
			  (mark-instr (program-body prog) (offset pc)))
		  (fix-program-segment (cdr programs) pc))
	    (cons (car prog) (fix-program-segment (cdr programs) pc))))
      nil))

(defn FIX-DATA-SEGMENT (data-segment)
  (put-value (append (firstn (offset (lr-fetch-fp data-segment))
			     (value (lr-heap-name) data-segment))
		     (difference (length (value (lr-heap-name)
						data-segment))
				 (offset (lr-fetch-fp data-segment))))
	     (lr-heap-name)
	      data-segment))

(defn FIND-NON-PROPER-INSTR (lst name p)
  (if (listp lst)
      (if (and (legal-labelp (car lst))
	       (proper-p-instructionp (unlabel (car lst)) name p))
	  (find-non-proper-instr (cdr lst) name p)
	  (car lst))
      nil))


(defn FIND-NON-PROPER-PROGRAMS (progs p)
  (if (listp progs)
      (if (proper-p-programp (car progs) p)
	  (cons (name (car progs)) (find-non-proper-programs (cdr progs) p))
	  (cons (list 'not
		       (name (car progs))
		       (find-non-proper-instr (program-body (car progs))
					      (name (car progs))
					      p))
		(find-non-proper-programs (cdr progs) p)))
      nil))

(defn PPS (state)
  (list 'p-state
	 (p-pc state)
	 (p-ctrl-stk state)
	 (p-temp-stk state)
	 (let ((p (p-current-program state)))
	   (append (list (name p) (formal-vars p) (temp-var-dcls p))
		   (mark-instr (program-body p) (offset (p-pc state)))))
	 (fix-data-segment (p-data-segment state))
	 (p-psw state)))

(defn LR-NODIFY-TAG (tag)
  (cond ((equal (untag tag) (lr-false-tag)) 'false)
	((equal (untag tag) (lr-true-tag)) 'true)
	((equal (untag tag) (lr-add1-tag)) 'add1)
	((equal (untag tag) (lr-cons-tag)) 'cons)
	((equal (untag tag) (lr-pack-tag)) 'pack)
	(t 'unknown)))
  
(defn LR-NODIFY (number nodes final)
  (if (listp nodes)
      (cons (list 'node
		   number
		   (lr-nodify-tag (car nodes))
		   (caddr nodes)
		   (cadddr nodes))
	    (lr-nodify (plus number (lr-node-size)) (cddddr nodes) final))
      final))

(defn LR-FIX-DATA-SEGMENT (data-seg)
  (put-value (lr-nodify 0
			(firstn (offset (lr-fetch-fp data-seg))
				(value (lr-heap-name) data-seg))
			(difference (length (value (lr-heap-name) data-seg))
				    (offset (lr-fetch-fp data-seg))))
	     (lr-heap-name)
	     data-seg))

(defn LRPS (state)
  (p-state (p-pc state)
	   (p-ctrl-stk state)
	   (p-temp-stk state)
	   (p-prog-segment state)
	   (lr-fix-data-segment (p-data-segment state))
	   (p-max-ctrl-stk-size state)
	   (p-max-temp-stk-size state)
	   (p-word-size state)
	   (p-psw state)))


;; Returns the object denoted by addr in the heap.
(defn LR-ABS (addr data-seg n)
  (if (zerop n)
      nil
      (let ((tag (untag (fetch addr data-seg))))
	(cond ((equal tag (lr-false-tag)) f)
	      ((equal tag (lr-true-tag)) t)
	      ((equal tag (lr-add1-tag))
	       (untag (fetch (add-addr addr (lr-unbox-nat-offset))
			     data-seg)))
	      ((equal tag (lr-cons-tag))
	       (cons (lr-abs (fetch (add-addr addr (lr-car-offset))
				    data-seg)
			     data-seg
			     (sub1 n))
		     (lr-abs (fetch (add-addr addr (lr-cdr-offset))
				    data-seg)
			     data-seg
			     (sub1 n))))
	       ((equal tag (lr-pack-tag))
		(pack (lr-abs (fetch (add-addr addr (lr-unpack-offset))
				     data-seg)
			      data-seg
			      (sub1 n))))
	       (t			; (EQUAL TAG (LR-MINUS-TAG))
		(minus (untag (fetch (add-addr addr
					       (lr-negative-guts-offset))
				     data-seg))))))))


(defn TOP-STK (p-or-p-state)
  (let ((temp-stk (if (p-statep p-or-p-state)
		      (p-temp-stk p-or-p-state)
		      (p-temp-stk p-or-p-state)))
	(data-segment (if (p-statep p-or-p-state)
			  (p-data-segment p-or-p-state)
			  (p-data-segment p-or-p-state))))
    (lr-abs (top temp-stk) data-segment 1000)))

;; This is accessed by the Piton accessors: NAME, FORMAL-VARS, TEMP-VAR-DCLS
;; and PROGRAM-BODY.  Also LOCAL-VARS.
(defn LR-MAKE-PROGRAM (name formals temps body)
  (cons name (cons formals (cons temps body))))

#||
stolen from matt kaufmann's code for gensym, but modified to probably be
less useful but simplier.

here is a sequence of events for generating a new symbol.
the main function is near the end, and is called gensym.
gensym returns a pair the new symbol and the next number list to try.
here are some examples:

>(r-loop)

trace mode: off   abbreviated output mode:  on
type ? for help.
*(gensym (unpack 'a*) '(49) '(a*0 a*1 a*2 a*3))
 '(a*4 53)
*(gensym (unpack 'a*) '(53) '(a*0 a*1 a*2 a*3 a*4))
 '(a*5 54)
*(gensym (unpack 'a*) '(50) '(a*2))
 '(a*3 52)
*(gensym (unpack 'a*) '(50) '(a*0))
 '(a*2 51)
*(gensym (unpack 'a) '(48) '(a*0 a*1))
 '(a0 49)
*(gensym (unpack 'a) '(48) '(a b))
 '(a0 49)
*(gensym (unpack 'a*2*) '(51) '(a*2*3))
 '(a*2*4 53)
*(gensym (unpack 'b*) '(50) '(a*0 a*1 a*2 a*3))
 '(b*2 51)
*ok
exiting r-loop.
nil

||#


(defn ASCII-0 () 48)
(defn ASCII-1 () 49)
(defn ASCII-9 () 57)

(defn ASCII-DASH () 45)

(defn LIST-ASCII-0 () (list (ascii-0)))
(defn LIST-ASCII-1 () (list (ascii-1)))

(defn INCREMENT-NUMLIST (numlist)
  ;; NUMLIST is a list of Ascii codes of digits, units digit first
  (if (listp numlist)
      (if (equal (car numlist) (ascii-9))
	  (cons (ascii-0) (increment-numlist (cdr numlist)))
	  (cons (add1 (car numlist)) (cdr numlist)))
      (list-ascii-1)))

(defn MAKE-SYMBOL (initial digit-list)
  (pack (append (append initial digit-list) 0)))

(disable make-symbol)

(defn COUNT-CODELIST1 (numlist)
  ;; NUMLIST is a list of Ascii codes, units digit first if we
  ;; think of them as being codes of digits of a number
  (if (listp numlist)
      (plus (car numlist)
	    (times 10 (count-codelist1 (cdr numlist))))
      0))

(defn SUBSEQP (list1 list2)
  (and (not (lessp (length list2) (length list1)))
       (equal (firstn (length list1) list2) list1)))

(disable subseqp)

(defn COUNT-CODELIST (initial ascii-list)
  (if (subseqp initial ascii-list)
      (count-codelist1 (restn (length initial) ascii-list))
      0))

(disable count-codelist)

(defn MAX-COUNT-CODELIST (initial list)
  (if (listp list)
      (max (count-codelist initial (unpack (car list)))
	   (max-count-codelist initial (cdr list)))
    0))

(prove-lemma INCREMENT-NUM-LIST-COUNT-CODE-LIST1 (rewrite)
  (lessp (count-codelist1 num-list)
	 (count-codelist1 (increment-numlist num-list)))
  ((disable plus-add1-arg1)))

(prove-lemma SUBSEQP-APPEND (rewrite)
  (subseqp (plist x) (append x anything))
  ((enable subseqp)))

(prove-lemma COUNT-CODELIST-MAKE-SYMBOL (rewrite)
  (implies (equal x (make-symbol initial num-list))
	   (equal (count-codelist (plist initial) (unpack x))
		  (count-codelist1 num-list)))
  ((enable count-codelist make-symbol)))

(prove-lemma MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST (rewrite)
  (implies (member (make-symbol initial num-list) atom-list)
	   (not (lessp (max-count-codelist (plist initial) atom-list)
		       (count-codelist1 num-list))))
  ((expand (max-count-codelist (plist initial) atom-list))))

;; Returns a pair, the new symbol and the next number to use
(defn GENSYM (initial num-list atom-list)
  (if (member (make-symbol initial num-list) atom-list)
      (gensym initial (increment-numlist num-list) atom-list)
      (cons (make-symbol initial num-list)
	    (increment-numlist num-list)))
  ((lessp (difference (add1 (max-count-codelist (plist initial) atom-list))
		      (count-codelist1 num-list)))))


(prove-lemma GENSYM-IS-NEW (rewrite)
  (not (member (car (gensym initial num-list atom-list)) atom-list)))

;; MAKE-TEMP-NAME-ALIST takes a temps-alist triple a la S-TEMPS and
;; returns an alist with entries of the form:
;; (<temp expression> . <variable>) where <variable> is guaranteed to
;; occur only once in the resulting alist and is guaranteed not to occur
;; in FORMALS.
(defn LR-MAKE-TEMP-NAME-ALIST-1 (initial num-list temp-list formals)
  (if (listp temp-list)
      (let ((gensym (gensym initial num-list formals)))
	(cons (cons (car temp-list) (car gensym))
	      (lr-make-temp-name-alist-1 initial
					 (cdr gensym)
					 (cdr temp-list)
					 formals)))
      nil))

(defn LR-MAKE-TEMP-NAME-ALIST (temp-list formals)
  (lr-make-temp-name-alist-1 (unpack 't*) (list-ascii-0) temp-list formals))

(defn LR-NEW-CONS (car cdr)
  (lr-new-node (tag 'nat (lr-cons-tag)) (tag 'nat 1) car cdr))
  
;; Deposit LIST of objects at ADDR, ADDR+1, ADDR+2, ... in DATA-SEG.
(defn DEPOSIT-A-LIST (list addr data-seg)
  (if (listp list)
      (deposit (car list)
	       addr
	       (deposit-a-list (cdr list)
			       (add1-addr addr)
			       data-seg))
      data-seg))

(defn LR-INIT-HEAP-CONTENTS (addr size)
  (if (zerop size)
      (list (tag 'nat (lr-init-tag)))
      (append (lr-new-node (tag 'nat (lr-init-tag))
			   (add-addr addr (lr-node-size))
			   (tag 'nat 0)
			   (tag 'nat 0))
	      (lr-init-heap-contents (add-addr addr (lr-node-size))
				     (sub1 size)))))

(defn LR-ADD-TO-DATA-SEG (data-seg new-node)
  (if (not (lessp (sub1 (length (value (lr-heap-name) data-seg)))
		  (plus (offset (fetch (lr-fp-addr) data-seg))
			(length new-node))))
      (deposit (fetch (add-addr (fetch (lr-fp-addr) data-seg)
				(lr-ref-count-offset))
		      data-seg)
	       (lr-fp-addr)
	       (deposit-a-list new-node
			       (fetch (lr-fp-addr) data-seg)
			       data-seg))
      data-seg))

(defn LR-INIT-DATA-SEG (heap-size)
  (deposit-a-list (list (tag 'nat (lr-false-tag))
			(tag 'nat 1)
			(lr-undef-addr)
			(lr-undef-addr))
		  (lr-f-addr)
		  (deposit-a-list (list (tag 'nat (lr-undefined-tag))
					(tag 'nat 1)
					(lr-undef-addr)
					(lr-undef-addr))
				  (lr-undef-addr)
				  (list (list (area-name (lr-fp-addr))
					      (add-addr (lr-f-addr)
							(lr-node-size)))
					(list (area-name (lr-answer-addr))
					      (tag 'nat 0))
					(cons (lr-heap-name)
					      (lr-init-heap-contents
					       (tag 'addr
						    (cons (lr-heap-name) 0))
					       heap-size))))))

(defn COUNT-LIST (flag object)
  (cond ((equal flag 'list)
	 (if (listp object)
	     (plus (count-list t (car object))
		   (count-list 'list (cdr object)))
	     1))
	((listp object)
	 (add1 (add1 (plus (count-list t (car object))
			   (count-list t (cdr object))))))
	((numberp object)
	 (add1 (count object)))
	(t 1)))

(prove-lemma NOT-EQUAL-0-COUNT-LIST (rewrite)
  (not (equal (count-list flag object) 0)))

(prove-lemma LESSP-COUNT-LIST-CDR-COUNT-LIST-WHOLE (rewrite)
  (implies (listp object)
	   (lessp (count-list 'list (cdr object))
		  (count-list 'list object))))

(prove-lemma LESSP-COUNT-NOT-LIST-CAR-COUNT-LIST-WHOLE (rewrite)
  (implies (listp object)
	   (lessp (count-list t (car object))
		  (count-list 'list object))))

;; LR-COMPILE-QUOTE returns a pair, the new HEAP and the new TABLE.
(defn LR-COMPILE-QUOTE (flag object heap table)
  (cond ((equal flag 'list)
	 (if (listp object)
	     (let ((car-pair (lr-compile-quote t (car object) heap table)))
	       (lr-compile-quote 'list
				 (cdr object)
				 (car car-pair)
				 (cdr car-pair)))
	     (cons heap table)))
	((definedp object table)
	 (cons heap table))
	((listp object)
	 (let ((pair (lr-compile-quote 'list
				       (list (car object) (cdr object))
				       heap
				       table)))
	   (cons (lr-add-to-data-seg (car pair)
				     (lr-new-cons (cdr (assoc
							(car object)
							(cdr pair)))
						  (cdr (assoc
							(cdr object)
							(cdr pair)))))
		 (cons (cons object (fetch (lr-fp-addr) (car pair)))
		       (cdr pair)))))
	((numberp object)
	 (cons (lr-add-to-data-seg heap
				   (lr-new-node (tag 'nat (lr-add1-tag))
						(tag 'nat 1)
						(tag 'nat object)
						(lr-undef-addr)))
	       (cons (cons object
			   (fetch (lr-fp-addr) heap))
		     table)))
	((truep object)
	 (cons (lr-add-to-data-seg heap (lr-new-node (tag 'nat
							  (lr-true-tag))
						     (tag 'nat 1)
						     (lr-undef-addr)
						     (lr-undef-addr)))
	       (cons (cons object (fetch (lr-fp-addr) heap)) table)))
	(t				; Assume it is undefined
	 (cons heap
	       (cons (cons object (lr-undef-addr)) table))))
  ((lessp (count-list flag object))))

;; LR-DATA-SEG-TABLE-BODY returns a pair, the CAR is the extension of
;; DATA-SEG with any constants laid down in it, the CDR is an alist
;; mapping objects in the logic to addresses in the new DATA-SEG
;; where they are represented.  The initial TABLE is such an alist
(defn LR-DATA-SEG-TABLE-BODY (flag expr data-seg table)
  (cond ((equal flag 'list)
	 (if (listp expr)
	     (let ((dst1 (lr-data-seg-table-body t
						 (car expr)
						 data-seg
						 table)))
	       (lr-data-seg-table-body 'list
				       (cdr expr)
				       (car dst1)
				       (cdr dst1)))
	     (cons data-seg table)))
	((listp expr)
	 (cond ((or (equal (car expr) (s-temp-fetch))
		    (equal (car expr) (s-temp-eval))
		    (equal (car expr) (s-temp-test)))
		(lr-data-seg-table-body t (cadr expr) data-seg table))
	       ((equal (car expr) 'quote)
		(lr-compile-quote t (cadr expr) data-seg table))
	       (t (lr-data-seg-table-body 'list
					  (cdr expr)
					  data-seg
					  table))))
	(t;; Should be a litatom
	 (cons data-seg table))))

(defn LR-DATA-SEG-TABLE-LIST (progs data-seg table)
  (if (listp progs)
      (lr-data-seg-table-list (cdr progs)
			      (car (lr-data-seg-table-body
				    t
				    (s-body (car progs))
				    data-seg
				    table))
			      (cdr (lr-data-seg-table-body
				    t
				    (s-body (car progs))
				    data-seg
				    table)))
      (cons data-seg table)))

(defn LR-INIT-DATA-SEG-TABLE (params data-seg table)
  (if (listp params)
      (let ((ds-tab (lr-compile-quote t (cdar params) data-seg table)))
	(lr-init-data-seg-table (cdr params) (car ds-tab) (cdr ds-tab)))
      (cons data-seg table)))

(defn LR-DATA-SEG-TABLE (progs params heap-size)
  (let ((init-ds-table1 (lr-compile-quote 'list
					  (list t 0)
					  (lr-init-data-seg heap-size)
					  (list (cons f (lr-f-addr))))))
    (let ((init-ds-table2 (lr-init-data-seg-table params
						  (car init-ds-table1)
						  (cdr init-ds-table1))))
      (lr-data-seg-table-list progs
			      (car init-ds-table2)
			      (cdr init-ds-table2)))))

(defn PAIR-FORMALS-WITH-ADDRESSES (formals table)
  (if (listp formals)
      (cons (cons (caar formals) (cdr (assoc (cdar formals) table)))
	    (pair-formals-with-addresses (cdr formals) table))
      nil))

(defn LR-MAKE-INITIAL-TEMPS (temp-vars)
  (if (listp temp-vars)
      (cons (cons (car temp-vars) (lr-undef-addr))
	    (lr-make-initial-temps (cdr temp-vars)))
      nil))

(defn LR-INITIAL-CSTK (params temp-alist table pc)
  (list (p-frame (append (pair-formals-with-addresses params table)
			 (lr-make-initial-temps (strip-cdrs temp-alist)))
		 pc)))

(defn LR-COMPILE-BODY (flag body temp-alist const-table)
  (if (equal flag 'list)
      (if (listp body)
	  (cons (lr-compile-body t (car body) temp-alist const-table)
		(lr-compile-body 'list (cdr body) temp-alist const-table))
	  nil)
      (if (listp body)
	  (cond ((or (equal (car body) (s-temp-fetch))
		     (equal (car body) (s-temp-eval))
		     (equal (car body) (s-temp-test)))
		 (list (car body)
		       (lr-compile-body t
					(cadr body)
					temp-alist
					const-table)
		       (value (cadr body) temp-alist)))
		((equal (car body) 'quote)
		 (list 'quote (value (cadr body) const-table)))
		(t (cons (car body)
			 (lr-compile-body 'list
					  (cdr body)
					  temp-alist
					  const-table))))
	  body)))

(defn LR-MAKE-TEMP-VAR-DCLS (temp-alist)
  (if (listp temp-alist)
      (cons (list (cdar temp-alist) (lr-undef-addr))
	    (lr-make-temp-var-dcls (cdr temp-alist)))
      nil))

(defn LR-COMPILE-PROGRAMS (programs const-table)
  (if (listp programs)
      (let ((prog (car programs)))
	(let ((temp-alist (lr-make-temp-name-alist (s-temp-list prog)
						   (s-formals prog))))
	  (cons (lr-make-program (car prog)
				 (s-formals prog)
				 (lr-make-temp-var-dcls temp-alist)
				 (lr-compile-body t
						  (s-body prog)
						  temp-alist
						  const-table))
		(lr-compile-programs (cdr programs) const-table))))
      nil))


(defn LR-P-C-SIZE (flag expr)
  (cond ((equal flag 'list)
	 (if (listp expr)
	     (plus (lr-p-c-size t (car expr))
		   (lr-p-c-size 'list (cdr expr)))
	     0))
	((listp expr)
	 (cond ((equal (car expr) 'if)
		(plus (lr-p-c-size t (cadr expr))
		      (lr-p-c-size t (caddr expr))
		      (lr-p-c-size t (cadddr expr)) 4))
	       ((equal (car expr) (s-temp-fetch)) 1)
	       ((equal (car expr) (s-temp-eval))
		(plus (lr-p-c-size t (cadr expr)) 1))
	       ((equal (car expr) (s-temp-test))
		(plus (lr-p-c-size t (cadr expr)) 7))
	       ((equal (car expr) 'quote) 1)
	       (t (plus (lr-p-c-size 'list (cdr expr)) 1))))
	(t 1)))

(defn LR-P-C-SIZE-LIST (n expr-list)
  (if (zerop n)
      0
      (if (lessp n (length expr-list))
	  (plus (lr-p-c-size t (get n expr-list))
		(lr-p-c-size-list (sub1 n) expr-list))
	  (lr-p-c-size-list (sub1 (length expr-list)) expr-list))))

;; LR-P-PC-1 returns the number of Piton instructions before the start of
;; the expression denoted by POS in the compilation of EXPR.
(defn LR-P-PC-1 (expr pos)
      (cond ((not (listp pos)) 0)
            ((not (listp expr)) 0)
	    ((zerop (car pos)) 0)
            ((equal (car expr) 'if)
	     (cond ((zerop (car pos)) 0)
		   ((equal (car pos) 1)
		    (lr-p-pc-1 (cadr expr) (cdr pos)))
		   ((equal (car pos) 2)
		    (plus 3
			  (lr-p-c-size t (cadr expr))
			  (lr-p-pc-1 (caddr expr) (cdr pos))))
		   (t (plus (lr-p-c-size t (cadr expr))
			    (lr-p-c-size t (caddr expr))
			    (lr-p-pc-1 (cadddr expr) (cdr pos))
			    4))))
            ((equal (car expr) (s-temp-fetch)) 0)
            ((equal (car expr) (s-temp-eval))
             (lr-p-pc-1 (cadr expr) (cdr pos)))
            ((equal (car expr) (s-temp-test))
             (plus (lr-p-pc-1 (cadr expr) (cdr pos)) 4))
            ((equal (car expr) 'quote) 0)
            (t (plus (lr-p-c-size-list (sub1 (car pos)) expr)
                     (lr-p-pc-1 (get (car pos) expr) (cdr pos))))))

(defn LR-P-PC (l)
  (tag 'pc (cons (area-name (p-pc l))
		 (lr-p-pc-1 (program-body (p-current-program l))
			    (offset (p-pc l))))))

(disable lr-p-pc)

(defn S->LR1 (s l table)
  (p-state (tag 'pc (cons (s-pname s) (s-pos s)))
	   (p-ctrl-stk l)
	   (p-temp-stk l)
	   (lr-compile-programs (s-progs s) table)
	   (p-data-segment l)
	   (p-max-ctrl-stk-size l)
	   (p-max-temp-stk-size l)
	   (p-word-size l)
	   (s-err-flag s)))

(disable s->lr1)

;; Returns an P-STATE.
;; FREE-HEAP-SIZE is number of free nodes in resulting P-STATE.
(defn S->LR (s fheap-size max-ctrl max-temp word-size)
  (let ((temp-alist (lr-make-temp-name-alist (strip-cars (s-temps s))
					     (strip-cars (s-params s))))
	(dataseg-table (lr-data-seg-table (s-progs s)
					  (s-params s)
					  fheap-size)))
    (let ((return-pc
	   (tag 'pc
		(cons (s-pname s)
		      (lr-p-pc-1 (lr-compile-body t
						  (s-body (s-prog s))
						  temp-alist
						  (cdr dataseg-table))
				 (s-pos s))))))
      (s->lr1 s
	      (p-state nil
		       (lr-initial-cstk (s-params s)
					temp-alist
					(cdr dataseg-table)
					return-pc)
		       nil
		       nil
		       (car dataseg-table)
		       max-ctrl
		       max-temp
		       word-size
		       nil)
	      (cdr dataseg-table)))))

(disable s->lr)

(defn LR-PARAMS (frame p)
  (firstn (length (formal-vars (p-current-program p))) (bindings frame)))

(disable lr-params)

(defn LR-TEMPS (frame p)
  (restn (length (formal-vars (p-current-program p))) (bindings frame)))

(disable lr-temps)

(defn LR-SET-EXPR (s1 s2 pos)
  (p-state (tag 'pc (cons (area-name (p-pc s2)) pos))
	   (p-ctrl-stk s1)
	   (p-temp-stk s1)
	   (p-prog-segment s2)
	   (p-data-segment s1)
	   (p-max-ctrl-stk-size s1)
	   (p-max-temp-stk-size s1)
	   (p-word-size s1)
	   (p-psw s1)))

(defn LR-SET-ERROR (s flag)
  (p-state (p-pc s)
	   (p-ctrl-stk s)
	   (p-temp-stk s)
	   (p-prog-segment s)
	   (p-data-segment s)
	   (p-max-ctrl-stk-size s)
	   (p-max-temp-stk-size s)
	   (p-word-size s)
	   flag))

(defn LR-SET-POS (s pos)
  (p-state (tag 'pc (cons (area-name (p-pc s)) pos))
	   (p-ctrl-stk s)
	   (p-temp-stk s)
	   (p-prog-segment s)
	   (p-data-segment s)
	   (p-max-ctrl-stk-size s)
	   (p-max-temp-stk-size s)
	   (p-word-size s)
	   (p-psw s)))

(defn LR-SET-TSTK (s temp-stk)
  (p-state (p-pc s)
	   (p-ctrl-stk s)
	   temp-stk
	   (p-prog-segment s)
	   (p-data-segment s)
	   (p-max-ctrl-stk-size s)
	   (p-max-temp-stk-size s)
	   (p-word-size s)
	   (p-psw s)))

(defn LR-POP-TSTK (s)
  (if (equal (p-psw s) 'run)
      (if (listp (p-temp-stk s))
	  (lr-set-tstk s (pop (p-temp-stk s)))
	  (lr-set-error s 'lr-pop-tstk-empty-stack))
      s))

(defn LR-PUSH-TSTK (s value)
  (if (equal (p-psw s) 'run)
      (if (lessp (length (p-temp-stk s)) (p-max-temp-stk-size s))
	  (lr-set-tstk s (push value (p-temp-stk s)))
	  (lr-set-error s 'lr-push-tstk-full-stack))
      s))

(disable lr-push-tstk)

(defn LR-IF-OK (l)
  (if (not (lessp (p-max-temp-stk-size l)
		  (plus 1 (length (p-temp-stk l)))))
      l
      (lr-set-error l 'if-temp-stk-overflow)))

(disable lr-if-ok)

(defn LR-SET-TEMP (s value var-name)
  (if (equal (p-psw s) 'run)
      (p-state (p-pc s)
	       (set-local-var-value value var-name (p-ctrl-stk s))
	       (p-temp-stk s)
	       (p-prog-segment s)
	       (p-data-segment s)
	       (p-max-ctrl-stk-size s)
	       (p-max-temp-stk-size s)
	       (p-word-size s)
	       (p-psw s))
      s))

(disable lr-set-temp)

(defn LR-EVAL-TEMP-SETP (s)
  (not (equal (local-var-value (caddr (lr-expr s)) (p-ctrl-stk s))
	      (lr-undef-addr))))

(disable lr-eval-temp-setp)

(defn LR-DO-TEMP-FETCH (s)
  (if (lr-eval-temp-setp s)
      (lr-push-tstk s
		    (local-var-value (caddr (lr-expr s))
				     (p-ctrl-stk s)))
      (lr-set-error s 'temp-fetch-not-set)))

(disable lr-do-temp-fetch)

(defn LR-POP-CSTK (s)
  (if (equal (p-psw s) 'run)
      (p-state (p-pc s)
	       (pop (p-ctrl-stk s))
	       (p-temp-stk s)
	       (p-prog-segment s)
	       (p-data-segment s)
	       (p-max-ctrl-stk-size s)
	       (p-max-temp-stk-size s)
	       (p-word-size s)
	       (p-psw s))
      s))

(disable lr-pop-cstk)

(defn LR-TYPE-CONTENTS-P (object tag contents)
  (and (equal (type object) tag)
       (equal (untag object) contents)))

;; The following functions are used for the Piton code and to compute the LR
;; value for certain classes of functions (e.g. all shell accessors).

;; NOTE: The 'clock' functions get a Piton state.  This is the state just
;; BEFORE the execution of the appropriate CALL instruction.  Therefore
;; to look at the parameters, it is necessary to look at the temp stack.
;; The clock function return the number of Piton instructions necessary to
;; run the CALL and the code for the SUBR.

;; Recognizers
(defn P-RECOGNIZER-CODE (name tag)
  (list name '() '()
	'(FETCH)
	(list 'PUSH-CONSTANT (tag 'nat tag))
	'(EQ)
	'(TEST-BOOL-AND-JUMP F FALSE)
	(list 'PUSH-CONSTANT (lr-t-addr))
	'(RET)
	(list 'DL 'FALSE '() (LIST 'PUSH-CONSTANT (lr-f-addr)))
	'(RET)))

(defn P-RECOGNIZER-CLOCK (p-state tag) 7)

;; Accessor
(defn P-ACCESSOR-CODE (name tag default offset)
  (list name '(X) '()
	'(PUSH-LOCAL X)
	'(FETCH)
	(list 'PUSH-CONSTANT (tag 'nat TAG))
	'(EQ)
	'(TEST-BOOL-AND-JUMP T ARG1)
	(list 'PUSH-CONSTANT default)
	'(RET)
	'(DL ARG1 () (PUSH-LOCAL X))
	(list 'PUSH-CONSTANT (tag 'nat offset))
	'(ADD-ADDR)
	'(FETCH)
	'(RET)))

(defn P-ACCESSOR-CLOCK (p tag)
  (if (equal (fetch (top (p-temp-stk p)) (p-data-segment p))
	     (tag 'nat tag))
      11
      8))

;; Now comes the actual code and values

(defn P-CAR-CODE ()
  (p-accessor-code 'car (lr-cons-tag) (lr-0-addr) (lr-car-offset)))

(defn P-CAR-CLOCK (p)
  (p-accessor-clock p (lr-cons-tag)))

(disable p-car-clock)

(defn P-CDR-CODE ()
  (p-accessor-code 'cdr (lr-cons-tag) (lr-0-addr) (lr-cdr-offset)))

(defn P-CDR-CLOCK (p)
  (p-accessor-clock p (lr-cons-tag)))

(disable p-cdr-clock)

(defn P-CONS-CODE ()
  ;; Takes two implicit args
  ;; Note that we assume that the CDR is on top of the stack
  ;; and the CAR is just below it.  This is what would normally be
  ;; the case if you evaluate left to right.
  (list 'cons '()
	'((TEMP (NAT 0)))
	'(PUSH-GLOBAL FREE-PTR)		; Put CDR in node + CDR-OFFSET
	(list 'PUSH-CONSTANT (tag 'nat (lr-cdr-offset)))
	'(ADD-ADDR)
	'(DEPOSIT)
	'(PUSH-GLOBAL FREE-PTR)		; Put CAR in node + CAR-OFFSET
	(list 'PUSH-CONSTANT (tag 'nat (lr-car-offset)))
	'(ADD-ADDR)
	'(DEPOSIT)
	'(PUSH-GLOBAL FREE-PTR)		; This is the result
	'(PUSH-GLOBAL FREE-PTR)		; Put FREE-PTR.NEXT on stack
	(list 'PUSH-CONSTANT (tag 'nat (lr-ref-count-offset)))
	'(ADD-ADDR)
	'(SET-LOCAL TEMP)
	'(FETCH)
	'(PUSH-CONSTANT (NAT 1))	; Set ref count to 1
	'(PUSH-LOCAL TEMP)
	'(DEPOSIT)
	(list 'PUSH-CONSTANT (tag 'nat (lr-cons-tag))) ; Put tag in node
	'(PUSH-GLOBAL FREE-PTR)
	'(DEPOSIT)
	'(POP-GLOBAL FREE-PTR)		; FREE-PTR <- FREE-PTR.NEXT
	'(RET)))

(defn P-CONS-CLOCK (p) 23)

(disable p-cons-clock)

(defn P-FALSE-CODE ()
  (list 'false '() '()
	(list 'push-constant (lr-f-addr))
	'(ret)))

(defn P-FALSE-CLOCK (p) 3)

(disable p-false-clock)

;; FALSEP TAKES ONE IMPLICIT ARG ON STACK.
(defn P-FALSEP-CODE ()
  (list 'falsep '() '()
	(list 'PUSH-CONSTANT (lr-f-addr))
	'(EQ)
	'(TEST-BOOL-AND-JUMP T TRUE)
	(list 'PUSH-CONSTANT (lr-f-addr))
	'(RET)
	(list 'DL 'TRUE '() (list 'PUSH-CONSTANT (lr-t-addr)))
	'(RET)))

(defn P-FALSEP-CLOCK (p) 6)

(disable p-falsep-clock)

;; Takes an implicit arg
(defn P-LISTP-CODE ()
  (p-recognizer-code 'listp (lr-cons-tag)))

(defn P-LISTP-CLOCK (p)
  (p-recognizer-clock p (lr-cons-tag)))

(disable p-listp-clock)

(defn P-NLISTP-CODE ()
  (list 'nlistp '() '()
	'(FETCH)
	(list 'PUSH-CONSTANT (tag 'nat (lr-cons-tag)))
	'(EQ)
	'(TEST-BOOL-AND-JUMP F TRUE)
	(list 'PUSH-CONSTANT (lr-f-addr))
	'(RET)
	(list 'DL 'TRUE '() (list 'PUSH-CONSTANT (lr-t-addr)))
	'(RET)))

(defn P-NLISTP-CLOCK (p) 7)

(disable p-nlistp-clock)

(defn P-TRUE-CODE ()
  (list 'true '() '()
	(list 'PUSH-CONSTANT (lr-t-addr))
	'(RET)))

(defn P-TRUE-CLOCK (p) 3)

(disable p-true-clock)

;; The old code for TRUEP is shown below.  I used to ensure that there was
;; only one occurence of TRUE in the data-segment [namely at address
;; (lr-t-addr)], however only TRUEP took advantage of this.  LR-PROPER-HEAPP
;; has been changed to not require only one occurrence, although only one
;; should appear.  However this means we actually have to test the tag, a
;; small performance penalty for some simplicity and freedom in the spec.
(defn P-TRUEP-CODE ()
  (p-recognizer-code 'truep (lr-true-tag)))

;(defn P-TRUEP-CODE ()
;  (list 'truep '() '()
;	(list 'PUSH-CONSTANT (lr-t-addr))
;	'(EQ)
;	'(TEST-BOOL-AND-JUMP T TRUE)
;	(list 'PUSH-CONSTANT (lr-f-addr))
;	'(RET)
;	(list 'DL 'TRUE '() (list 'PUSH-CONSTANT (lr-t-addr)))
;	'(RET)))

(defn P-TRUEP-CLOCK (p)
  (p-recognizer-clock p (lr-false-tag)))

;(defn P-TRUEP-CLOCK (p) 6)

(disable p-truep-clock)

(defn P-RUNTIME-SUPPORT-PROGRAMS ()
  (list (p-car-code)
	(p-cdr-code)
	(p-cons-code)
	(p-false-code)
	(p-falsep-code)
	(p-listp-code)
	(p-nlistp-code)
	(p-true-code)
	(p-truep-code)))

(disable p-runtime-support-programs)

(defn LR-CONVERT-DIGIT-TO-ASCII (digit)
  (plus (ascii-0) digit))

(defn LR-CONVERT-NUM-TO-ASCII (number list)
  (if (lessp number 10)
      (cons (lr-convert-digit-to-ascii number) list)
      (lr-convert-num-to-ascii (quotient number 10)
			       (cons (lr-convert-digit-to-ascii
				      (remainder number 10))
				     list)))
  ((lessp (fix number))))

(defn LR-MAKE-LABEL (n)
  (pack (cons (car (unpack 'L))
	      (cons (ascii-dash)
		    (append (lr-convert-num-to-ascii n nil) 0)))))

(disable lr-make-label)

(defn LABEL-INSTRS (instrs n)
  (if (listp instrs)
      (cons (dl (lr-make-label n) () (car instrs))
	    (label-instrs (cdr instrs) (add1 n)))
      nil))

(defn COMP-TEMP-TEST (expr instrs n)
  ;; Use value if computed,  otherwise compute it.  If we have (CAR EXPR)
  ;; not equal (S-TEMP-TEST) then store the result again
  (append (list (list 'PUSH-LOCAL (caddr expr))
		(list 'PUSH-CONSTANT (lr-undef-addr))
		'(EQ)
		(list 'TEST-BOOL-AND-JUMP 'F
		      (lr-make-label (plus n 6
					   (length instrs)))))
	  (append instrs
		  (list (list 'SET-LOCAL (caddr expr))
			(list 'JUMP
			      (lr-make-label
			       (plus n 7 (length instrs))))
			(list 'PUSH-LOCAL (caddr expr))))))

(defn COMP-IF (test-instrs then-instrs else-instrs n)
  (append test-instrs
	  (append (list (list 'PUSH-CONSTANT (lr-f-addr))
			'(EQ)
			(list 'TEST-BOOL-AND-JUMP 'T
			      (lr-make-label (plus n 4
						   (length test-instrs)
						   (length then-instrs)))))
		  (append then-instrs
			  (cons (list 'JUMP
				      (lr-make-label
				       (plus n 4
					     (length test-instrs)
					     (length then-instrs)
					     (length else-instrs))))
				else-instrs)))))

;; COMP-BODY-1 returns a list of Piton instructions to compile EXPR.
;; N is the number of Piton instructions previously generated, it is used
;; to generate unique labels.
(defn COMP-BODY-1 (flag expr n)
  (cond ((equal flag 'list)
	 (if (listp expr)
	     (append (comp-body-1 t (car expr) n)
		     (comp-body-1 'list
				  (cdr expr)
				  (plus n (lr-p-c-size t (car expr)))))
	     nil))
	((listp expr)
	 (cond ((equal (car expr) 'if)
		(comp-if (comp-body-1 t (cadr expr) n)
			 (comp-body-1 t
				      (caddr expr)
				      (plus n 3
					    (lr-p-c-size t (cadr expr))))
			 (comp-body-1 t
				      (cadddr expr)
				      (plus n 4
					    (lr-p-c-size t (cadr expr))
					    (lr-p-c-size t (caddr expr))))
			 n))
	       ((equal (car expr) (s-temp-fetch))
		;; Unconditionally use already computed value.
		(list (list 'PUSH-LOCAL (caddr expr))))
	       ((equal (car expr) (s-temp-eval))
		;; Unconditionally compute value.
		(append (comp-body-1 t (cadr expr) n)
			(list (list 'SET-LOCAL (caddr expr)))))
	       ((equal (car expr) (s-temp-test))
		(comp-temp-test expr
				(comp-body-1 t (cadr expr) (plus n 4))
				n))
	       ((equal (car expr) 'quote)
		(list (list 'PUSH-CONSTANT (cadr expr))))
	       (t (append (comp-body-1 'list (cdr expr) n)
			  (if (definedp (car expr)
					(p-runtime-support-programs))
			      (list (list 'CALL (car expr)))
			      (list (list 'CALL
					  (user-fname (car expr)))))))))
	(t ;; Should be a litatom
	 (list (list 'PUSH-LOCAL expr)))))

(disable comp-body-1)

(defn COMP-BODY (body)
  (label-instrs (append (comp-body-1 t body 0) '((RET))) 0))

(disable comp-body)

(defn COMP-PROGRAMS-1 (programs)
  (if (listp programs)
      (cons (lr-make-program (name (car programs))
			     (formal-vars (car programs))
			     (temp-var-dcls (car programs))
			     (comp-body (program-body (car programs))))
	    (comp-programs-1 (cdr programs)))
      nil))

(defn COMP-PROGRAMS (programs)
  (cons (lr-make-program (name (car programs))
			 (formal-vars (car programs))
			 (temp-var-dcls (car programs))
			 (label-instrs
			  (append (comp-body-1 t
					       (program-body (car programs))
					       0)
				  (list (list 'SET-GLOBAL
					      (area-name (lr-answer-addr)))
					'(RET)))
			  0))
	(append (comp-programs-1 (cdr programs))
		(p-runtime-support-programs))))

(disable comp-programs)

(defn LR-PROPER-EXPRP (flag expr pnames formals temps table)
  (cond ((equal flag 'list)
	 (if (listp expr)
	     (and (lr-proper-exprp t (car expr) pnames formals temps table)
		  (lr-proper-exprp 'list
				   (cdr expr)
				   pnames
				   formals
				   temps
				   table))
	     (equal expr nil)))
	((litatom expr) (member expr formals))
	((nlistp expr) f)
	((not (plistp expr)) f)
	((equal (car expr) (s-temp-fetch))
	 (and (member (caddr expr) temps) (equal (length expr) 3)))
	((or (equal (car expr) (s-temp-eval))
	     (equal (car expr) (s-temp-test)))
	 (and (member (caddr expr) temps)
	      (equal (length expr) 3)
	      (lr-proper-exprp t (cadr expr) pnames formals temps table)))
	((equal (car expr) 'quote)
	 ;; We need to know that the quoted thing is an address into
	 ;; the data segment, i.e. has TYPE = 'ADDR.  This is because
	 ;; a quote becomes a PUSH-CONSTANT, which can push a PC which would
	 ;; not work.
	 (and (equal (type (cadr expr)) 'addr)
	      (member (cadr expr) (strip-cdrs table))
	      (equal (length (cdr expr)) (arity (car expr)))))
	((subrp (car expr))
	 (and (equal (length (cdr expr)) (arity (car expr)))
	      ;; ***** This will have to change when user definedp subrs are
	      ;; implemented. *****
	      (or (equal (car expr) 'if)
		  (definedp (car expr) (p-runtime-support-programs)))
	      (not (member (car expr) pnames))
	      (lr-proper-exprp 'list (cdr expr)
			       pnames formals temps table)))
	((body (car expr))
	 (and (equal (length (cdr expr)) (arity (car expr)))
	      (member (car expr) pnames)
	      (lr-proper-exprp 'list (cdr expr)
			       pnames formals temps table)))
	(t f)))

(defn ALL-UNDEF-ADDRS (list)
  (if (listp list)
      (and (equal (car list) (lr-undef-addr))
	   (all-undef-addrs (cdr list)))
      t))

(defn LR-PROGRAMS-PROPERP-1 (programs program-names table)
  (if (listp programs)
      (and ;(not (subrp (name (car programs))))
	   ;(litatom (name (car programs)))
	   (all-litatoms (formal-vars (car programs)))
	   (all-litatoms (strip-cars (temp-var-dcls (car programs))))
	   (all-undef-addrs (strip-cadrs (temp-var-dcls (car programs))))
	   (lr-proper-exprp t
			    (program-body (car programs))
			    program-names
			    (formal-vars (car programs))
			    (strip-cars (temp-var-dcls (car programs)))
			    table)
	   (lr-programs-properp-1 (cdr programs) program-names table))
      t))

(disable lr-programs-properp-1)

(defn LR-PROGRAMS-PROPERP (l table)
  (and (definedp (area-name (p-pc l)) (p-prog-segment l))
       (equal (caar (p-prog-segment l)) 'main)
       (all-user-fnamesp (cdr (strip-cars (p-prog-segment l))))
       (lr-programs-properp-1 (p-prog-segment l)
			      (strip-logic-fnames (cdr (p-prog-segment l)))
			      table)))

(disable lr-programs-properp)

(prove-lemma LR-P-C-SIZE-FLAG-NOT-LIST-NOT-0 (rewrite)
  (implies (not (equal flag 'list))
	   (not (equal (lr-p-c-size flag expr) 0))))

(prove-lemma DIFFERENCE-DECREASES (rewrite)
  (implies (and (not (lessp x y))
		(not (zerop y)))
	   (equal (lessp (difference x y) x) t)))

(defn LR->P (p)
  (p-state (lr-p-pc p)
	   (p-ctrl-stk p)
	   (p-temp-stk p)
	   (comp-programs (p-prog-segment p))
	   (p-data-segment p)
	   (p-max-ctrl-stk-size p)
	   (p-max-temp-stk-size p)
	   (p-word-size p)
	   (p-psw p)))

(disable lr->p)

(defn P-SET-PC (p pc)
  (p-state pc
	   (p-ctrl-stk p)
	   (p-temp-stk p)
	   (p-prog-segment p)
	   (p-data-segment p)
	   (p-max-ctrl-stk-size p)
	   (p-max-temp-stk-size p)
	   (p-word-size p)
	   (p-psw p)))

;; It should be the case that (P-CURRENT-INSTRUCTION p) = (CALL subr)
;; therefore we need to run P one more step than the clock functions
;; below to do the CALL.
(defn P-RUN-SUBR (subr p)
  (case subr
    (car		(p p (p-car-clock p)))
    (cdr		(p p (p-cdr-clock p)))
    (cons		(p p (p-cons-clock p)))
    (false		(p p (p-false-clock p)))
    (falsep		(p p (p-falsep-clock p)))
    (listp		(p p (p-listp-clock p)))
    (nlistp		(p p (p-nlistp-clock p)))
    (true		(p p (p-true-clock p)))
    (truep		(p p (p-truep-clock p)))
    (otherwise		(p-halt p 'bad-subr))))

(disable p-run-subr)

(defn LR-RETURN-PC (l)
  (add-addr (lr-p-pc l) (lr-p-c-size 'list (cdr (lr-expr l)))))

(disable lr-return-pc)

(defn LR-APPLY-SUBR (l new-l)
  (let ((res (p-run-subr (car (lr-expr l))
			 (p-set-pc (lr->p new-l) (lr-return-pc l)))))
    (p-state (p-pc new-l)
	     (p-ctrl-stk res)
	     (p-temp-stk res)
	     (p-prog-segment new-l)
	     (p-data-segment res)
	     (p-max-ctrl-stk-size res)
	     (p-max-temp-stk-size res)
	     (p-word-size res)
	     (p-psw res))))

(disable lr-apply-subr)

(defn LR-FUNCALL (l new-l)
  (let ((prog (definition (user-fname (car (lr-expr l)))
			  (p-prog-segment l)))
	(newest-l (p-set-pc (lr->p new-l) (lr-return-pc l))))
    (if (p-call-okp (list 'call (user-fname (car (lr-expr l)))) newest-l)
	(p-state (tag 'pc (cons (user-fname (car (lr-expr l))) nil))
		 (push (make-p-call-frame (formal-vars prog)
					  (p-temp-stk new-l)
					  (temp-var-dcls prog)
					  (add1-addr (p-pc newest-l)))
		       (p-ctrl-stk new-l))
		 (popn (length (formal-vars prog)) (p-temp-stk new-l))
		 (p-prog-segment new-l)
		 (p-data-segment new-l)
		 (p-max-ctrl-stk-size new-l)
		 (p-max-temp-stk-size new-l)
		 (p-word-size new-l)
		 'run)
	(p-halt new-l (x-y-error-msg 'p 'call)))))

(disable lr-funcall)

;; The following lemmas are needed to admit LR-EVAL
(prove-lemma P-ACCESSORS-LR-SET-EXPR (rewrite)
  (and (equal (p-pc (lr-set-expr s1 s2 pos))
	      (tag 'pc (cons (area-name (p-pc s2)) pos)))
       (equal (p-ctrl-stk (lr-set-expr s1 s2 pos)) (p-ctrl-stk s1))
       (equal (p-temp-stk (lr-set-expr s1 s2 pos)) (p-temp-stk s1))
       (equal (p-prog-segment (lr-set-expr s1 s2 pos)) (p-prog-segment s2))
       (equal (p-data-segment (lr-set-expr s1 s2 pos)) (p-data-segment s1))
       (equal (p-max-ctrl-stk-size (lr-set-expr s1 s2 pos))
	      (p-max-ctrl-stk-size s1))
       (equal (p-max-temp-stk-size (lr-set-expr s1 s2 pos))
	      (p-max-temp-stk-size s1))
       (equal (p-word-size (lr-set-expr s1 s2 pos)) (p-word-size s1))
       (equal (p-psw (lr-set-expr s1 s2 pos)) (p-psw s1))))

(disable lr-set-expr)

(prove-lemma P-ACCESSORS-LR-SET-TSTK (rewrite)
  (and (equal (p-pc (lr-set-tstk s ts)) (p-pc s))
       (equal (p-ctrl-stk (lr-set-tstk s ts)) (p-ctrl-stk s))
       (equal (p-temp-stk (lr-set-tstk s ts)) ts)
       (equal (p-prog-segment (lr-set-tstk s ts)) (p-prog-segment s))
       (equal (p-data-segment (lr-set-tstk s ts)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-set-tstk s ts))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-set-tstk s ts))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-set-tstk s ts)) (p-word-size s))
       (equal (p-psw (lr-set-tstk s ts)) (p-psw s))))

(disable lr-set-tstk)

(prove-lemma P-ACCESSORS-LR-SET-ERROR (rewrite)
  (and (equal (p-pc (lr-set-error s flag)) (p-pc s))
       (equal (p-ctrl-stk (lr-set-error s flag)) (p-ctrl-stk s))
       (equal (p-temp-stk (lr-set-error s flag)) (p-temp-stk s))
       (equal (p-prog-segment (lr-set-error s flag)) (p-prog-segment s))
       (equal (p-data-segment (lr-set-error s flag)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-set-error s flag))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-set-error s flag))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-set-error s flag)) (p-word-size s))
       (equal (p-psw	(lr-set-error s flag)) flag)))

(disable lr-set-error)

(prove-lemma P-ACCESSORS-LR-SET-POS (rewrite)
  (and (equal (p-pc (lr-set-pos s pos)) (tag 'pc
					     (cons (area-name (p-pc s))
						   pos)))
       (equal (p-ctrl-stk (lr-set-pos s pos)) (p-ctrl-stk s))
       (equal (p-temp-stk (lr-set-pos s pos)) (p-temp-stk s))
       (equal (p-prog-segment (lr-set-pos s pos)) (p-prog-segment s))
       (equal (p-data-segment (lr-set-pos s pos)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-set-pos s pos))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-set-pos s pos))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-set-pos s pos)) (p-word-size s))
       (equal (p-psw (lr-set-pos s pos)) (p-psw s))))

(disable lr-set-pos)

(prove-lemma P-ACCESSORS-LR-POP-TSTK (rewrite)
  (and (equal (p-pc (lr-pop-tstk s)) (p-pc s))
       (equal (p-ctrl-stk (lr-pop-tstk s)) (p-ctrl-stk s))
       (equal (p-prog-segment (lr-pop-tstk s)) (p-prog-segment s))
       (equal (p-data-segment (lr-pop-tstk s)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-pop-tstk s))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-pop-tstk s))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-pop-tstk s)) (p-word-size s))))

(prove-lemma P-TEMP-STK-LR-POP-TSTK (rewrite)
  (equal (p-temp-stk (lr-pop-tstk s))
	 (if (and (listp (p-temp-stk s))
		  (equal (p-psw s) 'run))
	     (pop (p-temp-stk s))
	     (p-temp-stk s))))

(disable lr-pop-tstk)

(prove-lemma AREA-NAME-TAG (rewrite)
  (equal (area-name (tag tag adp)) (adp-name adp))
  ((enable area-name tag untag)))

(prove-lemma OFFSET-TAG (rewrite)
  (equal (offset (tag tag adp)) (adp-offset adp))
  ((enable offset tag untag)))

(prove-lemma P-CURRENT-PROGRAM-LR-SET-EXPR (rewrite)
  (equal (p-current-program (lr-set-expr s1 s2 pos)) (p-current-program s2))
  ((enable p-current-program)))

(prove-lemma P-CURRENT-PROGRAM-LR-SET-POS (rewrite)
  (equal (p-current-program (lr-set-pos s pos)) (p-current-program s))
  ((enable p-current-program)))

(prove-lemma LR-EXPR-LR-SET-EXPR (rewrite)
  (equal (lr-expr (lr-set-expr s1 s2 (dv (offset (p-pc s2)) n)))
	 (get n (lr-expr s2)))
  ((enable lr-expr p-current-program dv)))

(prove-lemma LR-EXPR-LR-SET-POS-T (rewrite)
  (equal (lr-expr (lr-set-pos s (dv (offset (p-pc s)) n)))
	 (get n (lr-expr s)))
  ((enable lr-expr dv)))

(prove-lemma LR-EXPR-FLAG-LIST-CAR (rewrite)
  (implies (listp (offset (p-pc p)))
	   (equal (car (lr-expr-list p)) (lr-expr p)))
  ((enable lr-expr lr-expr-list
	   car-restn-get)
   (use (cur-expr-append (pos1 (butlast (offset (p-pc p))))
			 (pos2 (last (offset (p-pc p))))
			 (body (program-body (p-current-program p)))))
   (expand (cur-expr (last (offset (p-pc p)))
		     (cur-expr (butlast (offset (p-pc p)))
			       (program-body (p-current-program p))))
	   (cur-expr (cdr (last (offset (p-pc p))))
		     (get (car (last (offset (p-pc p))))
			  (cur-expr (butlast (offset (p-pc p)))
				    (program-body (p-current-program p))))))
   (disable cur-expr
	    cur-expr-append)))

(prove-lemma NUMBER-CONS-LR-EXPR-T-LIST (rewrite)
  (implies (and (listp (lr-expr-list p))
		(listp (offset (p-pc p))))
	   (lessp (number-cons (lr-expr p))
		  (number-cons (lr-expr-list p))))
  ((enable lr-expr lr-expr-list)))

(prove-lemma LR-EXPR-LR-SET-EXPR-NX (rewrite)
  (implies (and (listp (offset (p-pc p)))
		(listp (lr-expr-list p)))
	   (equal (lr-expr-list (lr-set-expr p1 p (nx (offset (p-pc p)))))
		  (cdr (lr-expr-list p))))
  ((enable lr-expr-list
	   restn-cdr)))

(prove-lemma LR-EXPR-LIST-LR-SET-POS-DV-1 (rewrite)
  (implies (listp (lr-expr p))
	   (equal (lr-expr-list (lr-set-pos p (dv (offset (p-pc p)) 1)))
		  (cdr (lr-expr p))))
  ((enable lr-expr lr-expr-list)))

;; If FLAG is 'LIST then state contains a list of expressions,
;; otherwise it is just one.
;; Returns a P-STATE.  The result is left on the temp stack.
;; If the error flag of the resulting state is 'HALT then we terminated
;; normally.  If the flag is 'RUN we have not terminated yet.
;; If the flag is anything else we got an error.
(defn LR-EVAL (flag l c)
  (cond ((not (equal (p-psw l) 'run)) l)
	((equal flag 'list)
	 (if (nlistp (offset (p-pc l)))
	     (lr-set-error l 'bad-list-position)
	     (if (listp (lr-expr-list l))
		 (lr-eval 'list
			  (lr-set-expr (lr-eval t l c)
				       l
				       (nx (offset (p-pc l))))
			  c)
		 l)))
	((zerop c) (lr-set-error l 'out-of-time))
	((litatom (lr-expr l))
	 (lr-push-tstk l (local-var-value (lr-expr l) (p-ctrl-stk l))))
	((nlistp (lr-expr l)) (lr-set-error l 'bad-expression))
	((equal (car (lr-expr l)) 'if)
	 (let ((test (lr-if-ok (lr-eval t
					(lr-set-pos l
						    (dv (offset (p-pc l))
							1))
					c))))
	   (if (equal (p-psw test) 'run)
	       (if (not (equal (top (p-temp-stk test)) (lr-f-addr)))
		   (lr-eval t
			    (lr-set-expr (lr-pop-tstk test)
					 l
					 (dv (offset (p-pc l)) 2))
			    c)
		   (lr-eval t
			    (lr-set-expr (lr-pop-tstk test)
					 l
					 (dv (offset (p-pc l)) 3))
			    c))
	       test)))
	((equal (car (lr-expr l)) (s-temp-eval))
	 (let ((l1 (lr-eval t (lr-set-pos l (dv (offset (p-pc l)) 1)) c)))
	   (lr-set-temp l1 (top (p-temp-stk l1)) (caddr (lr-expr l)))))
	((equal (car (lr-expr l)) (s-temp-test))
	 (let ((l1 (lr-eval t (lr-set-pos l (dv (offset (p-pc l)) 1)) c)))
	   (if (not (lessp (p-max-temp-stk-size l)
			   (plus 2 (length (p-temp-stk l)))))
	       (if (lr-eval-temp-setp l)
		   (lr-do-temp-fetch l)
		   (lr-set-temp l1
				(top (p-temp-stk l1))
				(caddr (lr-expr l))))
	       (lr-set-error l 'lr-temp-setp-temp-stack-overflow))))
	((equal (car (lr-expr l)) (s-temp-fetch)) (lr-do-temp-fetch l))
	((equal (car (lr-expr l)) 'quote)
	 (lr-push-tstk l (cadr (lr-expr l))))
	((not (equal (p-psw (lr-eval 'list
				     (lr-set-pos l (dv (offset (p-pc l)) 1))
				     c))
		     'run))
	 (lr-eval 'list (lr-set-pos l (dv (offset (p-pc l)) 1)) c))
	((subrp (car (lr-expr l)))
	 (lr-apply-subr l
			(lr-eval 'list
				 (lr-set-pos l (dv (offset (p-pc l)) 1))
				 c)))
	((litatom (car (lr-expr l)))
	 (let ((fs (lr-funcall l
			       (lr-eval 'list
					(lr-set-pos l
						    (dv (offset (p-pc l))
							1))
					c))))
	   (lr-set-expr (lr-pop-cstk (lr-eval t fs (sub1 c)))
			l
			(offset (p-pc l)))))
	(t (lr-set-error l 'bad-instruction)))
  ((ord-lessp (cons (add1 c) (if (equal flag 'list)
				 (number-cons (lr-expr-list l))
				 (number-cons (lr-expr l)))))))

;; Proper LR STATES

;; Sometimes we only need to know that LR-PROPER-P-AREASP holds on
;; a data-segment instead of LR-PROPER-P-DATA-SEGMENTP
(defn LR-PROPER-P-AREASP (data-seg)
  (if (nlistp data-seg)
      (equal data-seg nil)
      (let ((area (car data-seg)))
	(and (litatom (car area))
	     (listp (cdr area))
	     (not (definedp (car area) (cdr data-seg)))
	     (lr-proper-p-areasp (cdr data-seg))))))

;; First we prove that LR-EVAL preserves PROPER-P-STATEP.

(prove-lemma P-ACCESSORS-LR-FUNCALL (rewrite)
  (and (equal (p-prog-segment (lr-funcall l new-l)) (p-prog-segment new-l))
       (equal (p-data-segment (lr-funcall l new-l)) (p-data-segment new-l))
       (equal (p-max-ctrl-stk-size (lr-funcall l new-l))
	      (p-max-ctrl-stk-size new-l))
       (equal (p-max-temp-stk-size (lr-funcall l new-l))
	      (p-max-temp-stk-size new-l))
       (equal (p-word-size (lr-funcall l new-l)) (p-word-size new-l)))
  ((enable lr-funcall)
   (disable-theory addition)
   (disable make-p-call-frame p-call-okp lr-p-c-size lr-p-c-size-list)))

(prove-lemma P-ACCESSORS-LR-PUSH-TSTK (rewrite)
  (and (equal (p-pc (lr-push-tstk s v)) (p-pc s))
       (equal (p-ctrl-stk (lr-push-tstk s v)) (p-ctrl-stk s))
       (equal (p-prog-segment (lr-push-tstk s v)) (p-prog-segment s))
       (equal (p-data-segment (lr-push-tstk s v)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-push-tstk s v))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-push-tstk s v))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-push-tstk s v)) (p-word-size s)))
  ((enable lr-push-tstk)))

(prove-lemma P-ACCESSORS-LR-IF-OK (rewrite)
  (and (equal (p-pc (lr-if-ok l)) (p-pc l))
       (equal (p-ctrl-stk (lr-if-ok l)) (p-ctrl-stk l))
       (equal (p-temp-stk (lr-if-ok l)) (p-temp-stk l))
       (equal (p-prog-segment (lr-if-ok l)) (p-prog-segment l))
       (equal (p-data-segment (lr-if-ok l)) (p-data-segment l))
       (equal (p-max-ctrl-stk-size (lr-if-ok l)) (p-max-ctrl-stk-size l))
       (equal (p-max-temp-stk-size (lr-if-ok l)) (p-max-temp-stk-size l))
       (equal (p-word-size (lr-if-ok l)) (p-word-size l)))
  ((enable lr-if-ok)))

(prove-lemma P-ACCESSORS-LR-SET-TEMP (rewrite)
  (and (equal (p-pc (lr-set-temp s v n)) (p-pc s))
       (equal (p-ctrl-stk (lr-set-temp s v n))
	      (if (equal (p-psw s) 'run)
		  (set-local-var-value v n (p-ctrl-stk s))
		  (p-ctrl-stk s)))
       (equal (p-temp-stk (lr-set-temp s v n)) (p-temp-stk s))
       (equal (p-prog-segment (lr-set-temp s v n)) (p-prog-segment s))
       (equal (p-data-segment (lr-set-temp s v n)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-set-temp s v n))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-set-temp s v n))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-set-temp s v n)) (p-word-size s))
       (equal (p-psw (lr-set-temp s v n)) (p-psw s)))
  ((enable lr-set-temp)
   (disable set-local-var-value)))

(prove-lemma P-ACCESSORS-LR-DO-TEMP-FETCH (rewrite)
  (and (equal (p-pc (lr-do-temp-fetch s)) (p-pc s))
       (equal (p-ctrl-stk (lr-do-temp-fetch s)) (p-ctrl-stk s))
       (equal (p-prog-segment (lr-do-temp-fetch s)) (p-prog-segment s))
       (equal (p-data-segment (lr-do-temp-fetch s)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-do-temp-fetch s))
	      (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-do-temp-fetch s))
	      (p-max-temp-stk-size s))
       (equal (p-word-size (lr-do-temp-fetch s)) (p-word-size s)))
  ((enable lr-do-temp-fetch)
   (disable local-var-value)))

(prove-lemma P-ACCESSORS-LR-POP-CSTK (rewrite)
  (and (equal (p-pc (lr-pop-cstk s)) (p-pc s))
       (equal (p-ctrl-stk (lr-pop-cstk s)) (if (equal (p-psw s) 'run)
						(pop (p-ctrl-stk s))
						(p-ctrl-stk s)))
       (equal (p-temp-stk (lr-pop-cstk s)) (p-temp-stk s))
       (equal (p-prog-segment (lr-pop-cstk s)) (p-prog-segment s))
       (equal (p-data-segment (lr-pop-cstk s)) (p-data-segment s))
       (equal (p-max-ctrl-stk-size (lr-pop-cstk s)) (p-max-ctrl-stk-size s))
       (equal (p-max-temp-stk-size (lr-pop-cstk s)) (p-max-temp-stk-size s))
       (equal (p-word-size (lr-pop-cstk s)) (p-word-size s))
       (equal (p-psw (lr-pop-cstk s)) (p-psw s)))
  ((enable lr-pop-cstk)))

(prove-lemma LR-EVAL-IF-P-PSW-1 (rewrite)
  (implies (and (not (equal flag 'list))
		(equal (p-psw (lr-eval flag l c)) 'run)
		(equal (car (lr-expr l)) 'if)
		(equal (p-psw l) 'run)
		(not (zerop c))
		(listp (lr-expr l)))
	   (equal (p-psw (lr-eval t
				  (lr-set-pos l (dv (offset (p-pc l)) 1))
				  c))
		  'run))
    ((enable lr-pop-tstk lr-if-ok)
     (expand (lr-eval flag l c))))

(disable lr-eval-if-p-psw-1)

(prove-lemma ADP-OFFSET-UNTAG-ADD-ADDR (rewrite)
  (equal (adp-offset (untag (add-addr addr n))) (plus (offset addr) n))
  ((enable offset untag add-addr tag)))

(prove-lemma ADP-OFFSET-UNTAG-SUB-ADDR (rewrite)
  (equal (adp-offset (untag (sub-addr addr n)))
	 (difference (offset addr) n))
  ((enable offset untag sub-addr tag)))

(prove-lemma ADP-NAME-UNTAG-SUB-ADDR (rewrite)
  (equal (adp-name (untag (sub-addr addr n))) (adp-name (untag addr)))
  ((enable adp-name untag sub-addr tag)))

(prove-lemma ADP-OFFSET-CONS (rewrite)
  (equal (adp-offset (cons area-name offset)) offset))

(prove-lemma P-ACCESSORS-LR->P (rewrite)
  (and (equal (p-pc (lr->p l)) (lr-p-pc l))
       (equal (p-ctrl-stk (lr->p l)) (p-ctrl-stk l))
       (equal (p-temp-stk (lr->p l)) (p-temp-stk l))
       (equal (p-prog-segment (lr->p l)) (comp-programs (p-prog-segment l)))
       (equal (p-data-segment (lr->p l)) (p-data-segment l))
       (equal (p-max-ctrl-stk-size (lr->p l)) (p-max-ctrl-stk-size l))
       (equal (p-max-temp-stk-size (lr->p l)) (p-max-temp-stk-size l))
       (equal (p-word-size (lr->p l)) (p-word-size l))
       (equal (p-psw (lr->p l)) (p-psw l)))
  ((enable lr->p)))

(prove-lemma TYPE-LR-P-PC (rewrite)
  (equal (type (lr-p-pc l)) 'pc)
  ((enable lr-p-pc)
   (disable lr-p-pc-1)))

(prove-lemma CDDR-NIL-LR-P-PC (rewrite)
  (equal (cddr (lr-p-pc l)) nil)
  ((enable lr-p-pc)
   (disable lr-p-pc-1)))

(prove-lemma LISTP-UNTAG-LR-P-PC (rewrite)
  (listp (untag (lr-p-pc l)))
  ((enable lr-p-pc)
   (disable lr-p-pc-1)))

(prove-lemma NUMBERP-CDR-LR-P-PC (rewrite)
  (numberp (cdr (untag (lr-p-pc l))))
  ((enable lr-p-pc)
   (disable lr-p-pc-1)))

(prove-lemma CAR-UNTAG-LR-P-PC (rewrite)
  (equal (car (untag (lr-p-pc p))) (car (untag (p-pc p))))
  ((enable area-name lr-p-pc)
   (disable lr-p-pc-1)))

(prove-lemma AREA-NAME-LR-P-PC (rewrite)
  (equal (area-name (lr-p-pc p)) (area-name (p-pc p)))
  ((enable lr-p-pc)
   (disable lr-p-pc-1)))

(prove-lemma DEFINEDP-COMP-PROGRAMS-1-DEFINEDP-ORIG (rewrite)
  (equal (definedp x (comp-programs-1 programs)) (definedp x programs))
  ((enable name)))

(prove-lemma DEFINEDP-APPEND (rewrite)
  (equal (definedp x (append l1 l2))
	 (or (definedp x l1) (definedp x l2))))

(prove-lemma DEFINEDP-COMP-PROGRAMS-DEFINEDP-ORIG (rewrite)
  (implies (definedp x programs)
	   (definedp x (comp-programs programs)))
  ((enable comp-programs name)
   (disable *1*p-runtime-support-programs)))

(prove-lemma P-ACCESSORS-P-HALT (rewrite)
  (and (equal (p-pc (p-halt p psw)) (p-pc p))
       (equal (p-ctrl-stk (p-halt p psw)) (p-ctrl-stk p))
       (equal (p-temp-stk (p-halt p psw)) (p-temp-stk p))
       (equal (p-prog-segment (p-halt p psw)) (p-prog-segment p))
       (equal (p-data-segment (p-halt p psw)) (p-data-segment p))
       (equal (p-max-ctrl-stk-size (p-halt p psw)) (p-max-ctrl-stk-size p))
       (equal (p-max-temp-stk-size (p-halt p psw)) (p-max-temp-stk-size p))
       (equal (p-word-size (p-halt p psw)) (p-word-size p))
       (equal (p-psw (p-halt p psw)) psw)))

(disable p-halt)

(prove-lemma P-ACCESSORS-P-SET-PC (rewrite)
  (and (equal (p-pc (p-set-pc p pc)) pc)
       (equal (p-ctrl-stk (p-set-pc p pc)) (p-ctrl-stk p))
       (equal (p-temp-stk (p-set-pc p pc)) (p-temp-stk p))
       (equal (p-prog-segment (p-set-pc p pc)) (p-prog-segment p))
       (equal (p-data-segment (p-set-pc p pc)) (p-data-segment p))
       (equal (p-max-ctrl-stk-size (p-set-pc p pc)) (p-max-ctrl-stk-size p))
       (equal (p-max-temp-stk-size (p-set-pc p pc)) (p-max-temp-stk-size p))
       (equal (p-word-size (p-set-pc p pc)) (p-word-size p))
       (equal (p-psw (p-set-pc p pc)) (p-psw p))))

(disable p-set-pc)

(prove-lemma P-PSW-NOT-RUN ()
  (implies (not (equal (p-psw p-state) 'run))
	   (equal (p p-state clock) p-state))
  ((enable p)))

(prove-lemma P-PSW-P-HALT-X-Y-ERROR-MSG (rewrite)
  (equal (p (p-halt p-state (x-y-error-msg x y)) n)
	 (p-halt p-state (x-y-error-msg x y)))
  ((enable p p-halt)
   (disable *1*x-y-error-msg)
   (use (p-psw-not-run (p-state (p-halt p-state (x-y-error-msg x y)))
		       (clock n)))))

(disable p-psw-p-halt-x-y-error-msg)

(prove-lemma P-ACCESSORS-P-RUN-SUBR (rewrite)
  (and (equal (p-prog-segment (p-run-subr subr p)) (p-prog-segment p))
       (equal (p-max-ctrl-stk-size (p-run-subr subr p))
	      (p-max-ctrl-stk-size p))
       (equal (p-max-temp-stk-size (p-run-subr subr p))
	      (p-max-temp-stk-size p))
       (equal (p-word-size (p-run-subr subr p)) (p-word-size p)))
  ((disable p-ins-okp
	    *1*x-y-error-msg)
   (enable p-run-subr
	   p-step1-opener
	   p-psw-p-halt-x-y-error-msg)))

(prove-lemma P-ACCESSORS-LR-APPLY-SUBR (rewrite)
  (and (equal (p-pc (lr-apply-subr l1 l2)) (p-pc l2))
       (equal (p-prog-segment (lr-apply-subr l1 l2)) (p-prog-segment l2))
       (equal (p-max-ctrl-stk-size (lr-apply-subr l1 l2))
	      (p-max-ctrl-stk-size l2))
       (equal (p-max-temp-stk-size (lr-apply-subr l1 l2))
	      (p-max-temp-stk-size l2))
       (equal (p-word-size (lr-apply-subr l1 l2)) (p-word-size l2)))
  ((enable lr-apply-subr p-invariant1)
   (disable p-ins-step lr-p-c-size lr-p-c-size-list
	    *1*x-y-error-msg p-ins-okp)))

(prove-lemma P-PROG-SEGMENT-LR-EVAL (rewrite)
  (equal (p-prog-segment (lr-eval flag l c)) (p-prog-segment l))
  ((induct (lr-eval flag l c))
   (expand (lr-eval flag l c) (lr-eval 'list l c) (lr-eval flag l 0))
   (disable lr-eval)))

(prove-lemma P-MAX-CTRL-STK-SIZE-LR-EVAL (rewrite)
  (equal (p-max-ctrl-stk-size (lr-eval flag l c)) (p-max-ctrl-stk-size l))
  ((induct (lr-eval flag l c))
   (expand (lr-eval flag l c) (lr-eval 'list l c) (lr-eval flag l 0))
   (disable lr-eval)))

(prove-lemma P-MAX-TEMP-STK-SIZE-LR-EVAL (rewrite)
  (equal (p-max-temp-stk-size (lr-eval flag l c)) (p-max-temp-stk-size l))
  ((induct (lr-eval flag l c))
   (expand (lr-eval flag l c) (lr-eval 'list l c) (lr-eval flag l 0))
   (disable lr-eval)))

(prove-lemma P-WORD-SIZE-LR-EVAL (rewrite)
  (equal (p-word-size (lr-eval flag l c)) (p-word-size l))
  ((induct (lr-eval flag l c))
   (expand (lr-eval flag l c) (lr-eval 'list l c) (lr-eval flag l 0))
   (disable lr-eval)))

(prove-lemma AREA-NAME-P-PC-LR-EVAL (rewrite)
  (equal (area-name (p-pc (lr-eval flag l c))) (area-name (p-pc l)))
  ((induct (lr-eval flag l c))
   (expand (lr-eval flag l c) (lr-eval 'list l c) (lr-eval flag l 0))
   (disable lr-eval)))

(prove-lemma LR-PROGRAMS-PROPERP-LR-EVAL (rewrite)
  (equal (lr-programs-properp (lr-eval flag l c) table)
	 (lr-programs-properp l table))
  ((enable lr-programs-properp)))

(prove-lemma DEFINEDP-DEPOSIT (rewrite)
  (equal (definedp tag (deposit anything addr data-seg))
	 (definedp tag data-seg))
  ((enable deposit)))

(prove-lemma DEPOSIT-A-LIST-CONS-OPENER (rewrite)
  (equal (deposit-a-list (cons x list) addr data-seg)
	 (deposit x addr (deposit-a-list list (add1-addr addr) data-seg))))

(prove-lemma DEPOSIT-A-LIST-NIL (rewrite)
  (equal (deposit-a-list nil addr data-seg) data-seg))

(disable deposit-a-list)

(prove-lemma ASSOC-PUT-ASSOC-3 (rewrite)
  (equal (assoc name1 (put-assoc val name2 alist))
	 (if (equal name1 name2)
	     (if (definedp name1 alist)
		 (cons name1 val)
		 f)
	     (assoc name1 alist)))
  ((do-not-induct t)
   (enable definedp-assoc-fact-1)))

(disable assoc-put-assoc-3)

(prove-lemma ADPP-LESSP-OFFSET-DEPOSIT (rewrite)
  (implies (and (lessp offset (length (cdr (assoc name data-seg))))
		(definedp name data-seg))
	   (lessp offset
		  (length (cdr (assoc name
				      (deposit anything
					       anywhere
					       data-seg))))))
  ((enable deposit
	   assoc-put-assoc-3
	   my-length-put)))

(prove-lemma ADPP-DEPOSIT-ANYTHING-AT-ALL (rewrite)
  (implies (adpp adp data-seg)
	   (adpp adp (deposit anything addr2 data-seg))))

(disable adpp-lessp-offset-deposit)
(disable adpp-deposit-anything-at-all)

(prove-lemma ADPP-UNTAG-DEFINEDP-AREA-NAME (rewrite)
  (implies (adpp (untag addr) data-seg)
	   (definedp (area-name addr) data-seg))
  ((enable area-name)))

(disable adpp-untag-definedp-area-name)

(prove-lemma ADPP-CONS-PACK-DEFINEDP-AREA-NAME (rewrite)
  (implies (adpp (cons (pack xxx) offset) data-seg)
	   (definedp (pack xxx) data-seg))
  ((enable area-name)))

(prove-lemma ADPP-UNTAG-NUMBERP-OFFSET (rewrite)
  (implies (adpp (untag addr) data-seg)
	   (numberp (offset addr)))
  ((enable offset)))

(disable adpp-untag-numberp-offset)

(prove-lemma ADPP-UNTAG-LISTP (rewrite)
  (implies (adpp (untag addr) data-seg)
	   (listp (untag addr)))
  ((enable offset)))

(disable adpp-untag-listp)

(prove-lemma ADPP-ADD-ADDR-0 (rewrite)
  (implies (and (adpp (untag addr) data-seg)
		(equal (cddr addr) nil)
		(equal (type addr) 'addr)
		(zerop n))
	   (equal (add-addr addr n) addr))
  ((enable adpp add-addr tag type untag)))

(disable adpp-add-addr-0)

(prove-lemma ADPP-UNTAG-LESSP-OFFSET (rewrite)
  (implies (adpp (untag addr) data-seg)
	   (lessp (offset addr) (length (cdr (assoc (area-name addr)
						    data-seg)))))
  ((enable area-name offset)))

(disable adpp-untag-lessp-offset)

(prove-lemma ADPP-SAME-SIGNATURE ()
  (implies (same-signature data-seg2 data-seg1)
	   (equal (adpp adp data-seg2)
		  (adpp adp data-seg1)))
  ((enable same-signature-implies-equal-lengths
	   same-signature-implies-equal-definedp)))

(disable adpp)

(prove-lemma P-OBJECTP-SIMILAR-P-STATES (rewrite)
  (implies (and (p-objectp object p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	   (p-objectp object p1))
  ((enable p-objectp
	   same-signature-implies-equal-definedp)
   (use (adpp-same-signature (adp (untag object))
			     (data-seg2 (p-data-segment p0))
			     (data-seg1 (p-data-segment p1))))
   (disable adpp bit-vectorp booleanp definedp pcpp
	    small-naturalp small-integerp)))

(prove-lemma ALL-P-OBJECTPS-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (all-p-objectps lst p0)
		(equal (p-word-size p0) (p-word-size p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(same-signature (p-data-segment p0) (p-data-segment p1)))
	   (all-p-objectps lst p1)))

(prove-lemma PROPER-P-DATA-SEGMENTP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-p-data-segmentp data-seg p0)
		(equal (p-word-size p0) (p-word-size p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(same-signature (p-data-segment p0) (p-data-segment p1)))
	   (proper-p-data-segmentp data-seg p1)))

(prove-lemma PROPER-P-TEMP-VAR-DCLSP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-p-temp-var-dclsp temp-var-dcls p0)
		(equal (p-word-size p0) (p-word-size p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(same-signature (p-data-segment p0) (p-data-segment p1)))
	   (proper-p-temp-var-dclsp temp-var-dcls p1)))

(prove-lemma PROPER-P-INSTRUCTIONP-SIMILAR-P-STATES (rewrite)
  (implies (and (proper-p-instructionp ins name p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	   (proper-p-instructionp ins name p1))
  ((enable proper-p-instructionp
	   same-signature-implies-equal-definedp)))

(prove-lemma PROPER-LABELED-P-INSTRUCTIONSP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-labeled-p-instructionsp lst name p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	   (proper-labeled-p-instructionsp lst name p1)))

(prove-lemma PROPER-P-PROG-SEGMENTP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-p-prog-segmentp programs p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	 (proper-p-prog-segmentp programs p1))
  ((disable fall-off-proofp proper-p-temp-var-dclsp)))

(prove-lemma PROPER-P-TEMP-STKP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-p-temp-stkp temp-stk p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	   (proper-p-temp-stkp temp-stk p1)))

(prove-lemma PROPER-P-ALISTP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-p-alistp bindings p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	   (proper-p-alistp bindings p1)))

(prove-lemma PROPER-P-CTRL-STKP-LR->P-SIMILAR-STATES (rewrite)
  (implies (and (proper-p-ctrl-stkp ctrl-stk name p0)
		(same-signature (p-data-segment p0) (p-data-segment p1))
		(equal (p-prog-segment p0) (p-prog-segment p1))
		(equal (p-word-size p0) (p-word-size p1)))
	   (proper-p-ctrl-stkp ctrl-stk name p1)))

;; Now we prove what the result of running the SUBRPs.  We
;; start with a sample state (that the rewriter can match with
;; P-APPLY-SUBR-STATE) and run it.  We are only interested in TEMP-STK and
;; DATA-SEGMENT of the result.  However the running of the Piton code can
;; be a bit tedious, so we try and prove both parts at once with the
;; following function P-GOOD-RESULTP.  This also has the not ERRORP check
;; inside of it so that we should only have one instance of the Piton
;; interpreter (P) in each theorem.  This should hopefully reduce the time
;; (and pain) of proving these theorems.
(defn P-GOOD-RESULTP (p data-seg temp-stk ctrl-stk pc)
  (if (not (equal (p-psw p) 'run))
      t
      (and (equal (p-data-segment p) data-seg)
	   (equal (p-temp-stk p) temp-stk)
	   (listp ctrl-stk)
	   (equal (p-ctrl-stk p) ctrl-stk)
	   (equal (p-pc p) pc))))

(prove-lemma ASSOC-APPEND-1 (rewrite)
  (equal (assoc x (append list1 list2))
	 (if (definedp x list1)
	     (assoc x list1)
	     (assoc x list2))))

(disable assoc-append-1)

(prove-lemma LR-PROGRAMS-PROPERP-1-ALL-USER-FNAMESP-NOT-USER-FNAMEP (rewrite)
  (implies (and (all-user-fnamesp (strip-cars programs))
		(not (user-fnamep x)))
	   (not (definedp x programs))))

(prove-lemma DEFINITIONS-SUBRPS-LR-PROGRAMS-PROPERP (rewrite)
  (implies (lr-programs-properp l table)
	   (and (equal (assoc 'car (comp-programs (p-prog-segment l)))
		       (p-car-code))
		(equal (assoc 'cdr (comp-programs (p-prog-segment l)))
		       (p-cdr-code))
		(equal (assoc 'cons (comp-programs (p-prog-segment l)))
		       (p-cons-code))
		(equal (assoc 'false (comp-programs (p-prog-segment l)))
		       (p-false-code))
		(equal (assoc 'falsep (comp-programs (p-prog-segment l)))
		       (p-falsep-code))
		(equal (assoc 'listp (comp-programs (p-prog-segment l)))
		       (p-listp-code))
		(equal (assoc 'nlistp (comp-programs (p-prog-segment l)))
		       (p-nlistp-code))
		(equal (assoc 'true (comp-programs (p-prog-segment l)))
		       (p-true-code))
		(equal (assoc 'truep (comp-programs (p-prog-segment l)))
		       (p-truep-code))))
  ((enable comp-programs name lr-programs-properp
	   assoc-append-1)
   (disable comp-programs-1)))

(disable lr-programs-properp-1-all-user-fnamesp-not-user-fnamep)
(disable definitions-subrps-lr-programs-properp)

;; and now some openers for p-good-resultp
(prove-lemma P-GOOD-RESULTP-P-STATE-OPENER (rewrite)
  (equal (p-good-resultp (p-state pc
				  ctrl-stk
				  temp-stk
				  prog-seg
				  data-seg
				  max-ctrl-stk-size
				  max-temp-stk-size
				  word-size
				  'run)
			 result-data-seg
			 result-temp-stk
			 result-ctrl-stk
			 result-pc)
	 (and (equal data-seg result-data-seg)
	      (equal temp-stk result-temp-stk)
	      (listp result-ctrl-stk)
	      (equal ctrl-stk result-ctrl-stk)
	      (equal pc result-pc))))

(prove-lemma P-GOOD-RESULTP-P-HALT-ERRORP-OPENER (rewrite)
  (implies (not (equal psw 'run))
	   (p-good-resultp (p-halt p psw) data-seg temp-stk ctrl-stk pc)))

(disable P-GOOD-RESULTP)

(prove-lemma ALL-P-OBJECTPS-BAD-TYPE (rewrite)
  (implies (and (not (equal (get offset lst)
			    (list (type (get offset lst))
				  (untag (get offset lst)))))
		(numberp offset)
		(lessp offset (length lst)))
	   (not (all-p-objectps lst p)))
  ((enable get p-objectp type untag)
   (disable booleanp bit-vectorp pcpp small-integerp
	    small-naturalp *1*p-runtime-support-programs
	    p-objectp-opener)))

(prove-lemma PROPER-P-DATA-SEGMENTP-BAD-TYPE ()
  (implies (and (not (equal (fetch addr data-seg)
			    (list (type (fetch addr data-seg))
				  (untag (fetch addr data-seg)))))
		(adpp (untag addr) data-seg))
	   (not (proper-p-data-segmentp data-seg p)))
  ((enable adpp fetch
	   definedp-assoc-fact-1
	   get-anything-nil)))

(prove-lemma P-CURRENT-PROGRAM-P-STATE (rewrite)
  (equal (p-current-program (p-state pc
				     ctrl-stk
				     temp-stk
				     prog-seg
				     data-seg
				     max-ctrl-stk-size
				     max-temp-stk-size
				     word-size
				     psw))
	 (assoc (area-name pc) prog-seg))
  ((enable p-current-program)))

(prove-lemma P-CURRENT-INSTRUCTION-OPENER (rewrite)
  (equal (p-current-instruction (p-state pc
					 temp-stk
					 ctrl-stk
					 prog-segment
					 data-segment
					 max-ctrl-stk-size
					 max-temp-stk-size
					 word-size
					 psw))
	 (unlabel (get (offset pc) (program-body (assoc (area-name pc)
							prog-segment)))))
  ((enable p-current-instruction p-current-program)))

(disable p-current-instruction-opener)

(prove-lemma FETCH-DEPOSIT (rewrite)
  (implies (and (numberp (offset addr1))
		(numberp (offset addr2)))
	   (equal (fetch addr1 (deposit value addr2 data-seg))
		  (if (definedp (area-name addr2) data-seg)
		      (if (equal (area-name addr1) (area-name addr2))
			  (if (equal (offset addr1) (offset addr2))
			      value
			      (fetch addr1 data-seg))
			  (fetch addr1 data-seg))
		      (fetch addr1 data-seg))))
  ((enable adpp area-name deposit fetch offset type untag
	   assoc-put-assoc-3
	   definedp-assoc-fact-1
	   get-anything-nil
	   my-get-put)))

;; add-addr
(prove-lemma AREA-NAME-ADD-ADDR (rewrite)
  (equal (area-name (add-addr addr n)) (area-name addr))
  ((enable area-name add-addr)))

(prove-lemma OFFSET-ADD-ADDR (rewrite)
  (equal (offset (add-addr addr n)) (plus (offset addr) n))
  ((enable offset add-addr)))

(prove-lemma ADP-NAME-UNTAG-ADD-ADDR (rewrite)
  (equal (adp-name (untag (add-addr addr n))) (area-name addr))
  ((enable area-name untag add-addr tag)))

(prove-lemma ADD-ADDR-OF-NON-NUMBER (rewrite)
  (implies (not (numberp n))
	   (equal (add-addr addr n) (add-addr addr 0)))
  ((enable add-addr)))

(prove-lemma ADD-ADDR-ADD-ADDR (rewrite)
  (equal (add-addr (add-addr addr n) m) (add-addr addr (plus n m)))
  ((enable add-addr)))

(prove-lemma LISTP-UNTAG-ADD-ADDR (rewrite)
  (listp (untag (add-addr addr n)))
  ((enable add-addr)))

(prove-lemma TYPE-ADD-ADDR (rewrite)
  (equal (type (add-addr addr n)) (type addr))
  ((enable add-addr)))

(prove-lemma CDDR-ADD-ADDR (rewrite)
  (equal (cddr (add-addr addr n)) nil)
  ((enable add-addr)))

(prove-lemma AREA-NAME-LR-RETURN-PC (rewrite)
  (equal (area-name (lr-return-pc l)) (area-name (p-pc l)))
  ((enable lr-return-pc)))

(prove-lemma LISTP-UNTAG-LR-RETURN-PC (rewrite)
  (listp (untag (lr-return-pc l)))
  ((enable lr-return-pc)))

(prove-lemma TYPE-LR-RETURN-PC (rewrite)
  (equal (type (lr-return-pc l)) 'pc)
  ((enable lr-return-pc)))

(prove-lemma CDDR-LR-RETURN-PC (rewrite)
  (equal (cddr (lr-return-pc l)) nil)
  ((enable lr-return-pc)))

(prove-lemma NUMBERP-OFFSET-RETURN-PC (rewrite)
  (numberp (offset (lr-return-pc l)))
  ((enable lr-return-pc)))

(prove-lemma NUMBERP-CDR-UNTAG-RETURN-PC (rewrite)
  (numberp (cdr (untag (lr-return-pc l))))
  ((enable offset)
   (use (numberp-offset-return-pc (l l)))
   (disable numberp-offset-return-pc)))

(prove-lemma CAR-UNTAG-LR-RETURN-PC (rewrite)
  (equal (car (untag (lr-return-pc l))) (car (untag (p-pc l))))
  ((enable area-name)
   (use (area-name-lr-return-pc (l l)))
   (disable area-name-lr-return-pc)))

;; sub-addr
(prove-lemma AREA-NAME-SUB-ADDR (rewrite)
  (equal (area-name (sub-addr addr n)) (area-name addr))
  ((enable area-name sub-addr)))

(prove-lemma CDDR-SUB-ADDR (rewrite)
  (equal (cddr (sub-addr addr n)) nil)
  ((enable sub-addr)))

(prove-lemma TYPE-SUB-ADDR (rewrite)
  (equal (type (sub-addr addr n)) (type addr))
  ((enable sub-addr)))

(prove-lemma LISTP-UNTAG-SUB-ADDR (rewrite)
  (listp (untag (sub-addr addr n)))
  ((enable sub-addr)))

(prove-lemma OFFSET-SUB-ADDR (rewrite)
  (equal (offset (sub-addr addr n)) (difference (offset addr) n))
  ((enable offset sub-addr)))

;; LR-BOUNDARY-NODEP
(prove-lemma LR-BOUNDARY-NODEP-SUB-ADDR (rewrite)
  (implies (lr-boundary-nodep addr)
	   (lr-boundary-nodep (sub-addr addr (identity (lr-node-size)))))
  ((disable difference-add1-arg2)))

(prove-lemma LR-BOUNDARY-NODEP-ADD-ADDR-LR-NODE-SIZE (rewrite)
  (implies (lr-boundary-nodep addr)
	   (lr-boundary-nodep (add-addr addr (identity (lr-node-size)))))
  ((enable lr-boundary-nodep)))

(disable lr-boundary-nodep)

;; LR-NODEP
(prove-lemma LR-NODEP-OPENER (rewrite)
  (equal (lr-nodep addr data-seg)
	 (and (equal (type addr) 'addr)
	      (equal (cddr addr) nil)
	      (listp addr)
	      (adpp (untag addr) data-seg)
	      (lr-boundary-nodep addr)
	      (equal (area-name addr) (identity (lr-heap-name))))))

(disable lr-nodep)

;; LR-GOOD-POINTERP
(prove-lemma LR-GOOD-POINTERP-OPENER (rewrite)
  (equal (lr-good-pointerp addr data-seg)
	 (and (equal (type addr) 'addr)
	      (equal (cddr addr) nil)
	      (listp addr)
	      (adpp (untag addr) data-seg)
	      (lr-boundary-nodep addr)
	      (equal (area-name addr) (identity (lr-heap-name)))
	      (equal (type (fetch (add-addr addr
					    (identity
					     (lr-ref-count-offset)))
				  data-seg))
		     'nat))))

(disable lr-good-pointerp)

(prove-lemma EQUAL-PLUS-REMAINDER-0-FACT ()
  (implies (and (equal (remainder offset1 max) 0)
		(equal (remainder offset2 max) 0)
		(lessp n max)
		(lessp m max)
		(numberp offset1)
		(numberp offset2))
	   (equal (equal (plus n offset1) (plus m offset2))
		  (and (equal (fix n) (fix m))
		       (equal offset1 offset2))))
  ((disable-theory addition remainders)
   (enable correctness-of-cancel-equal-plus commutativity-of-plus
	   remainder-noop remainder-zero)
   (induct (double-remainder-induction offset1 offset2 max))))

(prove-lemma LR-BOUNDARY-OFFSETP-EQUAL-PLUS-FACT (rewrite)
  (implies (and (lr-boundary-offsetp offset1)
		(lr-boundary-offsetp offset2)
		(lessp n (lr-node-size))
		(lessp m (lr-node-size))
		(numberp offset1)
		(numberp offset2))
	   (equal (equal (plus n offset1) (plus m offset2))
		  (and (equal (fix n) (fix m))
		       (equal offset1 offset2))))
  ((disable-theory addition quotients)
   (use (equal-plus-remainder-0-fact (offset1 offset1)
				     (offset2 offset2)
				     (max (lr-node-size))
				     (n n)
				     (m m)))))

(prove-lemma GOOD-POSP-LIST-NX-T-SIMPLE (rewrite)
  (implies (and (good-posp 'list pos body)
		(listp pos)
		(lessp (car (last pos))
		       (length (cur-expr (butlast pos) body))))
	   (and (good-posp 'list (nx pos) body)
		(good-posp1 pos body)))
  ((enable good-posp)))

(prove-lemma LR-PROGRAMS-PROPERP-1-LR-PROPER-EXPRP ()
  (implies (and (lr-programs-properp-1 progs program-names table)
		(member prog progs))
	   (lr-proper-exprp t
			   (program-body prog)
			   program-names
			   (formal-vars prog)
			   (strip-cars (temp-var-dcls prog))
			   table))
  ((disable lr-proper-exprp)
   (enable lr-programs-properp-1)))

(prove-lemma LR-PROPER-EXPRP-LIST-LR-PROPER-GET-T (rewrite)
  (implies (lr-proper-exprp 'list expr pnames formals temps table)
	   (equal (lr-proper-exprp t
				   (get n expr)
				   pnames formals temps table)
		  (lessp n (length expr))))
  ((enable get
	   get-anything-nil)
   (induct (get n expr))))

(prove-lemma LR-PROPER-EXPRP-T-LR-PROPER-GET-T (rewrite)
  (implies (and (not (equal (car expr) (s-temp-fetch)))
		(not (equal (car expr) (s-temp-eval)))
		(not (equal (car expr) (s-temp-test)))
		(not (equal (car expr) 'quote))
		(not (zerop n))
		(lr-proper-exprp t expr pnames formals temps table))
	   (equal (lr-proper-exprp t
				   (get n expr)
				   pnames formals temps table)
		  (lessp n (length expr))))
  ((enable get-anything-nil get-cons)
   (disable *1*p-runtime-support-programs)
   (expand (lr-proper-exprp t expr pnames formals temps table))))

(disable lr-proper-exprp-list-lr-proper-get-t)

(prove-lemma LR-PROPER-EXPRP-LR-PROPER-EXPRP-CUR-EXPR ()
  (implies (and (lr-proper-exprp t body pnames formals temps table)
		(good-posp1 pos body))
	   (lr-proper-exprp t
			    (cur-expr pos body)
			    pnames formals temps table))
  ((enable good-posp1)))

(prove-lemma LR-PROGRAMS-PROPERP-LR-PROGRAMS-PROPERP-1 (rewrite)
  (implies (and (lr-programs-properp l table)
		(equal prog-seg (p-prog-segment l)))
	   (and (lr-programs-properp-1 (p-prog-segment l)
				       (strip-logic-fnames (cdr prog-seg))
				       table)
		(definedp (area-name (p-pc l)) prog-seg)))
  ((enable lr-programs-properp)))

(prove-lemma LR-PROGRAMS-PROPERP-LR-PROPER-EXPRP-LR-EXPR ()
  (implies (and (lr-programs-properp l table)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l))))
	   (lr-proper-exprp t
			    (lr-expr l)
			    (strip-logic-fnames (cdr (p-prog-segment l)))
			    (formal-vars (p-current-program l))
			    (strip-cars (temp-var-dcls
					 (p-current-program l)))
			    table))
  ((use (lr-programs-properp-1-lr-proper-exprp
	 (prog (p-current-program l))
	 (program-names (strip-logic-fnames (cdr (p-prog-segment l))))
	 (progs (p-prog-segment l))
	 (table table))
	(lr-proper-exprp-lr-proper-exprp-cur-expr
	 (body (program-body (p-current-program l)))
	 (pnames (strip-logic-fnames (cdr (p-prog-segment l))))
	 (formals (formal-vars (p-current-program l)))
	 (temps (strip-cars (temp-var-dcls (p-current-program l))))
	 (pos (offset (p-pc l)))
	 (table table)))
   (enable cur-expr lr-expr strip-cars p-current-program
	   good-posp1-list-good-posp-list-t)
   (disable lr-proper-exprp)))

(prove-lemma LR-PROPER-EXPRP-LENGTH-CUR-EXPR ()
  (implies (and (lr-proper-exprp t expr pnames formals temps table)
		(listp expr)
		(or (subrp (car expr)) (body (car expr)))
		(not (equal (car expr) 'quote)))
	   (equal (length expr) (add1 (arity (car expr)))))
  ((disable lr-proper-exprp
	    *1*p-runtime-support-programs)
   (expand (lr-proper-exprp t expr pnames formals temps table))))

(prove-lemma LISTP-COMP-BODY-1 (rewrite)
  (equal (listp (comp-body-1 flag body n))
	 (if (equal flag 'list)
	     (listp body)
	     t))
  ((induct (comp-body-1 flag body n))
   (disable comp-if comp-temp-test)
   (expand (comp-body-1 flag body n)
	   (comp-body-1 'list body n))))

(prove-lemma CAR-APPEND (rewrite)
  (implies (listp x)
	   (equal (car (append x y)) (car x))))

(prove-lemma LENGTH-CDR-COMP-IF-COMP-BODY (rewrite)
  (equal (length (comp-if (comp-body-1 t test n1)
			  (comp-body-1 t then n2)
			  (comp-body-1 t else n3)
			  n))
	 (plus (length (comp-body-1 t test n1))
	       (length (comp-body-1 t then n2))
	       (length (comp-body-1 t else n3))
	       4)))

(prove-lemma LR-P-C-SIZE-LIST-0-OPENER (rewrite)
  (equal (lr-p-c-size-list 0 expr) 0))

(prove-lemma LR-P-C-SIZE-LIST-ADD1-OPENER (rewrite)
  (implies (lessp (add1 n) (length expr))
	   (equal (lr-p-c-size-list (add1 n) expr)
		  (plus (lr-p-c-size t (cadr expr))
			(lr-p-c-size-list n (cdr expr)))))
  ((expand (lr-p-c-size-list 1 expr))
   (induct (lr-p-c-size-list n expr))))

(prove-lemma LENGTH-COMP-BODY-1-LR-P-C-SIZE (rewrite)
  (equal (length (comp-body-1 flag body n))
	 (lr-p-c-size flag body))
  ((enable car-restn-get
	   get-add1-opener get-zerop)
   (induct (comp-body-1 flag body n))
   (disable comp-if lr-p-c-size lr-p-c-size-list)
   (expand (comp-body-1 flag body n) (comp-body-1 'list body n)
	   (lr-p-c-size flag body) (lr-p-c-size 'list body))))

(disable lr-p-c-size-list-add1-opener)

(prove-lemma LENGTH-LABEL-INSTRS (rewrite)
  (equal (length (label-instrs instrs n)) (length instrs)))

(prove-lemma LENGTH-COMP-BODY-LR-P-C-SIZE (rewrite)
  (equal (length (comp-body body)) (add1 (lr-p-c-size t body)))
  ((enable comp-body)
   (disable lr-p-c-size)))

(prove-lemma LR-P-C-SIZE-FLAG-LIST (rewrite)
  (equal (lr-p-c-size 'list (cdr expr))
	 (lr-p-c-size-list (sub1 (length expr)) expr))
  ((induct (length expr))
   (enable lr-p-c-size-list-add1-opener)
   (expand (lr-p-c-size-list 0 expr))
   (disable lr-p-c-size-list)))

(prove-lemma LR-PROPER-EXPRP-CAR-IF-CADR (rewrite)
  (implies (and (lr-proper-exprp t body pnames formals temps table)
		(listp body)
		(equal (car body) 'if))
	   (lr-proper-exprp t (cadr body) pnames formals temps table)))

(prove-lemma LR-PROPER-EXPRP-CAR-IF-CADDR (rewrite)
  (implies (and (lr-proper-exprp t body pnames formals temps table)
		(listp body)
		(equal (car body) 'if))
	   (lr-proper-exprp t (caddr body) pnames formals temps table)))

(prove-lemma LR-PROPER-EXPRP-CAR-IF-CADDDR (rewrite)
  (implies (and (lr-proper-exprp t body pnames formals temps table)
		(listp body)
		(equal (car body) 'if))
	   (lr-proper-exprp t (cadddr body) pnames formals temps table)))

(prove-lemma GOOD-POSP-LIST-T-OFFSET-PROGRAM-BODY (rewrite)
  (implies (and (good-posp 'list
			   (offset (p-pc l))
			   (program-body (p-current-program l)))
		(listp (lr-expr-list l))
		(listp (offset (p-pc l))))
	   (good-posp1 (offset (p-pc l))
		       (program-body (p-current-program l))))
  ((enable good-posp lr-expr-list)
   (disable good-posp-list)))

(prove-lemma GOOD-POSP-LIST-NX-OFFSET-PROGRAM-BODY (rewrite)
  (implies (and (good-posp 'list
			   (offset (p-pc l))
			   (program-body (p-current-program l)))
		(listp (offset (p-pc l)))
		(listp (lr-expr-list l)))
	   (good-posp 'list
		      (nx (offset (p-pc l)))
		      (program-body (p-current-program l))))
  ((enable good-posp lr-expr-list)))

(prove-lemma NAME-FORMAL-VARS-TEMP-VAR-DCLS-PROGRAM-BODY-CONS (rewrite)
  (and (equal (name (cons name rest)) name)
       (equal (formal-vars (cons name (cons formal-vars rest))) formal-vars)
       (equal (temp-var-dcls (cons name
				   (cons formal-vars
					 (cons temp-var-dcls
					       program-body))))
	      temp-var-dcls)
       (equal (program-body (cons name
				   (cons formal-vars
					 (cons temp-var-dcls
					       program-body))))
	      program-body))
  ((enable name formal-vars temp-var-dcls program-body)))

(prove-lemma PROGRAM-BODY-ASSOC-COMP-PROGRAMS-1 (rewrite)
  (implies (definedp name programs)
	   (equal (program-body (assoc name (comp-programs-1 programs)))
		  (comp-body (program-body (assoc name programs)))))
  ((enable name program-body)))

(prove-lemma PROGRAM-BODY-ASSOC-COMP-PROGRAMS (rewrite)
  (implies (definedp name programs)
	   (equal (program-body (assoc name (comp-programs programs)))
		  (if (equal name (name (car programs)))
		      (label-instrs
		       (append (comp-body-1 t
					    (program-body (car programs))
					    0)
			       (list (identity
				      (list 'SET-GLOBAL
					    (area-name (lr-answer-addr))))
				     '(RET)))
		       0)
		      (comp-body (program-body (assoc name
						      (cdr programs)))))))
  ((enable comp-programs name
	   assoc-append-1)
   (disable comp-programs-1)))

(prove-lemma DEFINEDP-AREA-NAME-MEMBER-P-CURRENT-PROGRAM (rewrite)
  (implies (definedp (area-name (p-pc l)) (p-prog-segment l))
	   (member (p-current-program l) (p-prog-segment l)))
  ((enable p-current-program)))

(defn INDUCT-HINT-6 (n body)
  (if (lessp n (length body))
      (induct-hint-6 (add1 n) body)
      t)
  ((lessp (difference (add1 (length body)) n))))

(prove-lemma LR-P-C-SIZE-LIST-0 (rewrite)
  (implies (listp body)
	   (equal (equal (lr-p-c-size-list n body) 0)
		  (or (zerop n)
		      (nlistp (cdr body))))))

(disable lr-p-c-size-list-0)

(prove-lemma LESSP-LR-P-C-SIZE-LIST-LESSP-SUB1-LENGTH (rewrite)
  (implies (not (equal (lr-p-c-size-list n body) 0))
	   (lessp (sub1 (lr-p-c-size-list n body))
		  (lr-p-c-size-list (sub1 (length body)) body)))
  ((induct (induct-hint-6 n body))
   (enable lr-p-c-size-list-0)))

(prove-lemma LR-P-PC-1-BODY-0 (rewrite)
  (equal (lr-p-pc-1 0 pos) 0))

(prove-lemma LESSP-LR-P-PC-1-LR-P-C-SIZE-HELPER-1 (rewrite)
  (implies (and (listp body)
		(not (zerop n))
		(lessp (lr-p-pc-1 (get n body) pos)
		       (lr-p-c-size t (get n body)))
		(not (equal (lr-p-pc-1 (get n body) pos) 0)))
	   (lessp (sub1 (plus (lr-p-c-size-list (sub1 n) body)
			      (lr-p-pc-1 (get n body) pos)))
		  (lr-p-c-size-list (sub1 (length body)) body)))
  ((use (lessp-lr-p-c-size-list-lessp-sub1-length (n n) (body body)))
   (enable get-large-index
	   lr-p-c-size-list-0)
   (expand (lr-p-c-size-list n body))
   (disable lr-p-c-size-list lr-p-pc-1
	    lessp-lr-p-c-size-list-lessp-sub1-length)))

(prove-lemma LESSP-LR-P-PC-1-LR-P-C-SIZE (rewrite)
  (lessp (lr-p-pc-1 body pos) (lr-p-c-size t body))
  ((induct (lr-p-pc-1 body pos))
   (expand (lr-p-pc-1 body pos) (lr-p-c-size t body))
   (disable lr-p-pc-1 lr-p-c-size lr-p-c-size-list)))

(disable lessp-lr-p-pc-1-lr-p-c-size-helper-1)

(prove-lemma NOT-LESSP-P-MAX-TEMP-STK-SIZE-LR-PUSH-TSTK (rewrite)
  (implies (equal (p-psw (lr-push-tstk l anything)) 'run)
	   (not (lessp (p-max-temp-stk-size l)
		       (length (p-temp-stk (lr-push-tstk l anything))))))
  ((enable lr-push-tstk)))

(prove-lemma PROPER-P-TEMP-STKP-LR->P-LR-PUSH-TSTK (rewrite)
  (equal (proper-p-temp-stkp temp-stkp (lr->p (lr-push-tstk l anything)))
	 (proper-p-temp-stkp temp-stkp (lr->p l))))

(prove-lemma PROPER-P-ALISTP-P-OBJECTP ()
  (implies (and (proper-p-alistp bindings l)
		(definedp name bindings))
	   (p-objectp (cdr (assoc name bindings)) l)))

(prove-lemma FORMAL-VARS-ASSOC-COMP-PROGRAMS-1 (rewrite)
  (implies (definedp name programs)
	   (equal (formal-vars (assoc name (comp-programs-1 programs)))
		  (formal-vars (assoc name programs))))
  ((enable formal-vars name)))

(prove-lemma FORMAL-VARS-ASSOC-COMP-PROGRAMS (rewrite)
  (implies (definedp name programs)
	   (equal (formal-vars (assoc name (comp-programs programs)))
		  (formal-vars (assoc name programs))))
  ((enable comp-programs name
	   assoc-append-1)
   (disable comp-programs-1
	    *1*p-runtime-support-programs)))

(prove-lemma TEMP-VAR-DCLS-ASSOC-COMP-PROGRAMS-1 (rewrite)
  (implies (definedp name programs)
	   (equal (temp-var-dcls (assoc name (comp-programs-1 programs)))
		  (temp-var-dcls (assoc name programs))))
  ((enable temp-var-dcls name)))

(prove-lemma TEMP-VAR-DCLS-ASSOC-COMP-PROGRAMS (rewrite)
  (implies (definedp name programs)
	   (equal (temp-var-dcls (assoc name (comp-programs programs)))
		  (temp-var-dcls (assoc name programs))))
  ((enable comp-programs name
	   assoc-append-1)
   (disable comp-programs-1
	    *1*p-runtime-support-programs)))

(prove-lemma LR-PROGRAMS-PROPERP-DEFINEDP-CAR-UNTAG-P-PC (rewrite)
  (implies (lr-programs-properp l table)
	   (definedp (car (untag (p-pc l))) (p-prog-segment l)))
  ((enable area-name lr-programs-properp)))

(prove-lemma P-OBJECTP-CDR-ASSOC-LITATOM-PROPER-P-ALISTP (rewrite)
  (implies (and (proper-p-alistp bindings lp)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(lr-programs-properp l table)
		(equal (strip-cars bindings)
		       (append
			(formal-vars
			 (assoc (car (untag (p-pc l)))
				(comp-programs-1 (p-prog-segment l))))
			(strip-cars
			 (temp-var-dcls
			  (assoc (car (untag (p-pc l)))
				 (comp-programs-1 (p-prog-segment l)))))))
		(litatom (lr-expr l)))
	   (p-objectp (cdr (assoc (lr-expr l) bindings)) lp))
  ((enable area-name lr-expr p-current-program)
   (use (lr-programs-properp-lr-proper-exprp-lr-expr (l l) (table table))
	(proper-p-alistp-p-objectp (bindings bindings)
				   (l lp)
				   (name (lr-expr l)))
	(member-strip-cars-definedp (x (lr-expr l)) (y bindings))
	(member-append
	 (a (lr-expr l))
	 (y (strip-cars (temp-var-dcls (p-current-program l))))
	 (x (formal-vars (p-current-program l)))))
   (disable comp-programs-1 cur-expr
	    member-append
	    p-objectp-opener)))

(prove-lemma PROPER-P-TEMP-STKP-LR-PUSH-TSTK-ASSOC-BINDINGS (rewrite)
  (implies (and (lr-programs-properp l table)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(proper-p-alistp (bindings (car (p-ctrl-stk l))) (lr->p l))
		(litatom (lr-expr l))
		(equal
		 (strip-cars (bindings (car (p-ctrl-stk l))))
		 (append
		  (formal-vars (assoc (car (untag (p-pc l)))
				      (comp-programs-1 (p-prog-segment l))))
		  (strip-cars
		   (temp-var-dcls
		    (assoc (car (untag (p-pc l)))
			   (comp-programs-1 (p-prog-segment l))))))))
	   (equal
	    (proper-p-temp-stkp
	     (p-temp-stk
	      (lr-push-tstk l
			    (cdr (assoc (lr-expr l)
					(bindings (car (p-ctrl-stk l)))))))
	     (lr->p l))
	    (proper-p-temp-stkp (p-temp-stk l) (lr->p l))))
  ((enable lr-push-tstk)
   (disable comp-programs-1
	    *1*p-runtime-support-programs)))

(prove-lemma LR-P-PC-LR-PUSH-TSTK (rewrite)
  (equal (lr-p-pc (lr-push-tstk l anything)) (lr-p-pc l))
  ((enable lr-p-pc p-current-program)))

(prove-lemma PROPER-P-STATEP-LR->P-LR-PUSH-TSTK (rewrite)
  (implies (and (proper-p-statep (lr->p l))
		(lr-programs-properp l table)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(equal (p-psw
			(lr-push-tstk
			 l
			 (cdr (assoc (lr-expr l)
				     (bindings (car (p-ctrl-stk l)))))))
		       'run)
		(litatom (lr-expr l)))
	   (proper-p-statep
	    (lr->p (lr-push-tstk
		    l
		    (cdr (assoc (lr-expr l)
				(bindings (car (p-ctrl-stk l)))))))))
  ((enable area-name p-current-program proper-p-statep)
   (disable definedp pcpp proper-p-prog-segmentp
	    *1*p-runtime-support-programs
	    proper-p-temp-stkp-lr-push-tstk-assoc-bindings)
   (use (proper-p-temp-stkp-lr-push-tstk-assoc-bindings (l l)
							(flag flag)))))

(prove-lemma GOOD-POSP1-CONS-LESSP-4-IF-LR-PROPER-EXPRP (rewrite)
  (implies (and (equal (car (cur-expr pos body)) 'if)
		(good-posp1 pos body)
		(lr-proper-exprp t body pnames formals temps table))
	   (and (good-posp1 (dv pos 1) body)
		(good-posp1 (dv pos 2) body)
		(good-posp1 (dv pos 3) body)))
  ((enable dv good-posp1)
   (use (lr-proper-exprp-length-cur-expr
	 (expr (cur-expr pos body))
	 (pnames pnames) (formals formals) (temps temps) (table table))
	(lr-proper-exprp-lr-proper-exprp-cur-expr
	 (body body) (pos pos)
	 (pnames pnames) (formals formals) (temps temps) (table table)))
   (disable lr-proper-exprp)))

(prove-lemma GOOD-POSP-CONS-LESSP-4-IF-LR-PROGRAMS-PROPERP (rewrite)
  (implies (and (equal (car (lr-expr l)) 'if)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(lr-programs-properp l table))
	   (and (good-posp1 (dv (offset (p-pc l)) 1)
			    (program-body (p-current-program l)))
		(good-posp1 (dv (offset (p-pc l)) 2)
			    (program-body (p-current-program l)))
		(good-posp1 (dv (offset (p-pc l)) 3)
			    (program-body (p-current-program l)))))
  ((enable lr-expr p-current-program)
   (disable cur-expr lr-proper-exprp)
   (use (lr-programs-properp-1-lr-proper-exprp
	 (prog (p-current-program l))
	 (program-names (strip-logic-fnames (cdr (p-prog-segment l))))
	 (progs (p-prog-segment l))
	 (table table)))))

(prove-lemma PROPER-P-STATEP-LR->P-LR-SET-POS (rewrite)
  (implies (and (lr-programs-properp l table)
		(proper-p-statep (lr->p l)))
	   (proper-p-statep (lr->p (lr-set-pos l pos))))
  ((enable adp-name area-name lr-p-pc lr-programs-properp name
	   proper-p-statep p-current-program)
   (disable lr-p-pc-1 proper-p-alistp proper-p-ctrl-stkp proper-p-temp-stkp
	    proper-p-prog-segmentp)))

(prove-lemma LR-P-PC-LR-POP-TSTK (rewrite)
  (equal (lr-p-pc (lr-pop-tstk l)) (lr-p-pc l))
  ((enable lr-p-pc p-current-program)))

(prove-lemma PROPER-P-STATEP-LR->P-LR-POP-TSTK (rewrite)
  (implies (proper-p-statep (lr->p l))
	   (proper-p-statep (lr->p (lr-pop-tstk l))))
  ((enable proper-p-statep)
   (disable exp p-ctrl-stk-size proper-p-alistp proper-p-ctrl-stkp
	    proper-p-data-segmentp proper-p-prog-segmentp)))

(prove-lemma GOOD-POSP-DV-1-TEMPS-LR-EXPR (rewrite)
  (implies (and (or (equal (car (lr-expr l)) (s-temp-eval))
		    (equal (car (lr-expr l)) (s-temp-test)))
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l))))
	   (good-posp1 (dv (offset (p-pc l)) 1)
		       (program-body (p-current-program l))))
  ((enable dv lr-expr)
   (expand (good-posp1 '(1)
		       (cur-expr (offset (p-pc l))
				 (program-body (p-current-program l)))))))

(prove-lemma PROPER-P-ALISTP-PUT-ASSOC (rewrite)
  (implies (and (proper-p-alistp bindings l)
		(p-objectp object l))
	   (proper-p-alistp (put-assoc object var-name bindings) l)))

(prove-lemma LISTP-P-TEMP-STK-LR-PUSH-TSTK (rewrite)
  (implies (equal (p-psw (lr-push-tstk l object)) 'run)
	   (listp (p-temp-stk (lr-push-tstk l object))))
  ((enable lr-push-tstk)))

(prove-lemma LR-P-PC-LR-SET-TEMP (rewrite)
  (equal (lr-p-pc (lr-set-temp l value var-name)) (lr-p-pc l))
  ((enable lr-p-pc p-current-program)))

(prove-lemma PROPER-P-STATEP-LR-SET-TEMP (rewrite)
  (implies (and (proper-p-statep (lr->p l))
		(listp (p-temp-stk l)))
	   (proper-p-statep (lr->p (lr-set-temp l
						(car (p-temp-stk l))
						var-name))))
  ((enable proper-p-statep)
   (disable exp proper-p-alistp proper-p-ctrl-stkp proper-p-data-segmentp
	    proper-p-prog-segmentp proper-p-temp-stkp)
   (expand (proper-p-temp-stkp (p-temp-stk l)
			       (lr->p (lr-set-temp l
						   (car (p-temp-stk l))
						   var-name)))
	   (proper-p-temp-stkp (p-temp-stk l) (lr->p l)))))

(prove-lemma P-OBJECTP-CDR-ASSOC-BINDINGS-PROPER-P-ALISTP (rewrite)
  (implies (and (proper-p-alistp bindings l)
		(definedp object bindings))
	   (p-objectp (cdr (assoc object bindings)) l)))

(prove-lemma DEFINEDP-CADDR-LR-EXPR-BINDINGS-CTRL-STK ()
  (implies (and (lr-programs-properp-1 progs program-names table)
		(definedp name progs)
		(or (equal (car (cur-expr pos
					  (program-body (assoc name
							       progs))))
			   (s-temp-fetch))
		    (equal (car (cur-expr pos
					  (program-body (assoc name
							       progs))))
			   (s-temp-test)))
		(good-posp1 pos (program-body (assoc name progs)))
		(equal
		 (strip-cars bindings)
		 (append (formal-vars (assoc name (comp-programs progs)))
			 (strip-cars
			  (temp-var-dcls (assoc name
						(comp-programs progs)))))))
	   (definedp (caddr (cur-expr pos (program-body (assoc name
							       progs))))
		     bindings))
  ((use (lr-programs-properp-1-lr-proper-exprp
	 (prog (assoc name progs))
	 (program-names program-names) (progs progs) (table table))
	(lr-proper-exprp-lr-proper-exprp-cur-expr
	 (body (program-body (assoc name progs)))
	 (pnames program-names)
	 (formals (formal-vars (assoc name progs)))
	 (temps (strip-cars (temp-var-dcls (assoc name progs))))
	 (pos pos)
	 (table table))
	(member-strip-cars-definedp
	 (x (caddr (cur-expr pos (program-body (assoc name progs)))))
	 (y bindings))
	(member-append (a (caddr (cur-expr pos
					   (program-body (assoc name
								progs)))))
		       (x (formal-vars (assoc name progs)))
		       (y (strip-cars (temp-var-dcls (assoc name progs))))))
   (expand
    (lr-proper-exprp t
		     (cur-expr pos (program-body (assoc name progs)))
		     program-names
		     (formal-vars (assoc name progs))
		     (strip-cars (temp-var-dcls (assoc name progs)))
		     table))
   (disable lr-proper-exprp
	    *1*p-runtime-support-programs
	    member-append
	    lr-proper-exprp-lr-proper-exprp-cur-expr)))

(prove-lemma PROPER-P-TEMP-STKP-P-TEMP-STK-LR-DO-TEMP-FETCH (rewrite)
  (implies (and (proper-p-framep (top (p-ctrl-stk l1))
				 (area-name (p-pc l1))
				 l2)
		(lr-programs-properp l1 table)
		(or (equal (car (lr-expr l1)) (s-temp-fetch))
		    (equal (car (lr-expr l1)) (s-temp-test)))
		(good-posp1 (offset (p-pc l1))
			    (program-body (p-current-program l1)))
		(same-signature (p-data-segment l1) (p-data-segment l2))
		(equal (p-prog-segment (lr->p l1)) (p-prog-segment l2))
		(equal (p-word-size l1) (p-word-size l2)))
	   (equal (proper-p-temp-stkp (p-temp-stk (lr-do-temp-fetch l1)) l2)
		  (proper-p-temp-stkp (p-temp-stk l1) l2)))
  ((enable lr-expr lr-do-temp-fetch lr-push-tstk p-current-program)
   (disable cur-expr lr-proper-exprp)
   (use (definedp-caddr-lr-expr-bindings-ctrl-stk
	  (progs (p-prog-segment l1))
	  (program-names (strip-logic-fnames (cdr (p-prog-segment l1))))
	  (bindings (bindings (car (p-ctrl-stk l1))))
	  (name (area-name (p-pc l1)))
	  (pos (offset (p-pc l1)))))))

(prove-lemma LENGTH-LR-DO-TEMP-FETCH (rewrite)
  (implies (equal (p-psw (lr-do-temp-fetch l)) 'run)
	   (not (lessp (p-max-temp-stk-size l)
		       (length (p-temp-stk (lr-do-temp-fetch l))))))
  ((enable lr-do-temp-fetch)))

(prove-lemma LR-P-PC-LR-DO-TEMP-FETCH (rewrite)
  (equal (lr-p-pc (lr-do-temp-fetch l)) (lr-p-pc l))
  ((enable lr-p-pc p-current-program)))

(prove-lemma PROPER-P-STATEP-LR-DO-TEMP-FETCH (rewrite)
  (implies (and (equal (p-psw (lr-do-temp-fetch l)) 'run)
		(lr-programs-properp l table)
		(or (equal (car (lr-expr l)) (s-temp-fetch))
		    (equal (car (lr-expr l)) (s-temp-test)))
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(proper-p-statep (lr->p l)))
	   (proper-p-statep (lr->p (lr-do-temp-fetch l))))
  ((enable proper-p-statep)
   (disable exp proper-p-alistp proper-p-ctrl-stkp proper-p-data-segmentp
	    proper-p-prog-segmentp proper-p-temp-stkp)))

(prove-lemma LENGTH-LR-PUSH-TSTK (rewrite)
  (implies (equal (p-psw (lr-push-tstk l object)) 'run)
	   (not (lessp (p-max-temp-stk-size l)
		       (length (p-temp-stk (lr-push-tstk l object))))))
  ((enable lr-push-tstk)))

(prove-lemma LISTP-P-TEMP-STK-LR-DO-TEMP-FETCH (rewrite)
  (implies (equal (p-psw (lr-do-temp-fetch l)) 'run)
	   (listp (p-temp-stk (lr-do-temp-fetch l))))
  ((enable lr-do-temp-fetch lr-push-tstk)))

(prove-lemma PROPER-P-PROG-SEGMENTP-APPEND (rewrite)
  (implies (plistp segment1)
	   (equal (proper-p-prog-segmentp (append segment1 segment2) p)
		  (and (proper-p-prog-segmentp segment1 p)
		       (proper-p-prog-segmentp segment2 p))))
  ((disable proper-p-programp)))

(prove-lemma LR-PROGRAMS-PROPERP-EXPR-QUOTE-TYPE-ADDR ()
  (implies (and (lr-programs-properp l table)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(listp (lr-expr l))
		(equal (car (lr-expr l)) 'quote))
	   (equal (type (cadr (lr-expr l))) 'addr))
  ((use (lr-programs-properp-lr-proper-exprp-lr-expr (l l) (table table)))))

(prove-lemma PROPER-P-INSTRUCTIONP-PUSH-CONSTANT-OPENER (rewrite)
  (equal (proper-p-instructionp (list 'push-constant object) name p)
	 (proper-p-push-constant-instructionp (list 'push-constant object)
					      name
					      p))
  ((enable proper-p-instructionp)))

(prove-lemma PROPER-LABELED-P-INSTRUCTIONSP-FIND-LABELP-NON-LITATOM ()
  (implies (and (proper-labeled-p-instructionsp body name p)
		(not (litatom label)))
	   (equal (find-labelp label body) f))
  ((enable legal-labelp)))

(prove-lemma LESSP-4-NOT-ZEROP-NOT-1-NOT-2-3 ()
  (implies (and (not (zerop n))
		(not (equal n 1))
		(not (equal n 2))
		(lessp n 4))
	   (equal n 3)))

(prove-lemma LESSP-4-NOT-ZEROP-NOT-1-NOT-2-3-GET-CAR-POS (rewrite)
  (implies (and (not (zerop (car pos)))
		(not (equal (car pos) 1))
		(not (equal (car pos) 2))
		(lessp (car pos) 4))
	   (equal (get (car pos) body) (cadddr body)))
  ((use (lessp-4-not-zerop-not-1-not-2-3 (n (car pos))))))

(disable lessp-4-not-zerop-not-1-not-2-3-get-car-pos)

(prove-lemma LESSP-INDEX-LESSP-LR-P-C-SIZE-LIST ()
  (not (lessp (lr-p-c-size-list (length (cdr body)) body)
	      (lr-p-c-size-list n body)))
  ((disable lr-p-c-size)))

(prove-lemma LESSP-PLUS-LR-P-C-SIZE-LR-P-PC-1-HELPER (rewrite)
  (implies (and (listp body)
		(not (zerop n))
		(not (lessp (lr-p-c-size t (get n body)) x))
		(lessp (sub1 n) (length (cdr body)))
		(equal len (length (cdr body))))
	   (equal (lessp (plus (lr-p-c-size-list len body) 1)
			 (plus (lr-p-c-size-list (sub1 n) body) x))
		  f))
  ((enable lr-p-c-size-list-0)
   (use (lessp-index-lessp-lr-p-c-size-list (n n) (body body)))
   (expand (lr-p-c-size-list n body))
   (disable lr-p-c-size lr-p-c-size-list lr-p-pc-1)))

(prove-lemma LESSP-PLUS-LR-P-C-SIZE-LR-P-PC-1 (rewrite)
  (implies (and (good-posp1 pos body)
		(lr-proper-exprp t body pnames formals temps table))
	   (not (lessp (lr-p-c-size t body)
		       (plus (lr-p-pc-1 body pos)
			     (lr-p-c-size t (cur-expr pos body))))))
  ((induct (lr-p-pc-1 body pos))
   (enable associativity-of-plus
	   get-anything-nil
	   lessp-4-not-zerop-not-1-not-2-3-get-car-pos)
   (expand (lr-p-pc-1 body pos)
	   (cur-expr pos body)
	   (lr-p-c-size t body)
	   (good-posp1 pos body)
	   (lr-proper-exprp t body pnames formals temps table))
   (disable cur-expr lr-p-pc-1 lr-p-c-size lr-p-c-size-list
	    lr-proper-exprp)
   (disable-theory addition)))

(defn INDUCT-HINT-7 (pos expr n)
  (cond ((nlistp pos) t)
	((nlistp expr) t)
	((equal (car expr) 'if)
	 (let ((then-n (plus n 3 (lr-p-c-size t (cadr expr)))))
	   (case (car pos)
	     (1 (induct-hint-7 (cdr pos) (cadr expr) n))
	     (2 (induct-hint-7 (cdr pos) (caddr expr) then-n))
	     (otherwise
	      (induct-hint-7 (cdr pos) (cadddr expr)
			     (plus 1 then-n
				   (lr-p-c-size t (caddr expr))))))))
	((equal (car expr) (s-temp-fetch)) t)
	((equal (car expr) (s-temp-eval))
	 (induct-hint-7 (cdr pos) (cadr expr) n))
	((equal (car expr) (s-temp-test))
	 (induct-hint-7 (cdr pos) (cadr expr) (plus n 4)))
	((equal (car expr) 'quote) t)
	(t (induct-hint-7 (cdr pos)
			  (get (car pos) expr)
			  (plus n
				(lr-p-c-size-list (sub1 (car pos))
						  expr))))))

(prove-lemma LR-P-C-SIZE-S-TEMP-TEST-EVAL-CADR-NOT-LESSP-FACT (rewrite)
  (implies (and (listp expr)
		(or (equal (car expr) (s-temp-eval))
		    (equal (car expr) (s-temp-test))))
	   (lessp (lr-p-c-size t (cadr expr)) (lr-p-c-size t expr)))
  ((expand (lr-p-c-size t expr))
   (disable-theory addition)
   (disable lr-p-c-size)))

(prove-lemma LENGTH-COMP-TEMP-TEST (rewrite)
  (implies (and (listp body)
		(equal (car body) (s-temp-test)))
	   (equal (length (comp-temp-test any-body
					  (comp-body-1 t (cadr body) n)
					  any-n))
		  (lr-p-c-size t body)))
  ((disable lr-p-c-size)
   (expand (lr-p-c-size t body))))

(prove-lemma PLISTP-COMP-TEMP-TEST (rewrite)
  (plistp (comp-temp-test body instrs n)))

(prove-lemma LENGTH-COMP-IF-ALT (rewrite)
  (implies (and (listp body)
		(equal (car body) 'if))
	   (equal (length (comp-if (comp-body-1 t (cadr body) n1)
				   (comp-body-1 t (caddr body) n2)
				   (comp-body-1 t (cadddr body) n3)
				   any-n))
		  (lr-p-c-size t body)))
  ((disable lr-p-c-size)
   (expand (lr-p-c-size t body))))

(prove-lemma PLISTP-COMP-IF (rewrite)
  (implies (and (plistp else-instrs)
		(listp else-instrs))
	   (plistp (comp-if test-intrs then-instrs else-instrs n))))

(prove-lemma PLISTP-COMP-BODY-1 (rewrite)
  (plistp (comp-body-1 flag body n))
  ((induct (comp-body-1 flag body n))
   (expand (comp-body-1 flag body n)
	   (comp-body-1 'list body n))
   (disable comp-if comp-temp-test)))

(prove-lemma LR-P-C-SIZE-LIST-FUNCALL-NOT-LESSP-FACT (rewrite)
  (implies (and (listp expr)
		(not (equal (car expr) (s-temp-fetch)))
		(not (equal (car expr) (s-temp-eval)))
		(not (equal (car expr) (s-temp-test)))
		(not (equal (car expr) 'quote))
		(not (equal (car expr) 'if)))
	   (lessp (lr-p-c-size-list (sub1 (length expr)) expr)
		  (lr-p-c-size t expr)))
  ((expand (lr-p-c-size t expr))
   (disable-theory addition)
   (disable lr-p-c-size)))

(prove-lemma LR-P-C-SIZE-NLISTP-BODY (rewrite)
  (implies (not (listp body))
	   (equal (lr-p-c-size t body) 1)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1-HELPER-1 (rewrite)
  (implies (and (good-posp1 pos (cadr body))
		(equal (car body) 'if)
		(listp body)
		(lr-proper-exprp t body pnames formals temps table))
	   (equal (firstn (lr-p-c-size t (cur-expr pos (cadr body)))
			  (restn (lr-p-pc-1 (cadr body) pos)
				 (comp-if (comp-body-1 t (cadr body) n)
					  then-instrs
					  else-instrs
					  n)))
		  (firstn (lr-p-c-size t (cur-expr pos (cadr body)))
			  (restn (lr-p-pc-1 (cadr body) pos)
				 (comp-body-1 t (cadr body) n)))))
  ((expand (lr-proper-exprp t body pnames formals temps table)
	   (lr-proper-exprp 'list (cdr body) pnames formals temps table))
   (disable-theory addition)
   (disable cur-expr firstn lr-proper-exprp lr-p-pc-1
	    lr-p-c-size restn)))

(prove-lemma FIRSTN-RESTN-PLUS-COMP-IF-1 (rewrite)
  (implies (and (equal j (length test))
		(listp then)
		(lessp m (length then))
		(numberp m)
		(listp test)
		(not (lessp (length then) (plus k m))))
	   (equal (firstn k
			  (restn (plus 3 j m)
				 (comp-if test then else n)))
		  (firstn k (restn m then))))
  ((enable restn-cdr)
   (disable firstn restn
	    firstn-with-large-index
	    restn-add1-opener
	    restn-with-large-index)))

(prove-lemma FIRSTN-UNLABEL-INSTRS-COMP-BODY-1-LR-P-PC-1-HELPER-2 (rewrite)
  (implies (and (good-posp1 pos (caddr body))
		(equal (car body) 'if)
		(listp body)
		(lr-proper-exprp t body pnames formals temps table))
	   (not (lessp (lr-p-c-size t (caddr body))
		       (plus (lr-p-pc-1 (caddr body) pos)
			     (lr-p-c-size t (cur-expr pos (caddr body)))))))
  ((expand (lr-proper-exprp t body pnames formals temps table)
	   (lr-proper-exprp 'list (cdr body) pnames formals temps table)
	   (lr-proper-exprp 'list (cddr body) pnames formals temps table))
   (disable-theory addition)
   (disable cur-expr lr-proper-exprp lr-p-c-size lr-p-pc-1)))

(prove-lemma FIRSTN-RESTN-PLUS-COMP-IF-2 (rewrite)
  (implies (and (equal j (length test))
		(equal i (length then))
		(listp then)
		(lessp m (length else))
		(numberp m)
		(listp test)
		(listp else)
		(not (lessp (length else) (plus m k))))
	   (equal (firstn k
			  (restn (plus j i m 4)
				 (comp-if test then else n)))
		  (firstn k (restn m else))))
  ((disable firstn restn
	    firstn-with-large-index
	    restn-add1-opener
	    restn-with-large-index)))

(prove-lemma FIRSTN-UNLABEL-INSTRS-COMP-BODY-1-LR-P-PC-1-HELPER-3 (rewrite)
  (implies (and (good-posp1 pos (cadddr body))
		(equal (car body) 'if)
		(listp body)
		(lr-proper-exprp t body pnames formals temps table))
	   (not (lessp (lr-p-c-size t (cadddr body))
		       (plus (lr-p-pc-1 (cadddr body) pos)
			     (lr-p-c-size t
					  (cur-expr pos (cadddr body)))))))
  ((expand (lr-proper-exprp t body pnames formals temps table)
	   (lr-proper-exprp 'list (cdr body) pnames formals temps table)
	   (lr-proper-exprp 'list (cddr body) pnames formals temps table)
	   (lr-proper-exprp 'list (cdddr body) pnames formals temps table))
   (disable-theory addition)
   (disable cur-expr lr-proper-exprp lr-p-c-size lr-p-pc-1)))

(prove-lemma PLUS-CONSTANT-FACT-HELPER-1 (rewrite)
  (equal (plus 1 n 3 x y) (plus n 4 x y)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1-HELPER-4 (rewrite)
  (implies (and (good-posp1 pos (cadr body))
		(listp body)
		(equal (car body) (s-temp-test))
		(lr-proper-exprp t body pnames formals temps table))
	   (equal (firstn (lr-p-c-size t (cur-expr pos (cadr body)))
			  (restn (plus (lr-p-pc-1 (cadr body) pos) 4)
				 (comp-temp-test body-1
						 (comp-body-1 t
							      (cadr body)
							      n)
						 m)))
		  (firstn (lr-p-c-size t (cur-expr pos (cadr body)))
			  (restn (lr-p-pc-1 (cadr body) pos)
				 (comp-body-1 t (cadr body) n)))))
  ((expand (lr-proper-exprp t body pnames formals temps table))
   (disable cur-expr firstn lr-proper-exprp
	    lr-p-c-size lr-p-pc-1 restn
	    firstn-with-large-index
	    lr-p-c-size-nlistp-body)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1-HELPER-5 (rewrite)
  (equal (plus 4 x) (plus x 4)))

(prove-lemma GOOD-POSP1-LR-PROPER-EXPRP-GET-CADDDR (rewrite)
  (implies (and (listp pos)
		(listp body)
		(equal (car body) 'if)
		(not (equal (car pos) 1))
		(not (equal (car pos) 2))
		(not (equal (car pos) 0))
		(numberp (car pos))
		(lr-proper-exprp t body pnames formals temps table)
		(lessp (sub1 (sub1 (sub1 (car pos))))
		       (length (cdddr body))))
	   (equal (get (car pos) body) (cadddr body)))
  ((enable lessp-4-not-zerop-not-1-not-2-3-get-car-pos)
   (expand (lr-proper-exprp t body pnames formals temps table))
   (disable lr-proper-exprp)))

(prove-lemma LR-PROPER-EXPRP-CADR-TEMPS (rewrite)
  (implies (and (lr-proper-exprp t expr pnames formals temps table)
		(or (equal (car expr) (s-temp-eval))
		    (equal (car expr) (s-temp-test))))
	   (lr-proper-exprp t (cadr expr) pnames formals temps table)))

(prove-lemma LESSP-PLUS-LR-P-C-SIZE-LR-P-PC-1-TEMPS (rewrite)
  (implies (and (good-posp1 pos (cadr body))
		(listp body)
		(or (equal (car body) (s-temp-eval))
		    (equal (car body) (s-temp-test)))
		(lr-proper-exprp t body pnames formals temps table))
	   (not (lessp (lr-p-c-size t (cadr body))
		       (plus (lr-p-pc-1 (cadr body) pos)
			     (lr-p-c-size t (cur-expr pos (cadr body)))))))
  ((expand (lr-proper-exprp t body pnames formals temps table))
   (disable lr-p-c-size lr-p-pc-1 lr-proper-exprp)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1-HELPER-6 (rewrite)
  (implies (and (listp body)
		(not (equal (car body) 'if))
		(not (equal (car body) (s-temp-fetch)))
		(not (equal (car body) (s-temp-eval)))
		(not (equal (car body) (s-temp-test)))
		(not (equal (car body) 'quote))
		(lr-proper-exprp t body pnames formals temps table)
		(not (zerop n)))
	   (not (lessp (lr-p-c-size-list (sub1 (length body)) body)
		       (plus (lr-p-c-size-list (sub1 n) body)
			     (lr-p-pc-1 (get n body) pos)))))
  ((enable get-large-index
	   lr-p-c-size-list-0)
   (expand (lr-proper-exprp t body pnames formals temps table)
	   (lr-p-c-size-list n body))
   (use (lessp-index-lessp-lr-p-c-size-list (body body) (n n)))
   (disable lr-p-c-size lr-p-c-size-list lr-p-pc-1 lr-proper-exprp
	    *1*p-runtime-support-programs
	    lessp-plus-lr-p-c-size-lr-p-pc-1-helper)))

(defn INDUCT-HINT-10 (n l x)
  (cond ((not (listp l)) t)
	((zerop n) t)
	((listp (cdr l))
	 (induct-hint-10 (sub1 n)
			 (cdr l)
			 (plus x (lr-p-c-size t (cadr l)))))
	(t t)))

(prove-lemma LR-P-C-SIZE-LIST-CAR-OPENER (rewrite)
  (implies (and (not (zerop n))
		(lessp n (length body)))
	   (equal (lr-p-c-size-list n body)
		  (plus (lr-p-c-size t (cadr body))
			(lr-p-c-size-list (sub1 n) (cdr body)))))
  ((enable lr-p-c-size-list-add1-opener)
   (induct (lr-p-c-size-list n body))
   (disable lr-p-c-size lr-p-c-size-list)))

(prove-lemma RESTN-COMP-BODY-1-LIST-FACT (rewrite)
  (implies (and (not (lessp (lr-p-c-size t (get m (cdr body))) j))
		(lessp m (length (cdr body)))
		(numberp m)
		(numberp n)
		(numberp j))
	   (equal (restn (plus (lr-p-c-size-list m body) j)
			 (comp-body-1 'list (cdr body) n))
		  (restn j
			 (comp-body-1 'list
				      (restn m (cdr body))
				      (plus n (lr-p-c-size-list m body))))))
  ((induct (induct-hint-10 m body n))
   (enable lr-p-c-size-list-0)
   (expand (get m (cdr body))
	   (comp-body-1 'list (cdr body) n))
   (disable lr-p-c-size lr-p-c-size-list)))

(disable lr-p-c-size-list-car-opener)

(prove-lemma FIRSTN-RESTN-SMALL-ENOUGH-CDR-COMP-BODY-1-LIST (rewrite)
  (implies (and (listp body)
		(not (lessp (lr-p-c-size t (car body)) (plus j k))))
	   (equal (firstn j (restn k (comp-body-1 'list body n)))
		  (firstn j (restn k (comp-body-1 t (car body) n)))))
  ((expand (comp-body-1 'list body n))
   (disable lr-p-c-size)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1-HELPER-7 (rewrite)
  (implies (and (listp body)
		(not (equal (car body) 'if))
		(not (equal (car body) (s-temp-fetch)))
		(not (equal (car body) (s-temp-eval)))
		(not (equal (car body) (s-temp-test)))
		(not (equal (car body) 'quote))
		(numberp n)
		(lr-proper-exprp t body pnames formals temps table)
		(not (zerop m))
		(lessp m (length body))
		(good-posp1 pos (get m body)))
	   (equal (firstn (lr-p-c-size t (cur-expr pos (get m body)))
			  (restn (plus (lr-p-c-size-list (sub1 m) body)
				       (lr-p-pc-1 (get m body) pos))
				 (comp-body-1 'list (cdr body) n)))
		  (firstn (lr-p-c-size t (cur-expr pos (get m body)))
			  (restn (lr-p-pc-1 (get m body) pos)
				 (comp-body-1 t
					      (get m body)
					      (plus n
						    (lr-p-c-size-list
						     (sub1 m)
						     body)))))))
  ((expand (lr-p-c-size-list m body)
	   (lr-p-c-size 'list (restn (sub1 m) (cdr body)))
	   (get m body)
	   (lr-proper-exprp t body pnames formals temps table))
   (use (lessp-index-lessp-lr-p-c-size-list (body body) (n m))
	(lr-proper-exprp-list-lr-proper-get-t
	 (expr (cdr body))
	 (n (sub1 m))
	 (temps temps) (formals formals) (pnames pnames) (table table)))
   (disable cur-expr firstn lr-proper-exprp
	    lr-p-c-size lr-p-c-size-list lr-p-pc-1 restn
	    *1*p-runtime-support-programs
	    firstn-with-large-index
	    lr-p-c-size-nlistp-body)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1-HELPER-8 (rewrite)
  (implies (and (listp body)
		(not (equal (car body) 'if))
		(not (equal (car body) (s-temp-fetch)))
		(not (equal (car body) (s-temp-eval)))
		(not (equal (car body) (s-temp-test)))
		(not (equal (car body) 'quote))
		(lr-proper-exprp t body pnames formals temps table)
		(not (zerop n))
		(lessp n (length body))
		(good-posp1 pos (get n body)))
	   (not (lessp (difference (lr-p-c-size-list (sub1 (length body))
						     body)
				   (plus (lr-p-c-size-list (sub1 n) body)
					 (lr-p-pc-1 (get n body) pos)))
		       (lr-p-c-size t (cur-expr pos (get n body))))))
  ((enable get-large-index
	   lr-p-c-size-list-0)
   (expand (lr-proper-exprp t body pnames formals temps table)
	   (lr-p-c-size-list n body))
   (use (lessp-index-lessp-lr-p-c-size-list (body body) (n n))
	(lessp-plus-lr-p-c-size-lr-p-pc-1
	 (pos pos) (body (get n body))
	 (pnames pnames) (formals formals) (temps temps)))
   (disable lr-p-c-size lr-p-c-size-list lr-p-pc-1 lr-proper-exprp
	    *1*p-runtime-support-programs
	    lessp-plus-lr-p-c-size-lr-p-pc-1-helper)))

(prove-lemma FIRSTN-LR-P-C-SIZE-RESTN-LR-P-PC-1-COMP-BODY-1 (rewrite)
  (implies (and (good-posp1 pos body)
		(lr-proper-exprp t body pnames formals temps table)
		(numberp n))
	   (equal (firstn (lr-p-c-size t (cur-expr pos body))
			  (restn (lr-p-pc-1 body pos)
				 (comp-body-1 t body n)))
		  (comp-body-1 t
			       (cur-expr pos body)
			       (plus n (lr-p-pc-1 body pos)))))
  ((expand (cur-expr pos body)
	   (good-posp1 pos body)
	   (lr-p-pc-1 body pos)
	   (comp-body-1 t body n))
   (induct (induct-hint-7 pos body n))
   (disable-theory addition)
   (enable associativity-of-plus
	   get-large-index
	   lessp-4-not-zerop-not-1-not-2-3-get-car-pos
	   plus-zero-arg2)
   (disable comp-if comp-temp-test cur-expr firstn lr-proper-exprp
	    lr-p-c-size lr-p-pc-1 plus restn
	    *1*p-runtime-support-programs
	    restn-add1-opener
	    restn-with-large-index)))

(disable firstn-lr-p-c-size-restn-lr-p-pc-1-comp-body-1-helper-5)

(prove-lemma NOT-LESSP-LR-P-C-SIZE-FLAG-T-1 (rewrite)
  (not (lessp (lr-p-c-size t body1) 1)))

(prove-lemma NOT-LESSP-X-X (rewrite)
  (equal (lessp x x) f))

(prove-lemma GET-PLUS (rewrite)
  (equal (get (plus x y) list) (get y (restn x list)))
  ((enable get
	   get-anything-nil)
   (disable append-firstn-restn)))

(disable get-plus)

(prove-lemma GET-FIRSTN-DIFFERENT-LISTS ()
  (implies (and (lessp k n)
		(equal (firstn n list1) (firstn n list2)))
	   (equal (get k list1) (get k list2)))
  ((enable get)
   (disable append-firstn-restn)))

(prove-lemma UNLABEL-LIST-LABEL (rewrite)
  (equal (unlabel (list 'dl lab comment instr)) instr)
  ((enable unlabel)))

(prove-lemma LEGAL-LABELP-LABEL-MAKE-LABEL (rewrite)
  (legal-labelp (list 'dl (lr-make-label n) comment instr))
  ((enable legal-labelp)))

(prove-lemma LR-MAKE-LABEL-NOT-NUMBERP (rewrite)
  (implies (not (numberp n))
	   (equal (lr-make-label n) (lr-make-label 0)))
  ((enable lr-make-label)))

(defn INDUCT-HINT-9 (m instrs n)
  (if (listp instrs)
      (induct-hint-9 (sub1 m) (cdr instrs) (add1 n))
      t))

(prove-lemma GET-LABEL-INSTRS (rewrite)
  (implies (lessp m (length instrs))
	   (equal (get m (label-instrs instrs n))
		  (list 'dl (lr-make-label (plus n m)) () (get m instrs))))
  ((enable get)
   (induct (induct-hint-9 m instrs n))))

(disable lr-make-label-not-numberp)

(prove-lemma GET-APPEND (rewrite)
  (equal (get n (append x y))
	 (if (lessp n (length x))
	     (get n x)
	     (get (difference n (length x)) y)))
  ((enable get)
   (disable commutativity-of-plus)))

(disable get-append)

(prove-lemma GET-LR-P-C-SIZE-LESSP-LR-P-C-SIZE-COMP-BODY-1 (rewrite)
  (implies (and (good-posp1 pos body)
		(lr-proper-exprp t body pnames formals temps table)
		(numberp n)
		(lessp m (lr-p-c-size t (cur-expr pos body))))
	   (equal (get (plus (lr-p-pc-1 body pos) m) (comp-body-1 t body n))
		  (get m (comp-body-1 t
				      (cur-expr pos body)
				      (plus n (lr-p-pc-1 body pos))))))
  ((enable get-plus)
   (use (get-firstn-different-lists
	 (k m)
	 (list1 (restn (lr-p-pc-1 body pos) (comp-body-1 t body n)))
	 (list2 (comp-body-1 t
			     (cur-expr pos body)
			     (plus n (lr-p-pc-1 body pos))))
	 (n (lr-p-c-size t (cur-expr pos body)))))
   (disable-theory addition)
   (disable cur-expr firstn lr-proper-exprp lr-p-c-size
	    lr-p-pc-1 plus restn
	    *1*p-runtime-support-programs)))

(prove-lemma GET-LR-P-PC-1-COMP-BODY-1-CUR-EXPR-COMP-BODY (rewrite)
  (implies (and (good-posp1 (offset (p-pc l)) (program-body prog))
		(listp (lr-expr l))
		(equal (car (lr-expr l)) 'quote)
		(lr-programs-properp l table)
		(equal prog (p-current-program l)))
	   (equal (get (lr-p-pc-1 (program-body prog) (offset (p-pc l)))
		       (comp-body (program-body prog)))
		  (list 'dl
			(lr-make-label (lr-p-pc-1 (program-body prog)
						  (offset (p-pc l))))
			()
			(list 'push-constant (cadr (lr-expr l))))))
  ((use (lr-programs-properp-1-lr-proper-exprp
	 (prog prog)
	 (program-names (strip-logic-fnames (cdr (p-prog-segment l))))
	 (progs (p-prog-segment l))
	 (table table))
	(get-lr-p-c-size-lessp-lr-p-c-size-comp-body-1
	 (pos (offset (p-pc l)))
	 (body (program-body prog))
	 (m 0) (n 0)
	 (pnames (strip-logic-fnames (cdr (p-prog-segment l))))
	 (formals (formal-vars prog))
	 (temps (strip-cars (temp-var-dcls prog)))))
   (enable comp-body lr-expr unlabel
	   get-append)
   (expand (comp-body-1 t
			(cur-expr (offset (p-pc l))
				  (program-body (p-current-program l)))
			(lr-p-pc-1 (program-body (p-current-program l))
				   (offset (p-pc l)))))
   (disable cur-expr comp-if comp-temp-test
	    lr-p-c-size lr-p-pc-1 lr-proper-exprp
	    get-lr-p-c-size-lessp-lr-p-c-size-comp-body-1)))

(prove-lemma GET-LR-P-PC-1-COMP-BODY-1-QUOTE (rewrite)
  (implies (and (good-posp1 (offset (p-pc l))
			    (program-body (car (p-prog-segment l))))
		(listp (lr-expr l))
		(equal (car (lr-expr l)) 'quote)
		(lr-programs-properp l table)
		(equal (area-name (p-pc l)) (caar (p-prog-segment l))))
	   (equal (get (lr-p-pc-1 (program-body (car (p-prog-segment l)))
				  (offset (p-pc l)))
		       (comp-body-1 t
				    (program-body (car (p-prog-segment l)))
				    0))
		  (list 'push-constant (cadr (lr-expr l)))))
  ((use (lr-programs-properp-1-lr-proper-exprp
	 (prog (car (p-prog-segment l)))
	 (program-names (strip-logic-fnames (cdr (p-prog-segment l))))
	 (progs (p-prog-segment l))
	 (table table))
	(get-lr-p-c-size-lessp-lr-p-c-size-comp-body-1
	 (pos (offset (p-pc l)))
	 (body (program-body (car (p-prog-segment l))))
	 (m 0) (n 0)
	 (pnames (strip-logic-fnames (cdr (p-prog-segment l))))
	 (formals (formal-vars (car (p-prog-segment l))))
	 (temps (strip-cars (temp-var-dcls (car (p-prog-segment l)))))
	 (table table)))
   (enable comp-body lr-expr p-current-program unlabel
	   get-append)
   (expand (comp-body-1 t
			(cur-expr (offset (p-pc l))
				  (program-body (car (p-prog-segment l))))
			(lr-p-pc-1 (program-body (car (p-prog-segment l)))
				   (offset (p-pc l)))))
   (disable cur-expr comp-if comp-temp-test
	    lr-p-c-size lr-p-pc-1 lr-proper-exprp
	    get-lr-p-c-size-lessp-lr-p-c-size-comp-body-1)))

(prove-lemma PROPER-P-TEMP-STKP-P-TEMP-STK-LR-PUSH-TSTK-QUOTE (rewrite)
  (implies (and (lr-programs-properp l table)
		(proper-p-prog-segmentp (comp-programs (p-prog-segment l))
					(lr->p l))
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(listp (lr-expr l))
		(equal (car (lr-expr l)) 'quote)
		(proper-p-temp-stkp (p-temp-stk l) (lr->p l)))
	   (proper-p-temp-stkp
	    (p-temp-stk (lr-push-tstk l (cadr (lr-expr l))))
	    (lr->p l)))
  ((enable lr-p-pc lr-push-tstk name p-current-program type unlabel
	   get-append)
   (disable-theory addition)
   (use (proper-p-prog-segmentp-implies-proper-p-programp
	 (segment (comp-programs (p-prog-segment l)))
	 (p (lr->p l))
	 (prog (p-current-program (lr->p l))))
	(proper-labeled-p-instructionsp-implies-labelp-and-instructionp
	 (lst (program-body (assoc (area-name (p-pc l))
				   (comp-programs (p-prog-segment l)))))
	 (name (area-name (p-pc l)))
	 (p (lr->p l))
	 (x (dl (lr-make-label (offset (lr-p-pc l))) ()
		(list 'push-constant (cadr (lr-expr l))))))
	(lr-programs-properp-expr-quote-type-addr
	 (l l) (flag flag) (table table))
	(proper-labeled-p-instructionsp-find-labelp-non-litatom
	 (body (program-body (assoc (area-name (p-pc l))
				   (comp-programs (p-prog-segment l)))))
	 (name (area-name (p-pc l)))
	 (p (lr->p l))
	 (label (cadr (lr-expr l))))
	(member-get
	 (n (offset (lr-p-pc l)))
	 (lst (program-body (assoc (area-name (p-pc l))
				   (comp-programs (p-prog-segment l)))))))
   (expand (proper-p-temp-stkp (cons (cadr (lr-expr l)) (p-temp-stk l))
			       (lr->p l)))
   (disable all-litatoms fall-off-proofp label-instrs lr-p-pc-1 lr-p-c-size
	    member-get
	    proper-labeled-p-instructionsp proper-p-prog-segmentp
	    proper-p-temp-var-dclsp proper-p-temp-stkp)))

(prove-lemma PROPER-P-STATEP-LR-PUSH-TSTK-QUOTE (rewrite)
  (implies (and (proper-p-statep (lr->p l))
		(listp (lr-expr l))
		(equal (car (lr-expr l)) 'quote)
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l)))
		(lr-programs-properp l table)
		(equal (p-psw (lr-push-tstk l (cadr (lr-expr l)))) 'run))
	   (proper-p-statep (lr->p (lr-push-tstk l (cadr (lr-expr l))))))
  ((enable proper-p-statep)
   (disable exp proper-p-alistp proper-p-ctrl-stkp proper-p-data-segmentp
	    proper-p-prog-segmentp)))

(prove-lemma GOOD-POSP-DV-1-FUNCALL-LR-EXPR (rewrite)
  (implies (and (listp (lr-expr l))
		(not (equal (car (lr-expr l)) 'if))
		(not (equal (car (lr-expr l)) (s-temp-eval)))
		(not (equal (car (lr-expr l)) (s-temp-test)))
		(not (equal (car (lr-expr l)) (s-temp-fetch)))
		(not (equal (car (lr-expr l)) 'quote))
		(good-posp1 (offset (p-pc l))
			    (program-body (p-current-program l))))
	   (good-posp 'list
		      (dv (offset (p-pc l)) 1)
		      (program-body (p-current-program l))))
  ((enable dv lr-expr good-posp good-posp1
	   listp-not-lessp-length-1)
   (expand (cur-expr (offset (p-pc l)) (program-body (p-current-program l)))
	   (cur-expr nil (program-body (p-current-program l))))
   (disable cur-expr)))

(prove-lemma PLISTP-PAIRLIST (rewrite)
  (plistp (pairlist x y)))

(prove-lemma ALL-P-OBJECTPS-APPEND (rewrite)
  (implies (plistp lst1)
	   (equal (all-p-objectps (append lst1 lst2) p)
		  (