(NOTE-LIB "fm9001-replay" T) Loading ./fm9001-piton/fm9001-replay.lib Finished loading ./fm9001-piton/fm9001-replay.lib Loading ./fm9001-piton/fm9001-replay.o Loading ./fm9001-piton/0fm9001-replay.o Finished loading ./fm9001-piton/0fm9001-replay.o Loading ./fm9001-piton/1fm9001-replay.o Finished loading ./fm9001-piton/1fm9001-replay.o Loading ./fm9001-piton/2fm9001-replay.o Finished loading ./fm9001-piton/2fm9001-replay.o Loading ./fm9001-piton/3fm9001-replay.o Finished loading ./fm9001-piton/3fm9001-replay.o Finished loading ./fm9001-piton/fm9001-replay.o (#./fm9001-piton/fm9001-replay.lib #./fm9001-piton/fm9001-replay) (SET-STATUS CLOSE-DATA-BASE-1 T ((BOOT-STRAP INITIAL) (ADD-SHELL ENABLE) ((DEFN *1*DEFN) ENABLE) (OTHERWISE DISABLE))) [ 0.8 0.0 0.0 ] CLOSE-DATA-BASE-1 (DEFN INCR (C X) (IF (NLISTP X) NIL (CONS (XOR C (CAR X)) (INCR (AND C (CAR X)) (CDR X))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, INCR is accepted under the definitional principle. From the definition we can conclude that (OR (LITATOM (INCR C X)) (LISTP (INCR C X))) is a theorem. [ 0.0 0.0 0.0 ] INCR (DEFN BITN (X N) (COND ((ZEROP N) F) ((EQUAL N 1) (CAR X)) (T (BITN (CDR X) (SUB1 N))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, BITN is accepted under the definitional principle. [ 0.0 0.0 0.0 ] BITN (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))) [ 0.1 0.0 0.0 ] P-STATE (DEFN ERRORP (PSW) (AND (NOT (EQUAL PSW 'RUN)) (NOT (EQUAL PSW 'HALT)))) Note that (OR (FALSEP (ERRORP PSW)) (TRUEP (ERRORP PSW))) is a theorem. [ 0.0 0.0 0.0 ] ERRORP (DEFN DEFINITION (NAME ALIST) (ASSOC NAME ALIST)) [ 0.0 0.0 0.0 ] DEFINITION (DEFN STRIP-CDRS (ALIST) (IF (NLISTP ALIST) NIL (CONS (CDAR ALIST) (STRIP-CDRS (CDR ALIST))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT ALIST) decreases according to the well-founded relation LESSP in each recursive call. Hence, STRIP-CDRS is accepted under the definitional principle. Observe that: (OR (LITATOM (STRIP-CDRS ALIST)) (LISTP (STRIP-CDRS ALIST))) is a theorem. [ 0.0 0.0 0.0 ] STRIP-CDRS (DEFN NAME (D) (CAR D)) [ 0.0 0.0 0.0 ] NAME (DEFN FORMAL-VARS (D) (CADR D)) [ 0.0 0.0 0.0 ] FORMAL-VARS (DEFN TEMP-VAR-DCLS (D) (CADDR D)) [ 0.0 0.0 0.0 ] TEMP-VAR-DCLS (DEFN PROGRAM-BODY (D) (CDDDR D)) [ 0.0 0.0 0.0 ] PROGRAM-BODY (DEFN LOCAL-VARS (D) (APPEND (FORMAL-VARS D) (STRIP-CARS (TEMP-VAR-DCLS D)))) From the definition we can conclude that: (OR (LITATOM (LOCAL-VARS D)) (LISTP (LOCAL-VARS D))) is a theorem. [ 0.0 0.0 0.0 ] LOCAL-VARS (DEFN ADP-NAME (ADP) (CAR ADP)) [ 0.0 0.0 0.0 ] ADP-NAME (DEFN ADP-OFFSET (ADP) (CDR ADP)) [ 0.0 0.0 0.0 ] ADP-OFFSET (DEFN SUB-ADP (ADP N) (CONS (ADP-NAME ADP) (DIFFERENCE (ADP-OFFSET ADP) N))) Note that (LISTP (SUB-ADP ADP N)) is a theorem. [ 0.0 0.0 0.0 ] SUB-ADP (DEFN GET (N LST) (IF (ZEROP N) (CAR LST) (GET (SUB1 N) (CDR LST)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, GET is accepted under the principle of definition. [ 0.0 0.0 0.0 ] GET (DEFN TAG (TYPE OBJ) (LIST TYPE OBJ)) From the definition we can conclude that (LISTP (TAG TYPE OBJ)) is a theorem. [ 0.0 0.0 0.0 ] TAG (DEFN TYPE (CONST) (CAR CONST)) [ 0.0 0.0 0.0 ] TYPE (DEFN UNTAG (CONST) (CADR CONST)) [ 0.0 0.0 0.0 ] UNTAG (DEFN AREA-NAME (X) (ADP-NAME (UNTAG X))) [ 0.0 0.0 0.0 ] AREA-NAME (DEFN SUB-ADDR (ADDR N) (TAG (TYPE ADDR) (SUB-ADP (UNTAG ADDR) N))) Note that (LISTP (SUB-ADDR ADDR N)) is a theorem. [ 0.0 0.0 0.0 ] SUB-ADDR (DEFN TOP (STK) (CAR STK)) [ 0.0 0.0 0.0 ] TOP (DEFN POP (STK) (CDR STK)) [ 0.0 0.0 0.0 ] POP (DEFN DL (LAB COMMENT INS) (LIST 'DL LAB COMMENT INS)) From the definition we can conclude that (LISTP (DL LAB COMMENT INS)) is a theorem. [ 0.0 0.0 0.0 ] DL (DEFN LABELLEDP (X) (EQUAL (CAR X) 'DL)) Observe that (OR (FALSEP (LABELLEDP X)) (TRUEP (LABELLEDP X))) is a theorem. [ 0.0 0.0 0.0 ] LABELLEDP (DEFN UNLABEL (X) (IF (LABELLEDP X) (CADDDR X) X)) [ 0.0 0.0 0.0 ] UNLABEL (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)))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of AND, LABELLEDP, and NLISTP establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, FIND-LABEL is accepted under the principle of definition. Note that (NUMBERP (FIND-LABEL X LST)) is a theorem. [ 0.0 0.0 0.0 ] FIND-LABEL (DEFN PC (LAB PROGRAM) (TAG 'PC (CONS (NAME PROGRAM) (FIND-LABEL LAB (PROGRAM-BODY PROGRAM))))) Observe that (LISTP (PC LAB PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] PC (DEFN BINDINGS (FRAME) (CAR FRAME)) [ 0.0 0.0 0.0 ] BINDINGS (DEFN RET-PC (FRAME) (CADR FRAME)) [ 0.0 0.0 0.0 ] RET-PC (DEFN P-FRAME-SIZE (FRAME) (PLUS 2 (LENGTH (BINDINGS FRAME)))) From the definition we can conclude that (NUMBERP (P-FRAME-SIZE FRAME)) is a theorem. [ 0.0 0.0 0.0 ] P-FRAME-SIZE (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))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT CTRL-STK) decreases according to the well-founded relation LESSP in each recursive call. Hence, P-CTRL-STK-SIZE is accepted under the definitional principle. Observe that: (NUMBERP (P-CTRL-STK-SIZE CTRL-STK)) is a theorem. [ 0.0 0.0 0.0 ] P-CTRL-STK-SIZE (DEFN ICODE-CALL (INS PCN PROGRAM) (LIST '(CPUSH_*) (TAG 'PC (CONS (NAME PROGRAM) (ADD1 PCN))) '(JUMP_*) (TAG 'PC (CONS (CADR INS) '(PRELUDE))))) Observe that (LISTP (ICODE-CALL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-CALL (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)))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT TEMP-VAR-DCLS) decreases according to the well-founded relation LESSP in each recursive call. Hence, GENERATE-PRELUDE1 is accepted under the definitional principle. From the definition we can conclude that: (OR (LITATOM (GENERATE-PRELUDE1 TEMP-VAR-DCLS)) (LISTP (GENERATE-PRELUDE1 TEMP-VAR-DCLS))) is a theorem. [ 0.0 0.0 0.0 ] GENERATE-PRELUDE1 (DEFN GENERATE-PRELUDE2 (FORMAL-VARS) (IF (NLISTP FORMAL-VARS) NIL (CONS '(CPUSH_+) (GENERATE-PRELUDE2 (CDR FORMAL-VARS))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT FORMAL-VARS) decreases according to the well-founded relation LESSP in each recursive call. Hence, GENERATE-PRELUDE2 is accepted under the definitional principle. Note that: (OR (LITATOM (GENERATE-PRELUDE2 FORMAL-VARS)) (LISTP (GENERATE-PRELUDE2 FORMAL-VARS))) is a theorem. [ 0.0 0.0 0.0 ] GENERATE-PRELUDE2 (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))))) Observe that: (OR (LITATOM (GENERATE-PRELUDE PROGRAM)) (LISTP (GENERATE-PRELUDE PROGRAM))) is a theorem. [ 0.0 0.0 0.0 ] GENERATE-PRELUDE (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)))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, FIND-POSITION-OF-VAR is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (FIND-POSITION-OF-VAR VAR LST)) is a theorem. [ 0.0 0.0 0.0 ] FIND-POSITION-OF-VAR (DEFN OFFSET-FROM-CSP (VAR PROGRAM) (FIND-POSITION-OF-VAR VAR (LOCAL-VARS PROGRAM))) Note that (NUMBERP (OFFSET-FROM-CSP VAR PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] OFFSET-FROM-CSP (DEFN GENERATE-POSTLUDE (PROGRAM) (CONS (DL (CONS (NAME PROGRAM) (LENGTH (PROGRAM-BODY PROGRAM))) '(POSTLUDE) '(MOVE_CSP_CFP)) '((CPOP_CFP) (CPOP_PC)))) Note that (LISTP (GENERATE-POSTLUDE PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] GENERATE-POSTLUDE (DEFN ICODE-RET (INS PCN PROGRAM) (LIST '(JUMP_*) (TAG 'PC (CONS (NAME PROGRAM) (LENGTH (PROGRAM-BODY PROGRAM)))))) WARNING: INS and PCN are in the arglist but not in the body of the definition of ICODE-RET. Observe that (LISTP (ICODE-RET INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-RET (DEFN ICODE-LOCN (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'NAT (OFFSET-FROM-CSP (CADR INS) PROGRAM)) '((ADD_X{N}_CSP) (MOVE_X_) (ADD_X{N}_CSP) (TPUSH_))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-LOCN. Note that (LISTP (ICODE-LOCN INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-LOCN (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))))) From the definition we can conclude that: (LISTP (ICODE-PUSH-CONSTANT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSH-CONSTANT (DEFN ICODE-PUSH-LOCAL (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'NAT (OFFSET-FROM-CSP (CADR INS) PROGRAM)) '((ADD_X{N}_CSP) (TPUSH_))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-PUSH-LOCAL. From the definition we can conclude that: (LISTP (ICODE-PUSH-LOCAL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSH-LOCAL (DEFN ICODE-PUSH-GLOBAL (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'ADDR (CONS (CADR INS) 0)) '((TPUSH_))))) WARNING: PCN and PROGRAM are in the arglist but not in the body of the definition of ICODE-PUSH-GLOBAL. From the definition we can conclude that: (LISTP (ICODE-PUSH-GLOBAL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSH-GLOBAL (DEFN ICODE-PUSH-CTRL-STK-FREE-SIZE (INS PCN PROGRAM) '((MOVE_X_*) (SYS-ADDR (FULL-CTRL-STK-ADDR . 0)) (MOVE_X_) (TPUSH_CSP) (SUB_{S}_X{S}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-PUSH-CTRL-STK-FREE-SIZE. Observe that (LISTP (ICODE-PUSH-CTRL-STK-FREE-SIZE INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSH-CTRL-STK-FREE-SIZE (DEFN ICODE-PUSH-TEMP-STK-FREE-SIZE (INS PCN PROGRAM) '((MOVE_X_*) (SYS-ADDR (FULL-TEMP-STK-ADDR . 0)) (MOVE_X_) (TPUSH_TSP) (SUB_{S}_X{S}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-PUSH-TEMP-STK-FREE-SIZE. Observe that (LISTP (ICODE-PUSH-TEMP-STK-FREE-SIZE INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSH-TEMP-STK-FREE-SIZE (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_) (CONS '(SUB__X{S}_Y{S}) (CONS '(TPUSH_X) (CONS '(MOVE_X_*) (CONS (TAG 'NAT (ADD1 (CADR INS))) '((SUB_{N}_X{N}))))))))))) WARNING: PCN and PROGRAM are in the arglist but not in the body of the definition of ICODE-PUSH-TEMP-STK-INDEX. Note that (LISTP (ICODE-PUSH-TEMP-STK-INDEX INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSH-TEMP-STK-INDEX (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_) (CONS '(SUB__X{S}_Y{S}) (CONS '(MOVE_X_*) (CONS (PC (CADR INS) PROGRAM) '((JUMP-Z_X)))))))))) WARNING: PCN is in the arglist but not in the body of the definition of: ICODE-JUMP-IF-TEMP-STK-FULL. From the definition we can conclude that: (LISTP (ICODE-JUMP-IF-TEMP-STK-FULL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-JUMP-IF-TEMP-STK-FULL (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_) (CONS '(SUB__X{S}_Y{S}) (CONS '(MOVE_X_*) (CONS (PC (CADR INS) PROGRAM) '((JUMP-Z_X)))))))))) WARNING: PCN is in the arglist but not in the body of the definition of: ICODE-JUMP-IF-TEMP-STK-EMPTY. From the definition we can conclude that: (LISTP (ICODE-JUMP-IF-TEMP-STK-EMPTY INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-JUMP-IF-TEMP-STK-EMPTY (DEFN ICODE-POP (INS PCN PROGRAM) '((TPOP_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-POP. Note that (LISTP (ICODE-POP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POP (DEFN ICODE-POP* (INS PCN PROGRAM) (LIST '(ADD_TSP_*{N}) (TAG 'NAT (CADR INS)))) WARNING: PCN and PROGRAM are in the arglist but not in the body of the definition of ICODE-POP*. Note that (LISTP (ICODE-POP* INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POP* (DEFN ICODE-POPN (INS PCN PROGRAM) '((TPOP_X) (ADD_TSP_X{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-POPN. Note that (LISTP (ICODE-POPN INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POPN (DEFN ICODE-POP-LOCAL (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'NAT (OFFSET-FROM-CSP (CADR INS) PROGRAM)) '((ADD_X{N}_CSP) (TPOP_))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-POP-LOCAL. From the definition we can conclude that: (LISTP (ICODE-POP-LOCAL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POP-LOCAL (DEFN ICODE-POP-GLOBAL (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'ADDR (CONS (CADR INS) 0)) '((TPOP_))))) WARNING: PCN and PROGRAM are in the arglist but not in the body of the definition of ICODE-POP-GLOBAL. From the definition we can conclude that: (LISTP (ICODE-POP-GLOBAL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POP-GLOBAL (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_) (ADD_X{N}_CSP) (TPOP_))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-POP-LOCN. Note that (LISTP (ICODE-POP-LOCN INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POP-LOCN (DEFN ICODE-POP-CALL (INS PCN PROGRAM) (CONS '(TPOP_X) (CONS '(CPUSH_*) (CONS (TAG 'PC (CONS (NAME PROGRAM) (ADD1 PCN))) '((JUMP_X{SUBR})))))) WARNING: INS is in the arglist but not in the body of the definition of ICODE-POP-CALL. Note that (LISTP (ICODE-POP-CALL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POP-CALL (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_) (SUB_X{S}_Y{N}) (TPUSH_))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-FETCH-TEMP-STK. From the definition we can conclude that: (LISTP (ICODE-FETCH-TEMP-STK INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-FETCH-TEMP-STK (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_) (SUB_X{S}_Y{N}) (TPOP_))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-DEPOSIT-TEMP-STK. From the definition we can conclude that: (LISTP (ICODE-DEPOSIT-TEMP-STK INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-DEPOSIT-TEMP-STK (DEFN ICODE-JUMP (INS PCN PROGRAM) (LIST '(JUMP_*) (PC (CADR INS) PROGRAM))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-JUMP. From the definition we can conclude that: (LISTP (ICODE-JUMP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-JUMP (DEFN JUMP_*-LST (LST PROGRAM) (IF (NLISTP LST) NIL (CONS '(JUMP_*) (CONS (PC (CAR LST) PROGRAM) (JUMP_*-LST (CDR LST) PROGRAM))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, JUMP_*-LST is accepted under the principle of definition. Note that: (OR (LITATOM (JUMP_*-LST LST PROGRAM)) (LISTP (JUMP_*-LST LST PROGRAM))) is a theorem. [ 0.0 0.0 0.0 ] JUMP_*-LST (DEFN ICODE-JUMP-CASE (INS PCN PROGRAM) (APPEND '((TPOP_X) (ADD_X_X{N}) (ADD_PC_X{N})) (JUMP_*-LST (CDR INS) PROGRAM))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-JUMP-CASE. From the definition we can conclude that: (OR (LITATOM (ICODE-JUMP-CASE INS PCN PROGRAM)) (LISTP (ICODE-JUMP-CASE INS PCN PROGRAM))) is a theorem. [ 0.0 0.0 0.0 ] ICODE-JUMP-CASE (DEFN ICODE-PUSHJ (INS PCN PROGRAM) (LIST '(TPUSH_*) (TAG 'PC (CONS (NAME PROGRAM) (ADD1 PCN))) '(JUMP_*) (PC (CADR INS) PROGRAM))) Observe that (LISTP (ICODE-PUSHJ INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-PUSHJ (DEFN ICODE-POPJ (INS PCN PROGRAM) '((TPOP_PC))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-POPJ. Note that (LISTP (ICODE-POPJ INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-POPJ (DEFN ICODE-SET-LOCAL (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'NAT (OFFSET-FROM-CSP (CADR INS) PROGRAM)) '((ADD_X{N}_CSP) (MOVE__))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-SET-LOCAL. From the definition we can conclude that: (LISTP (ICODE-SET-LOCAL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SET-LOCAL (DEFN ICODE-SET-GLOBAL (INS PCN PROGRAM) (CONS '(MOVE_X_*) (CONS (TAG 'ADDR (CONS (CADR INS) 0)) '((MOVE__))))) WARNING: PCN and PROGRAM are in the arglist but not in the body of the definition of ICODE-SET-GLOBAL. From the definition we can conclude that: (LISTP (ICODE-SET-GLOBAL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SET-GLOBAL (DEFN ICODE-TEST-NAT-AND-JUMP (INS PCN PROGRAM) (IF (EQUAL (CADR INS) 'ZERO) (CONS '(TPOP{N}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-Z_X))))) (CONS '(TPOP{N}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-NZ_X))))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-TEST-NAT-AND-JUMP. Observe that (LISTP (ICODE-TEST-NAT-AND-JUMP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-TEST-NAT-AND-JUMP (DEFN ICODE-TEST-INT-AND-JUMP (INS PCN PROGRAM) (CASE (CAR (CDR INS)) (ZERO (CONS '(TPOP{I}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-Z_X)))))) (NOT-ZERO (CONS '(TPOP{I}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-NZ_X)))))) (NEG (CONS '(TPOP{I}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-N_X)))))) (NOT-NEG (CONS '(TPOP{I}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-NN_X)))))) (POS (LIST '(TPOP{I}__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}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-N_X) (JUMP-Z_X)))))))) From the definition we can conclude that: (LISTP (ICODE-TEST-INT-AND-JUMP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-TEST-INT-AND-JUMP (DEFN ICODE-TEST-BOOL-AND-JUMP (INS PCN PROGRAM) (IF (EQUAL (CADR INS) 'T) (CONS '(TPOP{B}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-NZ_X))))) (CONS '(TPOP{B}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-Z_X))))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-TEST-BOOL-AND-JUMP. Observe that (LISTP (ICODE-TEST-BOOL-AND-JUMP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-TEST-BOOL-AND-JUMP (DEFN ICODE-TEST-BITV-AND-JUMP (INS PCN PROGRAM) (IF (EQUAL (CADR INS) 'ALL-ZERO) (CONS '(TPOP{V}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-Z_X))))) (CONS '(TPOP{V}__Y) (CONS '(MOVE_X_*) (CONS (PC (CADDR INS) PROGRAM) '((JUMP-NZ_X))))))) WARNING: PCN is in the arglist but not in the body of the definition of ICODE-TEST-BITV-AND-JUMP. Observe that (LISTP (ICODE-TEST-BITV-AND-JUMP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-TEST-BITV-AND-JUMP (DEFN ICODE-NO-OP (INS PCN PROGRAM) '((MOVE_X_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-NO-OP. Note that (LISTP (ICODE-NO-OP INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-NO-OP (DEFN ICODE-ADD-ADDR (INS PCN PROGRAM) '((TPOP_X) (ADD_{A}_X{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD-ADDR. Note that (LISTP (ICODE-ADD-ADDR INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD-ADDR (DEFN ICODE-SUB-ADDR (INS PCN PROGRAM) '((TPOP_X) (SUB_{A}_X{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB-ADDR. Note that (LISTP (ICODE-SUB-ADDR INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB-ADDR (DEFN ICODE-EQ (INS PCN PROGRAM) '((TPOP_X) (XOR___X) (XOR__) (MOVE-Z__*) (BOOL T))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-EQ. From the definition we can conclude that: (LISTP (ICODE-EQ INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-EQ (DEFN ICODE-LT-ADDR (INS PCN PROGRAM) '((TPOP_X) (SUB__{A}_X{A}) (XOR__) (MOVE-C__*) (BOOL T))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-LT-ADDR. From the definition we can conclude that: (LISTP (ICODE-LT-ADDR INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-LT-ADDR (DEFN ICODE-FETCH (INS PCN PROGRAM) '((TPOP_X) (TPUSH_))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-FETCH. Note that (LISTP (ICODE-FETCH INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-FETCH (DEFN ICODE-DEPOSIT (INS PCN PROGRAM) '((TPOP_X) (TPOP_))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-DEPOSIT. Note that (LISTP (ICODE-DEPOSIT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-DEPOSIT (DEFN ICODE-ADD-INT (INS PCN PROGRAM) '((TPOP_X) (ADD_{I}_X{I}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD-INT. Note that (LISTP (ICODE-ADD-INT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD-INT (DEFN ICODE-ADD-INT-WITH-CARRY (INS PCN PROGRAM) '((TPOP_X) (TPOP_Y) (ASR___{B}) (ADDC__X{I}_Y{I}) (MOVE-V__*) (BOOL T) (TPUSH_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD-INT-WITH-CARRY. Note that (LISTP (ICODE-ADD-INT-WITH-CARRY INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD-INT-WITH-CARRY (DEFN ICODE-ADD1-INT (INS PCN PROGRAM) '((INCR__{I}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD1-INT. Note that (LISTP (ICODE-ADD1-INT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD1-INT (DEFN ICODE-SUB-INT (INS PCN PROGRAM) '((TPOP_X) (SUB_{I}_X{I}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB-INT. Note that (LISTP (ICODE-SUB-INT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB-INT (DEFN ICODE-SUB-INT-WITH-CARRY (INS PCN PROGRAM) '((TPOP_Y) (TPOP_X) (ASR___{B}) (SUBB__X{I}_Y{I}) (MOVE-V__*) (BOOL T) (TPUSH_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB-INT-WITH-CARRY. Note that (LISTP (ICODE-SUB-INT-WITH-CARRY INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB-INT-WITH-CARRY (DEFN ICODE-SUB1-INT (INS PCN PROGRAM) '((DECR__{I}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB1-INT. Note that (LISTP (ICODE-SUB1-INT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB1-INT (DEFN ICODE-NEG-INT (INS PCN PROGRAM) '((NEG__{I}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-NEG-INT. Note that (LISTP (ICODE-NEG-INT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-NEG-INT (DEFN ICODE-LT-INT (INS PCN PROGRAM) '((TPOP_X) (SUB__{I}_X{I}) (MOVE__*) (BOOL F) (MOVE-V__*) (BOOL T) (MOVE_X_*) (BOOL F) (MOVE-N_X_*) (BOOL T) (XOR_{B}_X{B}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-LT-INT. Observe that (LISTP (ICODE-LT-INT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-LT-INT (DEFN ICODE-INT-TO-NAT (INS PCN PROGRAM) '((INT-TO-NAT))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-INT-TO-NAT. Note that (LISTP (ICODE-INT-TO-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-INT-TO-NAT (DEFN ICODE-ADD-NAT (INS PCN PROGRAM) '((TPOP_X) (ADD_{N}_X{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD-NAT. Note that (LISTP (ICODE-ADD-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD-NAT (DEFN ICODE-ADD-NAT-WITH-CARRY (INS PCN PROGRAM) '((TPOP_X) (TPOP_Y) (ASR___{B}) (ADDC__X{N}_Y{N}) (MOVE-C__*) (BOOL T) (TPUSH_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD-NAT-WITH-CARRY. Note that (LISTP (ICODE-ADD-NAT-WITH-CARRY INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD-NAT-WITH-CARRY (DEFN ICODE-ADD1-NAT (INS PCN PROGRAM) '((INCR__{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-ADD1-NAT. Note that (LISTP (ICODE-ADD1-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-ADD1-NAT (DEFN ICODE-SUB-NAT (INS PCN PROGRAM) '((TPOP_X) (SUB_{N}_X{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB-NAT. Note that (LISTP (ICODE-SUB-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB-NAT (DEFN ICODE-SUB-NAT-WITH-CARRY (INS PCN PROGRAM) '((TPOP_Y) (TPOP_X) (ASR___{B}) (SUBB__X{N}_Y{N}) (MOVE-C__*) (BOOL T) (TPUSH_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB-NAT-WITH-CARRY. Note that (LISTP (ICODE-SUB-NAT-WITH-CARRY INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB-NAT-WITH-CARRY (DEFN ICODE-SUB1-NAT (INS PCN PROGRAM) '((DECR__{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-SUB1-NAT. Note that (LISTP (ICODE-SUB1-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-SUB1-NAT (DEFN ICODE-LT-NAT (INS PCN PROGRAM) '((TPOP_X) (SUB__{N}_X{N}) (XOR__) (MOVE-C__*) (BOOL T))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-LT-NAT. From the definition we can conclude that: (LISTP (ICODE-LT-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-LT-NAT (DEFN ICODE-MULT2-NAT (INS PCN PROGRAM) '((ADD__{N}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-MULT2-NAT. Note that (LISTP (ICODE-MULT2-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-MULT2-NAT (DEFN ICODE-MULT2-NAT-WITH-CARRY-OUT (INS PCN PROGRAM) '((TPOP_X) (ADD__X_X{N}) (TPUSH_*) (BOOL F) (MOVE-C__*) (BOOL T) (TPUSH_X))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-MULT2-NAT-WITH-CARRY-OUT. From the definition we can conclude that: (LISTP (ICODE-MULT2-NAT-WITH-CARRY-OUT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-MULT2-NAT-WITH-CARRY-OUT (DEFN ICODE-DIV2-NAT (INS PCN PROGRAM) '((TPOP__X) (LSR__X_X{N}) (TPUSH_X) (TPUSH_*) (NAT 0) (MOVE-C__*) (NAT 1))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-DIV2-NAT. From the definition we can conclude that: (LISTP (ICODE-DIV2-NAT INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-DIV2-NAT (DEFN ICODE-OR-BITV (INS PCN PROGRAM) '((TPOP_X) (OR_{V}_X{V}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-OR-BITV. Note that (LISTP (ICODE-OR-BITV INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-OR-BITV (DEFN ICODE-AND-BITV (INS PCN PROGRAM) '((TPOP_X) (AND_{V}_X{V}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-AND-BITV. Note that (LISTP (ICODE-AND-BITV INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-AND-BITV (DEFN ICODE-NOT-BITV (INS PCN PROGRAM) '((NOT__{V}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-NOT-BITV. Note that (LISTP (ICODE-NOT-BITV INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-NOT-BITV (DEFN ICODE-XOR-BITV (INS PCN PROGRAM) '((TPOP_X) (XOR_{V}_X{V}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-XOR-BITV. Note that (LISTP (ICODE-XOR-BITV INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-XOR-BITV (DEFN ICODE-RSH-BITV (INS PCN PROGRAM) '((LSR__{V}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-RSH-BITV. Note that (LISTP (ICODE-RSH-BITV INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-RSH-BITV (DEFN ICODE-LSH-BITV (INS PCN PROGRAM) '((ADD__{V}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-LSH-BITV. Note that (LISTP (ICODE-LSH-BITV INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-LSH-BITV (DEFN ICODE-OR-BOOL (INS PCN PROGRAM) '((TPOP_X) (OR_{B}_X{B}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-OR-BOOL. Note that (LISTP (ICODE-OR-BOOL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-OR-BOOL (DEFN ICODE-AND-BOOL (INS PCN PROGRAM) '((TPOP_X) (AND_{B}_X{B}))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-AND-BOOL. Note that (LISTP (ICODE-AND-BOOL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-AND-BOOL (DEFN ICODE-NOT-BOOL (INS PCN PROGRAM) '((XOR_{B}_*{B}) (BOOL T))) WARNING: INS, PCN, and PROGRAM are in the arglist but not in the body of the definition of ICODE-NOT-BOOL. From the definition we can conclude that: (LISTP (ICODE-NOT-BOOL INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE-NOT-BOOL (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))))) From the definition we can conclude that: (OR (LITATOM (ICODE1 INS PCN PROG)) (LISTP (ICODE1 INS PCN PROG))) is a theorem. [ 0.1 0.0 0.0 ] ICODE1 (DEFN DL-BLOCK (LAB COMMENT BLOCK) (CONS (DL LAB COMMENT (CAR BLOCK)) (CDR BLOCK))) Observe that (LISTP (DL-BLOCK LAB COMMENT BLOCK)) is a theorem. [ 0.0 0.0 0.0 ] DL-BLOCK (DEFN ICODE (INS PCN PROGRAM) (DL-BLOCK (CONS (NAME PROGRAM) PCN) INS (ICODE1 (UNLABEL INS) PCN PROGRAM))) Note that (LISTP (ICODE INS PCN PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICODE (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)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, ICOMPILE-PROGRAM-BODY is accepted under the definitional principle. From the definition we can conclude that: (OR (LITATOM (ICOMPILE-PROGRAM-BODY LST PCN PROGRAM)) (LISTP (ICOMPILE-PROGRAM-BODY LST PCN PROGRAM))) is a theorem. [ 0.0 0.0 0.0 ] ICOMPILE-PROGRAM-BODY (DEFN ICOMPILE-PROGRAM (PROGRAM) (CONS (NAME PROGRAM) (APPEND (GENERATE-PRELUDE PROGRAM) (APPEND (ICOMPILE-PROGRAM-BODY (PROGRAM-BODY PROGRAM) 0 PROGRAM) (GENERATE-POSTLUDE PROGRAM))))) From the definition we can conclude that: (LISTP (ICOMPILE-PROGRAM PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] ICOMPILE-PROGRAM (DEFN ICOMPILE (PROGRAMS) (IF (NLISTP PROGRAMS) NIL (CONS (ICOMPILE-PROGRAM (CAR PROGRAMS)) (ICOMPILE (CDR PROGRAMS))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT PROGRAMS) decreases according to the well-founded relation LESSP in each recursive call. Hence, ICOMPILE is accepted under the definitional principle. Observe that: (OR (LITATOM (ICOMPILE PROGRAMS)) (LISTP (ICOMPILE PROGRAMS))) is a theorem. [ 0.0 0.0 0.0 ] ICOMPILE (DEFN SEGMENT-LENGTH (SEGMENT) (IF (NLISTP SEGMENT) 0 (PLUS (LENGTH (CDAR SEGMENT)) (SEGMENT-LENGTH (CDR SEGMENT))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT SEGMENT) decreases according to the well-founded relation LESSP in each recursive call. Hence, SEGMENT-LENGTH is accepted under the definitional principle. Note that: (NUMBERP (SEGMENT-LENGTH SEGMENT)) is a theorem. [ 0.0 0.0 0.0 ] SEGMENT-LENGTH (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)) Note that (NUMBERP (TOTAL-P-SYSTEM-SIZE P LOAD-ADDR)) is a theorem. [ 0.0 0.0 0.0 ] TOTAL-P-SYSTEM-SIZE (DEFN P-LOADABLEP (P LOAD-ADDR) (LESSP (TOTAL-P-SYSTEM-SIZE P LOAD-ADDR) (EXP 2 (P-WORD-SIZE P)))) Note that: (OR (FALSEP (P-LOADABLEP P LOAD-ADDR)) (TRUEP (P-LOADABLEP P LOAD-ADDR))) is a theorem. [ 0.0 0.0 0.0 ] P-LOADABLEP (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))) [ 0.1 0.0 0.0 ] R-STATE (DEFN NAT-0S (N) (IF (ZEROP N) NIL (CONS (TAG 'NAT 0) (NAT-0S (SUB1 N))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, NAT-0S is accepted under the principle of definition. Note that: (OR (LITATOM (NAT-0S N)) (LISTP (NAT-0S N))) is a theorem. [ 0.0 0.0 0.0 ] NAT-0S (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)))))) Note that (LISTP (P->R_TEMP-STK TEMP-STK MAX-TEMP-STK-SIZE)) is a theorem. [ 0.0 0.0 0.0 ] P->R_TEMP-STK (DEFN P->R_CSP (STK MAX) (TAG 'SYS-ADDR (CONS 'CSTK (DIFFERENCE MAX (P-CTRL-STK-SIZE STK))))) Observe that (LISTP (P->R_CSP STK MAX)) is a theorem. [ 0.0 0.0 0.0 ] P->R_CSP (DEFN P->R_CFP (STK MAX) (SUB-ADDR (P->R_CSP (POP STK) MAX) 2)) Note that (LISTP (P->R_CFP STK MAX)) is a theorem. [ 0.0 0.0 0.0 ] P->R_CFP (DEFN P->R_P-FRAME (PFRAME STK MAX) (APPEND (STRIP-CDRS (BINDINGS PFRAME)) (LIST (P->R_CFP STK MAX) (RET-PC PFRAME)))) Note that (LISTP (P->R_P-FRAME PFRAME STK MAX)) is a theorem. [ 0.0 0.0 0.0 ] P->R_P-FRAME (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)))) Linear arithmetic, the lemma CDR-LESSP, and the definitions of POP and NLISTP inform us that the measure (COUNT STK) decreases according to the well-founded relation LESSP in each recursive call. Hence, P->R_CTRL-STK1 is accepted under the definitional principle. Note that: (OR (LITATOM (P->R_CTRL-STK1 STK MAX)) (LISTP (P->R_CTRL-STK1 STK MAX))) is a theorem. [ 0.0 0.0 0.0 ] P->R_CTRL-STK1 (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)))))) From the definition we can conclude that (LISTP (P->R_CTRL-STK STK MAX)) is a theorem. [ 0.0 0.0 0.0 ] P->R_CTRL-STK (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))))) From the definition we can conclude that: (LISTP (P->R_SYS-DATA-SEGMENT CTRL-STK MAX-CTRL-STK-SIZE TEMP-STK MAX-TEMP-STK-SIZE)) is a theorem. [ 0.0 0.0 0.0 ] P->R_SYS-DATA-SEGMENT (DEFN P->R_TSP (STK MAX) (TAG 'SYS-ADDR (CONS 'TSTK (DIFFERENCE MAX (LENGTH STK))))) Observe that (LISTP (P->R_TSP STK MAX)) is a theorem. [ 0.0 0.0 0.0 ] P->R_TSP (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))) From the definition we can conclude that (R-STATEP (P->R P)) is a theorem. [ 0.0 0.0 0.0 ] P->R (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))) [ 0.1 0.0 0.0 ] I-STATE (DEFN R->I_PC (PC PROGRAMS) (TAG 'IPC (CONS (AREA-NAME PC) (FIND-LABEL (UNTAG PC) (CDR (ICOMPILE-PROGRAM (DEFINITION (AREA-NAME PC) PROGRAMS))))))) Note that (LISTP (R->I_PC PC PROGRAMS)) is a theorem. [ 0.0 0.0 0.0 ] R->I_PC (DEFN R->I_PSW (PSW) (IF (EQUAL PSW 'HALT) 'RUN PSW)) Note that (OR (LITATOM (R->I_PSW PSW)) (EQUAL (R->I_PSW PSW) PSW)) is a theorem. [ 0.0 0.0 0.0 ] R->I_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)))) Observe that (I-STATEP (R->I R)) is a theorem. [ 0.0 0.0 0.0 ] R->I (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))) [ 0.0 0.0 0.0 ] M-STATE (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))))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT SEGMENT) decreases according to the well-founded relation LESSP in each recursive call. Hence, LINK-TABLE-FOR-SEGMENT is accepted under the definitional principle. Observe that: (OR (LITATOM (LINK-TABLE-FOR-SEGMENT SEGMENT ADDR0)) (LISTP (LINK-TABLE-FOR-SEGMENT SEGMENT ADDR0))) is a theorem. [ 0.0 0.0 0.0 ] LINK-TABLE-FOR-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))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of LABELLEDP and NLISTP can be used to prove that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, LINK-TABLE-FOR-LABELS is accepted under the principle of definition. Note that: (OR (LITATOM (LINK-TABLE-FOR-LABELS LST ADDR0)) (LISTP (LINK-TABLE-FOR-LABELS LST ADDR0))) is a theorem. [ 0.0 0.0 0.0 ] LINK-TABLE-FOR-LABELS (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))))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT SEGMENT) decreases according to the well-founded relation LESSP in each recursive call. Hence, LINK-TABLE-FOR-PROG-LABELS is accepted under the definitional principle. From the definition we can conclude that: (OR (LITATOM (LINK-TABLE-FOR-PROG-LABELS SEGMENT ADDR0)) (LISTP (LINK-TABLE-FOR-PROG-LABELS SEGMENT ADDR0))) is a theorem. [ 0.0 0.0 0.0 ] LINK-TABLE-FOR-PROG-LABELS (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)))))) Observe that (LISTP (I-LINK-TABLES I LOAD-ADDR)) is a theorem. [ 0.0 0.0 0.0 ] I-LINK-TABLES (DEFN PROG-LINKS (LINK-TABLES) (CAR LINK-TABLES)) [ 0.0 0.0 0.0 ] PROG-LINKS (DEFN PROG-LABEL-TABLES (LINK-TABLES) (CADR LINK-TABLES)) [ 0.0 0.0 0.0 ] PROG-LABEL-TABLES (DEFN USR-DATA-LINKS (LINK-TABLES) (CADDR LINK-TABLES)) [ 0.0 0.0 0.0 ] USR-DATA-LINKS (DEFN SYS-DATA-LINKS (LINK-TABLES) (CADDDR LINK-TABLES)) [ 0.0 0.0 0.0 ] SYS-DATA-LINKS (DEFN LABEL-LINKS (LABEL PROG-LABEL-TABLES) (CDR (ASSOC (ADP-NAME LABEL) PROG-LABEL-TABLES))) [ 0.0 0.0 0.0 ] LABEL-LINKS (DEFN BASE-ADDRESS (NAME LINK-TABLE) (CDR (ASSOC NAME LINK-TABLE))) [ 0.0 0.0 0.0 ] BASE-ADDRESS (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))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of AND, NOT, and NLISTP establish that the measure (COUNT LINK-TABLE) decreases according to the well-founded relation LESSP in each recursive call. Hence, FIND-CONTAINING-AREA-NAME is accepted under the definitional principle. [ 0.0 0.0 0.0 ] FIND-CONTAINING-AREA-NAME (DEFN INVERT-BASE-ADDRESS (N LINK-TABLE) (FIND-CONTAINING-AREA-NAME N LINK-TABLE)) [ 0.0 0.0 0.0 ] INVERT-BASE-ADDRESS (DEFN LABEL-ADDRESS (LABEL PROG-LABEL-TABLES) (BASE-ADDRESS LABEL (LABEL-LINKS LABEL PROG-LABEL-TABLES))) [ 0.0 0.0 0.0 ] LABEL-ADDRESS (DEFN ASSOC-CDRP (N ALIST) (COND ((NLISTP ALIST) F) ((EQUAL N (CDAR ALIST)) T) (T (ASSOC-CDRP N (CDR ALIST))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT ALIST) decreases according to the well-founded relation LESSP in each recursive call. Hence, ASSOC-CDRP is accepted under the definitional principle. From the definition we can conclude that: (OR (FALSEP (ASSOC-CDRP N ALIST)) (TRUEP (ASSOC-CDRP N ALIST))) is a theorem. [ 0.0 0.0 0.0 ] ASSOC-CDRP (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))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to establish that the measure (COUNT LABEL-TABLES) decreases according to the well-founded relation LESSP in each recursive call. Hence, FIND-CONTAINING-LABEL-TABLE is accepted under the principle of definition. [ 0.0 0.0 0.0 ] FIND-CONTAINING-LABEL-TABLE (DEFN INVERT-LABEL-ADDRESS (N PROG-LABEL-TABLES) (INVERT-BASE-ADDRESS N (FIND-CONTAINING-LABEL-TABLE N PROG-LABEL-TABLES))) [ 0.0 0.0 0.0 ] INVERT-LABEL-ADDRESS (DEFN ABSOLUTE-ADDRESS (ADP LINK-TABLE) (PLUS (BASE-ADDRESS (ADP-NAME ADP) LINK-TABLE) (ADP-OFFSET ADP))) Note that (NUMBERP (ABSOLUTE-ADDRESS ADP LINK-TABLE)) is a theorem. [ 0.0 0.0 0.0 ] ABSOLUTE-ADDRESS (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)))) Observe that (LISTP (INVERT-ABSOLUTE-ADDRESS N LINK-TABLE)) is a theorem. [ 0.0 0.0 0.0 ] INVERT-ABSOLUTE-ADDRESS (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))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT WORD-SIZE) decreases according to the well-founded relation LESSP in each recursive call. Hence, BITV-TO-V is accepted under the definitional principle. Observe that: (OR (LITATOM (BITV-TO-V LST WORD-SIZE)) (LISTP (BITV-TO-V LST WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] BITV-TO-V (DEFN V-TO-BITV (V) (IF (NLISTP V) NIL (APPEND (V-TO-BITV (CDR V)) (LIST (IF (CAR V) 1 0))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT V) decreases according to the well-founded relation LESSP in each recursive call. Hence, V-TO-BITV is accepted under the principle of definition. From the definition we can conclude that (OR (LITATOM (V-TO-BITV V)) (LISTP (V-TO-BITV V))) is a theorem. [ 0.0 0.0 0.0 ] V-TO-BITV (DEFN BOOL-TO-V (B WORD-SIZE) (IF (EQUAL B 'F) (NAT-TO-V 0 WORD-SIZE) (NAT-TO-V 1 WORD-SIZE))) From the definition we can conclude that: (OR (LITATOM (BOOL-TO-V B WORD-SIZE)) (LISTP (BOOL-TO-V B WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] BOOL-TO-V (DEFN V-TO-BOOL (V) (IF (CAR V) 'T 'F)) Observe that (LITATOM (V-TO-BOOL V)) is a theorem. [ 0.0 0.0 0.0 ] V-TO-BOOL (DEFN ADDR-TO-V (ADP USR-DATA-LINKS WORD-SIZE) (NAT-TO-V (ABSOLUTE-ADDRESS ADP USR-DATA-LINKS) WORD-SIZE)) Note that: (OR (LITATOM (ADDR-TO-V ADP USR-DATA-LINKS WORD-SIZE)) (LISTP (ADDR-TO-V ADP USR-DATA-LINKS WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] ADDR-TO-V (DEFN V-TO-ADDR (V USR-DATA-LINKS) (INVERT-ABSOLUTE-ADDRESS (V-TO-NAT V) USR-DATA-LINKS)) Note that (LISTP (V-TO-ADDR V USR-DATA-LINKS)) is a theorem. [ 0.0 0.0 0.0 ] V-TO-ADDR (DEFN SUBR-TO-V (SUBR PROG-LINKS WORD-SIZE) (NAT-TO-V (BASE-ADDRESS SUBR PROG-LINKS) WORD-SIZE)) Note that: (OR (LITATOM (SUBR-TO-V SUBR PROG-LINKS WORD-SIZE)) (LISTP (SUBR-TO-V SUBR PROG-LINKS WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] SUBR-TO-V (DEFN V-TO-SUBR (V PROG-LINKS) (INVERT-BASE-ADDRESS (V-TO-NAT V) PROG-LINKS)) [ 0.0 0.0 0.0 ] V-TO-SUBR (DEFN SYS-ADDR-TO-V (ADP SYS-DATA-LINKS WORD-SIZE) (NAT-TO-V (ABSOLUTE-ADDRESS ADP SYS-DATA-LINKS) WORD-SIZE)) Note that: (OR (LITATOM (SYS-ADDR-TO-V ADP SYS-DATA-LINKS WORD-SIZE)) (LISTP (SYS-ADDR-TO-V ADP SYS-DATA-LINKS WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] SYS-ADDR-TO-V (DEFN V-TO-SYS-ADDR (V SYS-DATA-LINKS) (INVERT-ABSOLUTE-ADDRESS (V-TO-NAT V) SYS-DATA-LINKS)) Note that (LISTP (V-TO-SYS-ADDR V SYS-DATA-LINKS)) is a theorem. [ 0.0 0.0 0.0 ] V-TO-SYS-ADDR (DEFN LABEL-TO-V (ILAB PROG-LABEL-TABLES WORD-SIZE) (NAT-TO-V (LABEL-ADDRESS ILAB PROG-LABEL-TABLES) WORD-SIZE)) Note that: (OR (LITATOM (LABEL-TO-V ILAB PROG-LABEL-TABLES WORD-SIZE)) (LISTP (LABEL-TO-V ILAB PROG-LABEL-TABLES WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LABEL-TO-V (DEFN V-TO-LABEL (V PROG-LABEL-TABLES) (INVERT-LABEL-ADDRESS (V-TO-NAT V) PROG-LABEL-TABLES)) [ 0.0 0.0 0.0 ] V-TO-LABEL (DEFN IPC-TO-V (PCPP PROG-LINKS WORD-SIZE) (NAT-TO-V (ABSOLUTE-ADDRESS PCPP PROG-LINKS) WORD-SIZE)) Note that: (OR (LITATOM (IPC-TO-V PCPP PROG-LINKS WORD-SIZE)) (LISTP (IPC-TO-V PCPP PROG-LINKS WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] IPC-TO-V (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)))) Observe that: (OR (LITATOM (LINK-DATA-WORD X LINK-TABLES WORD-SIZE)) (LISTP (LINK-DATA-WORD X LINK-TABLES WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LINK-DATA-WORD (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)))) Observe that (LISTP (UNLINK-DATA-WORD TYPE V LINK-TABLES)) is a theorem. [ 0.0 0.0 0.0 ] UNLINK-DATA-WORD (DEFN LINK-INSTRUCTION-ALIST NIL '((ADD__X_X{N} (ADD (C) X X)) (ADD__{V} (ADD NIL (TSP) (TSP))) (ADD__{N} (ADD NIL (TSP) (TSP))) (ADD_{A}_X{N} (ADD NIL (TSP) X)) (ADD_TSP_*{N} (ADD NIL TSP (PC 1))) (ADD_TSP_X{N} (ADD NIL TSP X)) (ADD_{I}_X{I} (ADD NIL (TSP) X)) (ADD_{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__X{N}_Y{N} (ADDC (C) X Y)) (ADDC__X{I}_Y{I} (ADDC (V) X Y)) (AND_{V}_X{V} (AND NIL (TSP) X)) (AND_{B}_X{B} (AND NIL (TSP) X)) (ASR___{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_+ (MOVE NIL (-1 CSP) (TSP 1))) (CPUSH_CFP (MOVE NIL (-1 CSP) CFP)) (DECR__{I} (DECR NIL (TSP) (TSP))) (DECR__{N} (DECR NIL (TSP) (TSP))) (INCR__{I} (INCR NIL (TSP) (TSP))) (INCR__{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__X_X{N} (LSR (C) X X)) (LSR__{V} (LSR NIL (TSP) (TSP))) (MOVE-C__* (MOVE-C NIL (TSP) (PC 1))) (MOVE-V__* (MOVE-V NIL (TSP) (PC 1))) (MOVE-Z__* (MOVE-Z NIL (TSP) (PC 1))) (MOVE-N_X_* (MOVE-N NIL X (PC 1))) (MOVE__* (MOVE NIL (TSP) (PC 1))) (MOVE__ (MOVE NIL (X) (TSP))) (MOVE__ (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_ (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_ (MOVE NIL Y (Y))) (MOVE_Y_TSP (MOVE NIL Y TSP)) (NEG__{I} (NEG NIL (TSP) (TSP))) (NOT__{V} (NOT NIL (TSP) (TSP))) (OR_{V}_X{V} (OR NIL (TSP) X)) (OR_{B}_X{B} (OR NIL (TSP) X)) (SUB__{A}_X{A} (SUB (C) (TSP) X)) (SUB__{N}_X{N} (SUB (C) (TSP) X)) (SUB__{I}_X{I} (SUB (N V) (TSP) X)) (SUB_{A}_X{N} (SUB NIL (TSP) X)) (SUB_X{S}_Y{N} (SUB NIL X Y)) (SUB_{I}_X{I} (SUB NIL (TSP) X)) (SUB_{N}_X{N} (SUB NIL (TSP) X)) (SUB_{S}_X{S} (SUB NIL (TSP) X)) (SUB__X{S}_Y{S} (SUB (Z) X Y)) (SUBB__X{N}_Y{N} (SUBB (C) X Y)) (SUBB__X{I}_Y{I} (SUBB (V) X Y)) (TPOP__X (MOVE (C) X (TSP 1))) (TPOP_ (MOVE NIL (X) (TSP 1))) (TPOP_ (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}__Y (MOVE (Z) Y (TSP 1))) (TPOP{B}__Y (MOVE (Z) Y (TSP 1))) (TPOP{I}__Y (MOVE (Z N) Y (TSP 1))) (TPOP{N}__Y (MOVE (Z) Y (TSP 1))) (TPUSH_* (MOVE NIL (-1 TSP) (PC 1))) (TPUSH_ (MOVE NIL (-1 TSP) (X))) (TPUSH_ (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__ (XOR NIL (TSP) (TSP))) (XOR_{V}_X{V} (XOR NIL (TSP) X)) (XOR_{B}_*{B} (XOR NIL (TSP) (PC 1))) (XOR_{B}_X{B} (XOR NIL (TSP) X)) (XOR___X (XOR (Z) (TSP) X)))) From the definition we can conclude that (LISTP (LINK-INSTRUCTION-ALIST)) is a theorem. [ 0.0 0.0 0.0 ] LINK-INSTRUCTION-ALIST (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 MODE-A (EXP 2 4)) REG-A) WORD-SIZE)) Observe that: (OR (LITATOM (PACK-INSTRUCTION OP MOVE-BITS CVNZ MODE-B REG-B MODE-A REG-A WORD-SIZE)) (LISTP (PACK-INSTRUCTION OP MOVE-BITS CVNZ MODE-B REG-B MODE-A REG-A WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] PACK-INSTRUCTION (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))))) [ 0.0 0.0 0.0 ] EXTRACT-OP (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))) From the definition we can conclude that: (NUMBERP (EXTRACT-MOVE-BITS OPCODE)) is a theorem. [ 0.0 0.0 0.0 ] EXTRACT-MOVE-BITS (DEFN EXTRACT-MODE (REG-SPEC) (COND ((LITATOM REG-SPEC) 0) ((EQUAL (CDR REG-SPEC) NIL) 1) ((EQUAL (CAR REG-SPEC) -1) 2) (T 3))) Note that (NUMBERP (EXTRACT-MODE REG-SPEC)) is a theorem. [ 0.0 0.0 0.0 ] EXTRACT-MODE (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)))) From the definition we can conclude that: (NUMBERP (EXTRACT-CVNZ FLG-NAMES)) is a theorem. [ 0.0 0.0 0.0 ] EXTRACT-CVNZ (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)))) [ 0.0 0.0 0.0 ] EXTRACT-REG1 (DEFN EXTRACT-REG (REG-SPEC) (CADR (ASSOC (EXTRACT-REG1 REG-SPEC) '((PC 15) (CFP 1) (CSP 2) (TSP 3) (X 4) (Y 5))))) [ 0.0 0.0 0.0 ] EXTRACT-REG (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)) Observe that: (OR (LITATOM (MCI INS WORD-SIZE)) (LISTP (MCI INS WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] MCI (DEFN ICODE-INSTRUCTIONP (INS) (EQUAL (CDR INS) NIL)) Observe that: (OR (FALSEP (ICODE-INSTRUCTIONP INS)) (TRUEP (ICODE-INSTRUCTIONP INS))) is a theorem. [ 0.0 0.0 0.0 ] ICODE-INSTRUCTIONP (DEFN LINK-INSTR-WORD (INS WORD-SIZE) (MCI (CADR (ASSOC (CAR INS) (LINK-INSTRUCTION-ALIST))) WORD-SIZE)) Note that: (OR (LITATOM (LINK-INSTR-WORD INS WORD-SIZE)) (LISTP (LINK-INSTR-WORD INS WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LINK-INSTR-WORD (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))) From the definition we can conclude that: (OR (LITATOM (LINK-WORD X LINK-TABLES WORD-SIZE)) (LISTP (LINK-WORD X LINK-TABLES WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LINK-WORD (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)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, LINK-AREA is accepted under the definitional principle. From the definition we can conclude that: (OR (LITATOM (LINK-AREA LST LINK-TABLES WORD-SIZE)) (LISTP (LINK-AREA LST LINK-TABLES WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LINK-AREA (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)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT SEGMENT) decreases according to the well-founded relation LESSP in each recursive call. Hence, LINK-SEGMENT is accepted under the definitional principle. From the definition we can conclude that: (OR (LITATOM (LINK-SEGMENT SEGMENT LINK-TABLES WORD-SIZE)) (LISTP (LINK-SEGMENT SEGMENT LINK-TABLES WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LINK-SEGMENT (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)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, BOOT-CODE is accepted under the definitional principle. Observe that: (OR (LITATOM (BOOT-CODE LST N WORD-SIZE)) (LISTP (BOOT-CODE LST N WORD-SIZE))) is a theorem. [ 0.3 0.0 0.0 ] BOOT-CODE (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))))) Note that: (OR (LITATOM (LINK-MEM BOOT-LST LOAD-ADDR USR-DATA-SEGMENT PROG-SEGMENT SYS-DATA-SEGMENT LINK-TABLES WORD-SIZE)) (LISTP (LINK-MEM BOOT-LST LOAD-ADDR USR-DATA-SEGMENT PROG-SEGMENT SYS-DATA-SEGMENT LINK-TABLES WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] LINK-MEM (DEFN BOOL-TO-LOGICAL (B) (IF (EQUAL B 'F) F T)) Observe that: (OR (FALSEP (BOOL-TO-LOGICAL B)) (TRUEP (BOOL-TO-LOGICAL B))) is a theorem. [ 0.0 0.0 0.0 ] BOOL-TO-LOGICAL (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)))) Note that (M-STATEP (I->M I BOOT-LST LOAD-ADDR)) is a theorem. [ 0.0 0.0 0.0 ] I->M (PROVE-LEMMA MY-LESSP-QUOTIENT (REWRITE) (IMPLIES (AND (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT SIZE 2) SIZE))) WARNING: Note that the proposed lemma MY-LESSP-QUOTIENT is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. Give the conjecture the name *1. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest two inductions, both of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (ZEROP 2) (p SIZE)) (IMPLIES (AND (NOT (ZEROP 2)) (LESSP SIZE 2)) (p SIZE)) (IMPLIES (AND (NOT (ZEROP 2)) (NOT (LESSP SIZE 2)) (p (DIFFERENCE SIZE 2))) (p SIZE))). Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of ZEROP establish that the measure (COUNT SIZE) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following four new conjectures: Case 4. (IMPLIES (AND (ZEROP 2) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT SIZE 2) SIZE)). This simplifies, opening up the function ZEROP, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP 2)) (LESSP SIZE 2) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT SIZE 2) SIZE)). This simplifies, using linear arithmetic, to the new conjecture: (IMPLIES (AND (NOT (ZEROP 2)) (LESSP 1 2) (NUMBERP 1) (NOT (EQUAL 1 0))) (LESSP (QUOTIENT 1 2) 1)), which again simplifies, opening up the functions ZEROP, LESSP, NUMBERP, EQUAL, and QUOTIENT, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP 2)) (NOT (LESSP SIZE 2)) (EQUAL (DIFFERENCE SIZE 2) 0) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT SIZE 2) SIZE)), which simplifies, rewriting with SUB1-ADD1, and opening up ZEROP, QUOTIENT, EQUAL, NUMBERP, and LESSP, to: (IMPLIES (AND (NOT (LESSP SIZE 2)) (EQUAL (DIFFERENCE SIZE 2) 0) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT (DIFFERENCE SIZE 2) 2) (SUB1 SIZE))), which again simplifies, expanding the functions QUOTIENT, EQUAL, and LESSP, to the conjecture: (IMPLIES (AND (NOT (LESSP SIZE 2)) (EQUAL (DIFFERENCE SIZE 2) 0) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (NOT (EQUAL (SUB1 SIZE) 0))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP 2)) (NOT (LESSP SIZE 2)) (LESSP (QUOTIENT (DIFFERENCE SIZE 2) 2) (DIFFERENCE SIZE 2)) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT SIZE 2) SIZE)), which simplifies, rewriting with SUB1-ADD1, and expanding the definitions of ZEROP, QUOTIENT, EQUAL, NUMBERP, and LESSP, to: (IMPLIES (AND (NOT (LESSP SIZE 2)) (LESSP (QUOTIENT (DIFFERENCE SIZE 2) 2) (DIFFERENCE SIZE 2)) (NUMBERP SIZE) (NOT (EQUAL SIZE 0))) (LESSP (QUOTIENT (DIFFERENCE SIZE 2) 2) (SUB1 SIZE))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] MY-LESSP-QUOTIENT (DEFN RAM-TREE (LST SIZE) (COND ((ZEROP SIZE) (STUB (NAT-TO-V 0 32))) ((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)))) Linear arithmetic, the lemmas COUNT-NUMBERP and MY-LESSP-QUOTIENT, and the definitions of NLISTP and ZEROP can be used to show that the measure (COUNT SIZE) decreases according to the well-founded relation LESSP in each recursive call. Hence, RAM-TREE is accepted under the definitional principle. Note that: (OR (LISTP (RAM-TREE LST SIZE)) (RAMP (RAM-TREE LST SIZE)) (STUBP (RAM-TREE LST SIZE))) is a theorem. [ 0.0 0.0 0.0 ] RAM-TREE (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)))) Note that (LISTP (FM-STATE REGS C V N Z MEM)) is a theorem. [ 0.0 0.0 0.0 ] FM-STATE (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)))) From the definition we can conclude that (LISTP (M->FM9001 M)) is a theorem. [ 0.0 0.0 0.0 ] M->FM9001 (DEFN LOAD (P BOOT-LST LOAD-ADDR) (M->FM9001 (I->M (R->I (P->R P)) BOOT-LST LOAD-ADDR))) From the definition we can conclude that: (LISTP (LOAD P BOOT-LST LOAD-ADDR)) is a theorem. [ 0.0 0.0 0.0 ] LOAD (DEFN LINK-TABLES (P LOAD-ADDR) (I-LINK-TABLES (R->I (P->R P)) LOAD-ADDR)) Note that (LISTP (LINK-TABLES P LOAD-ADDR)) is a theorem. [ 0.0 0.0 0.0 ] LINK-TABLES (DEFN TYPE-LST (LST) (IF (NLISTP LST) NIL (CONS (TYPE (CAR LST)) (TYPE-LST (CDR LST))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, TYPE-LST is accepted under the definitional principle. Observe that: (OR (LITATOM (TYPE-LST LST)) (LISTP (TYPE-LST LST))) is a theorem. [ 0.0 0.0 0.0 ] TYPE-LST (DEFN AREA-TYPE-SPECIFICATION (AREA) (CONS (CAR AREA) (TYPE-LST (CDR AREA)))) From the definition we can conclude that: (LISTP (AREA-TYPE-SPECIFICATION AREA)) is a theorem. [ 0.0 0.0 0.0 ] AREA-TYPE-SPECIFICATION (DEFN TYPE-SPECIFICATION (SEGMENT) (IF (NLISTP SEGMENT) NIL (CONS (AREA-TYPE-SPECIFICATION (CAR SEGMENT)) (TYPE-SPECIFICATION (CDR SEGMENT))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT SEGMENT) decreases according to the well-founded relation LESSP in each recursive call. Hence, TYPE-SPECIFICATION is accepted under the definitional principle. Observe that: (OR (LITATOM (TYPE-SPECIFICATION SEGMENT)) (LISTP (TYPE-SPECIFICATION SEGMENT))) is a theorem. [ 0.0 0.0 0.0 ] TYPE-SPECIFICATION (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)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT TYPE-LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, DISPLAY-FM9001-ARRAY is accepted under the principle of definition. Observe that: (OR (LITATOM (DISPLAY-FM9001-ARRAY TYPE-LST N FM-MEM LINK-TABLES)) (LISTP (DISPLAY-FM9001-ARRAY TYPE-LST N FM-MEM LINK-TABLES))) is a theorem. [ 0.0 0.0 0.0 ] DISPLAY-FM9001-ARRAY (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))) Observe that: (LISTP (DISPLAY-FM9001-DATA-AREA AREA-TYPE-SPEC FM-MEM LINK-TABLES)) is a theorem. [ 0.0 0.0 0.0 ] DISPLAY-FM9001-DATA-AREA (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)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT TYPE-SPEC) decreases according to the well-founded relation LESSP in each recursive call. Hence, DISPLAY-FM9001-DATA-SEGMENT1 is accepted under the definitional principle. Note that: (OR (LITATOM (DISPLAY-FM9001-DATA-SEGMENT1 TYPE-SPEC FM-MEM LINK-TABLES)) (LISTP (DISPLAY-FM9001-DATA-SEGMENT1 TYPE-SPEC FM-MEM LINK-TABLES))) is a theorem. [ 0.0 0.0 0.0 ] DISPLAY-FM9001-DATA-SEGMENT1 (DEFN DISPLAY-FM9001-DATA-SEGMENT (FM-STATE TYPE-SPEC LINK-TABLES) (DISPLAY-FM9001-DATA-SEGMENT1 TYPE-SPEC (CADR FM-STATE) LINK-TABLES)) Observe that: (OR (LITATOM (DISPLAY-FM9001-DATA-SEGMENT FM-STATE TYPE-SPEC LINK-TABLES)) (LISTP (DISPLAY-FM9001-DATA-SEGMENT FM-STATE TYPE-SPEC LINK-TABLES))) is a theorem. [ 0.0 0.0 0.0 ] DISPLAY-FM9001-DATA-SEGMENT (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))) [ 0.0 0.0 0.0 ] V-NTH1 (DEFN CURRENT-INSTRUCTION (REGS MEM) (V-NTH1 (V-NTH1 (NAT-TO-V 15 4) REGS) MEM)) [ 0.0 0.0 0.0 ] CURRENT-INSTRUCTION (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))) Observe that: (OR (OR (FALSEP (M-STORE-RESULTP STORE-CC C V N Z)) (TRUEP (M-STORE-RESULTP STORE-CC C V N Z))) (EQUAL (M-STORE-RESULTP STORE-CC C V N Z) C) (EQUAL (M-STORE-RESULTP STORE-CC C V N Z) V) (EQUAL (M-STORE-RESULTP STORE-CC C V N Z) N) (EQUAL (M-STORE-RESULTP STORE-CC C V N Z) Z)) is a theorem. [ 0.0 0.0 0.0 ] M-STORE-RESULTP (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)))) WARNING: Note that the rewrite rule M-STORE-RESULTP-IS-STORE-RESULTP will be stored so as to apply only to terms with the nonrecursive function symbol M-STORE-RESULTP. This simplifies, applying CDR-CONS and CAR-CONS, and unfolding M-STORE-RESULTP, Z-FLAG, N-FLAG, V-FLAG, C-FLAG, SUB1, NUMBERP, EQUAL, NTH, and STORE-RESULTP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] M-STORE-RESULTP-IS-STORE-RESULTP (DISABLE M-STORE-RESULTP) [ 0.0 0.0 0.0 ] M-STORE-RESULTP-OFF (DISABLE STORE-RESULTP) [ 0.0 0.0 0.0 ] STORE-RESULTP-OFF1 (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))) Observe that: (M-STATEP (M-ALU-OPERATION REGS C V N Z MEM INS OPERAND-A OPERAND-B B-ADDRESS)) is a theorem. [ 0.0 0.0 0.0 ] M-ALU-OPERATION (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))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT RADDR) decreases according to the well-founded relation LESSP in each recursive call. Hence, READ-MEM1-RAM-TREE-HINT is accepted under the definitional principle. Observe that (TRUEP (READ-MEM1-RAM-TREE-HINT RADDR LST)) is a theorem. [ 0.0 0.0 0.0 ] READ-MEM1-RAM-TREE-HINT (DEFN REV (X) (IF (NLISTP X) NIL (APPEND (REV (CDR X)) (LIST (CAR X))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, REV is accepted under the principle of definition. Note that: (OR (LITATOM (REV X)) (LISTP (REV X))) is a theorem. [ 0.0 0.0 0.0 ] REV (ENABLE APPEND) [ 0.0 0.0 0.0 ] APPEND-ON (PROVE-LEMMA REV1-IS-REV (REWRITE) (EQUAL (REV1 X A) (APPEND (REV X) A))) Name the conjecture *1. Perhaps we can prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP X) (p X A)) (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X) (CONS (CAR X) A))) (p X A))). Linear arithmetic, the lemmas CDR-LESSEQP, LESSP-X-X, and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for A. The above induction scheme produces the following two new goals: Case 2. (IMPLIES (NLISTP X) (EQUAL (REV1 X A) (APPEND (REV X) A))). This simplifies, expanding NLISTP, REV1, REV, LISTP, and APPEND, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (EQUAL (REV1 (CDR X) (CONS (CAR X) A)) (APPEND (REV (CDR X)) (CONS (CAR X) A)))) (EQUAL (REV1 X A) (APPEND (REV X) A))). This simplifies, unfolding NLISTP, REV1, and REV, to: (IMPLIES (AND (LISTP X) (EQUAL (REV1 (CDR X) (CONS (CAR X) A)) (APPEND (REV (CDR X)) (CONS (CAR X) A)))) (EQUAL (REV1 (CDR X) (CONS (CAR X) A)) (APPEND (APPEND (REV (CDR X)) (LIST (CAR X))) A))). Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X) and (CAR X). This produces: (IMPLIES (EQUAL (REV1 Z (CONS V A)) (APPEND (REV Z) (CONS V A))) (EQUAL (REV1 Z (CONS V A)) (APPEND (APPEND (REV Z) (LIST V)) A))). We use the above equality hypothesis by substituting: (APPEND (REV Z) (CONS V A)) for (REV1 Z (CONS V A)) and throwing away the equality. We must thus prove the formula: (EQUAL (APPEND (REV Z) (CONS V A)) (APPEND (APPEND (REV Z) (LIST V)) A)). We will try to prove the above formula by generalizing it, replacing (REV Z) by Y. We must thus prove the formula: (EQUAL (APPEND Y (CONS V A)) (APPEND (APPEND Y (LIST V)) A)). Call the above conjecture *1.1. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP Y) (p (CDR Y) V A)) (p Y V A)) (IMPLIES (NOT (LISTP Y)) (p Y V A))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following two new conjectures: Case 2. (IMPLIES (AND (LISTP Y) (EQUAL (APPEND (CDR Y) (CONS V A)) (APPEND (APPEND (CDR Y) (LIST V)) A))) (EQUAL (APPEND Y (CONS V A)) (APPEND (APPEND Y (LIST V)) A))). This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the definition of APPEND, to: T. Case 1. (IMPLIES (NOT (LISTP Y)) (EQUAL (APPEND Y (CONS V A)) (APPEND (APPEND Y (LIST V)) A))), which simplifies, applying CDR-CONS and CAR-CONS, and unfolding the definitions of APPEND and LISTP, to: T. That finishes the proof of *1.1, which, consequently, also finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] REV1-IS-REV (PROVE-LEMMA APPEND-NIL (REWRITE) (IMPLIES (PROPERP X) (EQUAL (APPEND X NIL) X))) Name the conjecture *1. We will appeal to induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following three new formulas: Case 3. (IMPLIES (AND (LISTP X) (NOT (PROPERP (CDR X))) (PROPERP X)) (EQUAL (APPEND X NIL) X)). This simplifies, expanding the definition of PROPERP, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (APPEND (CDR X) NIL) (CDR X)) (PROPERP X)) (EQUAL (APPEND X NIL) X)). This simplifies, applying CONS-CAR-CDR, and expanding the definitions of PROPERP and APPEND, to: T. Case 1. (IMPLIES (AND (NOT (LISTP X)) (PROPERP X)) (EQUAL (APPEND X NIL) X)), which simplifies, opening up PROPERP, APPEND, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] APPEND-NIL (PROVE-LEMMA PROPERP-REV (REWRITE) (PROPERP (REV X))) Call the conjecture *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP X) (p X)) (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X))) (p X))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (NLISTP X) (PROPERP (REV X))), which simplifies, expanding the definitions of NLISTP, REV, and PROPERP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (PROPERP (REV (CDR X)))) (PROPERP (REV X))), which simplifies, expanding the definitions of NLISTP and REV, to: (IMPLIES (AND (LISTP X) (PROPERP (REV (CDR X)))) (PROPERP (APPEND (REV (CDR X)) (LIST (CAR X))))). Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to eliminate (CDR X) and (CAR X). The result is: (IMPLIES (PROPERP (REV Z)) (PROPERP (APPEND (REV Z) (LIST V)))). We will try to prove the above formula by generalizing it, replacing (REV Z) by Y. This generates the conjecture: (IMPLIES (PROPERP Y) (PROPERP (APPEND Y (LIST V)))). Call the above conjecture *1.1. We will appeal to induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP Y) (p (CDR Y) V)) (p Y V)) (IMPLIES (NOT (LISTP Y)) (p Y V))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following three new conjectures: Case 3. (IMPLIES (AND (LISTP Y) (NOT (PROPERP (CDR Y))) (PROPERP Y)) (PROPERP (APPEND Y (LIST V)))). This simplifies, opening up the definition of PROPERP, to: T. Case 2. (IMPLIES (AND (LISTP Y) (PROPERP (APPEND (CDR Y) (LIST V))) (PROPERP Y)) (PROPERP (APPEND Y (LIST V)))). This simplifies, applying CDR-CONS, and expanding the definitions of PROPERP and APPEND, to: T. Case 1. (IMPLIES (AND (NOT (LISTP Y)) (PROPERP Y)) (PROPERP (APPEND Y (LIST V)))), which simplifies, applying CDR-CONS, and opening up the definitions of PROPERP, LISTP, and APPEND, to: T. That finishes the proof of *1.1, which, in turn, also finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PROPERP-REV (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)))) This formula simplifies, opening up NAT-TO-V, to: (IMPLIES (STUBP (RAM-TREE LST N)) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which we will name *1. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p LST N)) (IMPLIES (AND (NOT (ZEROP N)) (NLISTP LST)) (p LST N)) (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (EQUAL N 1)) (p LST N)) (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (NOT (EQUAL N 1)) (p (RESTN (QUOTIENT N 2) LST) (QUOTIENT N 2)) (p (FIRSTN (QUOTIENT N 2) LST) (QUOTIENT N 2))) (p LST N))). Linear arithmetic, the lemmas COUNT-NUMBERP and MY-LESSP-QUOTIENT, and the definitions of NLISTP and ZEROP can be used to prove that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instances chosen for LST. The above induction scheme produces seven new formulas: Case 7. (IMPLIES (AND (ZEROP N) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, opening up the definitions of ZEROP, STUB, NAT-TO-V, EQUAL, RAM-TREE, STUBP, and STUB-GUTS, to: T. Case 6. (IMPLIES (AND (NOT (ZEROP N)) (NLISTP LST) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, opening up the functions ZEROP, NLISTP, RAM-TREE, NAT-TO-V, STUB, STUBP, STUB-GUTS, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (EQUAL N 1) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, unfolding the functions ZEROP, NLISTP, NUMBERP, EQUAL, and RAM-TREE, to: T. Case 4. (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (NOT (EQUAL N 1)) (NOT (STUBP (RAM-TREE (RESTN (QUOTIENT N 2) LST) (QUOTIENT N 2)))) (NOT (STUBP (RAM-TREE (FIRSTN (QUOTIENT N 2) LST) (QUOTIENT N 2)))) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, expanding the definitions of ZEROP, NLISTP, and RAM-TREE, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (NOT (EQUAL N 1)) (EQUAL (STUB-GUTS (RAM-TREE (RESTN (QUOTIENT N 2) LST) (QUOTIENT N 2))) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F)) (NOT (STUBP (RAM-TREE (FIRSTN (QUOTIENT N 2) LST) (QUOTIENT N 2)))) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, opening up the definitions of ZEROP, NLISTP, and RAM-TREE, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (NOT (EQUAL N 1)) (NOT (STUBP (RAM-TREE (RESTN (QUOTIENT N 2) LST) (QUOTIENT N 2)))) (EQUAL (STUB-GUTS (RAM-TREE (FIRSTN (QUOTIENT N 2) LST) (QUOTIENT N 2))) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F)) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, unfolding the definitions of ZEROP, NLISTP, and RAM-TREE, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (NOT (NLISTP LST)) (NOT (EQUAL N 1)) (EQUAL (STUB-GUTS (RAM-TREE (RESTN (QUOTIENT N 2) LST) (QUOTIENT N 2))) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F)) (EQUAL (STUB-GUTS (RAM-TREE (FIRSTN (QUOTIENT N 2) LST) (QUOTIENT N 2))) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F)) (STUBP (RAM-TREE LST N))) (EQUAL (STUB-GUTS (RAM-TREE LST N)) (LIST F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F))), which simplifies, unfolding the definitions of ZEROP, NLISTP, and RAM-TREE, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] READ-MEM1-REV-RAM-TREE-LEMMA1 (ENABLE PLUS-0) [ 0.0 0.0 0.0 ] PLUS-0-ON (ENABLE PLUS-ADD1-SUB1) [ 0.0 0.0 0.0 ] PLUS-ADD1-SUB1-ON (ENABLE PLUS-ADD1) [ 0.0 0.0 0.0 ] PLUS-ADD1-ON1 (ENABLE ASSOCIATIVITY-OF-PLUS) [ 0.0 0.0 0.0 ] ASSOCIATIVITY-OF-PLUS-ON1 (ENABLE COMMUTATIVITY-OF-PLUS) [ 0.0 0.0 0.0 ] COMMUTATIVITY-OF-PLUS-ON1 (ENABLE TIMES-COMMUTES) [ 0.0 0.0 0.0 ] TIMES-COMMUTES-ON (ENABLE TIMES-ADD1-AGAIN) [ 0.0 0.0 0.0 ] TIMES-ADD1-AGAIN-ON (ENABLE TIMES-1) [ 0.0 0.0 0.0 ] TIMES-1-ON (ENABLE TIMES-DISTRIBUTES-OVER-PLUS) [ 0.0 0.0 0.0 ] TIMES-DISTRIBUTES-OVER-PLUS-ON1 (ENABLE ASSOCIATIVITY-OF-TIMES) [ 0.0 0.0 0.0 ] ASSOCIATIVITY-OF-TIMES-ON1 (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))))) This formula simplifies, applying the lemma TIMES-COMMUTES, to: (EQUAL (V-TO-NAT (APPEND A B)) (PLUS (V-TO-NAT A) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH A))))), which we will name *1. We will appeal to induction. There are four plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP A) (p (CDR A) B)) (p A B)) (IMPLIES (NOT (LISTP A)) (p A B))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following two new formulas: Case 2. (IMPLIES (AND (LISTP A) (EQUAL (V-TO-NAT (APPEND (CDR A) B)) (PLUS (V-TO-NAT (CDR A)) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A))))))) (EQUAL (V-TO-NAT (APPEND A B)) (PLUS (V-TO-NAT A) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH A)))))). This simplifies, rewriting with PLUS-ADD1, PLUS-0, TIMES-1, CDR-CONS, CAR-CONS, SUB1-ADD1, TIMES-DISTRIBUTES-OVER-PLUS, ASSOCIATIVITY-OF-PLUS, and COMMUTATIVITY-OF-PLUS, and opening up APPEND, ZEROP, TIMES, EQUAL, NUMBERP, SUB1, V-TO-NAT, LENGTH, and EXP, to two new formulas: Case 2.2. (IMPLIES (AND (LISTP A) (EQUAL (V-TO-NAT (APPEND (CDR A) B)) (PLUS (V-TO-NAT (CDR A)) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A)))))) (NOT (CAR A))) (EQUAL (PLUS (V-TO-NAT (APPEND (CDR A) B)) (V-TO-NAT (APPEND (CDR A) B))) (PLUS (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A)))) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A)))) (V-TO-NAT (CDR A)) (V-TO-NAT (CDR A))))), which again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (LISTP A) (EQUAL (V-TO-NAT (APPEND (CDR A) B)) (PLUS (V-TO-NAT (CDR A)) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A)))))) (CAR A)) (EQUAL (ADD1 (PLUS (V-TO-NAT (APPEND (CDR A) B)) (V-TO-NAT (APPEND (CDR A) B)))) (PLUS (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A)))) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH (CDR A)))) (ADD1 (PLUS (V-TO-NAT (CDR A)) (V-TO-NAT (CDR A))))))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (NOT (LISTP A)) (EQUAL (V-TO-NAT (APPEND A B)) (PLUS (V-TO-NAT A) (TIMES (V-TO-NAT B) (EXP 2 (LENGTH A)))))), which simplifies, rewriting with TIMES-1, TIMES-COMMUTES, and PLUS-0, and opening up APPEND, V-TO-NAT, LENGTH, EXP, and ZEROP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] MY-V-TO-NAT-APPEND (ENABLE PLUS) [ 0.0 0.0 0.0 ] PLUS-ON (ENABLE DIFFERENCE) [ 0.0 0.0 0.0 ] DIFFERENCE-ON (PROVE-LEMMA DIFFERENCE-ADD1-ADD1-X-2 (REWRITE) (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2) (FIX X))) This formula simplifies, applying SUB1-ADD1, and opening up the functions SUB1, NUMBERP, EQUAL, DIFFERENCE, and FIX, to: (IMPLIES (AND (NUMBERP X) (EQUAL X 0)) (EQUAL 0 X)), which again simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-ADD1-ADD1-X-2 (ENABLE QUOTIENT-PLUS-X-X-2) [ 0.0 0.0 0.0 ] QUOTIENT-PLUS-X-X-2-ON (ENABLE LENGTH-FIRSTN) [ 0.0 0.0 0.0 ] LENGTH-FIRSTN-ON (ENABLE LENGTH-RESTN) [ 0.0 0.0 0.0 ] LENGTH-RESTN-ON (PROVE-LEMMA MY-LESSP-V-TO-NAT-EXP (REWRITE) (IMPLIES (EQUAL N (LENGTH V)) (LESSP (V-TO-NAT V) (EXP 2 N)))) WARNING: When the linear lemma MY-LESSP-V-TO-NAT-EXP is stored under (EXP 2 N) it contains the free variable V which will be chosen by instantiating the hypothesis (EQUAL N (LENGTH V)). WARNING: When the linear lemma MY-LESSP-V-TO-NAT-EXP is stored under (V-TO-NAT V) it contains the free variable N which will be chosen by instantiating the hypothesis (EQUAL N (LENGTH V)). WARNING: Note that the proposed lemma MY-LESSP-V-TO-NAT-EXP is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. Call the conjecture *1. We will try to prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP V) (p V)) (IMPLIES (AND (NOT (NLISTP V)) (p (CDR V))) (p V))). Linear arithmetic, the lemmas CDR-LESSEQP, LESSP-X-X, and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT V) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (NLISTP V) (LESSP (V-TO-NAT V) (EXP 2 (LENGTH V)))), which simplifies, opening up the functions NLISTP, V-TO-NAT, LENGTH, EXP, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP V)) (LESSP (V-TO-NAT (CDR V)) (EXP 2 (LENGTH (CDR V))))) (LESSP (V-TO-NAT V) (EXP 2 (LENGTH V)))), which simplifies, applying TIMES-1, PLUS-0, PLUS-ADD1, and SUB1-ADD1, and unfolding the functions NLISTP, V-TO-NAT, SUB1, NUMBERP, EQUAL, TIMES, ZEROP, LENGTH, and EXP, to the following two new conjectures: Case 1.2. (IMPLIES (AND (LISTP V) (LESSP (V-TO-NAT (CDR V)) (EXP 2 (LENGTH (CDR V)))) (NOT (CAR V))) (LESSP (PLUS (V-TO-NAT (CDR V)) (V-TO-NAT (CDR V))) (PLUS (EXP 2 (LENGTH (CDR V))) (EXP 2 (LENGTH (CDR V)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (LISTP V) (LESSP (V-TO-NAT (CDR V)) (EXP 2 (LENGTH (CDR V)))) (CAR V)) (LESSP (ADD1 (PLUS (V-TO-NAT (CDR V)) (V-TO-NAT (CDR V)))) (PLUS (EXP 2 (LENGTH (CDR V))) (EXP 2 (LENGTH (CDR V)))))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] MY-LESSP-V-TO-NAT-EXP (PROVE-LEMMA LENGTH-REV (REWRITE) (EQUAL (LENGTH (REV X)) (LENGTH X))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP X) (p X)) (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X))) (p X))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (NLISTP X) (EQUAL (LENGTH (REV X)) (LENGTH X))). This simplifies, expanding the functions NLISTP, REV, LENGTH, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (EQUAL (LENGTH (REV (CDR X))) (LENGTH (CDR X)))) (EQUAL (LENGTH (REV X)) (LENGTH X))). This simplifies, opening up NLISTP, REV, and LENGTH, to the new formula: (IMPLIES (AND (LISTP X) (EQUAL (LENGTH (REV (CDR X))) (LENGTH (CDR X)))) (EQUAL (LENGTH (APPEND (REV (CDR X)) (LIST (CAR X)))) (ADD1 (LENGTH (CDR X))))). Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X) and (CAR X). We would thus like to prove: (IMPLIES (EQUAL (LENGTH (REV Z)) (LENGTH Z)) (EQUAL (LENGTH (APPEND (REV Z) (LIST V))) (ADD1 (LENGTH Z)))). We use the above equality hypothesis by substituting (LENGTH (REV Z)) for (LENGTH Z) and throwing away the equality. This generates: (EQUAL (LENGTH (APPEND (REV Z) (LIST V))) (ADD1 (LENGTH (REV Z)))). We will try to prove the above formula by generalizing it, replacing (REV Z) by Y. The result is: (EQUAL (LENGTH (APPEND Y (LIST V))) (ADD1 (LENGTH Y))). Call the above conjecture *1.1. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP Y) (p (CDR Y) V)) (p Y V)) (IMPLIES (NOT (LISTP Y)) (p Y V))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following two new goals: Case 2. (IMPLIES (AND (LISTP Y) (EQUAL (LENGTH (APPEND (CDR Y) (LIST V))) (ADD1 (LENGTH (CDR Y))))) (EQUAL (LENGTH (APPEND Y (LIST V))) (ADD1 (LENGTH Y)))). This simplifies, rewriting with CDR-CONS, and unfolding the functions APPEND and LENGTH, to: T. Case 1. (IMPLIES (NOT (LISTP Y)) (EQUAL (LENGTH (APPEND Y (LIST V))) (ADD1 (LENGTH Y)))), which simplifies, applying CDR-CONS, and expanding the functions APPEND, ADD1, LENGTH, and EQUAL, to: T. That finishes the proof of *1.1, which, consequently, also finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-REV (PROVE-LEMMA NTH-FIRSTN (REWRITE) (IMPLIES (LESSP I N) (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST)))) Call the conjecture *1. We will try to prove it by induction. There are six plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N))) (p I N LST)) (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (OR (EQUAL I 0) (NOT (NUMBERP I)))) (p I N LST)) (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (p (SUB1 I) (SUB1 N) (CDR LST))) (p I N LST))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT inform us that the measure (COUNT I) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instances chosen for LST and N. The above induction scheme generates four new goals: Case 4. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N))) (LESSP I N)) (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST))), which simplifies, opening up the functions NOT, OR, EQUAL, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (OR (EQUAL I 0) (NOT (NUMBERP I))) (LESSP I N)) (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST))), which simplifies, expanding NOT, OR, EQUAL, LESSP, FIRSTN, and NTH, to four new formulas: Case 3.4. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL I 0) (NOT (LISTP LST))) (EQUAL (CAR NIL) (CAR LST))), which again simplifies, applying the lemma CAR-NLISTP, and opening up the definitions of CAR and EQUAL, to: T. Case 3.3. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL I 0) (LISTP LST)) (EQUAL (CAR (CONS (CAR LST) (FIRSTN (SUB1 N) (CDR LST)))) (CAR LST))), which again simplifies, applying CAR-CONS, to: T. Case 3.2. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NUMBERP I)) (NOT (LISTP LST))) (EQUAL (CAR NIL) (CAR LST))). However this again simplifies, applying the lemma CAR-NLISTP, and opening up the functions CAR and EQUAL, to: T. Case 3.1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NUMBERP I)) (LISTP LST)) (EQUAL (CAR (CONS (CAR LST) (FIRSTN (SUB1 N) (CDR LST)))) (CAR LST))), which again simplifies, applying the lemma CAR-CONS, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (NOT (LESSP (SUB1 I) (SUB1 N))) (LESSP I N)) (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST))), which simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP I 1) (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (NOT (LESSP (SUB1 I) (SUB1 N))) (LESSP I N)) (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST))). But this again simplifies, opening up SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (EQUAL (NTH (SUB1 I) (FIRSTN (SUB1 N) (CDR LST))) (NTH (SUB1 I) (CDR LST))) (LESSP I N)) (EQUAL (NTH I (FIRSTN N LST)) (NTH I LST))), which simplifies, opening up NOT, OR, LESSP, FIRSTN, and NTH, to two new conjectures: Case 1.2. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (NTH (SUB1 I) (FIRSTN (SUB1 N) (CDR LST))) (NTH (SUB1 I) (CDR LST))) (LESSP (SUB1 I) (SUB1 N)) (NOT (LISTP LST))) (EQUAL (NTH I NIL) (NTH (SUB1 I) (CDR LST)))), which again simplifies, expanding the definitions of CDR and NTH, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (NTH (SUB1 I) (FIRSTN (SUB1 N) (CDR LST))) (NTH (SUB1 I) (CDR LST))) (LESSP (SUB1 I) (SUB1 N)) (NOT (LISTP LST))) (EQUAL (NTH (SUB1 I) 0) (NTH (SUB1 I) (CDR LST)))). However this further simplifies, applying CDR-NLISTP, and unfolding LISTP and FIRSTN, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (NTH (SUB1 I) (FIRSTN (SUB1 N) (CDR LST))) (NTH (SUB1 I) (CDR LST))) (LESSP (SUB1 I) (SUB1 N)) (LISTP LST)) (EQUAL (NTH I (CONS (CAR LST) (FIRSTN (SUB1 N) (CDR LST)))) (NTH (SUB1 I) (CDR LST)))). However this again simplifies, appealing to the lemma CDR-CONS, and opening up the definition of NTH,