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

 You may copy and distribute verbatim copies of this Nqthm-1992 event script as
 you receive it, in any medium, including embedding it verbatim in derivative
 works, provided that you conspicuously and appropriately publish on each copy
 a valid copyright notice "Copyright (C) 1994 by Computational Logic, Inc.  All
 Rights Reserved."

 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.
|#

; FM9001 Piton 

; J Strother Moore
; October, 1991

; History 

; This file contains the complete script of the events establishing
; that Piton is correctly implemented on top of the FM9001.  The
; original correctness proof for Piton was done for the FM8502 and is
; reported accurately and completely in CLI Tech Report 22.  That
; report is still basically accurate.  FM9001 differs from FM8502
; primarily in that instructions are in a slightly different format
; and the instruction set is slightly different.  However, when Hunt
; and Brock developed FM9001 from FM8502 they explicitly considered
; Piton's use of the FM8502 instruction set.  For each FM8502
; instruction-instance used by the Piton compiler, they included an
; FM9001 instruction that could provide the same functionality.  Thus,
; to port the Piton implementation from FM8502 to FM9001 it was only
; necessary to change the code linkers, essentially from
; LINK-INSTR-WORD on down.

; However, porting the proof from FM8502 to FM9001 was harder than
; suggested by the instruction set changes alone.  FM9001 uses a
; different formal representation of memory -- a binary tree instead
; of a linear list -- and uses a different formalization of bit
; vectors -- lists of Booleans instead of the BITV shell.  But most
; dramatically, the FM8502 proof used an experimental version of NQTHM
; that was supposed to become the released version.  That experimental
; NQTHM, called XNQTHM, provided "books".  Indeed, it was the FM8502
; Piton effort that caused books to be invented in the first place.
; With books, the XNQTHM user could develop a large body of lemmas in
; one session and then, in the course of later sessions, extract
; selected results to build upon.  Thus, books were incremental as
; opposed to the monolithic "core dump" view of state saving provided
; by NQTHM's lib files.  The FM8502 Piton proofs used four different
; (major) books: one to handle the p->r diagram, one for r->i, one for
; i->m (where we also handled m=FM8502), and then one in which the
; main correctness result was derived by extracting the key theorems
; from the three preceding books.  In addition, the original
; development devoted a book each to the definitions of the various
; machines (p, r, i, and m) and to the implementation of the compiler
; and link-assembler so they could be loaded and run in isolation from
; the correctness proof.  (This was in fact necessary since, for
; example, both the p->r book and the r->i book both needed access to
; the definition of the r machine and the implementation.)  Finally, I
; redid the FM8502 correctness proof in book form so that Piton could
; build on the definition of FM8502 without the clutter of its
; correctness proof or gate-level implementation.

; In the summer of 1989, Boyer and I began the process of "blessing"
; XNQTHM in preparation for its release as the new NQTHM.  However,
; after several months of trying to combine macros and books, we
; decided to start afresh.  We thereby embarked on the NTHM Project,
; where books are central to the whole design.  That is another story.
; However, one impact of the decision not to release XNQTHM was the
; need to reproduce the Piton proofs in a publicly available NQTHM.  I
; decided to wait until FM9001 was done and then to do the new Piton
; in NQTHM (rather than XNQTHM).

; This has had a major detrimental effect on the readability of the
; proof script.  Books allowed a clean hierarchical decomposition of
; the various layers of the problem.  This was lost when I
; (essentially) just concatenated the event lists from all of the
; Piton books into one massive script.  Of course, I had to start this
; proof effort in the library file created for the FM9001 correctness
; proof, the only NQTHM file containing "the" correct definition of
; FM9001.  To achieve the effect of isolation provided by books, each
; major section is separated from the others by thousands of DISABLE
; events which effectively erase the rule base developed thus far.  In
; addition, some names had to be changed because of clashes which were
; allowed under the book mechanism.  In short, the "new" proof of
; Piton is, in many ways, a step backward from the original one.  This
; was particularly frustrating for me since NTHM's books (which are
; implemented and seem to work) provide even greater functionality
; than XNQTHM's books.  The ideal thing to have done would have been
; for everybody else to take ten years' vacation while Boyer and I
; perfected and released NTHM, and then to develop the new FM9001 stack
; in NTHM.

; I ported the first of Piton's 3 commutative diagrams to the FM9001
; in May, 1991.  At that time, the FM9001 correctness proof was not
; completed.  I "borrowed" a lib file from Bishop that contained the
; majority of the proof and did the bottom-most diagram in that lib.
; Actually, I introduced a fourth layer to Piton: the link from M to
; FM9001 (the corresponding level in the FM8502 proof was an equality)
; has become a full-fledged commutative diagram that handles the
; memory.  See M->FM9001, which is now the fourth application in LOAD,
; and ONE-WAY-CORRESPONDENCE-M-FM9001.  In one week in May, I
; successfully proved that the M machine was implemented on FM9001.  I
; then waited until my decks were clear (October, 1991) to port the
; rest of the proof.  It has taken roughly 2 weeks to do the rest.

; A major new proof burden was introduced by the new memory representation.
; See the events surrounding PLAUSIBLE-DATA-LINK-TABLEP.  The basic problem
; was that in order to display the FM9001 memory to recover the M memory (i.e.,
; to get the "up" arrow in the bottom-most diagram), it was necessary to know
; that no address exceeded the size the of FM9001 memory.  This in turn
; required showing that the size of the final memory was the same as that
; for the initial memory.  This in turn forced us to prove the analogous
; fact all the way up, i.e., for M, I, R, and P.  At the higher levels, of
; course, what we proved was that the machines preserved the "signatures"
; of the program and data segments.  While this work could have been
; rather naturally done at the time we were dealing with the respective
; machines in their component diagrams, we did not recognize the need for the
; theorems until we had redone all of the old diagrams and were trying to
; combine everything at the very end.  Thus, you will see at the end of this
; script some hideous lemmas about the r and p machines where we tediously
; enable things that were "naturally" enabled earlier in the script.

; The book structure of the original proof can be seen by searching
; for comments of the form "; Book:".

; November, 1991: After the first successful port to FM9001 a new
; patch was installed: The loader was changed to allow us to specify
; the location at which the Piton data segment was laid down in
; memory.  This was done so that part of the data segment could be
; memory mapped to allow us to do some output from Piton.  This was
; achieved by swapping the positions of the prog segment and the data
; segment (in the original Piton work, the prog segment was laid out
; first, followed by the data segment and then the system data).  Now
; the data segment is laid out first, then the program segment, and
; then the system data segment.  Furthermore, all of this is laid out
; starting at a given location, generally named the LOAD-ADDR, and the
; contents of memory below that point is specified by an oracle,
; generally named BOOT-LST.

; This change has had drastic effects rippling through the Piton
; proof.

; This takes roughly 8 hours on a Sparc 2 in AKCL and generates 30Mb
; of .proof output and a .lib file of about 20Mb.

(note-lib "fm9001-replay" t)

(set-status close-data-base-1 t ((boot-strap initial)
                                 (add-shell enable)
                                 ((defn *1*defn) enable)
                                 (otherwise disable)))

; Book:  Implementation.events

; We first define the implementation of Piton.  It is odd that we
; start there rather than with the semantics of the P machine.
; Logically and historically we started with the semantics.  But we
; are building the proof from the bottom up and in the beginning all
; we have is FM9001 and the implementation and we will build the m
; machine to explain the link part of the implementation, the i
; machine to build the code generator part, etc.

(DEFN INCR (C X)
  (IF (NLISTP X)
      NIL
      (CONS (XOR C (CAR X))
            (INCR (AND C (CAR X)) (CDR X)))))

(DEFN BITN (X N)
  (COND ((ZEROP N) F)
        ((EQUAL N 1) (CAR X))
        (T (BITN (CDR X) (SUB1 N)))))

(ADD-SHELL P-STATE NIL P-STATEP
           ((P-PC (NONE-OF) ZERO)
            (P-CTRL-STK (NONE-OF) ZERO)
            (P-TEMP-STK (NONE-OF) ZERO)
            (P-PROG-SEGMENT (NONE-OF) ZERO)
            (P-DATA-SEGMENT (NONE-OF) ZERO)
            (P-MAX-CTRL-STK-SIZE (NONE-OF) ZERO)
            (P-MAX-TEMP-STK-SIZE (NONE-OF) ZERO)
            (P-WORD-SIZE (NONE-OF) ZERO)
            (P-PSW (NONE-OF) ZERO)))

(DEFN ERRORP
      (PSW)
      (AND (NOT (EQUAL PSW 'RUN))
           (NOT (EQUAL PSW 'HALT))))

(DEFN DEFINITION
      (NAME ALIST)
      (ASSOC NAME ALIST))

(DEFN STRIP-CDRS
      (ALIST)
      (IF (NLISTP ALIST)
          NIL
          (CONS (CDAR ALIST)
                (STRIP-CDRS (CDR ALIST)))))

(DEFN NAME (D) (CAR D))

(DEFN FORMAL-VARS (D) (CADR D))

(DEFN TEMP-VAR-DCLS (D) (CADDR D))

(DEFN PROGRAM-BODY (D) (CDDDR D))

(DEFN LOCAL-VARS
      (D)
      (APPEND (FORMAL-VARS D)
              (STRIP-CARS (TEMP-VAR-DCLS D))))

(DEFN ADP-NAME (ADP) (CAR ADP))

(DEFN ADP-OFFSET (ADP) (CDR ADP))

(DEFN SUB-ADP
      (ADP N)
      (CONS (ADP-NAME ADP)
            (DIFFERENCE (ADP-OFFSET ADP) N)))

(DEFN GET
      (N LST)
      (IF (ZEROP N)
          (CAR LST)
          (GET (SUB1 N) (CDR LST))))

(DEFN TAG (TYPE OBJ) (LIST TYPE OBJ))

(DEFN TYPE (CONST) (CAR CONST))

(DEFN UNTAG (CONST) (CADR CONST))

(DEFN AREA-NAME
      (X)
      (ADP-NAME (UNTAG X)))

(DEFN SUB-ADDR
      (ADDR N)
      (TAG (TYPE ADDR)
           (SUB-ADP (UNTAG ADDR) N)))

(DEFN TOP (STK) (CAR STK))

(DEFN POP (STK) (CDR STK))

(DEFN DL
      (LAB COMMENT INS)
      (LIST 'DL LAB COMMENT INS))

(DEFN LABELLEDP
      (X)
      (EQUAL (CAR X) 'DL))

(DEFN UNLABEL
      (X)
      (IF (LABELLEDP X) (CADDDR X) X))

(DEFN FIND-LABEL
      (X LST)
      (COND ((NLISTP LST) 0)
            ((AND (LABELLEDP (CAR LST))
                  (EQUAL X (CADAR LST)))
             0)
            (T (ADD1 (FIND-LABEL X (CDR LST))))))

(DEFN PC
      (LAB PROGRAM)
      (TAG 'PC
           (CONS (NAME PROGRAM)
                 (FIND-LABEL LAB
                             (PROGRAM-BODY PROGRAM)))))

(DEFN BINDINGS (FRAME) (CAR FRAME))

(DEFN RET-PC (FRAME) (CADR FRAME))

(DEFN P-FRAME-SIZE
      (FRAME)
      (PLUS 2 (LENGTH (BINDINGS FRAME))))

(DEFN P-CTRL-STK-SIZE
      (CTRL-STK)
      (IF (NLISTP CTRL-STK)
          0
          (PLUS (P-FRAME-SIZE (TOP CTRL-STK))
                (P-CTRL-STK-SIZE (CDR CTRL-STK)))))

(DEFN ICODE-CALL
      (INS PCN PROGRAM)
      (LIST '(CPUSH_*)
            (TAG 'PC
                 (CONS (NAME PROGRAM) (ADD1 PCN)))
            '(JUMP_*)
            (TAG 'PC
                 (CONS (CADR INS) '(PRELUDE)))))

(DEFN GENERATE-PRELUDE1
      (TEMP-VAR-DCLS)
      (IF (NLISTP TEMP-VAR-DCLS)
          NIL
          (CONS '(CPUSH_*)
                (CONS (CADAR TEMP-VAR-DCLS)
                      (GENERATE-PRELUDE1 (CDR TEMP-VAR-DCLS))))))

(DEFN GENERATE-PRELUDE2
      (FORMAL-VARS)
      (IF (NLISTP FORMAL-VARS)
          NIL
          (CONS '(CPUSH_<TSP>+)
                (GENERATE-PRELUDE2 (CDR FORMAL-VARS)))))

(DEFN GENERATE-PRELUDE
      (PROGRAM)
      (APPEND (CONS (DL (CONS (NAME PROGRAM) '(PRELUDE))
                        '(PRELUDE)
                        '(CPUSH_CFP))
                    '((MOVE_CFP_CSP)))
              (APPEND (GENERATE-PRELUDE1 (REVERSE (TEMP-VAR-DCLS PROGRAM)))
                      (GENERATE-PRELUDE2 (FORMAL-VARS PROGRAM)))))

(DEFN FIND-POSITION-OF-VAR
      (VAR LST)
      (COND ((NLISTP LST) 0)
            ((EQUAL VAR (CAR LST)) 0)
            (T (ADD1 (FIND-POSITION-OF-VAR VAR
                                           (CDR LST))))))

(DEFN OFFSET-FROM-CSP
      (VAR PROGRAM)
      (FIND-POSITION-OF-VAR VAR
                            (LOCAL-VARS PROGRAM)))

(DEFN GENERATE-POSTLUDE
      (PROGRAM)
      (CONS (DL (CONS (NAME PROGRAM)
                      (LENGTH (PROGRAM-BODY PROGRAM)))
                '(POSTLUDE)
                '(MOVE_CSP_CFP))
            '((CPOP_CFP) (CPOP_PC))))

(DEFN ICODE-RET
      (INS PCN PROGRAM)
      (LIST '(JUMP_*)
            (TAG 'PC
                 (CONS (NAME PROGRAM)
                       (LENGTH (PROGRAM-BODY PROGRAM))))))

(DEFN ICODE-LOCN
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'NAT
                       (OFFSET-FROM-CSP (CADR INS) PROGRAM))
                  '((ADD_X{N}_CSP)
                    (MOVE_X_<X{S}>)
                    (ADD_X{N}_CSP)
                    (TPUSH_<X{S}>)))))

(DEFN ICODE-PUSH-CONSTANT
      (INS PCN PROGRAM)
      (LIST '(TPUSH_*)
            (COND ((EQUAL (CADR INS) 'PC)
                   (TAG 'PC
                        (CONS (NAME PROGRAM) (ADD1 PCN))))
                  ((NLISTP (CADR INS))
                   (PC (CADR INS) PROGRAM))
                  (T (CADR INS)))))

(DEFN ICODE-PUSH-LOCAL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'NAT
                       (OFFSET-FROM-CSP (CADR INS) PROGRAM))
                  '((ADD_X{N}_CSP) (TPUSH_<X{S}>)))))

(DEFN ICODE-PUSH-GLOBAL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'ADDR (CONS (CADR INS) 0))
                  '((TPUSH_<X{A}>)))))

(DEFN ICODE-PUSH-CTRL-STK-FREE-SIZE
      (INS PCN PROGRAM)
      '((MOVE_X_*)
        (SYS-ADDR (FULL-CTRL-STK-ADDR . 0))
        (MOVE_X_<X{S}>)
        (TPUSH_CSP)
        (SUB_<TSP>{S}_X{S})))

(DEFN ICODE-PUSH-TEMP-STK-FREE-SIZE
      (INS PCN PROGRAM)
      '((MOVE_X_*)
        (SYS-ADDR (FULL-TEMP-STK-ADDR . 0))
        (MOVE_X_<X{S}>)
        (TPUSH_TSP)
        (SUB_<TSP>{S}_X{S})))

(DEFN ICODE-PUSH-TEMP-STK-INDEX
 (INS PCN PROGRAM)
 (CONS
      '(MOVE_Y_TSP)
      (CONS '(MOVE_X_*)
            (CONS '(SYS-ADDR (EMPTY-TEMP-STK-ADDR . 0))
                  (CONS '(MOVE_X_<X{S}>)
                        (CONS '(SUB_<Z>_X{S}_Y{S})
                              (CONS '(TPUSH_X)
                                    (CONS '(MOVE_X_*)
                                          (CONS (TAG 'NAT (ADD1 (CADR INS)))
                                                '((SUB_<TSP>{N}_X{N})))))))))))

(DEFN ICODE-JUMP-IF-TEMP-STK-FULL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_TSP)
            (CONS '(MOVE_Y_*)
                  (CONS '(SYS-ADDR (FULL-TEMP-STK-ADDR . 0))
                        (CONS '(MOVE_Y_<Y{S}>)
                              (CONS '(SUB_<Z>_X{S}_Y{S})
                                    (CONS '(MOVE_X_*)
                                          (CONS (PC (CADR INS) PROGRAM)
                                                '((JUMP-Z_X))))))))))

(DEFN ICODE-JUMP-IF-TEMP-STK-EMPTY
      (INS PCN PROGRAM)
      (CONS '(MOVE_Y_TSP)
            (CONS '(MOVE_X_*)
                  (CONS '(SYS-ADDR (EMPTY-TEMP-STK-ADDR . 0))
                        (CONS '(MOVE_X_<X{S}>)
                              (CONS '(SUB_<Z>_X{S}_Y{S})
                                    (CONS '(MOVE_X_*)
                                          (CONS (PC (CADR INS) PROGRAM)
                                                '((JUMP-Z_X))))))))))

(DEFN ICODE-POP
      (INS PCN PROGRAM)
      '((TPOP_X)))

(DEFN ICODE-POP*
      (INS PCN PROGRAM)
      (LIST '(ADD_TSP_*{N})
            (TAG 'NAT (CADR INS))))

(DEFN ICODE-POPN
      (INS PCN PROGRAM)
      '((TPOP_X) (ADD_TSP_X{N})))

(DEFN ICODE-POP-LOCAL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'NAT
                       (OFFSET-FROM-CSP (CADR INS) PROGRAM))
                  '((ADD_X{N}_CSP) (TPOP_<X{S}>)))))

(DEFN ICODE-POP-GLOBAL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'ADDR (CONS (CADR INS) 0))
                  '((TPOP_<X{A}>)))))

(DEFN ICODE-POP-LOCN
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'NAT
                       (OFFSET-FROM-CSP (CADR INS) PROGRAM))
                  '((ADD_X{N}_CSP)
                    (MOVE_X_<X{S}>)
                    (ADD_X{N}_CSP)
                    (TPOP_<X{S}>)))))

(DEFN ICODE-POP-CALL
      (INS PCN PROGRAM)
      (CONS '(TPOP_X)
            (CONS '(CPUSH_*)
                  (CONS (TAG 'PC
                             (CONS (NAME PROGRAM) (ADD1 PCN)))
                        '((JUMP_X{SUBR}))))))

(DEFN ICODE-FETCH-TEMP-STK
      (INS PCN PROGRAM)
      '((TPOP_Y)
        (INCR_Y_Y{N})
        (MOVE_X_*)
        (SYS-ADDR (EMPTY-TEMP-STK-ADDR . 0))
        (MOVE_X_<X{S}>)
        (SUB_X{S}_Y{N})
        (TPUSH_<X{S}>)))

(DEFN ICODE-DEPOSIT-TEMP-STK
      (INS PCN PROGRAM)
      '((TPOP_Y)
        (INCR_Y_Y{N})
        (MOVE_X_*)
        (SYS-ADDR (EMPTY-TEMP-STK-ADDR . 0))
        (MOVE_X_<X{S}>)
        (SUB_X{S}_Y{N})
        (TPOP_<X{S}>)))

(DEFN ICODE-JUMP
      (INS PCN PROGRAM)
      (LIST '(JUMP_*)
            (PC (CADR INS) PROGRAM)))

(DEFN JUMP_*-LST
      (LST PROGRAM)
      (IF (NLISTP LST)
          NIL
          (CONS '(JUMP_*)
                (CONS (PC (CAR LST) PROGRAM)
                      (JUMP_*-LST (CDR LST) PROGRAM)))))

(DEFN ICODE-JUMP-CASE
      (INS PCN PROGRAM)
      (APPEND '((TPOP_X) (ADD_X_X{N}) (ADD_PC_X{N}))
              (JUMP_*-LST (CDR INS) PROGRAM)))

(DEFN ICODE-PUSHJ
      (INS PCN PROGRAM)
      (LIST '(TPUSH_*)
            (TAG 'PC
                 (CONS (NAME PROGRAM) (ADD1 PCN)))
            '(JUMP_*)
            (PC (CADR INS) PROGRAM)))

(DEFN ICODE-POPJ
      (INS PCN PROGRAM)
      '((TPOP_PC)))

(DEFN ICODE-SET-LOCAL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'NAT
                       (OFFSET-FROM-CSP (CADR INS) PROGRAM))
                  '((ADD_X{N}_CSP)
                    (MOVE_<X{S}>_<TSP>)))))

(DEFN ICODE-SET-GLOBAL
      (INS PCN PROGRAM)
      (CONS '(MOVE_X_*)
            (CONS (TAG 'ADDR (CONS (CADR INS) 0))
                  '((MOVE_<X{A}>_<TSP>)))))

(DEFN ICODE-TEST-NAT-AND-JUMP
      (INS PCN PROGRAM)
      (IF (EQUAL (CADR INS) 'ZERO)
          (CONS '(TPOP{N}_<Z>_Y)
                (CONS '(MOVE_X_*)
                      (CONS (PC (CADDR INS) PROGRAM)
                            '((JUMP-Z_X)))))
          (CONS '(TPOP{N}_<Z>_Y)
                (CONS '(MOVE_X_*)
                      (CONS (PC (CADDR INS) PROGRAM)
                            '((JUMP-NZ_X)))))))

(DEFN ICODE-TEST-INT-AND-JUMP
      (INS PCN PROGRAM)
      (CASE (CAR (CDR INS))
            (ZERO (CONS '(TPOP{I}_<ZN>_Y)
                        (CONS '(MOVE_X_*)
                              (CONS (PC (CADDR INS) PROGRAM)
                                    '((JUMP-Z_X))))))
            (NOT-ZERO (CONS '(TPOP{I}_<ZN>_Y)
                            (CONS '(MOVE_X_*)
                                  (CONS (PC (CADDR INS) PROGRAM)
                                        '((JUMP-NZ_X))))))
            (NEG (CONS '(TPOP{I}_<ZN>_Y)
                       (CONS '(MOVE_X_*)
                             (CONS (PC (CADDR INS) PROGRAM)
                                   '((JUMP-N_X))))))
            (NOT-NEG (CONS '(TPOP{I}_<ZN>_Y)
                           (CONS '(MOVE_X_*)
                                 (CONS (PC (CADDR INS) PROGRAM)
                                       '((JUMP-NN_X))))))
            (POS (LIST '(TPOP{I}_<ZN>_Y)
                       '(MOVE_X_*)
                       (TAG 'PC
                            (CONS (NAME PROGRAM) (ADD1 PCN)))
                       '(JUMP-N_X)
                       '(JUMP-Z_X)
                       '(JUMP_*)
                       (PC (CADDR INS) PROGRAM)))
            (OTHERWISE (CONS '(TPOP{I}_<ZN>_Y)
                             (CONS '(MOVE_X_*)
                                   (CONS (PC (CADDR INS) PROGRAM)
                                         '((JUMP-N_X) (JUMP-Z_X))))))))

(DEFN ICODE-TEST-BOOL-AND-JUMP
      (INS PCN PROGRAM)
      (IF (EQUAL (CADR INS) 'T)
          (CONS '(TPOP{B}_<Z>_Y)
                (CONS '(MOVE_X_*)
                      (CONS (PC (CADDR INS) PROGRAM)
                            '((JUMP-NZ_X)))))
          (CONS '(TPOP{B}_<Z>_Y)
                (CONS '(MOVE_X_*)
                      (CONS (PC (CADDR INS) PROGRAM)
                            '((JUMP-Z_X)))))))

(DEFN ICODE-TEST-BITV-AND-JUMP
      (INS PCN PROGRAM)
      (IF (EQUAL (CADR INS) 'ALL-ZERO)
          (CONS '(TPOP{V}_<Z>_Y)
                (CONS '(MOVE_X_*)
                      (CONS (PC (CADDR INS) PROGRAM)
                            '((JUMP-Z_X)))))
          (CONS '(TPOP{V}_<Z>_Y)
                (CONS '(MOVE_X_*)
                      (CONS (PC (CADDR INS) PROGRAM)
                            '((JUMP-NZ_X)))))))

(DEFN ICODE-NO-OP
      (INS PCN PROGRAM)
      '((MOVE_X_X)))

(DEFN ICODE-ADD-ADDR
      (INS PCN PROGRAM)
      '((TPOP_X) (ADD_<TSP>{A}_X{N})))

(DEFN ICODE-SUB-ADDR
      (INS PCN PROGRAM)
      '((TPOP_X) (SUB_<TSP>{A}_X{N})))

(DEFN ICODE-EQ
      (INS PCN PROGRAM)
      '((TPOP_X)
        (XOR_<Z>_<TSP>_X)
        (XOR_<TSP>_<TSP>)
        (MOVE-Z_<TSP>_*)
        (BOOL T)))

(DEFN ICODE-LT-ADDR
      (INS PCN PROGRAM)
      '((TPOP_X)
        (SUB_<C>_<TSP>{A}_X{A})
        (XOR_<TSP>_<TSP>)
        (MOVE-C_<TSP>_*)
        (BOOL T)))

(DEFN ICODE-FETCH
      (INS PCN PROGRAM)
      '((TPOP_X) (TPUSH_<X{A}>)))

(DEFN ICODE-DEPOSIT
      (INS PCN PROGRAM)
      '((TPOP_X) (TPOP_<X{A}>)))

(DEFN ICODE-ADD-INT
      (INS PCN PROGRAM)
      '((TPOP_X) (ADD_<TSP>{I}_X{I})))

(DEFN ICODE-ADD-INT-WITH-CARRY
      (INS PCN PROGRAM)
      '((TPOP_X)
        (TPOP_Y)
        (ASR_<C>_<TSP>_<TSP>{B})
        (ADDC_<V>_X{I}_Y{I})
        (MOVE-V_<TSP>_*)
        (BOOL T)
        (TPUSH_X)))

(DEFN ICODE-ADD1-INT
      (INS PCN PROGRAM)
      '((INCR_<TSP>_<TSP>{I})))

(DEFN ICODE-SUB-INT
      (INS PCN PROGRAM)
      '((TPOP_X) (SUB_<TSP>{I}_X{I})))

(DEFN ICODE-SUB-INT-WITH-CARRY
      (INS PCN PROGRAM)
      '((TPOP_Y)
        (TPOP_X)
        (ASR_<C>_<TSP>_<TSP>{B})
        (SUBB_<V>_X{I}_Y{I})
        (MOVE-V_<TSP>_*)
        (BOOL T)
        (TPUSH_X)))

(DEFN ICODE-SUB1-INT
      (INS PCN PROGRAM)
      '((DECR_<TSP>_<TSP>{I})))

(DEFN ICODE-NEG-INT
      (INS PCN PROGRAM)
      '((NEG_<TSP>_<TSP>{I})))

(DEFN ICODE-LT-INT
      (INS PCN PROGRAM)
      '((TPOP_X)
        (SUB_<NV>_<TSP>{I}_X{I})
        (MOVE_<TSP>_*)
        (BOOL F)
        (MOVE-V_<TSP>_*)
        (BOOL T)
        (MOVE_X_*)
        (BOOL F)
        (MOVE-N_X_*)
        (BOOL T)
        (XOR_<TSP>{B}_X{B})))

(DEFN ICODE-INT-TO-NAT
      (INS PCN PROGRAM)
      '((INT-TO-NAT)))

(DEFN ICODE-ADD-NAT
      (INS PCN PROGRAM)
      '((TPOP_X) (ADD_<TSP>{N}_X{N})))

(DEFN ICODE-ADD-NAT-WITH-CARRY
      (INS PCN PROGRAM)
      '((TPOP_X)
        (TPOP_Y)
        (ASR_<C>_<TSP>_<TSP>{B})
        (ADDC_<C>_X{N}_Y{N})
        (MOVE-C_<TSP>_*)
        (BOOL T)
        (TPUSH_X)))

(DEFN ICODE-ADD1-NAT
      (INS PCN PROGRAM)
      '((INCR_<TSP>_<TSP>{N})))

(DEFN ICODE-SUB-NAT
      (INS PCN PROGRAM)
      '((TPOP_X) (SUB_<TSP>{N}_X{N})))

(DEFN ICODE-SUB-NAT-WITH-CARRY
      (INS PCN PROGRAM)
      '((TPOP_Y)
        (TPOP_X)
        (ASR_<C>_<TSP>_<TSP>{B})
        (SUBB_<C>_X{N}_Y{N})
        (MOVE-C_<TSP>_*)
        (BOOL T)
        (TPUSH_X)))

(DEFN ICODE-SUB1-NAT
      (INS PCN PROGRAM)
      '((DECR_<TSP>_<TSP>{N})))

(DEFN ICODE-LT-NAT
      (INS PCN PROGRAM)
      '((TPOP_X)
        (SUB_<C>_<TSP>{N}_X{N})
        (XOR_<TSP>_<TSP>)
        (MOVE-C_<TSP>_*)
        (BOOL T)))

(DEFN ICODE-MULT2-NAT
      (INS PCN PROGRAM)
      '((ADD_<TSP>_<TSP>{N})))

(DEFN ICODE-MULT2-NAT-WITH-CARRY-OUT
      (INS PCN PROGRAM)
      '((TPOP_X)
        (ADD_<C>_X_X{N})
        (TPUSH_*)
        (BOOL F)
        (MOVE-C_<TSP>_*)
        (BOOL T)
        (TPUSH_X)))

(DEFN ICODE-DIV2-NAT
      (INS PCN PROGRAM)
      '((TPOP_<C>_X)
        (LSR_<C>_X_X{N})
        (TPUSH_X)
        (TPUSH_*)
        (NAT 0)
        (MOVE-C_<TSP>_*)
        (NAT 1)))

(DEFN ICODE-OR-BITV
      (INS PCN PROGRAM)
      '((TPOP_X) (OR_<TSP>{V}_X{V})))

(DEFN ICODE-AND-BITV
      (INS PCN PROGRAM)
      '((TPOP_X) (AND_<TSP>{V}_X{V})))

(DEFN ICODE-NOT-BITV
      (INS PCN PROGRAM)
      '((NOT_<TSP>_<TSP>{V})))

(DEFN ICODE-XOR-BITV
      (INS PCN PROGRAM)
      '((TPOP_X) (XOR_<TSP>{V}_X{V})))

(DEFN ICODE-RSH-BITV
      (INS PCN PROGRAM)
      '((LSR_<TSP>_<TSP>{V})))

(DEFN ICODE-LSH-BITV
      (INS PCN PROGRAM)
      '((ADD_<TSP>_<TSP>{V})))

(DEFN ICODE-OR-BOOL
      (INS PCN PROGRAM)
      '((TPOP_X) (OR_<TSP>{B}_X{B})))

(DEFN ICODE-AND-BOOL
      (INS PCN PROGRAM)
      '((TPOP_X) (AND_<TSP>{B}_X{B})))

(DEFN ICODE-NOT-BOOL
      (INS PCN PROGRAM)
      '((XOR_<TSP>{B}_*{B}) (BOOL T)))

(DEFN ICODE1
      (INS PCN PROG)
      (CASE (CAR INS)
            (CALL (ICODE-CALL INS PCN PROG))
            (RET (ICODE-RET INS PCN PROG))
            (LOCN (ICODE-LOCN INS PCN PROG))
            (PUSH-CONSTANT (ICODE-PUSH-CONSTANT INS PCN PROG))
            (PUSH-LOCAL (ICODE-PUSH-LOCAL INS PCN PROG))
            (PUSH-GLOBAL (ICODE-PUSH-GLOBAL INS PCN PROG))
            (PUSH-CTRL-STK-FREE-SIZE (ICODE-PUSH-CTRL-STK-FREE-SIZE INS PCN
                                                                    PROG))
            (PUSH-TEMP-STK-FREE-SIZE (ICODE-PUSH-TEMP-STK-FREE-SIZE INS PCN
                                                                    PROG))
            (PUSH-TEMP-STK-INDEX (ICODE-PUSH-TEMP-STK-INDEX INS PCN PROG))
            (JUMP-IF-TEMP-STK-FULL (ICODE-JUMP-IF-TEMP-STK-FULL INS PCN PROG))
            (JUMP-IF-TEMP-STK-EMPTY (ICODE-JUMP-IF-TEMP-STK-EMPTY INS PCN
                                                                  PROG))
            (POP (ICODE-POP INS PCN PROG))
            (POP* (ICODE-POP* INS PCN PROG))
            (POPN (ICODE-POPN INS PCN PROG))
            (POP-LOCAL (ICODE-POP-LOCAL INS PCN PROG))
            (POP-GLOBAL (ICODE-POP-GLOBAL INS PCN PROG))
            (POP-LOCN (ICODE-POP-LOCN INS PCN PROG))
            (POP-CALL (ICODE-POP-CALL INS PCN PROG))
            (FETCH-TEMP-STK (ICODE-FETCH-TEMP-STK INS PCN PROG))
            (DEPOSIT-TEMP-STK (ICODE-DEPOSIT-TEMP-STK INS PCN PROG))
            (JUMP (ICODE-JUMP INS PCN PROG))
            (JUMP-CASE (ICODE-JUMP-CASE INS PCN PROG))
            (PUSHJ (ICODE-PUSHJ INS PCN PROG))
            (POPJ (ICODE-POPJ INS PCN PROG))
            (SET-LOCAL (ICODE-SET-LOCAL INS PCN PROG))
            (SET-GLOBAL (ICODE-SET-GLOBAL INS PCN PROG))
            (TEST-NAT-AND-JUMP (ICODE-TEST-NAT-AND-JUMP INS PCN PROG))
            (TEST-INT-AND-JUMP (ICODE-TEST-INT-AND-JUMP INS PCN PROG))
            (TEST-BOOL-AND-JUMP (ICODE-TEST-BOOL-AND-JUMP INS PCN PROG))
            (TEST-BITV-AND-JUMP (ICODE-TEST-BITV-AND-JUMP INS PCN PROG))
            (NO-OP (ICODE-NO-OP INS PCN PROG))
            (ADD-ADDR (ICODE-ADD-ADDR INS PCN PROG))
            (SUB-ADDR (ICODE-SUB-ADDR INS PCN PROG))
            (EQ (ICODE-EQ INS PCN PROG))
            (LT-ADDR (ICODE-LT-ADDR INS PCN PROG))
            (FETCH (ICODE-FETCH INS PCN PROG))
            (DEPOSIT (ICODE-DEPOSIT INS PCN PROG))
            (ADD-INT (ICODE-ADD-INT INS PCN PROG))
            (ADD-INT-WITH-CARRY (ICODE-ADD-INT-WITH-CARRY INS PCN PROG))
            (ADD1-INT (ICODE-ADD1-INT INS PCN PROG))
            (SUB-INT (ICODE-SUB-INT INS PCN PROG))
            (SUB-INT-WITH-CARRY (ICODE-SUB-INT-WITH-CARRY INS PCN PROG))
            (SUB1-INT (ICODE-SUB1-INT INS PCN PROG))
            (NEG-INT (ICODE-NEG-INT INS PCN PROG))
            (LT-INT (ICODE-LT-INT INS PCN PROG))
            (INT-TO-NAT (ICODE-INT-TO-NAT INS PCN PROG))
            (ADD-NAT (ICODE-ADD-NAT INS PCN PROG))
            (ADD-NAT-WITH-CARRY (ICODE-ADD-NAT-WITH-CARRY INS PCN PROG))
            (ADD1-NAT (ICODE-ADD1-NAT INS PCN PROG))
            (SUB-NAT (ICODE-SUB-NAT INS PCN PROG))
            (SUB-NAT-WITH-CARRY (ICODE-SUB-NAT-WITH-CARRY INS PCN PROG))
            (SUB1-NAT (ICODE-SUB1-NAT INS PCN PROG))
            (LT-NAT (ICODE-LT-NAT INS PCN PROG))
            (MULT2-NAT (ICODE-MULT2-NAT INS PCN PROG))
            (MULT2-NAT-WITH-CARRY-OUT (ICODE-MULT2-NAT-WITH-CARRY-OUT INS PCN
                                                                      PROG))
            (DIV2-NAT (ICODE-DIV2-NAT INS PCN PROG))
            (OR-BITV (ICODE-OR-BITV INS PCN PROG))
            (AND-BITV (ICODE-AND-BITV INS PCN PROG))
            (NOT-BITV (ICODE-NOT-BITV INS PCN PROG))
            (XOR-BITV (ICODE-XOR-BITV INS PCN PROG))
            (RSH-BITV (ICODE-RSH-BITV INS PCN PROG))
            (LSH-BITV (ICODE-LSH-BITV INS PCN PROG))
            (OR-BOOL (ICODE-OR-BOOL INS PCN PROG))
            (AND-BOOL (ICODE-AND-BOOL INS PCN PROG))
            (NOT-BOOL (ICODE-NOT-BOOL INS PCN PROG))
            (OTHERWISE '((ERROR)))))

(DEFN DL-BLOCK
      (LAB COMMENT BLOCK)
      (CONS (DL LAB COMMENT (CAR BLOCK))
            (CDR BLOCK)))

(DEFN ICODE
      (INS PCN PROGRAM)
      (DL-BLOCK (CONS (NAME PROGRAM) PCN)
                INS
                (ICODE1 (UNLABEL INS) PCN PROGRAM)))

(DEFN ICOMPILE-PROGRAM-BODY
      (LST PCN PROGRAM)
      (IF (NLISTP LST)
          NIL
          (APPEND (ICODE (CAR LST) PCN PROGRAM)
                  (ICOMPILE-PROGRAM-BODY (CDR LST)
                                         (ADD1 PCN)
                                         PROGRAM))))

(DEFN ICOMPILE-PROGRAM
      (PROGRAM)
      (CONS (NAME PROGRAM)
            (APPEND (GENERATE-PRELUDE PROGRAM)
                    (APPEND (ICOMPILE-PROGRAM-BODY (PROGRAM-BODY PROGRAM)
                                                   0 PROGRAM)
                            (GENERATE-POSTLUDE PROGRAM)))))

(DEFN ICOMPILE
      (PROGRAMS)
      (IF (NLISTP PROGRAMS)
          NIL
          (CONS (ICOMPILE-PROGRAM (CAR PROGRAMS))
                (ICOMPILE (CDR PROGRAMS)))))

(DEFN SEGMENT-LENGTH
      (SEGMENT)
      (IF (NLISTP SEGMENT)
          0
          (PLUS (LENGTH (CDAR SEGMENT))
                (SEGMENT-LENGTH (CDR SEGMENT)))))

(DEFN TOTAL-P-SYSTEM-SIZE (P LOAD-ADDR)
      (PLUS LOAD-ADDR
            (SEGMENT-LENGTH (P-DATA-SEGMENT P))
            (SEGMENT-LENGTH (ICOMPILE (P-PROG-SEGMENT P)))
            (ADD1 (P-MAX-CTRL-STK-SIZE P))
            (ADD1 (P-MAX-TEMP-STK-SIZE P))
            3))

(DEFN P-LOADABLEP (P LOAD-ADDR)
      (LESSP (TOTAL-P-SYSTEM-SIZE P LOAD-ADDR)
             (EXP 2 (P-WORD-SIZE P))))

(ADD-SHELL R-STATE NIL R-STATEP
           ((R-PC (NONE-OF) ZERO)
            (R-CFP (NONE-OF) ZERO)
            (R-CSP (NONE-OF) ZERO)
            (R-TSP (NONE-OF) ZERO)
            (R-X (NONE-OF) ZERO)
            (R-Y (NONE-OF) ZERO)
            (R-C-FLG (NONE-OF) ZERO)
            (R-V-FLG (NONE-OF) ZERO)
            (R-N-FLG (NONE-OF) ZERO)
            (R-Z-FLG (NONE-OF) ZERO)
            (R-PROG-SEGMENT (NONE-OF) ZERO)
            (R-USR-DATA-SEGMENT (NONE-OF) ZERO)
            (R-SYS-DATA-SEGMENT (NONE-OF) ZERO)
            (R-WORD-SIZE (NONE-OF) ZERO)
            (R-PSW (NONE-OF) ZERO)))

(DEFN NAT-0S
      (N)
      (IF (ZEROP N)
          NIL
          (CONS (TAG 'NAT 0)
                (NAT-0S (SUB1 N)))))

(DEFN P->R_TEMP-STK
      (TEMP-STK MAX-TEMP-STK-SIZE)
      (CONS 'TSTK
            (APPEND (NAT-0S (DIFFERENCE MAX-TEMP-STK-SIZE
                                        (LENGTH TEMP-STK)))
                    (APPEND TEMP-STK
                            (LIST (TAG 'NAT 0))))))

(DEFN P->R_CSP
      (STK MAX)
      (TAG 'SYS-ADDR
           (CONS 'CSTK
                 (DIFFERENCE MAX
                             (P-CTRL-STK-SIZE STK)))))

(DEFN P->R_CFP
      (STK MAX)
      (SUB-ADDR (P->R_CSP (POP STK) MAX) 2))

(DEFN P->R_P-FRAME
      (PFRAME STK MAX)
      (APPEND (STRIP-CDRS (BINDINGS PFRAME))
              (LIST (P->R_CFP STK MAX)
                    (RET-PC PFRAME))))

(DEFN P->R_CTRL-STK1
      (STK MAX)
      (IF (NLISTP STK)
          NIL
          (APPEND (P->R_P-FRAME (TOP STK) (POP STK) MAX)
                  (P->R_CTRL-STK1 (POP STK) MAX))))

(DEFN P->R_CTRL-STK
      (STK MAX)
      (CONS 'CSTK
            (APPEND (NAT-0S (DIFFERENCE MAX
                                        (P-CTRL-STK-SIZE STK)))
                    (APPEND (P->R_CTRL-STK1 STK MAX)
                            (LIST (TAG 'NAT 0))))))

(DEFN P->R_SYS-DATA-SEGMENT
      (CTRL-STK MAX-CTRL-STK-SIZE TEMP-STK MAX-TEMP-STK-SIZE)
      (LIST (P->R_CTRL-STK CTRL-STK MAX-CTRL-STK-SIZE)
            (P->R_TEMP-STK TEMP-STK MAX-TEMP-STK-SIZE)
            (LIST 'FULL-CTRL-STK-ADDR
                  (TAG 'SYS-ADDR '(CSTK . 0)))
            (LIST 'FULL-TEMP-STK-ADDR
                  (TAG 'SYS-ADDR '(TSTK . 0)))
            (LIST 'EMPTY-TEMP-STK-ADDR
                  (TAG 'SYS-ADDR
                       (CONS 'TSTK MAX-TEMP-STK-SIZE)))))

(DEFN P->R_TSP
      (STK MAX)
      (TAG 'SYS-ADDR
           (CONS 'TSTK
                 (DIFFERENCE MAX (LENGTH STK)))))

(DEFN P->R
      (P)
      (R-STATE (P-PC P)
               (P->R_CFP (P-CTRL-STK P)
                         (P-MAX-CTRL-STK-SIZE P))
               (P->R_CSP (P-CTRL-STK P)
                         (P-MAX-CTRL-STK-SIZE P))
               (P->R_TSP (P-TEMP-STK P)
                         (P-MAX-TEMP-STK-SIZE P))
               '(NAT 0)
               '(NAT 0)
               '(BOOL F)
               '(BOOL F)
               '(BOOL F)
               '(BOOL F)
               (P-PROG-SEGMENT P)
               (P-DATA-SEGMENT P)
               (P->R_SYS-DATA-SEGMENT (P-CTRL-STK P)
                                      (P-MAX-CTRL-STK-SIZE P)
                                      (P-TEMP-STK P)
                                      (P-MAX-TEMP-STK-SIZE P))
               (P-WORD-SIZE P)
               (P-PSW P)))

(ADD-SHELL I-STATE NIL I-STATEP
           ((I-PC (NONE-OF) ZERO)
            (I-CFP (NONE-OF) ZERO)
            (I-CSP (NONE-OF) ZERO)
            (I-TSP (NONE-OF) ZERO)
            (I-X (NONE-OF) ZERO)
            (I-Y (NONE-OF) ZERO)
            (I-C-FLG (NONE-OF) ZERO)
            (I-V-FLG (NONE-OF) ZERO)
            (I-N-FLG (NONE-OF) ZERO)
            (I-Z-FLG (NONE-OF) ZERO)
            (I-PROG-SEGMENT (NONE-OF) ZERO)
            (I-USR-DATA-SEGMENT (NONE-OF) ZERO)
            (I-SYS-DATA-SEGMENT (NONE-OF) ZERO)
            (I-WORD-SIZE (NONE-OF) ZERO)
            (I-PSW (NONE-OF) ZERO)))

(DEFN R->I_PC
      (PC PROGRAMS)
      (TAG 'IPC
           (CONS (AREA-NAME PC)
                 (FIND-LABEL (UNTAG PC)
                             (CDR (ICOMPILE-PROGRAM (DEFINITION (AREA-NAME PC)
                                                                PROGRAMS)))))))

(DEFN R->I_PSW
      (PSW)
      (IF (EQUAL PSW 'HALT) 'RUN PSW))

(DEFN R->I
      (R)
      (I-STATE (R->I_PC (R-PC R) (R-PROG-SEGMENT R))
               (R-CFP R)
               (R-CSP R)
               (R-TSP R)
               (R-X R)
               (R-Y R)
               (R-C-FLG R)
               (R-V-FLG R)
               (R-N-FLG R)
               (R-Z-FLG R)
               (ICOMPILE (R-PROG-SEGMENT R))
               (R-USR-DATA-SEGMENT R)
               (R-SYS-DATA-SEGMENT R)
               (R-WORD-SIZE R)
               (R->I_PSW (R-PSW R))))

(ADD-SHELL M-STATE NIL M-STATEP
           ((M-REGS (NONE-OF) ZERO)
            (M-C-FLG (NONE-OF) ZERO)
            (M-V-FLG (NONE-OF) ZERO)
            (M-N-FLG (NONE-OF) ZERO)
            (M-Z-FLG (NONE-OF) ZERO)
            (M-MEM (NONE-OF) ZERO)))

(DEFN LINK-TABLE-FOR-SEGMENT (SEGMENT ADDR0)
      (IF (NLISTP SEGMENT)
          NIL
          (CONS (CONS (CAAR SEGMENT) ADDR0)
                (LINK-TABLE-FOR-SEGMENT (CDR SEGMENT)
                                        (PLUS ADDR0
                                              (LENGTH (CDAR SEGMENT)))))))

(DEFN LINK-TABLE-FOR-LABELS
      (LST ADDR0)
      (COND ((NLISTP LST) NIL)
            ((LABELLEDP (CAR LST))
             (CONS (CONS (CADAR LST) ADDR0)
                   (LINK-TABLE-FOR-LABELS (CDR LST)
                                          (ADD1 ADDR0))))
            (T (LINK-TABLE-FOR-LABELS (CDR LST)
                                      (ADD1 ADDR0)))))

(DEFN LINK-TABLE-FOR-PROG-LABELS
      (SEGMENT ADDR0)
      (IF (NLISTP SEGMENT)
          NIL
          (CONS (CONS (CAAR SEGMENT)
                      (LINK-TABLE-FOR-LABELS (CDAR SEGMENT)
                                             ADDR0))
                (LINK-TABLE-FOR-PROG-LABELS (CDR SEGMENT)
                                            (PLUS ADDR0
                                                  (LENGTH (CDAR SEGMENT)))))))

(DEFN I-LINK-TABLES (I LOAD-ADDR)
  (LIST
   (LINK-TABLE-FOR-SEGMENT (I-PROG-SEGMENT I)
                           (PLUS LOAD-ADDR
                                 (SEGMENT-LENGTH (I-USR-DATA-SEGMENT I))))
   (LINK-TABLE-FOR-PROG-LABELS (I-PROG-SEGMENT I)
                               (PLUS LOAD-ADDR
                                     (SEGMENT-LENGTH (I-USR-DATA-SEGMENT I))))
   (LINK-TABLE-FOR-SEGMENT (I-USR-DATA-SEGMENT I)
                           LOAD-ADDR)
   (LINK-TABLE-FOR-SEGMENT (I-SYS-DATA-SEGMENT I)
                           (PLUS LOAD-ADDR
                                 (SEGMENT-LENGTH (I-PROG-SEGMENT I))
                                 (SEGMENT-LENGTH (I-USR-DATA-SEGMENT I))))))

(DEFN PROG-LINKS
      (LINK-TABLES)
      (CAR LINK-TABLES))

(DEFN PROG-LABEL-TABLES
      (LINK-TABLES)
      (CADR LINK-TABLES))

(DEFN USR-DATA-LINKS
      (LINK-TABLES)
      (CADDR LINK-TABLES))

(DEFN SYS-DATA-LINKS
      (LINK-TABLES)
      (CADDDR LINK-TABLES))

(DEFN LABEL-LINKS
      (LABEL PROG-LABEL-TABLES)
      (CDR (ASSOC (ADP-NAME LABEL)
                  PROG-LABEL-TABLES)))

(DEFN BASE-ADDRESS
      (NAME LINK-TABLE)
      (CDR (ASSOC NAME LINK-TABLE)))

(DEFN FIND-CONTAINING-AREA-NAME
      (N LINK-TABLE)
      (COND ((NLISTP LINK-TABLE) 0)
            ((NLISTP (CDR LINK-TABLE))
             (CAAR LINK-TABLE))
            ((AND (NOT (LESSP N (CDAR LINK-TABLE)))
                  (LESSP N (CDADR LINK-TABLE)))
             (CAAR LINK-TABLE))
            (T (FIND-CONTAINING-AREA-NAME N
                                          (CDR LINK-TABLE)))))

(DEFN INVERT-BASE-ADDRESS
      (N LINK-TABLE)
      (FIND-CONTAINING-AREA-NAME N LINK-TABLE))

(DEFN LABEL-ADDRESS
      (LABEL PROG-LABEL-TABLES)
      (BASE-ADDRESS LABEL
                    (LABEL-LINKS LABEL PROG-LABEL-TABLES)))

(DEFN ASSOC-CDRP
      (N ALIST)
      (COND ((NLISTP ALIST) F)
            ((EQUAL N (CDAR ALIST)) T)
            (T (ASSOC-CDRP N (CDR ALIST)))))

(DEFN FIND-CONTAINING-LABEL-TABLE
      (N LABEL-TABLES)
      (COND ((NLISTP LABEL-TABLES) F)
            ((ASSOC-CDRP N (CDAR LABEL-TABLES))
             (CDAR LABEL-TABLES))
            (T (FIND-CONTAINING-LABEL-TABLE N
                                            (CDR LABEL-TABLES)))))

(DEFN INVERT-LABEL-ADDRESS
      (N PROG-LABEL-TABLES)
      (INVERT-BASE-ADDRESS N
                           (FIND-CONTAINING-LABEL-TABLE N PROG-LABEL-TABLES)))

(DEFN ABSOLUTE-ADDRESS
      (ADP LINK-TABLE)
      (PLUS (BASE-ADDRESS (ADP-NAME ADP)
                          LINK-TABLE)
            (ADP-OFFSET ADP)))

(DEFN INVERT-ABSOLUTE-ADDRESS
      (N LINK-TABLE)
      (CONS (FIND-CONTAINING-AREA-NAME N LINK-TABLE)
            (DIFFERENCE N
                        (BASE-ADDRESS (FIND-CONTAINING-AREA-NAME N LINK-TABLE)
                                      LINK-TABLE))))

(DEFN BITV-TO-V (LST WORD-SIZE)
  (IF (ZEROP WORD-SIZE)
      NIL
      (APPEND (BITV-TO-V (CDR LST)
                         (SUB1 WORD-SIZE))
              (LIST (IF (EQUAL (CAR LST) 0) F T)))))

(DEFN V-TO-BITV (V)
      (IF (NLISTP V)
          NIL
          (APPEND (V-TO-BITV (CDR V))
                  (LIST (IF (CAR V) 1 0)))))

(DEFN BOOL-TO-V
      (B WORD-SIZE)
      (IF (EQUAL B 'F)
          (NAT-TO-V 0 WORD-SIZE)
          (NAT-TO-V 1 WORD-SIZE)))

(DEFN V-TO-BOOL (V)
  (IF (CAR V) 'T 'F))

(DEFN ADDR-TO-V
      (ADP USR-DATA-LINKS WORD-SIZE)
      (NAT-TO-V (ABSOLUTE-ADDRESS ADP USR-DATA-LINKS)
                 WORD-SIZE))

(DEFN V-TO-ADDR
      (V USR-DATA-LINKS)
      (INVERT-ABSOLUTE-ADDRESS (V-TO-NAT V)
                               USR-DATA-LINKS))

(DEFN SUBR-TO-V
      (SUBR PROG-LINKS WORD-SIZE)
      (NAT-TO-V (BASE-ADDRESS SUBR PROG-LINKS)
                 WORD-SIZE))

(DEFN V-TO-SUBR
      (V PROG-LINKS)
      (INVERT-BASE-ADDRESS (V-TO-NAT V)
                           PROG-LINKS))

(DEFN SYS-ADDR-TO-V
      (ADP SYS-DATA-LINKS WORD-SIZE)
      (NAT-TO-V (ABSOLUTE-ADDRESS ADP SYS-DATA-LINKS)
                 WORD-SIZE))

(DEFN V-TO-SYS-ADDR
      (V SYS-DATA-LINKS)
      (INVERT-ABSOLUTE-ADDRESS (V-TO-NAT V)
                               SYS-DATA-LINKS))

(DEFN LABEL-TO-V
      (ILAB PROG-LABEL-TABLES WORD-SIZE)
      (NAT-TO-V (LABEL-ADDRESS ILAB PROG-LABEL-TABLES)
                 WORD-SIZE))

(DEFN V-TO-LABEL
      (V PROG-LABEL-TABLES)
      (INVERT-LABEL-ADDRESS (V-TO-NAT V)
                            PROG-LABEL-TABLES))

(DEFN IPC-TO-V
      (PCPP PROG-LINKS WORD-SIZE)
      (NAT-TO-V (ABSOLUTE-ADDRESS PCPP PROG-LINKS)
                 WORD-SIZE))

(DEFN LINK-DATA-WORD
      (X LINK-TABLES WORD-SIZE)
      (CASE (TYPE X)
            (NAT (NAT-TO-V (UNTAG X) WORD-SIZE))
            (INT (INT-TO-V (UNTAG X) WORD-SIZE))
            (BITV (BITV-TO-V (UNTAG X) WORD-SIZE))
            (BOOL (BOOL-TO-V (UNTAG X) WORD-SIZE))
            (ADDR (ADDR-TO-V (UNTAG X)
                              (USR-DATA-LINKS LINK-TABLES)
                              WORD-SIZE))
            (SUBR (SUBR-TO-V (UNTAG X)
                              (PROG-LINKS LINK-TABLES)
                              WORD-SIZE))
            (SYS-ADDR (SYS-ADDR-TO-V (UNTAG X)
                                      (SYS-DATA-LINKS LINK-TABLES)
                                      WORD-SIZE))
            (PC (LABEL-TO-V (UNTAG X)
                             (PROG-LABEL-TABLES LINK-TABLES)
                             WORD-SIZE))
            (IPC (IPC-TO-V (UNTAG X)
                            (PROG-LINKS LINK-TABLES)
                            WORD-SIZE))
            (OTHERWISE (NAT-TO-V 0 WORD-SIZE))))

(DEFN UNLINK-DATA-WORD
      (TYPE V LINK-TABLES)
      (CASE TYPE
            (NAT (TAG 'NAT (V-TO-NAT V)))
            (INT (TAG 'INT (V-TO-INT V)))
            (BITV (TAG 'BITV (V-TO-BITV V)))
            (BOOL (TAG 'BOOL (V-TO-BOOL V)))
            (ADDR (TAG 'ADDR
                       (V-TO-ADDR V
                                   (USR-DATA-LINKS LINK-TABLES))))
            (SUBR (TAG 'SUBR
                       (V-TO-SUBR V
                                   (PROG-LINKS LINK-TABLES))))
            (SYS-ADDR (TAG 'SYS-ADDR
                           (V-TO-SYS-ADDR V
                                           (SYS-DATA-LINKS LINK-TABLES))))
            (PC (TAG 'PC
                     (V-TO-LABEL V
                                  (PROG-LABEL-TABLES LINK-TABLES))))
            (OTHERWISE '(UNRECOGNIZED I-LEVEL TYPE))))

(DEFN LINK-INSTRUCTION-ALIST
      NIL
      '((ADD_<C>_X_X{N} (ADD (C) X X))
        (ADD_<TSP>_<TSP>{V} (ADD NIL (TSP) (TSP)))
        (ADD_<TSP>_<TSP>{N} (ADD NIL (TSP) (TSP)))
        (ADD_<TSP>{A}_X{N} (ADD NIL (TSP) X))
        (ADD_TSP_*{N} (ADD NIL TSP (PC 1)))
        (ADD_TSP_X{N} (ADD NIL TSP X))
        (ADD_<TSP>{I}_X{I} (ADD NIL (TSP) X))
        (ADD_<TSP>{N}_X{N} (ADD NIL (TSP) X))
        (ADD_PC_X{N} (ADD NIL PC X))
        (ADD_X_X{N} (ADD NIL X X))
        (ADD_X{N}_CSP (ADD NIL X CSP))
        (ADDC_<C>_X{N}_Y{N} (ADDC (C) X Y))
        (ADDC_<V>_X{I}_Y{I} (ADDC (V) X Y))
        (AND_<TSP>{V}_X{V} (AND NIL (TSP) X))
        (AND_<TSP>{B}_X{B} (AND NIL (TSP) X))
        (ASR_<C>_<TSP>_<TSP>{B} (ASR (C) (TSP) (TSP)))
        (CPOP_CFP (MOVE NIL CFP (CSP 1)))
        (CPOP_PC (MOVE NIL PC (CSP 1)))
        (CPUSH_* (MOVE NIL (-1 CSP) (PC 1)))
        (CPUSH_<TSP>+ (MOVE NIL (-1 CSP) (TSP 1)))
        (CPUSH_CFP (MOVE NIL (-1 CSP) CFP))
        (DECR_<TSP>_<TSP>{I} (DECR NIL (TSP) (TSP)))
        (DECR_<TSP>_<TSP>{N} (DECR NIL (TSP) (TSP)))
        (INCR_<TSP>_<TSP>{I} (INCR NIL (TSP) (TSP)))
        (INCR_<TSP>_<TSP>{N} (INCR NIL (TSP) (TSP)))
        (INCR_Y_Y{N} (INCR NIL Y Y))
        (INT-TO-NAT (MOVE NIL X X))
        (JUMP-N_X (MOVE-N NIL PC X))
        (JUMP-NN_X (MOVE-NN NIL PC X))
        (JUMP-NZ_X (MOVE-NZ NIL PC X))
        (JUMP-Z_X (MOVE-Z NIL PC X))
        (JUMP_* (MOVE NIL PC (PC)))
        (JUMP_X{SUBR} (MOVE NIL PC X))
        (LSR_<C>_X_X{N} (LSR (C) X X))
        (LSR_<TSP>_<TSP>{V} (LSR NIL (TSP) (TSP)))
        (MOVE-C_<TSP>_* (MOVE-C NIL (TSP) (PC 1)))
        (MOVE-V_<TSP>_* (MOVE-V NIL (TSP) (PC 1)))
        (MOVE-Z_<TSP>_* (MOVE-Z NIL (TSP) (PC 1)))
        (MOVE-N_X_* (MOVE-N NIL X (PC 1)))
        (MOVE_<TSP>_* (MOVE NIL (TSP) (PC 1)))
        (MOVE_<X{A}>_<TSP> (MOVE NIL (X) (TSP)))
        (MOVE_<X{S}>_<TSP> (MOVE NIL (X) (TSP)))
        (MOVE_CFP_CSP (MOVE NIL CFP CSP))
        (MOVE_CSP_CFP (MOVE NIL CSP CFP))
        (MOVE_X_* (MOVE NIL X (PC 1)))
        (MOVE_X_<X{S}> (MOVE NIL X (X)))
        (MOVE_X_TSP (MOVE NIL X TSP))
        (MOVE_X_X (MOVE NIL X X))
        (MOVE_Y_* (MOVE NIL Y (PC 1)))
        (MOVE_Y_<Y{S}> (MOVE NIL Y (Y)))
        (MOVE_Y_TSP (MOVE NIL Y TSP))
        (NEG_<TSP>_<TSP>{I} (NEG NIL (TSP) (TSP)))
        (NOT_<TSP>_<TSP>{V} (NOT NIL (TSP) (TSP)))
        (OR_<TSP>{V}_X{V} (OR NIL (TSP) X))
        (OR_<TSP>{B}_X{B} (OR NIL (TSP) X))
        (SUB_<C>_<TSP>{A}_X{A} (SUB (C) (TSP) X))
        (SUB_<C>_<TSP>{N}_X{N} (SUB (C) (TSP) X))
        (SUB_<NV>_<TSP>{I}_X{I} (SUB (N V) (TSP) X))
        (SUB_<TSP>{A}_X{N} (SUB NIL (TSP) X))
        (SUB_X{S}_Y{N} (SUB NIL X Y))
        (SUB_<TSP>{I}_X{I} (SUB NIL (TSP) X))
        (SUB_<TSP>{N}_X{N} (SUB NIL (TSP) X))
        (SUB_<TSP>{S}_X{S} (SUB NIL (TSP) X))
        (SUB_<Z>_X{S}_Y{S} (SUB (Z) X Y))
        (SUBB_<C>_X{N}_Y{N} (SUBB (C) X Y))
        (SUBB_<V>_X{I}_Y{I} (SUBB (V) X Y))
        (TPOP_<C>_X (MOVE (C) X (TSP 1)))
        (TPOP_<X{A}> (MOVE NIL (X) (TSP 1)))
        (TPOP_<X{S}> (MOVE NIL (X) (TSP 1)))
        (TPOP_PC (MOVE NIL PC (TSP 1)))
        (TPOP_X (MOVE NIL X (TSP 1)))
        (TPOP_Y (MOVE NIL Y (TSP 1)))
        (TPOP{V}_<Z>_Y (MOVE (Z) Y (TSP 1)))
        (TPOP{B}_<Z>_Y (MOVE (Z) Y (TSP 1)))
        (TPOP{I}_<ZN>_Y (MOVE (Z N) Y (TSP 1)))
        (TPOP{N}_<Z>_Y (MOVE (Z) Y (TSP 1)))
        (TPUSH_* (MOVE NIL (-1 TSP) (PC 1)))
        (TPUSH_<X{A}> (MOVE NIL (-1 TSP) (X)))
        (TPUSH_<X{S}> (MOVE NIL (-1 TSP) (X)))
        (TPUSH_CSP (MOVE NIL (-1 TSP) CSP))
        (TPUSH_TSP (MOVE NIL (-1 TSP) TSP))
        (TPUSH_X (MOVE NIL (-1 TSP) X))
        (XOR_<TSP>_<TSP> (XOR NIL (TSP) (TSP)))
        (XOR_<TSP>{V}_X{V} (XOR NIL (TSP) X))
        (XOR_<TSP>{B}_*{B} (XOR NIL (TSP) (PC 1)))
        (XOR_<TSP>{B}_X{B} (XOR NIL (TSP) X))
        (XOR_<Z>_<TSP>_X (XOR (Z) (TSP) X))))

(DEFN PACK-INSTRUCTION
      (OP MOVE-BITS CVNZ MODE-B REG-B MODE-A REG-A WORD-SIZE)
      (NAT-TO-V (PLUS (TIMES OP (EXP 2 24))
                      (TIMES MOVE-BITS (EXP 2 20))
                      (TIMES CVNZ (EXP 2 16))
                      (TIMES MODE-B (EXP 2 14))
                      (TIMES REG-B (EXP 2 10))
;                     (TIMES 0000 (EXP 2 6))
                      (TIMES MODE-A (EXP 2 4))
                      REG-A)
                 WORD-SIZE))

(DEFN EXTRACT-OP
      (OPCODE)
      (CADR (ASSOC OPCODE
                   '((INCR 1)
                     (ADDC 2)
                     (ADD 3)
                     (NEG 4)
                     (DECR 5)
                     (SUBB 6)
                     (SUB 7)
                     (ROR 8)
                     (ASR 9)
                     (LSR 10)
                     (XOR 11)
                     (OR 12)
                     (AND 13)
                     (NOT 14)
                     (MOVE 15)
                     (MOVE-NC 15)
                     (MOVE-C 15)
                     (MOVE-NV 15)
                     (MOVE-V 15)
                     (MOVE-NZ 15)
                     (MOVE-Z 15)
                     (MOVE-NN 15)
                     (MOVE-N 15)))))

(DEFN EXTRACT-MOVE-BITS (OPCODE)
  (CASE OPCODE
        (MOVE 14)
        (MOVE-NC 0)
        (MOVE-C 1)
        (MOVE-NV 2)
        (MOVE-V 3)
        (MOVE-NZ 6)
        (MOVE-Z 7)
        (MOVE-NN 4)
        (MOVE-N 5)
        (OTHERWISE 14)))

(DEFN EXTRACT-MODE
      (REG-SPEC)
      (COND ((LITATOM REG-SPEC) 0)
            ((EQUAL (CDR REG-SPEC) NIL) 1)
            ((EQUAL (CAR REG-SPEC) -1) 2)
            (T 3)))

(DEFN EXTRACT-CVNZ
      (FLG-NAMES)
      (PLUS (TIMES (IF (MEMBER 'C FLG-NAMES) 1 0)
                   (EXP 2 3))
            (TIMES (IF (MEMBER 'V FLG-NAMES) 1 0)
                   (EXP 2 2))
            (TIMES (IF (MEMBER 'N FLG-NAMES) 1 0)
                   (EXP 2 1))
            (TIMES (IF (MEMBER 'Z FLG-NAMES) 1 0)
                   (EXP 2 0))))

(DEFN EXTRACT-REG1
      (REG-SPEC)
      (COND ((LITATOM REG-SPEC) REG-SPEC)
            ((EQUAL (CDR REG-SPEC) NIL)
             (CAR REG-SPEC))
            ((EQUAL (CAR REG-SPEC) -1)
             (CADR REG-SPEC))
            (T (CAR REG-SPEC))))

(DEFN EXTRACT-REG
      (REG-SPEC)
      (CADR (ASSOC (EXTRACT-REG1 REG-SPEC)
                   '((PC 15)
                     (CFP 1)
                     (CSP 2)
                     (TSP 3)
                     (X 4)
                     (Y 5)))))

(DEFN MCI
      (INS WORD-SIZE)
      (PACK-INSTRUCTION (EXTRACT-OP (CAR INS))
                        (EXTRACT-MOVE-BITS (CAR INS))
                        (EXTRACT-CVNZ (CADR INS))
                        (EXTRACT-MODE (CADDR INS))
                        (EXTRACT-REG (CADDR INS))
                        (EXTRACT-MODE (CADDDR INS))
                        (EXTRACT-REG (CADDDR INS))
                        WORD-SIZE))

(DEFN ICODE-INSTRUCTIONP
      (INS)
      (EQUAL (CDR INS) NIL))

(DEFN LINK-INSTR-WORD
      (INS WORD-SIZE)
      (MCI (CADR (ASSOC (CAR INS)
                        (LINK-INSTRUCTION-ALIST)))
           WORD-SIZE))

(DEFN LINK-WORD
      (X LINK-TABLES WORD-SIZE)
      (IF (ICODE-INSTRUCTIONP X)
          (LINK-INSTR-WORD X WORD-SIZE)
          (LINK-DATA-WORD X LINK-TABLES WORD-SIZE)))

(DEFN LINK-AREA
      (LST LINK-TABLES WORD-SIZE)
      (IF (NLISTP LST)
          NIL
          (CONS (LINK-WORD (UNLABEL (CAR LST))
                           LINK-TABLES WORD-SIZE)
                (LINK-AREA (CDR LST)
                           LINK-TABLES WORD-SIZE))))

(DEFN LINK-SEGMENT
      (SEGMENT LINK-TABLES WORD-SIZE)
      (IF (NLISTP SEGMENT)
          NIL
          (APPEND (LINK-AREA (CDAR SEGMENT)
                             LINK-TABLES WORD-SIZE)
                  (LINK-SEGMENT (CDR SEGMENT)
                                LINK-TABLES WORD-SIZE))))

(defn boot-code (lst n word-size)
  (if (zerop n)
      nil
      (cons (nat-to-v (car lst) word-size)
            (boot-code (cdr lst) (sub1 n) word-size))))

(DEFN LINK-MEM (boot-lst LOAD-ADDR USR-DATA-SEGMENT PROG-SEGMENT SYS-DATA-SEGMENT
                         LINK-TABLES WORD-SIZE)
  (append
   (boot-code boot-lst load-addr word-size)
   (APPEND (LINK-SEGMENT USR-DATA-SEGMENT LINK-TABLES WORD-SIZE)
           (APPEND (LINK-SEGMENT PROG-SEGMENT LINK-TABLES WORD-SIZE)
                   (LINK-SEGMENT SYS-DATA-SEGMENT LINK-TABLES WORD-SIZE)))))

(DEFN BOOL-TO-LOGICAL
      (B)
      (IF (EQUAL B 'F) F T))

(DEFN I->M (I BOOT-LST LOAD-ADDR)
  (LET ((TABLES (I-LINK-TABLES I LOAD-ADDR))
        (W (I-WORD-SIZE I)))
  (M-STATE (LIST (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD (I-CFP I) TABLES W)
                 (LINK-WORD (I-CSP I) TABLES W)
                 (LINK-WORD (I-TSP I) TABLES W)
                 (LINK-WORD (I-X I) TABLES W)
                 (LINK-WORD (I-Y I) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD '(NAT 0) TABLES W)
                 (LINK-WORD (I-PC I) TABLES W))
           (BOOL-TO-LOGICAL (UNTAG (I-C-FLG I)))
           (BOOL-TO-LOGICAL (UNTAG (I-V-FLG I)))
           (BOOL-TO-LOGICAL (UNTAG (I-N-FLG I)))
           (BOOL-TO-LOGICAL (UNTAG (I-Z-FLG I)))
           (LINK-MEM BOOT-LST
                     LOAD-ADDR
                     (I-USR-DATA-SEGMENT I)
                     (I-PROG-SEGMENT I)
                     (I-SYS-DATA-SEGMENT I)
                     TABLES
                     W))))

(PROVE-LEMMA MY-LESSP-QUOTIENT (REWRITE)
             (IMPLIES (AND (NUMBERP SIZE)
                           (NOT (EQUAL SIZE 0)))
                      (LESSP (QUOTIENT SIZE 2) SIZE)))

(DEFN RAM-TREE (LST SIZE)
  (COND ((ZEROP SIZE) (STUB (NAT-TO-V 0 32)))   ; never happens
        ((NLISTP LST) (STUB (NAT-TO-V 0 32)))
        ((EQUAL SIZE 1) (RAM (CAR LST)))
        (T (CONS (RAM-TREE (FIRSTN (QUOTIENT SIZE 2) LST) (QUOTIENT SIZE 2))
                 (RAM-TREE (RESTN (QUOTIENT SIZE 2) LST)  (QUOTIENT SIZE 2)))))
  ((LESSP (COUNT SIZE))))

(DEFN FM-STATE (REGS C V N Z MEM)
  (LIST (LIST (RAM-TREE REGS 16)
              (LIST Z N V C))
        (RAM-TREE MEM (EXP 2 32))))

(DEFN M->FM9001 (M)
  (LIST (LIST (RAM-TREE (M-REGS M) 16)
              (LIST (M-Z-FLG M)
                    (M-N-FLG M)
                    (M-V-FLG M)
                    (M-C-FLG M)))
        (RAM-TREE (M-MEM M) (EXP 2 32))))

(DEFN LOAD (P boot-lst LOAD-ADDR) (M->FM9001 (I->M (R->I (P->R P)) boot-lst LOAD-ADDR)))

(DEFN LINK-TABLES (P LOAD-ADDR)
      (I-LINK-TABLES (R->I (P->R P)) LOAD-ADDR))

(DEFN TYPE-LST
      (LST)
      (IF (NLISTP LST)
          NIL
          (CONS (TYPE (CAR LST))
                (TYPE-LST (CDR LST)))))

(DEFN AREA-TYPE-SPECIFICATION
      (AREA)
      (CONS (CAR AREA)
            (TYPE-LST (CDR AREA))))

(DEFN TYPE-SPECIFICATION
      (SEGMENT)
      (IF (NLISTP SEGMENT)
          NIL
          (CONS (AREA-TYPE-SPECIFICATION (CAR SEGMENT))
                (TYPE-SPECIFICATION (CDR SEGMENT)))))

(DEFN DISPLAY-FM9001-ARRAY (TYPE-LST N FM-MEM LINK-TABLES)
  (IF (NLISTP TYPE-LST)
      NIL
      (CONS (UNLINK-DATA-WORD (CAR TYPE-LST)
                              (READ-MEM (NAT-TO-V N 32) FM-MEM)
                              LINK-TABLES)
            (DISPLAY-FM9001-ARRAY (CDR TYPE-LST)
                                  (ADD1 N)
                                  FM-MEM LINK-TABLES))))

(DEFN DISPLAY-FM9001-DATA-AREA (AREA-TYPE-SPEC FM-MEM LINK-TABLES)
  (CONS (CAR AREA-TYPE-SPEC)
        (DISPLAY-FM9001-ARRAY (CDR AREA-TYPE-SPEC)
                              (BASE-ADDRESS (CAR AREA-TYPE-SPEC)
                                            (USR-DATA-LINKS LINK-TABLES))
                              FM-MEM LINK-TABLES)))

(DEFN DISPLAY-FM9001-DATA-SEGMENT1 (TYPE-SPEC FM-MEM LINK-TABLES)
  (IF (NLISTP TYPE-SPEC)
      NIL
      (CONS (DISPLAY-FM9001-DATA-AREA (CAR TYPE-SPEC) FM-MEM LINK-TABLES)
            (DISPLAY-FM9001-DATA-SEGMENT1 (CDR TYPE-SPEC) FM-MEM LINK-TABLES))))

(DEFN DISPLAY-FM9001-DATA-SEGMENT (FM-STATE TYPE-SPEC LINK-TABLES)
      (DISPLAY-FM9001-DATA-SEGMENT1 TYPE-SPEC
                                    (CADR FM-STATE)
                                    LINK-TABLES))

; Book:  m.events.  Now we define the m machine.

(DEFN V-NTH1 (V-N LST)
  (IF (LESSP (V-TO-NAT V-N) (LENGTH LST))
      (NTH (V-TO-NAT V-N) LST)
      (NAT-TO-V 0 32)))

(DEFN CURRENT-INSTRUCTION (REGS MEM)
  (V-NTH1 (V-NTH1 (NAT-TO-V 15 4) REGS) MEM))

(DEFN M-STORE-RESULTP (STORE-CC C V N Z)
  (CASE STORE-CC
        ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE)
         (NOT C))
        ((*1*TRUE *1*FALSE *1*FALSE *1*FALSE)
         C)
        ((*1*FALSE *1*TRUE *1*FALSE *1*FALSE)
         (NOT V))
        ((*1*TRUE *1*TRUE *1*FALSE *1*FALSE)
         V)
        ((*1*FALSE *1*FALSE *1*TRUE *1*FALSE)
         (NOT N))
        ((*1*TRUE *1*FALSE *1*TRUE *1*FALSE)
         N)
        ((*1*FALSE *1*TRUE *1*TRUE *1*FALSE)
         (NOT Z))
        ((*1*TRUE *1*TRUE *1*TRUE *1*FALSE)
         Z)
        ((*1*FALSE *1*FALSE *1*FALSE *1*TRUE)
         (AND (NOT C)
              (NOT Z)))
        ((*1*TRUE *1*FALSE *1*FALSE *1*TRUE)
         (OR C Z))
        ((*1*FALSE *1*TRUE *1*FALSE *1*TRUE)
         (OR (AND N V)
             (AND (NOT N)
                  (NOT V))))
        ((*1*TRUE *1*TRUE *1*FALSE *1*TRUE)
         (OR (AND N
                  (NOT V))
             (AND (NOT N)
                  V)))
        ((*1*FALSE *1*FALSE *1*TRUE *1*TRUE)
         (OR (AND N
                  V
                  (NOT Z))
             (AND (NOT N)
                  (NOT V)
                  (NOT Z))))
        ((*1*TRUE *1*FALSE *1*TRUE *1*TRUE)
         (OR Z
             (AND N
                  (NOT V))
             (AND (NOT N)
                  V)))
        ((*1*FALSE *1*TRUE *1*TRUE *1*TRUE) T)
        (OTHERWISE F)))

(PROVE-LEMMA M-STORE-RESULTP-IS-STORE-RESULTP (REWRITE)
  (EQUAL (M-STORE-RESULTP STORE-CC C V N Z)
         (STORE-RESULTP STORE-CC (LIST Z N V C))))

(DISABLE M-STORE-RESULTP)
(DISABLE STORE-RESULTP)

(DEFN M-ALU-OPERATION (REGS C V N Z MEM INS OPERAND-A OPERAND-B B-ADDRESS)
  (M-STATE (IF (AND (M-STORE-RESULTP (STORE-CC INS) C V N Z)
                      (REG-DIRECT-P (MODE-B INS)))
                (UPDATE-V-NTH (RN-B INS)
                              REGS
                              (BV (V-ALU C
                                         OPERAND-A OPERAND-B
                                         (OP-CODE INS))))
                REGS)
           (B-IF (C-SET (SET-FLAGS INS))
                 (C (V-ALU C
                           OPERAND-A OPERAND-B
                           (OP-CODE INS)))
                 C)
           (B-IF (V-SET (SET-FLAGS INS))
                 (V (V-ALU C
                           OPERAND-A OPERAND-B
                           (OP-CODE INS)))
                 V)
           (B-IF (N-SET (SET-FLAGS INS))
                 (N (V-ALU C
                           OPERAND-A OPERAND-B
                           (OP-CODE INS)))
                 N)
           (B-IF (Z-SET (SET-FLAGS INS))
                 (ZB (V-ALU C
                            OPERAND-A OPERAND-B
                            (OP-CODE INS)))
                 Z)
           (IF (AND (M-STORE-RESULTP (STORE-CC INS) C V N Z)
                      (NOT (REG-DIRECT-P (MODE-B INS))))
                (UPDATE-V-NTH B-ADDRESS MEM
                              (BV (V-ALU C
                                         OPERAND-A OPERAND-B
                                         (OP-CODE INS))))
                MEM)))

(DEFN READ-MEM1-RAM-TREE-HINT (RADDR LST)
  (COND ((NLISTP RADDR) T)
        ((CAR RADDR)
         (READ-MEM1-RAM-TREE-HINT (CDR RADDR)
                                  (RESTN (EXP 2 (LENGTH (CDR RADDR))) LST)))
        (T (READ-MEM1-RAM-TREE-HINT (CDR RADDR)
                                    (FIRSTN (EXP 2 (LENGTH (CDR RADDR))) LST)))))

(DEFN REV (X)
  (IF (NLISTP X)
      NIL
      (APPEND (REV (CDR X)) (LIST (CAR X)))))

(ENABLE APPEND)

(PROVE-LEMMA REV1-IS-REV (REWRITE)
  (EQUAL (REV1 X A) (APPEND (REV X) A)))

(PROVE-LEMMA APPEND-NIL (REWRITE)
  (IMPLIES (PROPERP X) (EQUAL (APPEND X NIL) X)))

(PROVE-LEMMA PROPERP-REV (REWRITE) (PROPERP (REV X)))

(PROVE-LEMMA READ-MEM1-REV-RAM-TREE-LEMMA1 (REWRITE)
  (IMPLIES (STUBP (RAM-TREE LST N))
           (EQUAL (STUB-GUTS (RAM-TREE LST N)) (NAT-TO-V 0 32))))

(ENABLE PLUS-0)
(ENABLE PLUS-ADD1-SUB1)
(ENABLE PLUS-ADD1)
(enable ASSOCIATIVITY-OF-PLUS)
(enable commutativity-of-plus)
(ENABLE TIMES-COMMUTES)
(ENABLE TIMES-ADD1-AGAIN)
(ENABLE TIMES-1)
(enable times-distributes-over-plus)
(enable ASSOCIATIVITY-OF-TIMES)


(PROVE-LEMMA MY-V-TO-NAT-APPEND (REWRITE)
  (EQUAL (V-TO-NAT (APPEND A B))
         (PLUS (V-TO-NAT A) (TIMES (EXP 2 (LENGTH A)) (V-TO-NAT B)))))

(ENABLE PLUS)

(ENABLE DIFFERENCE)

(PROVE-LEMMA DIFFERENCE-ADD1-ADD1-X-2 (REWRITE)
  (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2) (FIX X)))

(enable QUOTIENT-PLUS-X-X-2)

(ENABLE LENGTH-FIRSTN)

(ENABLE LENGTH-RESTN)

(PROVE-LEMMA my-LESSP-V-TO-NAT-EXP (REWRITE)
  (IMPLIES (EQUAL N (LENGTH V))
           (LESSP (V-TO-NAT V) (EXP 2 N))))

(PROVE-LEMMA LENGTH-REV (REWRITE) (EQUAL (LENGTH (REV X)) (LENGTH X)))

(PROVE-LEMMA NTH-FIRSTN (REWRITE)
  (IMPLIES (LESSP I N)
           (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST))))

(PROVE-LEMMA LESSP-DIFFERENCE (REWRITE)
  (EQUAL (LESSP V (DIFFERENCE L E))
         (IF (LESSP E L)
             (LESSP (PLUS E V) L)
             F)))

(PROVE-LEMMA NTH-RESTN-PLUS (REWRITE)
  (IMPLIES (LESSP I (LENGTH LST))
           (EQUAL (NTH N
                       (RESTN I LST))
                  (NTH (PLUS I N)
                       LST))))

(PROVE-LEMMA READ-MEM1-REV-RAM-TREE NIL
  (IMPLIES (NOT (LESSP (EXP 2 (LENGTH RADDR)) (LENGTH LST)))
           (EQUAL (V-NTH1 (REV RADDR) LST)
                  (READ-MEM1 RADDR (RAM-TREE LST (EXP 2 (LENGTH RADDR))))))
  ((INDUCT (READ-MEM1-RAM-TREE-HINT RADDR LST))))

(PROVE-LEMMA REV-APPEND (REWRITE)
  (EQUAL (REV (APPEND A B)) (APPEND (REV B) (REV A))))

(PROVE-LEMMA V-TO-NAT-REV-REV (REWRITE)
  (EQUAL (V-TO-NAT (REV (REV ADDR))) (V-TO-NAT ADDR)))

(PROVE-LEMMA READ-MEM-RAM-TREE (REWRITE)
  (IMPLIES (AND (EQUAL E (EXP 2 (LENGTH ADDR)))
                (NOT (LESSP E (LENGTH LST))))
           (EQUAL (V-NTH1 ADDR LST)
                  (READ-MEM ADDR (RAM-TREE LST E))))
  ((USE (READ-MEM1-REV-RAM-TREE (RADDR (REV ADDR))))))

(DISABLE V-NTH1)
(DISABLE READ-MEM)

(PROVE-LEMMA RESTN-UPDATE-NTH-PLUS (REWRITE)
  (EQUAL (RESTN E (UPDATE-NTH (PLUS V E) L VAL))
         (UPDATE-NTH V (RESTN E L) VAL)))

(PROVE-LEMMA FIRSTN-UPDATE-NTH-PLUS (REWRITE)
  (EQUAL (FIRSTN E (UPDATE-NTH (PLUS V E) L VAL))
         (FIRSTN E L)))

(PROVE-LEMMA RESTN-UPDATE-NTH (REWRITE)
  (IMPLIES (LESSP V E)
           (EQUAL (RESTN E (UPDATE-NTH V L VAL))
                  (RESTN E L))))

(PROVE-LEMMA FIRSTN-UPDATE-NTH (REWRITE)
  (IMPLIES (LESSP V E)
           (EQUAL (FIRSTN E (UPDATE-NTH V L VAL))
                  (UPDATE-NTH V (FIRSTN E L) VAL))))

(PROVE-LEMMA WRITE-MEM1-REV-RAM-TREE NIL
  (IMPLIES (NOT (LESSP (EXP 2 (LENGTH RADDR)) (LENGTH LST)))
           (EQUAL (RAM-TREE (UPDATE-V-NTH (REV RADDR) LST VAL)
                            (EXP 2 (LENGTH RADDR)))
                  (WRITE-MEM1 RADDR (RAM-TREE LST (EXP 2 (LENGTH RADDR))) VAL)))
  ((INDUCT (READ-MEM1-RAM-TREE-HINT RADDR LST))))

(PROVE-LEMMA WRITE-MEM-RAM-TREE (REWRITE)
  (IMPLIES (AND (EQUAL E (EXP 2 (LENGTH ADDR)))
                (NOT (LESSP E (LENGTH LST))))
           (EQUAL (RAM-TREE (UPDATE-V-NTH ADDR LST VAL) E)
                  (WRITE-MEM ADDR (RAM-TREE LST E) VAL)))
  ((USE (WRITE-MEM1-REV-RAM-TREE (RADDR (REV ADDR))))))

(DISABLE UPDATE-V-NTH)
(DISABLE WRITE-MEM)

(PROVE-LEMMA LENGTH-RN-B (REWRITE)
  (EQUAL (LENGTH (RN-B INS)) 4)
  ((ENABLE LENGTH-SUBRANGE)))

(PROVE-LEMMA M-ALU-OPERATION-IS-FM9001-ALU-OPERATION (REWRITE)
   (IMPLIES (AND (EQUAL (LENGTH B-ADDRESS) 32)
                 (EQUAL (LENGTH REGS) 16)
                 (NOT (LESSP (EXP 2 32) (LENGTH MEM))))
            (EQUAL (M->FM9001
                    (M-ALU-OPERATION REGS C V N Z MEM
                                     INS OPERAND-A OPERAND-B B-ADDRESS))
                   (FM9001-ALU-OPERATION (RAM-TREE REGS 16)
                                         (LIST Z N V C)
                                         (RAM-TREE MEM (EXP 2 32))
                                         INS OPERAND-A OPERAND-B B-ADDRESS)))
   ((DISABLE REG-DIRECT-P STORE-CC MODE-B RN-B BV V-ALU OP-CODE C-SET
             V-SET N-SET Z-SET SET-FLAGS)))

(DEFN BVP-LISTP (LST)
  (IF (NLISTP LST)
      (EQUAL LST NIL)
      (AND (BVP (CAR LST))
           (EQUAL (LENGTH (CAR LST)) 32)
           (BVP-LISTP (CDR LST)))))

(DEFN PROPER-M-STATEP (M)
  (AND (M-STATEP M)
       (BVP-LISTP (M-REGS M))
       (BVP-LISTP (M-MEM M))
       (EQUAL (LENGTH (M-REGS M)) 16)
       (NOT (LESSP (EXP 2 32) (LENGTH (M-MEM M))))))

(PROVE-LEMMA LENGTH-NTH (REWRITE)
  (IMPLIES (AND (BVP-LISTP LST)
                (LESSP N (LENGTH LST)))
           (AND (BVP (NTH N LST))
                (EQUAL (LENGTH (NTH N LST)) 32))))

(PROVE-LEMMA LENGTH-V-NTH1 (REWRITE)
  (IMPLIES (BVP-LISTP LST)
           (AND (BVP (V-NTH1 ADDR LST))
                (EQUAL (LENGTH (V-NTH1 ADDR LST)) 32)))
  ((ENABLE V-NTH1)))

(PROVE-LEMMA LENGTH-READ-MEM (REWRITE)
  (IMPLIES (AND (BVP-LISTP LST)
                (EQUAL K (EXP 2 (LENGTH ADDR)))
                (NOT (LESSP K (LENGTH LST))))
           (AND (BVP (READ-MEM ADDR (RAM-TREE LST K)))
                (EQUAL (LENGTH (READ-MEM ADDR (RAM-TREE LST K))) 32)))
  ((ENABLE READ-MEM)
   (DISABLE READ-MEM-RAM-TREE)
   (USE (READ-MEM-RAM-TREE (E (EXP 2 (LENGTH ADDR)))))))

(PROVE-LEMMA BVP-LISTP-UPDATE-NTH (REWRITE)
  (IMPLIES (AND (BVP VAL)
                (EQUAL (LENGTH VAL) 32)
                (BVP-LISTP LST))
           (BVP-LISTP (UPDATE-NTH N LST VAL))))

(PROVE-LEMMA BVP-LISTP-UPDATE-V-NTH (REWRITE)
  (IMPLIES (AND (BVP VAL)
                (EQUAL (LENGTH VAL) 32)
                (BVP-LISTP LST))
           (BVP-LISTP (UPDATE-V-NTH ADDR LST VAL)))
  ((ENABLE UPDATE-V-NTH)))

(ENABLE BVP-BV-V-ALU)

(PROVE-LEMMA LENGTH-BV-V-ALU (REWRITE)
  (IMPLIES (AND (EQUAL (LENGTH A) (LENGTH B))
                (LISTP A))
           (EQUAL (LENGTH (BV (V-ALU C A B OP))) (LENGTH A)))
  ((DISABLE V-BUF V-NOT V-AND V-OR V-XOR V-LSR V-ASR V-ROR V-SUBTRACTER-OUTPUT
            V-ADDER-OUTPUT)
   (ENABLE LENGTH-V-BUF LENGTH-V-NOT LENGTH-V-AND LENGTH-V-OR LENGTH-V-XOR
           LENGTH-V-LSR LENGTH-V-ASR LENGTH-V-ROR LENGTH-OF-V-ADDER-OUTPUT
           LENGTH-OF-V-SUBTRACTER-OUTPUT LENGTH-NAT-TO-V)))

(PROVE-LEMMA LENGTH-UPDATE-NTH (REWRITE)
  (EQUAL (LENGTH (UPDATE-NTH I LST VAL)) (LENGTH LST)))

(PROVE-LEMMA LENGTH-UPDATE-V-NTH (REWRITE)
  (EQUAL (LENGTH (UPDATE-V-NTH V LST VAL)) (LENGTH LST))
  ((ENABLE UPDATE-V-NTH)))

(PROVE-LEMMA M-ALU-OPERATION-PRESERVES-HYPS (REWRITE)
  (IMPLIES
   (AND (BVP-LISTP MEM)
        (BVP-LISTP REGS)
        (BVP OPERAND-A)
        (EQUAL (LENGTH OPERAND-A) 32)
        (EQUAL (LENGTH OPERAND-B) 32)
        (LISTP OPERAND-A)
        (EQUAL (LENGTH B-ADDRESS) 32)
        (EQUAL (LENGTH REGS) 16)
        (NOT (LESSP (EXP 2 32) (LENGTH MEM))))
   (PROPER-M-STATEP (M-ALU-OPERATION REGS C V N Z MEM
                                     INS OPERAND-A OPERAND-B B-ADDRESS)))
  ((DISABLE REG-DIRECT-P STORE-CC MODE-B RN-B BV V-ALU OP-CODE C-SET
            V-SET N-SET Z-SET SET-FLAGS)))

(DISABLE M-ALU-OPERATION)
(DISABLE FM9001-ALU-OPERATION)

(DEFN M-OPERAND-B (REGS C V N Z MEM INS OPERAND-A)
  (M-ALU-OPERATION (IF (PRE-DEC-P (MODE-B INS))
                       (UPDATE-V-NTH (RN-B INS)
                                     REGS
                                     (V-DEC (V-NTH1 (RN-B INS) REGS)))
                       (IF (POST-INC-P (MODE-B INS))
                           (UPDATE-V-NTH (RN-B INS)
                                         REGS
                                         (V-INC (V-NTH1 (RN-B INS) REGS)))
                           REGS))
                   C V N Z MEM INS OPERAND-A
                   (IF (REG-DIRECT-P (MODE-B INS))
                       (V-NTH1 (RN-B INS) REGS)
                       (V-NTH1 (IF (PRE-DEC-P (MODE-B INS))
                                   (V-DEC (V-NTH1 (RN-B INS) REGS))
                                   (V-NTH1 (RN-B INS) REGS))
                               MEM))
                   (IF (PRE-DEC-P (MODE-B INS))
                       (V-DEC (V-NTH1 (RN-B INS) REGS))
                       (V-NTH1 (RN-B INS) REGS))))

(ENABLE LENGTH-V-NOT)

(PROVE-LEMMA LENGTH-V-ADDER (REWRITE)
  (EQUAL (LENGTH (V-ADDER C A B)) (ADD1 (LENGTH A))))

(ENABLE LENGTH-NAT-TO-V)

(PROVE-LEMMA LENGTH-V-DEC (REWRITE)
             (EQUAL (LENGTH (V-DEC V)) (LENGTH V)))

(PROVE-LEMMA M-OPERAND-B-IS-FM9001-OPERAND-B (REWRITE)
  (IMPLIES (AND (BVP-LISTP REGS)
                (EQUAL (LENGTH REGS) 16)
                (NOT (LESSP (EXP 2 32) (LENGTH MEM))))
           (EQUAL (M->FM9001 (M-OPERAND-B REGS C V N Z MEM INS OPERAND-A))
                  (FM9001-OPERAND-B (RAM-TREE REGS 16)
                                    (LIST Z N V C)
                                    (RAM-TREE MEM (EXP 2 32))
                                    INS OPERAND-A)))
  ((DISABLE M->FM9001 PRE-DEC-P MODE-B RN-B V-DEC POST-INC-P V-INC REG-DIRECT-P)))

(PROVE-LEMMA LENGTH-V-INC (REWRITE)
  (EQUAL (LENGTH (V-INC V)) (LENGTH V)))
  
(PROVE-LEMMA BVP-FIRSTN-V-ADDER (REWRITE)
  (IMPLIES (EQUAL N (LENGTH A))
           (BVP (FIRSTN N (V-ADDER C A B)))))

(PROVE-LEMMA BVP-V-DEC (REWRITE)
  (BVP (V-DEC V)))

(PROVE-LEMMA BVP-V-INC (REWRITE)
  (BVP (V-INC V)))

(PROVE-LEMMA BVP-LISTP-IF (REWRITE)
  (IMPLIES (AND (BVP-LISTP B)
                (BVP-LISTP C))
           (BVP-LISTP (IF A B C))))

(enable LENGTH-IF)

(PROVE-LEMMA LISTP-OPERAND-A NIL
  (IMPLIES (EQUAL (LENGTH OPERAND-A) 32)
           (LISTP OPERAND-A)))

(PROVE-LEMMA M-OPERAND-B-PRESERVES-HYPS (REWRITE)
  (IMPLIES
   (AND (BVP-LISTP REGS)
        (BVP-LISTP MEM)
        (BVP OPERAND-A)
        (EQUAL (LENGTH OPERAND-A) 32)
        (EQUAL (LENGTH REGS) 16)
        (NOT (LESSP (EXP 2 32) (LENGTH MEM))))
   (PROPER-M-STATEP (M-OPERAND-B REGS C V N Z MEM INS OPERAND-A)))
  ((USE (LISTP-OPERAND-A))
   (DISABLE M->FM9001 PRE-DEC-P MODE-B RN-B V-DEC POST-INC-P V-INC REG-DIRECT-P)))

(DISABLE M-OPERAND-B)
(DISABLE FM9001-OPERAND-B)

(DEFN M-OPERAND-A (REGS C V N Z MEM INS)
  (M-OPERAND-B
   (IF (A-IMMEDIATE-P INS)
       REGS
       (IF (PRE-DEC-P (MODE-A INS))
           (UPDATE-V-NTH (RN-A INS)
                         REGS
                         (V-DEC (V-NTH1 (RN-A INS) REGS)))
           (IF (POST-INC-P (MODE-A INS))
               (UPDATE-V-NTH (RN-A INS)
                             REGS
                             (V-INC (V-NTH1 (RN-A INS) REGS)))
               REGS)))
   C V N Z MEM INS
   (IF (A-IMMEDIATE-P INS)
       (SIGN-EXTEND (A-IMMEDIATE INS) 32)
       (IF (REG-DIRECT-P (MODE-A INS))
           (V-NTH1 (RN-A INS) REGS)
           (IF (PRE-DEC-P (MODE-A INS))
               (V-NTH1 (V-DEC (V-NTH1 (RN-A INS) REGS))
                       MEM)
               (V-NTH1 (V-NTH1 (RN-A INS) REGS)
                       MEM))))))

(PROVE-LEMMA LENGTH-RN-A (REWRITE)
  (EQUAL (LENGTH (RN-A INS)) 4)
  ((ENABLE LENGTH-SUBRANGE)))

(PROVE-LEMMA M-OPERAND-A-IS-FM9001-OPERAND-A (REWRITE)
  (IMPLIES
   (AND (BVP-LISTP REGS)
        (EQUAL (LENGTH REGS) 16)
        (NOT (LESSP (EXP 2 32) (LENGTH MEM))))
   (EQUAL (M->FM9001 (M-OPERAND-A REGS C V N Z MEM INS))
          (FM9001-OPERAND-A (RAM-TREE REGS 16)
                            (LIST Z N V C)
                            (RAM-TREE MEM (EXP 2 32))
                            INS)))
  ((DISABLE M->FM9001 A-IMMEDIATE-P PRE-DEC-P MODE-A RN-A RN-B
            V-DEC POST-INC-P V-INC SIGN-EXTEND A-IMMEDIATE REG-DIRECT-P)))

(PROVE-LEMMA M-OPERAND-A-PRESERVES-HYPS (REWRITE)
  (IMPLIES
   (AND (BVP-LISTP REGS)
        (BVP-LISTP MEM)
        (EQUAL (LENGTH REGS) 16)
        (NOT (LESSP (EXP 2 32) (LENGTH MEM))))
   (PROPER-M-STATEP (M-OPERAND-A REGS C V N Z MEM INS)))
  ((ENABLE BVP-SIGN-EXTEND LENGTH-SIGN-EXTEND)
   (DISABLE M->FM9001 A-IMMEDIATE-P PRE-DEC-P MODE-A RN-A RN-B
            V-DEC POST-INC-P V-INC SIGN-EXTEND A-IMMEDIATE REG-DIRECT-P)))


(DISABLE M-OPERAND-A)
(DISABLE FM9001-OPERAND-A)

(DEFN M-STEP1 (CURRENT-INSTRUCTION M)
  (M-OPERAND-A (UPDATE-V-NTH (NAT-TO-V 15 4) (M-REGS M)
                             (V-INC (V-NTH1 (NAT-TO-V 15 4) (M-REGS M))))
               (M-C-FLG M)
               (M-V-FLG M)
               (M-N-FLG M)
               (M-Z-FLG M)
               (M-MEM M)
               CURRENT-INSTRUCTION))

(DEFN M-STEP (M)
  (M-STEP1 (CURRENT-INSTRUCTION (M-REGS M)
                                (M-MEM M))
           M))

(PROVE-LEMMA M-STEP-IS-FM9001-STEP (REWRITE)
  (IMPLIES
   (AND
    (BVP-LISTP (M-REGS M))
    (EQUAL (LENGTH (M-REGS M)) 16)
    (NOT (LESSP (EXP 2 32) (LENGTH (M-MEM M)))))
   (EQUAL (M->FM9001 (M-STEP M))
          (FM9001-STEP (M->FM9001 M) (NAT-TO-V 15 4))))
((EXPAND (M->FM9001 M))
 (DISABLE M->FM9001 V-INC V-DEC  RN-A RN-B)))

(PROVE-LEMMA M-STEP-PRESERVES-HYPS (REWRITE)
  (IMPLIES
   (AND
    (BVP-LISTP (M-REGS M))
    (BVP-LISTP (M-MEM M))
    (EQUAL (LENGTH (M-REGS M)) 16)
    (NOT (LESSP (EXP 2 32) (LENGTH (M-MEM M)))))
   (PROPER-M-STATEP (M-STEP M))))

(DISABLE M-STEP)
(DISABLE M->FM9001)
(DISABLE FM9001-STEP)

(DEFN M (M N)
  (IF (ZEROP N)
      M
      (M (M-STEP M) (SUB1 N))))

(PROVE-LEMMA ONE-WAY-CORRESPONDENCE-M-FM9001 (REWRITE)
  (IMPLIES (PROPER-M-STATEP M)
           (EQUAL (M->FM9001 (M M N))
                  (FM9001 (M->FM9001 M) N)))
  ((INDUCT (M M N))
   (DISABLE NAT-TO-V *1*NAT-TO-V)))

; Book:  i.events.  Now we move up to the i machine.

(set-status close-data-base-2 t ((boot-strap initial)
                                 (add-shell enable)
                                 ((defn *1*defn) enable)
                                 (otherwise disable)))

(DEFN PUT-ASSOC
      (VAL NAME ALIST)
      (COND ((NLISTP ALIST) ALIST)
            ((EQUAL NAME (CAAR ALIST))
             (CONS (CONS NAME VAL) (CDR ALIST)))
            (T (CONS (CAR ALIST)
                     (PUT-ASSOC VAL NAME (CDR ALIST))))))

(DEFN DEFINEDP
      (NAME ALIST)
      (COND ((NLISTP ALIST) F)
            ((EQUAL NAME (CAAR ALIST)) T)
            (T (DEFINEDP NAME (CDR ALIST)))))

; DEFINIENS, below, used to be named VALUE but that name is now used
; in FM9001.

(DEFN DEFINIENS
      (NAME ALIST)
      (CDR (DEFINITION NAME ALIST)))

(DEFN PUT-VALUE
      (VAL NAME ALIST)
      (PUT-ASSOC VAL NAME ALIST))

(DEFN ADPP
      (X SEGMENT)
      (AND (LISTP X)
           (NUMBERP (ADP-OFFSET X))
           (DEFINEDP (ADP-NAME X) SEGMENT)
           (LESSP (ADP-OFFSET X)
                  (LENGTH (definiens (ADP-NAME X) SEGMENT)))))

(DEFN ADD-ADP
      (ADP N)
      (CONS (ADP-NAME ADP)
            (PLUS (ADP-OFFSET ADP) N)))

(DEFN ADD1-ADP (ADP) (ADD-ADP ADP 1))

(DEFN SUB1-ADP (ADP) (SUB-ADP ADP 1))

(DEFN PUT
      (VAL N LST)
      (IF (ZEROP N)
          (IF (LISTP LST)
              (CONS VAL (CDR LST))
              (LIST VAL))
          (CONS (CAR LST)
                (PUT VAL (SUB1 N) (CDR LST)))))

(DEFN FETCH-ADP
      (ADP SEGMENT)
      (GET (ADP-OFFSET ADP)
           (definiens (ADP-NAME ADP) SEGMENT)))

(DEFN DEPOSIT-ADP
      (VAL ADP SEGMENT)
      (PUT-VALUE (PUT VAL
                      (ADP-OFFSET ADP)
                      (definiens (ADP-NAME ADP) SEGMENT))
                 (ADP-NAME ADP)
                 SEGMENT))

(DEFN ADDRESSP
      (X SEGMENT)
      (ADPP (UNTAG X) SEGMENT))

(DEFN OFFSET
      (X)
      (ADP-OFFSET (UNTAG X)))

(DEFN ADD-ADDR
      (ADDR N)
      (TAG (TYPE ADDR)
           (ADD-ADP (UNTAG ADDR) N)))

(DEFN ADD1-ADDR
      (ADDR)
      (ADD-ADDR ADDR 1))

(DEFN SUB1-ADDR
      (ADDR)
      (SUB-ADDR ADDR 1))

(DEFN FETCH
      (ADDR SEGMENT)
      (FETCH-ADP (UNTAG ADDR) SEGMENT))

(DEFN DEPOSIT
      (VAL ADDR SEGMENT)
      (DEPOSIT-ADP VAL
                   (UNTAG ADDR)
                   SEGMENT))

(DEFN BOOLEANP
      (X)
      (OR (EQUAL X 'T) (EQUAL X 'F)))

(DEFN BOOL
      (X)
      (TAG 'BOOL (IF X 'T 'F)))

(DEFN OR-BOOL
      (X Y)
      (IF (EQUAL X 'F) Y 'T))

(DEFN AND-BOOL
      (X Y)
      (IF (EQUAL X 'F) 'F Y))

(DEFN XOR-BOOL
      (X Y)
      (COND ((EQUAL X 'F) Y)
            ((EQUAL Y 'F) 'T)
            (T 'F)))

(DEFN SMALL-NATURALP
      (I WORD-SIZE)
      (AND (NUMBERP I)
           (LESSP I (EXP 2 WORD-SIZE))))

(DEFN BOOL-TO-NAT
      (FLG)
      (IF (EQUAL FLG 'F) 0 1))

(DEFN FIX-SMALL-NATURAL
      (N WORD-SIZE)
      (REMAINDER N (EXP 2 WORD-SIZE)))

(DEFN SMALL-INTEGERP
      (I WORD-SIZE)
      (AND (INTEGERP I)
           (NOT (ILESSP I
                        (MINUS (EXP 2 (SUB1 WORD-SIZE)))))
           (ILESSP I (EXP 2 (SUB1 WORD-SIZE)))))

(DEFN INEGATE
      (I)
      (COND ((NEGATIVEP I) (NEGATIVE-GUTS I))
            ((ZEROP I) 0)
            (T (MINUS I))))

(DEFN FIX-SMALL-INTEGER
      (I WORD-SIZE)
      (COND ((SMALL-INTEGERP I WORD-SIZE) I)
            ((NEGATIVEP I)
             (IPLUS I (EXP 2 WORD-SIZE)))
            (T (IPLUS I (MINUS (EXP 2 WORD-SIZE))))))

(DEFN BITP
      (X)
      (OR (EQUAL X 0) (EQUAL X 1)))

(DEFN BIT-VECTORP
      (X N)
      (IF (NLISTP X)
          (AND (EQUAL X NIL) (ZEROP N))
          (AND (NOT (ZEROP N))
               (BITP (CAR X))
               (BIT-VECTORP (CDR X) (SUB1 N)))))

(DEFN OR-BIT
      (BIT1 BIT2)
      (IF (EQUAL BIT1 0)
          (IF (EQUAL BIT2 0) 0 1)
          1))

(DEFN NOT-BIT
      (BIT)
      (IF (EQUAL BIT 0) 1 0))

(DEFN AND-BIT
      (BIT1 BIT2)
      (COND ((EQUAL BIT1 0) 0)
            ((EQUAL BIT2 0) 0)
            (T 1)))

(DEFN XOR-BIT
      (BIT1 BIT2)
      (COND ((EQUAL BIT1 0)
             (IF (EQUAL BIT2 0) 0 1))
            ((EQUAL BIT2 0) 1)
            (T 0)))

(DEFN OR-BITV
      (A B)
      (IF (NLISTP A)
          NIL
          (CONS (OR-BIT (CAR A) (CAR B))
                (OR-BITV (CDR A) (CDR B)))))

(DEFN NOT-BITV
      (A)
      (IF (NLISTP A)
          NIL
          (CONS (NOT-BIT (CAR A))
                (NOT-BITV (CDR A)))))

(DEFN AND-BITV
      (A B)
      (IF (NLISTP A)
          NIL
          (CONS (AND-BIT (CAR A) (CAR B))
                (AND-BITV (CDR A) (CDR B)))))

(DEFN XOR-BITV
      (A B)
      (IF (NLISTP A)
          NIL
          (CONS (XOR-BIT (CAR A) (CAR B))
                (XOR-BITV (CDR A) (CDR B)))))

(DEFN ALL-BUT-LAST
      (A)
      (COND ((NLISTP A) NIL)
            ((NLISTP (CDR A)) NIL)
            (T (CONS (CAR A)
                     (ALL-BUT-LAST (CDR A))))))

(DEFN RSH-BITV
      (A)
      (CONS 0 (ALL-BUT-LAST A)))

(DEFN LSH-BITV
      (A)
      (APPEND (CDR A) '(0)))

(DEFN ALL-ZERO-BITVP
      (A)
      (IF (LISTP A)
          (AND (EQUAL (CAR A) 0)
               (ALL-ZERO-BITVP (CDR A)))
          T))

(DEFN FIND-LABELP
      (X LST)
      (COND ((NLISTP LST) F)
            ((AND (LABELLEDP (CAR LST))
                  (EQUAL X (CADAR LST)))
             T)
            (T (FIND-LABELP X (CDR LST)))))

(DEFN X-Y-ERROR-MSG
      (X Y)
      (PACK (APPEND (UNPACK 'ILLEGAL-)
                    (APPEND (UNPACK Y)
                            (CDR (UNPACK 'G-INSTRUCTION))))))

(DEFN CSTKP
      (X SEGMENT)
      (AND (EQUAL (TYPE X) 'SYS-ADDR)
           (ADDRESSP X SEGMENT)
           (EQUAL (AREA-NAME X) 'CSTK)
           (EQUAL (CDDR X) NIL)))

(DEFN TSTKP
      (X SEGMENT)
      (AND (EQUAL (TYPE X) 'SYS-ADDR)
           (ADDRESSP X SEGMENT)
           (EQUAL (AREA-NAME X) 'TSTK)
           (EQUAL (CDDR X) NIL)))

(DEFN PUSH-STK
      (SYS-ADDR)
      (SUB1-ADDR SYS-ADDR))

(DEFN POP-STK
      (SYS-ADDR)
      (ADD1-ADDR SYS-ADDR))

(DEFN STK-LENGTH
      (ADDR SEGMENT)
      (SUB1 (DIFFERENCE (LENGTH (definiens (AREA-NAME ADDR) SEGMENT))
                        (OFFSET ADDR))))

(DEFN EMPTY-STKP
      (ADDR SEGMENT)
      (ZEROP (STK-LENGTH ADDR SEGMENT)))

(DEFN FREE-STK-SIZE
      (ADDR)
      (OFFSET ADDR))

(DEFN ICODE-LABELP
      (LAB SEGMENT)
      (AND (DEFINEDP (ADP-NAME LAB) SEGMENT)
           (FIND-LABELP LAB
                        (definiens (ADP-NAME LAB) SEGMENT))))

(DEFN I-OBJECTP
      (X I)
      (AND (LISTP X)
           (EQUAL (CDDR X) NIL)
           (CASE (TYPE X)
                 (NAT (SMALL-NATURALP (UNTAG X)
                                      (I-WORD-SIZE I)))
                 (INT (SMALL-INTEGERP (UNTAG X)
                                      (I-WORD-SIZE I)))
                 (BITV (BIT-VECTORP (UNTAG X)
                                    (I-WORD-SIZE I)))
                 (BOOL (BOOLEANP (UNTAG X)))
                 (ADDR (ADPP (UNTAG X)
                             (I-USR-DATA-SEGMENT I)))
                 (PC (ICODE-LABELP (UNTAG X)
                                   (I-PROG-SEGMENT I)))
                 (SUBR (ADPP (CONS (UNTAG X) 0)
                             (I-PROG-SEGMENT I)))
                 (SYS-ADDR (ADPP (UNTAG X)
                                 (I-SYS-DATA-SEGMENT I)))
                 (IPC (ADPP (UNTAG X) (I-PROG-SEGMENT I)))
                 (OTHERWISE F))))

(DEFN I-OBJECTP-TYPE
      (TYPE X I)
      (AND (EQUAL TYPE (TYPE X))
           (I-OBJECTP X I)))

(DEFN I-USR-DATA-TYPEP
      (TYPE)
      (MEMBER TYPE
              '(NAT INT BITV BOOL ADDR SUBR PC)))

(DEFN I-USR-DATA-OBJECTP
      (X I)
      (AND (I-OBJECTP X I)
           (I-USR-DATA-TYPEP (TYPE X))))

(DEFN TOTAL-I-SYSTEM-SIZE
      (I load-addr)
      (PLUS load-addr
            (SEGMENT-LENGTH (I-USR-DATA-SEGMENT I))
            (SEGMENT-LENGTH (I-PROG-SEGMENT I))
            (SEGMENT-LENGTH (I-SYS-DATA-SEGMENT I))))

(DEFN I-LOADABLEP
      (I load-addr)
      (LESSP (TOTAL-I-SYSTEM-SIZE I load-addr)
             (EXP 2 (I-WORD-SIZE I))))

(DEFN I-STATE-OKP
      (I load-addr)
      (AND (I-STATEP I)
           (I-OBJECTP-TYPE 'IPC (I-PC I) I)
           (CSTKP (I-CFP I)
                  (I-SYS-DATA-SEGMENT I))
           (CSTKP (I-CSP I)
                  (I-SYS-DATA-SEGMENT I))
           (TSTKP (I-TSP I)
                  (I-SYS-DATA-SEGMENT I))
           (I-OBJECTP-TYPE 'BOOL (I-C-FLG I) I)
           (I-OBJECTP-TYPE 'BOOL (I-V-FLG I) I)
           (I-OBJECTP-TYPE 'BOOL (I-N-FLG I) I)
           (I-OBJECTP-TYPE 'BOOL (I-Z-FLG I) I)
           (I-LOADABLEP I load-addr)))

(DEFN ALL-I-USR-DATA-OBJECTPS
      (LST I)
      (IF (NLISTP LST)
          (EQUAL LST NIL)
          (AND (I-USR-DATA-OBJECTP (CAR LST) I)
               (ALL-I-USR-DATA-OBJECTPS (CDR LST)
                                        I))))

(DEFN PROPER-I-USR-DATA-AREA
      (AREA I)
      (AND (LITATOM (CAR AREA))
           (LISTP (CDR AREA))
           (ALL-I-USR-DATA-OBJECTPS (CDR AREA)
                                    I)))

(DEFN PROPER-I-USR-DATA-SEGMENTP
      (DATA-SEGMENT I)
      (IF (NLISTP DATA-SEGMENT)
          (EQUAL DATA-SEGMENT NIL)
          (AND (PROPER-I-USR-DATA-AREA (CAR DATA-SEGMENT)
                                       I)
               (NOT (DEFINEDP (CAAR DATA-SEGMENT)
                              (CDR DATA-SEGMENT)))
               (PROPER-I-USR-DATA-SEGMENTP (CDR DATA-SEGMENT)
                                           I))))

(DEFN ADD1-I-PC
      (I)
      (ADD1-ADDR (I-PC I)))

(DEFN ADD1-I-PCP
      (I)
      (ADDRESSP (ADD1-I-PC I)
                (I-PROG-SEGMENT I)))

(DEFN ADD2-I-PC
      (I)
      (ADD1-ADDR (ADD1-ADDR (I-PC I))))

(DEFN ADD2-I-PCP
      (I)
      (ADDRESSP (ADD2-I-PC I)
                (I-PROG-SEGMENT I)))

(DEFN I-CURRENT-INSTRUCTION
      (I)
      (UNLABEL (FETCH (I-PC I) (I-PROG-SEGMENT I))))

(DEFN I-NEXTWORD
      (I)
      (UNLABEL (FETCH (ADD1-I-PC I)
                      (I-PROG-SEGMENT I))))

(DEFN IPC
      (LAB PROGRAM)
      (TAG 'IPC
           (CONS (NAME PROGRAM)
                 (FIND-LABEL LAB (CDR PROGRAM)))))

(DEFN I-HALT
      (I PSW)
      (I-STATE (I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               PSW))

(DEFN XOR-XXX (OBJ1 OBJ2 I LOAD-ADDR)
      (XOR-BITV (V-TO-BITV (LINK-DATA-WORD OBJ1
                                            (I-LINK-TABLES I LOAD-ADDR)
                                            (I-WORD-SIZE I)))
                (V-TO-BITV (LINK-DATA-WORD OBJ2
                                            (I-LINK-TABLES I LOAD-ADDR)
                                            (I-WORD-SIZE I)))))

(DEFN I-ADD_<C>_X_X{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-X I) I)))

(DEFN I-ADD_<C>_X_X{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (TAG 'NAT
                    (FIX-SMALL-NATURAL (TIMES 2 (UNTAG (I-X I)))
                                       (I-WORD-SIZE I)))
               (I-Y I)
               (BOOL (NOT (SMALL-NATURALP (TIMES 2 (UNTAG (I-X I)))
                                          (I-WORD-SIZE I))))
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_<TSP>_<TSP>{V}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'BITV
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-ADD_<TSP>_<TSP>{V}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'BITV
                             (LSH-BITV (UNTAG (FETCH (I-TSP I)
                                                     (I-SYS-DATA-SEGMENT I)))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_<TSP>_<TSP>{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'NAT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-NATURALP (TIMES 2
                                  (UNTAG (FETCH (I-TSP I)
                                                (I-SYS-DATA-SEGMENT I))))
                           (I-WORD-SIZE I))))

(DEFN I-ADD_<TSP>_<TSP>{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'NAT
                             (TIMES 2
                                    (UNTAG (FETCH (I-TSP I)
                                                  (I-SYS-DATA-SEGMENT I)))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_<TSP>{A}_X{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (I-OBJECTP-TYPE 'ADDR
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (I-OBJECTP-TYPE 'ADDR
                           (ADD-ADDR (FETCH (I-TSP I)
                                            (I-SYS-DATA-SEGMENT I))
                                     (UNTAG (I-X I)))
                           I)))

(DEFN I-ADD_<TSP>{A}_X{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (ADD-ADDR (FETCH (I-TSP I)
                                         (I-SYS-DATA-SEGMENT I))
                                  (UNTAG (I-X I)))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_TSP_*{N}-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP-TYPE 'NAT
                           (I-NEXTWORD I)
                           I)
           (ADDRESSP (ADD-ADDR (I-TSP I)
                               (UNTAG (I-NEXTWORD I)))
                     (I-SYS-DATA-SEGMENT I))))

(DEFN I-ADD_TSP_*{N}-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (ADD-ADDR (I-TSP I)
                         (UNTAG (I-NEXTWORD I)))
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_TSP_X{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (ADDRESSP (ADD-ADDR (I-TSP I) (UNTAG (I-X I)))
                     (I-SYS-DATA-SEGMENT I))))

(DEFN I-ADD_TSP_X{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (ADD-ADDR (I-TSP I) (UNTAG (I-X I)))
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_<TSP>{I}_X{I}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'INT (I-X I) I)
           (I-OBJECTP-TYPE 'INT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-INTEGERP (IPLUS (UNTAG (FETCH (I-TSP I)
                                                (I-SYS-DATA-SEGMENT I)))
                                  (UNTAG (I-X I)))
                           (I-WORD-SIZE I))))

(DEFN I-ADD_<TSP>{I}_X{I}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'INT
                             (IPLUS (UNTAG (FETCH (I-TSP I)
                                                  (I-SYS-DATA-SEGMENT I)))
                                    (UNTAG (I-X I))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_<TSP>{N}_X{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (I-OBJECTP-TYPE 'NAT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-NATURALP (PLUS (UNTAG (FETCH (I-TSP I)
                                               (I-SYS-DATA-SEGMENT I)))
                                 (UNTAG (I-X I)))
                           (I-WORD-SIZE I))))

(DEFN I-ADD_<TSP>{N}_X{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'NAT
                             (PLUS (UNTAG (FETCH (I-TSP I)
                                                 (I-SYS-DATA-SEGMENT I)))
                                   (UNTAG (I-X I))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_PC_X{N}-OKP
      (I)
      (AND (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (ADDRESSP (ADD-ADDR (I-PC I)
                               (ADD1 (UNTAG (I-X I))))
                     (I-PROG-SEGMENT I))))

(DEFN I-ADD_PC_X{N}-STEP
      (I)
      (I-STATE (ADD-ADDR (I-PC I)
                         (ADD1 (UNTAG (I-X I))))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_X_X{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (SMALL-NATURALP (TIMES 2 (UNTAG (I-X I)))
                           (I-WORD-SIZE I))))

(DEFN I-ADD_X_X{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (TAG 'NAT (TIMES 2 (UNTAG (I-X I))))
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADD_X{N}_CSP-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (ADDRESSP (ADD-ADDR (I-CSP I) (UNTAG (I-X I)))
                     (I-SYS-DATA-SEGMENT I))))

(DEFN I-ADD_X{N}_CSP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (ADD-ADDR (I-CSP I) (UNTAG (I-X I)))
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ADDC_<C>_X{N}_Y{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-X I) I)
           (I-OBJECTP-TYPE 'NAT (I-Y I) I)))

(DEFN I-ADDC_<C>_X{N}_Y{N}-STEP
    (I)
    (I-STATE (ADD1-I-PC I)
             (I-CFP I)
             (I-CSP I)
             (I-TSP I)
             (TAG 'NAT
                  (FIX-SMALL-NATURAL (PLUS (BOOL-TO-NAT (UNTAG (I-C-FLG I)))
                                           (UNTAG (I-Y I))
                                           (UNTAG (I-X I)))
                                     (I-WORD-SIZE I)))
             (I-Y I)
             (BOOL (NOT (SMALL-NATURALP (PLUS (BOOL-TO-NAT (UNTAG (I-C-FLG I)))
                                              (UNTAG (I-Y I))
                                              (UNTAG (I-X I)))
                                        (I-WORD-SIZE I))))
             (I-V-FLG I)
             (I-N-FLG I)
             (I-Z-FLG I)
             (I-PROG-SEGMENT I)
             (I-USR-DATA-SEGMENT I)
             (I-SYS-DATA-SEGMENT I)
             (I-WORD-SIZE I)
             'RUN))

(DEFN I-ADDC_<V>_X{I}_Y{I}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'INT (I-X I) I)
           (I-OBJECTP-TYPE 'INT (I-Y I) I)))

(DEFN I-ADDC_<V>_X{I}_Y{I}-STEP
   (I)
   (I-STATE (ADD1-I-PC I)
            (I-CFP I)
            (I-CSP I)
            (I-TSP I)
            (TAG 'INT
                 (FIX-SMALL-INTEGER (IPLUS (BOOL-TO-NAT (UNTAG (I-C-FLG I)))
                                           (IPLUS (UNTAG (I-Y I))
                                                  (UNTAG (I-X I))))
                                    (I-WORD-SIZE I)))
            (I-Y I)
            (I-C-FLG I)
            (BOOL (NOT (SMALL-INTEGERP (IPLUS (BOOL-TO-NAT (UNTAG (I-C-FLG I)))
                                              (IPLUS (UNTAG (I-Y I))
                                                     (UNTAG (I-X I))))
                                       (I-WORD-SIZE I))))
            (I-N-FLG I)
            (I-Z-FLG I)
            (I-PROG-SEGMENT I)
            (I-USR-DATA-SEGMENT I)
            (I-SYS-DATA-SEGMENT I)
            (I-WORD-SIZE I)
            'RUN))

(DEFN I-AND_<TSP>{V}_X{V}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'BITV (I-X I) I)
           (I-OBJECTP-TYPE 'BITV
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-AND_<TSP>{V}_X{V}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'BITV
                             (AND-BITV (UNTAG (FETCH (I-TSP I)
                                                     (I-SYS-DATA-SEGMENT I)))
                                       (UNTAG (I-X I))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-AND_<TSP>{B}_X{B}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'BOOL (I-X I) I)
           (I-OBJECTP-TYPE 'BOOL
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-AND_<TSP>{B}_X{B}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'BOOL
                             (AND-BOOL (UNTAG (FETCH (I-TSP I)
                                                     (I-SYS-DATA-SEGMENT I)))
                                       (UNTAG (I-X I))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-ASR_<C>_<TSP>_<TSP>{B}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'BOOL
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-ASR_<C>_<TSP>_<TSP>{B}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (FETCH (I-TSP I)
                      (I-SYS-DATA-SEGMENT I))
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'BOOL 'F)
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-CPOP_CFP-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-CSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (CSTKP (FETCH (I-CSP I)
                         (I-SYS-DATA-SEGMENT I))
                  (I-SYS-DATA-SEGMENT I))))

(DEFN I-CPOP_CFP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (FETCH (I-CSP I)
                      (I-SYS-DATA-SEGMENT I))
               (POP-STK (I-CSP I))
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-CPOP_PC-OKP
      (I)
      (AND (NOT (EMPTY-STKP (I-CSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'PC
                           (FETCH (I-CSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-CPOP_PC-STEP
      (I)
      (I-STATE (IPC (UNTAG (FETCH (I-CSP I)
                                  (I-SYS-DATA-SEGMENT I)))
                    (DEFINITION (AREA-NAME (FETCH (I-CSP I)
                                                  (I-SYS-DATA-SEGMENT I)))
                                (I-PROG-SEGMENT I)))
               (I-CFP I)
               (POP-STK (I-CSP I))
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-CPUSH_*-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP (I-NEXTWORD I) I)
           (NOT (ZEROP (FREE-STK-SIZE (I-CSP I))))))

(DEFN I-CPUSH_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (PUSH-STK (I-CSP I))
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (I-NEXTWORD I)
                        (PUSH-STK (I-CSP I))
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-CPUSH_<TSP>+-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (NOT (ZEROP (FREE-STK-SIZE (I-CSP I))))))

(DEFN I-CPUSH_<TSP>+-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (PUSH-STK (I-CSP I))
               (POP-STK (I-TSP I))
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (FETCH (I-TSP I)
                               (I-SYS-DATA-SEGMENT I))
                        (PUSH-STK (I-CSP I))
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-CPUSH_CFP-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (ZEROP (FREE-STK-SIZE (I-CSP I))))))

(DEFN I-CPUSH_CFP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (PUSH-STK (I-CSP I))
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (I-CFP I)
                        (PUSH-STK (I-CSP I))
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-DECR_<TSP>_<TSP>{I}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'INT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-INTEGERP (IDIFFERENCE (UNTAG (FETCH (I-TSP I)
                                                      (I-SYS-DATA-SEGMENT I)))
                                        1)
                           (I-WORD-SIZE I))))

(DEFN I-DECR_<TSP>_<TSP>{I}-STEP
     (I)
     (I-STATE (ADD1-I-PC I)
              (I-CFP I)
              (I-CSP I)
              (I-TSP I)
              (I-X I)
              (I-Y I)
              (I-C-FLG I)
              (I-V-FLG I)
              (I-N-FLG I)
              (I-Z-FLG I)
              (I-PROG-SEGMENT I)
              (I-USR-DATA-SEGMENT I)
              (DEPOSIT (TAG 'INT
                            (IDIFFERENCE (UNTAG (FETCH (I-TSP I)
                                                       (I-SYS-DATA-SEGMENT I)))
                                         1))
                       (I-TSP I)
                       (I-SYS-DATA-SEGMENT I))
              (I-WORD-SIZE I)
              'RUN))

(DEFN I-DECR_<TSP>_<TSP>{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'NAT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (NOT (ZEROP (UNTAG (FETCH (I-TSP I)
                                     (I-SYS-DATA-SEGMENT I)))))))

(DEFN I-DECR_<TSP>_<TSP>{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'NAT
                             (SUB1 (UNTAG (FETCH (I-TSP I)
                                                 (I-SYS-DATA-SEGMENT I)))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-INCR_<TSP>_<TSP>{I}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'INT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-INTEGERP (IPLUS (UNTAG (FETCH (I-TSP I)
                                                (I-SYS-DATA-SEGMENT I)))
                                  1)
                           (I-WORD-SIZE I))))

(DEFN I-INCR_<TSP>_<TSP>{I}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'INT
                             (IPLUS (UNTAG (FETCH (I-TSP I)
                                                  (I-SYS-DATA-SEGMENT I)))
                                    1))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-INCR_<TSP>_<TSP>{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'NAT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-NATURALP (ADD1 (UNTAG (FETCH (I-TSP I)
                                               (I-SYS-DATA-SEGMENT I))))
                           (I-WORD-SIZE I))))

(DEFN I-INCR_<TSP>_<TSP>{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'NAT
                             (ADD1 (UNTAG (FETCH (I-TSP I)
                                                 (I-SYS-DATA-SEGMENT I)))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-INCR_Y_Y{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-Y I) I)
           (SMALL-NATURALP (ADD1 (UNTAG (I-Y I)))
                           (I-WORD-SIZE I))))

(DEFN I-INCR_Y_Y{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (TAG 'NAT (ADD1 (UNTAG (I-Y I))))
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-INT-TO-NAT-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'INT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (NOT (NEGATIVEP (UNTAG (FETCH (I-TSP I)
                                         (I-SYS-DATA-SEGMENT I)))))))

(DEFN I-INT-TO-NAT-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'NAT
                             (UNTAG (FETCH (I-TSP I)
                                           (I-SYS-DATA-SEGMENT I))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-JUMP-N_X-OKP
      (I)
      (IF (EQUAL (UNTAG (I-N-FLG I)) 'F)
          (ADD1-I-PCP I)
          (I-OBJECTP-TYPE 'PC (I-X I) I)))

(DEFN I-JUMP-N_X-STEP
      (I)
      (I-STATE (IF (EQUAL (UNTAG (I-N-FLG I)) 'F)
                   (ADD1-I-PC I)
                   (IPC (UNTAG (I-X I))
                        (DEFINITION (AREA-NAME (I-X I))
                                    (I-PROG-SEGMENT I))))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-JUMP-NN_X-OKP
      (I)
      (IF (EQUAL (UNTAG (I-N-FLG I)) 'F)
          (I-OBJECTP-TYPE 'PC (I-X I) I)
          (ADD1-I-PCP I)))

(DEFN I-JUMP-NN_X-STEP
      (I)
      (I-STATE (IF (EQUAL (UNTAG (I-N-FLG I)) 'F)
                   (IPC (UNTAG (I-X I))
                        (DEFINITION (AREA-NAME (I-X I))
                                    (I-PROG-SEGMENT I)))
                   (ADD1-I-PC I))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-JUMP-NZ_X-OKP
      (I)
      (IF (EQUAL (UNTAG (I-Z-FLG I)) 'F)
          (I-OBJECTP-TYPE 'PC (I-X I) I)
          (ADD1-I-PCP I)))

(DEFN I-JUMP-NZ_X-STEP
      (I)
      (I-STATE (IF (EQUAL (UNTAG (I-Z-FLG I)) 'F)
                   (IPC (UNTAG (I-X I))
                        (DEFINITION (AREA-NAME (I-X I))
                                    (I-PROG-SEGMENT I)))
                   (ADD1-I-PC I))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-JUMP-Z_X-OKP
      (I)
      (IF (EQUAL (UNTAG (I-Z-FLG I)) 'F)
          (ADD1-I-PCP I)
          (I-OBJECTP-TYPE 'PC (I-X I) I)))

(DEFN I-JUMP-Z_X-STEP
      (I)
      (I-STATE (IF (EQUAL (UNTAG (I-Z-FLG I)) 'F)
                   (ADD1-I-PC I)
                   (IPC (UNTAG (I-X I))
                        (DEFINITION (AREA-NAME (I-X I))
                                    (I-PROG-SEGMENT I))))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-JUMP_*-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'PC
                           (I-NEXTWORD I)
                           I)))

(DEFN I-JUMP_*-STEP
      (I)
      (I-STATE (IPC (UNTAG (I-NEXTWORD I))
                    (DEFINITION (AREA-NAME (I-NEXTWORD I))
                                (I-PROG-SEGMENT I)))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-JUMP_X{SUBR}-OKP
      (I)
      (I-OBJECTP-TYPE 'SUBR (I-X I) I))

(DEFN I-JUMP_X{SUBR}-STEP
      (I)
      (I-STATE (TAG 'IPC (CONS (UNTAG (I-X I)) 0))
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-LSR_<C>_X_X{N}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'NAT (I-X I) I)))

(DEFN I-LSR_<C>_X_X{N}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (TAG 'NAT
                    (QUOTIENT (UNTAG (I-X I)) 2))
               (I-Y I)
               (BOOL (EQUAL (REMAINDER (UNTAG (I-X I)) 2)
                            1))
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-LSR_<TSP>_<TSP>{V}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'BITV
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-LSR_<TSP>_<TSP>{V}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'BITV
                             (RSH-BITV (UNTAG (FETCH (I-TSP I)
                                                     (I-SYS-DATA-SEGMENT I)))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE-C_<TSP>_*-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP (I-NEXTWORD I) I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))))

(DEFN I-MOVE-C_<TSP>_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (IF (EQUAL (UNTAG (I-C-FLG I)) 'F)
                   (I-SYS-DATA-SEGMENT I)
                   (DEPOSIT (I-NEXTWORD I)
                            (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE-V_<TSP>_*-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP (I-NEXTWORD I) I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))))

(DEFN I-MOVE-V_<TSP>_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (IF (EQUAL (UNTAG (I-V-FLG I)) 'F)
                   (I-SYS-DATA-SEGMENT I)
                   (DEPOSIT (I-NEXTWORD I)
                            (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE-Z_<TSP>_*-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP (I-NEXTWORD I) I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))))

(DEFN I-MOVE-Z_<TSP>_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (IF (EQUAL (UNTAG (I-Z-FLG I)) 'F)
                   (I-SYS-DATA-SEGMENT I)
                   (DEPOSIT (I-NEXTWORD I)
                            (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE-N_X_*-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP (I-NEXTWORD I) I)))

(DEFN I-MOVE-N_X_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (IF (EQUAL (UNTAG (I-N-FLG I)) 'F)
                   (I-X I)
                   (I-NEXTWORD I))
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_<TSP>_*-OKP
      (I)
      (AND (ADD2-I-PCP I)
           (I-OBJECTP (I-NEXTWORD I) I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))))

(DEFN I-MOVE_<TSP>_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (I-NEXTWORD I)
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_<X{A}>_<TSP>-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'ADDR (I-X I) I)))

(DEFN I-MOVE_<X{A}>_<TSP>-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (DEPOSIT (FETCH (I-TSP I)
                               (I-SYS-DATA-SEGMENT I))
                        (I-X I)
                        (I-USR-DATA-SEGMENT I))
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_<X{S}>_<TSP>-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'SYS-ADDR
                           (I-X I)
                           I)))

(DEFN I-MOVE_<X{S}>_<TSP>-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (FETCH (I-TSP I)
                               (I-SYS-DATA-SEGMENT I))
                        (I-X I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_CFP_CSP-OKP
      (I)
      (ADD1-I-PCP I))

(DEFN I-MOVE_CFP_CSP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CSP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_CSP_CFP-OKP
      (I)
      (ADD1-I-PCP I))

(DEFN I-MOVE_CSP_CFP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CFP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_X_*-OKP
      (I)
      (ADD2-I-PCP I))

(DEFN I-MOVE_X_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-NEXTWORD I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_X_<X{S}>-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'SYS-ADDR (I-X I) I)
           (I-OBJECTP (FETCH (I-X I) (I-SYS-DATA-SEGMENT I))
                      I)))

(DEFN I-MOVE_X_<X{S}>-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (FETCH (I-X I) (I-SYS-DATA-SEGMENT I))
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_X_TSP-OKP
      (I)
      (ADD1-I-PCP I))

(DEFN I-MOVE_X_TSP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-TSP I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_X_X-OKP
      (I)
      (ADD1-I-PCP I))

(DEFN I-MOVE_X_X-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_Y_*-OKP
      (I)
      (ADD2-I-PCP I))

(DEFN I-MOVE_Y_*-STEP
      (I)
      (I-STATE (ADD2-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-NEXTWORD I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_Y_<Y{S}>-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (I-OBJECTP-TYPE 'SYS-ADDR (I-Y I) I)
           (I-OBJECTP (FETCH (I-Y I) (I-SYS-DATA-SEGMENT I))
                      I)))

(DEFN I-MOVE_Y_<Y{S}>-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (FETCH (I-Y I) (I-SYS-DATA-SEGMENT I))
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-MOVE_Y_TSP-OKP
      (I)
      (ADD1-I-PCP I))

(DEFN I-MOVE_Y_TSP-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-TSP I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (I-SYS-DATA-SEGMENT I)
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-NEG_<TSP>_<TSP>{I}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'INT
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)
           (SMALL-INTEGERP (INEGATE (UNTAG (FETCH (I-TSP I)
                                                  (I-SYS-DATA-SEGMENT I))))
                           (I-WORD-SIZE I))))

(DEFN I-NEG_<TSP>_<TSP>{I}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-CSP I)
               (I-TSP I)
               (I-X I)
               (I-Y I)
               (I-C-FLG I)
               (I-V-FLG I)
               (I-N-FLG I)
               (I-Z-FLG I)
               (I-PROG-SEGMENT I)
               (I-USR-DATA-SEGMENT I)
               (DEPOSIT (TAG 'INT
                             (INEGATE (UNTAG (FETCH (I-TSP I)
                                                    (I-SYS-DATA-SEGMENT I)))))
                        (I-TSP I)
                        (I-SYS-DATA-SEGMENT I))
               (I-WORD-SIZE I)
               'RUN))

(DEFN I-NOT_<TSP>_<TSP>{V}-OKP
      (I)
      (AND (ADD1-I-PCP I)
           (NOT (EMPTY-STKP (I-TSP I)
                            (I-SYS-DATA-SEGMENT I)))
           (I-OBJECTP-TYPE 'BITV
                           (FETCH (I-TSP I)
                                  (I-SYS-DATA-SEGMENT I))
                           I)))

(DEFN I-NOT_<TSP>_<TSP>{V}-STEP
      (I)
      (I-STATE (ADD1-I-PC I)
               (I-CFP I)
               (I-