(NOTE-LIB "c1") Nqthm-1992 mods: (PC-NQTHM-1992) Loading ./mg/c1.lib Finished loading ./mg/c1.lib Loading ./mg/c1.lisp Finished loading ./mg/c1.lisp (#./mg/c1.lib #./mg/c1.lisp) (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.0 0.0 0.0 ] P-STATE (DEFN P-HALT (P PSW) (P-STATE (P-PC P) (P-CTRL-STK P) (P-TEMP-STK P) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) PSW)) Observe that (P-STATEP (P-HALT P PSW)) is a theorem. [ 0.0 0.0 0.0 ] P-HALT (DEFN DEFINITION (NAME ALIST) (ASSOC NAME ALIST)) [ 0.0 0.0 0.0 ] DEFINITION (DEFN PUT-VALUE (VAL NAME ALIST) (PUT-ASSOC VAL NAME ALIST)) Note that: (OR (LISTP (PUT-VALUE VAL NAME ALIST)) (EQUAL (PUT-VALUE VAL NAME ALIST) ALIST)) is a theorem. [ 0.0 0.0 0.0 ] PUT-VALUE (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 ADP-NAME (ADP) (CAR ADP)) [ 0.0 0.0 0.0 ] ADP-NAME (DISABLE ADP-NAME) [ 0.0 0.0 0.0 ] ADP-NAME-OFF (DEFN ADP-OFFSET (ADP) (CDR ADP)) [ 0.0 0.0 0.0 ] ADP-OFFSET (DISABLE ADP-OFFSET) [ 0.0 0.0 0.0 ] ADP-OFFSET-OFF (PROVE-LEMMA ADP-NAME-CONS (REWRITE) (EQUAL (ADP-NAME (CONS X Y)) X) ((ENABLE ADP-NAME))) This conjecture can be simplified, using the abbreviations CAR-CONS and ADP-NAME, to: (EQUAL X X). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ADP-NAME-CONS (PROVE-LEMMA ADP-OFFSET-CONS (REWRITE) (EQUAL (ADP-OFFSET (CONS X Y)) Y) ((ENABLE ADP-OFFSET))) This conjecture can be simplified, using the abbreviations CDR-CONS and ADP-OFFSET, to: (EQUAL Y Y). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ADP-OFFSET-CONS (DEFN ADPP (X SEGMENT) (AND (LISTP X) (NUMBERP (ADP-OFFSET X)) (DEFINEDP (ADP-NAME X) SEGMENT) (LESSP (ADP-OFFSET X) (LENGTH (VALUE (ADP-NAME X) SEGMENT))))) Note that (OR (FALSEP (ADPP X SEGMENT)) (TRUEP (ADPP X SEGMENT))) is a theorem. [ 0.0 0.0 0.0 ] ADPP (DEFN PCPP (X SEGMENT) (AND (LISTP X) (NUMBERP (ADP-OFFSET X)) (DEFINEDP (ADP-NAME X) SEGMENT) (LESSP (ADP-OFFSET X) (LENGTH (PROGRAM-BODY (DEFINITION (ADP-NAME X) SEGMENT)))))) Observe that (OR (FALSEP (PCPP X SEGMENT)) (TRUEP (PCPP X SEGMENT))) is a theorem. [ 0.0 0.0 0.0 ] PCPP (DEFN ADD-ADP (ADP N) (CONS (ADP-NAME ADP) (PLUS (ADP-OFFSET ADP) N))) Note that (LISTP (ADD-ADP ADP N)) is a theorem. [ 0.0 0.0 0.0 ] ADD-ADP (DEFN ADD1-ADP (ADP) (ADD-ADP ADP 1)) Observe that (LISTP (ADD1-ADP ADP)) is a theorem. [ 0.0 0.0 0.0 ] ADD1-ADP (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 FETCH-ADP (ADP SEGMENT) (GET (ADP-OFFSET ADP) (VALUE (ADP-NAME ADP) SEGMENT))) [ 0.0 0.0 0.0 ] FETCH-ADP (DEFN DEPOSIT-ADP (VAL ADP SEGMENT) (PUT-VALUE (PUT VAL (ADP-OFFSET ADP) (VALUE (ADP-NAME ADP) SEGMENT)) (ADP-NAME ADP) SEGMENT)) Note that: (OR (LISTP (DEPOSIT-ADP VAL ADP SEGMENT)) (EQUAL (DEPOSIT-ADP VAL ADP SEGMENT) SEGMENT)) is a theorem. [ 0.0 0.0 0.0 ] DEPOSIT-ADP (DEFN RGET (N LST) (GET (SUB1 (DIFFERENCE (LENGTH LST) N)) LST)) [ 0.0 0.0 0.0 ] RGET (DEFN RPUT (VAL N LST) (PUT VAL (SUB1 (DIFFERENCE (LENGTH LST) N)) LST)) Observe that (LISTP (RPUT VAL N LST)) is a theorem. [ 0.0 0.0 0.0 ] RPUT (PROVE-LEMMA RPUT-PRESERVES-LENGTH (REWRITE) (IMPLIES (LESSP Y (LENGTH Z)) (EQUAL (LENGTH (RPUT X Y Z)) (LENGTH Z))) ((ENABLE PUT-PRESERVES-LENGTH RPUT))) This conjecture simplifies, using linear arithmetic, applying PUT-PRESERVES-LENGTH, and expanding the function RPUT, to: (IMPLIES (AND (LESSP Y (LENGTH Z)) (LESSP (LENGTH Z) Y)) (EQUAL (LENGTH (RPUT X Y Z)) (LENGTH Z))). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RPUT-PRESERVES-LENGTH (DISABLE RGET) [ 0.0 0.0 0.0 ] RGET-OFF (DISABLE RPUT) [ 0.0 0.0 0.0 ] RPUT-OFF (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 (PROVE-LEMMA TYPE-EXPANSION (REWRITE) (EQUAL (TYPE (CONS X Y)) X) ((ENABLE TYPE))) WARNING: Note that the rewrite rule TYPE-EXPANSION will be stored so as to apply only to terms with the nonrecursive function symbol TYPE. This conjecture can be simplified, using the abbreviations CAR-CONS and TYPE, to: (EQUAL X X). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TYPE-EXPANSION (PROVE-LEMMA TYPE-TAG (REWRITE) (EQUAL (TYPE (TAG X Y)) X)) WARNING: Note that the rewrite rule TYPE-TAG will be stored so as to apply only to terms with the nonrecursive function symbol TYPE. This conjecture can be simplified, using the abbreviations CAR-CONS, TAG, and TYPE, to: (EQUAL X X). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TYPE-TAG (PROVE-LEMMA UNTAG-TAG (REWRITE) (EQUAL (UNTAG (TAG X Y)) Y)) WARNING: Note that the rewrite rule UNTAG-TAG will be stored so as to apply only to terms with the nonrecursive function symbol UNTAG. This conjecture can be simplified, using the abbreviations CAR-CONS, CDR-CONS, TAG, and UNTAG, to: (EQUAL Y Y). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] UNTAG-TAG (PROVE-LEMMA UNTAG-CONS (REWRITE) (EQUAL (UNTAG (LIST X Y)) Y) ((ENABLE UNTAG))) WARNING: Note that the rewrite rule UNTAG-CONS will be stored so as to apply only to terms with the nonrecursive function symbol UNTAG. This formula can be simplified, using the abbreviations CAR-CONS, CDR-CONS, and UNTAG, to: (EQUAL Y Y), which simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] UNTAG-CONS (DISABLE TYPE) [ 0.0 0.0 0.0 ] TYPE-OFF (DISABLE TAG) [ 0.0 0.0 0.0 ] TAG-OFF (DISABLE UNTAG) [ 0.0 0.0 0.0 ] UNTAG-OFF (DEFN AREA-NAME (X) (ADP-NAME (UNTAG X))) [ 0.0 0.0 0.0 ] AREA-NAME (DEFN OFFSET (X) (ADP-OFFSET (UNTAG X))) [ 0.0 0.0 0.0 ] OFFSET (DEFN ADD-ADDR (ADDR N) (TAG (TYPE ADDR) (ADD-ADP (UNTAG ADDR) N))) Note that (LISTP (ADD-ADDR ADDR N)) is a theorem. [ 0.0 0.0 0.0 ] ADD-ADDR (DEFN ADD1-ADDR (ADDR) (ADD-ADDR ADDR 1)) Observe that (LISTP (ADD1-ADDR ADDR)) is a theorem. [ 0.0 0.0 0.0 ] ADD1-ADDR (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 SUB1-ADDR (ADDR) (SUB-ADDR ADDR 1)) Observe that (LISTP (SUB1-ADDR ADDR)) is a theorem. [ 0.0 0.0 0.0 ] SUB1-ADDR (DEFN FETCH (ADDR SEGMENT) (FETCH-ADP (UNTAG ADDR) SEGMENT)) [ 0.0 0.0 0.0 ] FETCH (DEFN DEPOSIT (VAL ADDR SEGMENT) (DEPOSIT-ADP VAL (UNTAG ADDR) SEGMENT)) Note that: (OR (LISTP (DEPOSIT VAL ADDR SEGMENT)) (EQUAL (DEPOSIT VAL ADDR SEGMENT) SEGMENT)) is a theorem. [ 0.0 0.0 0.0 ] DEPOSIT (DEFN ADD1-NAT (NAT) (TAG 'NAT (ADD1 (UNTAG NAT)))) From the definition we can conclude that (LISTP (ADD1-NAT NAT)) is a theorem. [ 0.0 0.0 0.0 ] ADD1-NAT (PROVE-LEMMA UNTAG-ADD1-NAT (REWRITE) (EQUAL (UNTAG (ADD1-NAT NAT)) (ADD1 (UNTAG NAT))) ((ENABLE UNTAG ADD1-NAT TAG))) This formula can be simplified, using the abbreviations CAR-CONS, CDR-CONS, TAG, ADD1-NAT, and UNTAG, to the new conjecture: (EQUAL (ADD1 (CADR NAT)) (ADD1 (CADR NAT))), which simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] UNTAG-ADD1-NAT (DEFN BOOLEANP (X) (OR (EQUAL X 'T) (EQUAL X 'F))) Observe that (OR (FALSEP (BOOLEANP X)) (TRUEP (BOOLEANP X))) is a theorem. [ 0.0 0.0 0.0 ] BOOLEANP (DEFN BOOL (X) (TAG 'BOOL (IF X 'T 'F))) Observe that (LISTP (BOOL X)) is a theorem. [ 0.0 0.0 0.0 ] BOOL (DEFN OR-BOOL (X Y) (IF (EQUAL X 'F) Y 'T)) From the definition we can conclude that: (OR (LITATOM (OR-BOOL X Y)) (EQUAL (OR-BOOL X Y) Y)) is a theorem. [ 0.0 0.0 0.0 ] OR-BOOL (DEFN AND-BOOL (X Y) (IF (EQUAL X 'F) 'F Y)) From the definition we can conclude that: (OR (LITATOM (AND-BOOL X Y)) (EQUAL (AND-BOOL X Y) Y)) is a theorem. [ 0.0 0.0 0.0 ] AND-BOOL (DEFN NOT-BOOL (X) (IF (EQUAL X 'F) 'T 'F)) Observe that (LITATOM (NOT-BOOL X)) is a theorem. [ 0.0 0.0 0.0 ] NOT-BOOL (DEFN SMALL-NATURALP (I WORD-SIZE) (AND (NUMBERP I) (LESSP I (EXP 2 WORD-SIZE)))) Note that: (OR (FALSEP (SMALL-NATURALP I WORD-SIZE)) (TRUEP (SMALL-NATURALP I WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] SMALL-NATURALP (DISABLE SMALL-NATURALP) [ 0.0 0.0 0.0 ] SMALL-NATURALP-OFF (DEFN BOOL-TO-NAT (FLG) (IF (EQUAL FLG 'F) 0 1)) Observe that (NUMBERP (BOOL-TO-NAT FLG)) is a theorem. [ 0.0 0.0 0.0 ] BOOL-TO-NAT (DEFN SMALL-INTEGERP (I WORD-SIZE) (AND (INTEGERP I) (NOT (ILESSP I (MINUS (EXP 2 (SUB1 WORD-SIZE))))) (ILESSP I (EXP 2 (SUB1 WORD-SIZE))))) Note that: (OR (FALSEP (SMALL-INTEGERP I WORD-SIZE)) (TRUEP (SMALL-INTEGERP I WORD-SIZE))) is a theorem. [ 0.0 0.0 0.0 ] SMALL-INTEGERP (DISABLE SMALL-INTEGERP) [ 0.0 0.0 0.0 ] SMALL-INTEGERP-OFF (DEFN FIX-SMALL-INTEGER (I WORD-SIZE) (IF (SMALL-INTEGERP I WORD-SIZE) I (IF (NEGATIVEP I) (IPLUS I (EXP 2 WORD-SIZE)) (IPLUS I (MINUS (EXP 2 WORD-SIZE)))))) Observe that: (OR (OR (NUMBERP (FIX-SMALL-INTEGER I WORD-SIZE)) (NEGATIVEP (FIX-SMALL-INTEGER I WORD-SIZE))) (EQUAL (FIX-SMALL-INTEGER I WORD-SIZE) I)) is a theorem. [ 0.0 0.0 0.0 ] FIX-SMALL-INTEGER (DEFN PUSH (X STK) (CONS X STK)) From the definition we can conclude that (LISTP (PUSH X STK)) is a theorem. [ 0.0 0.0 0.0 ] PUSH (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 POPN (N X) (IF (ZEROP N) X (POPN (SUB1 N) (CDR X)))) 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, POPN is accepted under the principle of definition. [ 0.0 0.0 0.0 ] POPN (PROVE-LEMMA POPN-ADD1 (REWRITE) (AND (EQUAL (POPN (ADD1 N) (PUSH X Y)) (POPN N Y)) (EQUAL (POPN (ADD1 N) (CONS X Y)) (POPN N Y))) ((ENABLE POPN))) WARNING: Note that the proposed lemma POPN-ADD1 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviations AND and PUSH, to the new formula: (EQUAL (POPN (ADD1 N) (CONS X Y)) (POPN N Y)), which simplifies, rewriting with CDR-CONS and SUB1-ADD1, and expanding POPN, to: (IMPLIES (NOT (NUMBERP N)) (EQUAL (POPN 0 Y) (POPN N Y))), which again simplifies, expanding the functions EQUAL and POPN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] POPN-ADD1 (PROVE-LEMMA POPN-ZERO (REWRITE) (EQUAL (POPN 0 X) X) ((ENABLE POPN))) This conjecture simplifies, unfolding the definitions of EQUAL and POPN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] POPN-ZERO (PROVE-LEMMA POPN-LENGTH (REWRITE) (IMPLIES (EQUAL N (LENGTH LST)) (EQUAL (POPN N (APPEND LST STK)) STK)) ((ENABLE POPN POP))) Give the conjecture the name *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 LST) (p (CDR LST) STK)) (p LST STK)) (IMPLIES (NOT (LISTP LST)) (p LST STK))). Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new formulas: Case 2. (IMPLIES (AND (LISTP LST) (EQUAL (POPN (LENGTH (CDR LST)) (APPEND (CDR LST) STK)) STK)) (EQUAL (POPN (LENGTH LST) (APPEND LST STK)) STK)). This simplifies, rewriting with the lemma POPN-ADD1, and unfolding LENGTH and APPEND, to: T. Case 1. (IMPLIES (NOT (LISTP LST)) (EQUAL (POPN (LENGTH LST) (APPEND LST STK)) STK)). This simplifies, rewriting with POPN-ZERO, and expanding the functions LENGTH and APPEND, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] POPN-LENGTH (PROVE-LEMMA POPN-PLUS (REWRITE) (IMPLIES (EQUAL M (LENGTH LST1)) (EQUAL (POPN (PLUS M N) (APPEND LST1 LST2)) (POPN N LST2))) ((ENABLE POPN))) Give the conjecture the name *1. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest three inductions. They merge into two likely candidate inductions, both of which are unflawed. However, one of these is more likely than the other. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP LST1) (p (CDR LST1) N LST2)) (p LST1 N LST2)) (IMPLIES (NOT (LISTP LST1)) (p LST1 N LST2))). Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT LST1) 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 LST1) (EQUAL (POPN (PLUS (LENGTH (CDR LST1)) N) (APPEND (CDR LST1) LST2)) (POPN N LST2))) (EQUAL (POPN (PLUS (LENGTH LST1) N) (APPEND LST1 LST2)) (POPN N LST2))). This simplifies, appealing to the lemmas SUB1-ADD1 and POPN-ADD1, and unfolding LENGTH, PLUS, and APPEND, to: T. Case 1. (IMPLIES (NOT (LISTP LST1)) (EQUAL (POPN (PLUS (LENGTH LST1) N) (APPEND LST1 LST2)) (POPN N LST2))). This simplifies, expanding the definitions of LENGTH, EQUAL, PLUS, and APPEND, to: (IMPLIES (AND (NOT (LISTP LST1)) (NOT (NUMBERP N))) (EQUAL (POPN 0 LST2) (POPN N LST2))), which again simplifies, applying POPN-ZERO, and expanding POPN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] POPN-PLUS (DEFN TOP1 (STK) (TOP (POP STK))) [ 0.0 0.0 0.0 ] TOP1 (DEFN TOP2 (STK) (TOP (POP (POP STK)))) [ 0.0 0.0 0.0 ] TOP2 (PROVE-LEMMA POP-PUSH (REWRITE) (EQUAL (POP (PUSH X Y)) Y)) WARNING: Note that the rewrite rule POP-PUSH will be stored so as to apply only to terms with the nonrecursive function symbol POP. This conjecture can be simplified, using the abbreviations CDR-CONS, PUSH, and POP, to: (EQUAL Y Y). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] POP-PUSH (PROVE-LEMMA POP-CONS (REWRITE) (EQUAL (POP (CONS X Y)) Y) ((ENABLE POP))) WARNING: Note that the rewrite rule POP-CONS will be stored so as to apply only to terms with the nonrecursive function symbol POP. This conjecture can be simplified, using the abbreviations CDR-CONS and POP, to: (EQUAL Y Y). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] POP-CONS (PROVE-LEMMA CAR-CDR-PUSH (REWRITE) (AND (EQUAL (CAR (PUSH X Y)) X) (EQUAL (CDR (PUSH X Y)) Y)) ((ENABLE PUSH))) WARNING: Note that the proposed lemma CAR-CDR-PUSH is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviations AND, CDR-CONS, CAR-CONS, and PUSH, to the following two new conjectures: Case 2. (EQUAL X X). This simplifies, clearly, to: T. Case 1. (EQUAL Y Y). This simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] CAR-CDR-PUSH (PROVE-LEMMA PUSH-LISTP (REWRITE) (AND (LISTP (PUSH X Y)) (EQUAL (NLISTP (PUSH X Y)) F)) ((ENABLE PUSH))) WARNING: Note that the rewrite rule PUSH-LISTP will be stored so as to apply only to terms with the nonrecursive function symbol NLISTP. WARNING: Note that the proposed lemma PUSH-LISTP is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This conjecture can be simplified, using the abbreviations AND and PUSH, to two new goals: Case 2. (LISTP (CONS X Y)), which simplifies, clearly, to: T. Case 1. (EQUAL (NLISTP (CONS X Y)) F). This simplifies, unfolding the functions NLISTP and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PUSH-LISTP (PROVE-LEMMA TOP-PUSH (REWRITE) (EQUAL (TOP (PUSH X Y)) X)) WARNING: Note that the rewrite rule TOP-PUSH will be stored so as to apply only to terms with the nonrecursive function symbol TOP. This conjecture can be simplified, using the abbreviations CAR-CONS, PUSH, and TOP, to: (EQUAL X X). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TOP-PUSH (PROVE-LEMMA TOP1-PUSH (REWRITE) (EQUAL (TOP1 (PUSH X (PUSH Y Z))) Y)) WARNING: Note that the rewrite rule TOP1-PUSH will be stored so as to apply only to terms with the nonrecursive function symbol TOP1. This formula can be simplified, using the abbreviations CAR-CONS, CDR-CONS, POP, TOP, PUSH, and TOP1, to the new conjecture: (EQUAL Y Y), which simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TOP1-PUSH (PROVE-LEMMA TOP2-PUSH (REWRITE) (EQUAL (TOP2 (PUSH X (PUSH Y (PUSH Z W)))) Z)) WARNING: Note that the rewrite rule TOP2-PUSH will be stored so as to apply only to terms with the nonrecursive function symbol TOP2. This conjecture can be simplified, using the abbreviations CAR-CONS, CDR-CONS, POP, TOP, PUSH, and TOP2, to: (EQUAL Z Z). This simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TOP2-PUSH (PROVE-LEMMA LENGTH-PUSH (REWRITE) (EQUAL (LENGTH (PUSH X Y)) (ADD1 (LENGTH Y)))) This conjecture can be simplified, using the abbreviation PUSH, to the conjecture: (EQUAL (LENGTH (CONS X Y)) (ADD1 (LENGTH Y))). This simplifies, applying CDR-CONS, and unfolding the definition of LENGTH, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-PUSH (PROVE-LEMMA TOP-CONS (REWRITE) (EQUAL (TOP (CONS X Y)) X)) WARNING: Note that the rewrite rule TOP-CONS will be stored so as to apply only to terms with the nonrecursive function symbol TOP. This conjecture can be simplified, using the abbreviations CAR-CONS and TOP, to: (EQUAL X X). This simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TOP-CONS (DISABLE POP) [ 0.0 0.0 0.0 ] POP-OFF (DISABLE PUSH) [ 0.0 0.0 0.0 ] PUSH-OFF (DISABLE TOP) [ 0.0 0.0 0.0 ] TOP-OFF (DISABLE TOP1) [ 0.0 0.0 0.0 ] TOP1-OFF (DISABLE TOP2) [ 0.0 0.0 0.0 ] TOP2-OFF (DISABLE POPN) [ 0.0 0.0 0.0 ] POPN-OFF (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 (PROVE-LEMMA LABELLEDP-EXPANSION (REWRITE) (EQUAL (LABELLEDP (CONS 'DL ARGS)) T)) WARNING: Note that the rewrite rule LABELLEDP-EXPANSION will be stored so as to apply only to terms with the nonrecursive function symbol LABELLEDP. This conjecture can be simplified, using the abbreviations APPEND-CONS-REWRITE2, PACK-EQUAL, CAR-CONS, and LABELLEDP, to the conjecture: (EQUAL (EQUAL 0 0) T). This simplifies, expanding EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LABELLEDP-EXPANSION (DEFN UNLABEL (X) (IF (LABELLEDP X) (CADDDR X) X)) [ 0.0 0.0 0.0 ] UNLABEL (PROVE-LEMMA UNLABEL-EXPANSION (REWRITE) (EQUAL (UNLABEL (CONS 'DL ARGS)) (CADDR ARGS))) WARNING: Note that the rewrite rule UNLABEL-EXPANSION will be stored so as to apply only to terms with the nonrecursive function symbol UNLABEL. This conjecture simplifies, rewriting with CDR-CONS and LABELLEDP-EXPANSION, and unfolding UNLABEL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] UNLABEL-EXPANSION (PROVE-LEMMA UNLABEL-UNLABELLEDP (REWRITE) (IMPLIES (NOT (EQUAL X 'DL)) (EQUAL (UNLABEL (CONS X Y)) (CONS X Y))) ((ENABLE UNLABEL LABELLEDP))) WARNING: Note that the rewrite rule UNLABEL-UNLABELLEDP will be stored so as to apply only to terms with the nonrecursive function symbol UNLABEL. This simplifies, rewriting with CAR-CONS, and opening up LABELLEDP and UNLABEL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] UNLABEL-UNLABELLEDP (DISABLE UNLABEL) [ 0.0 0.0 0.0 ] UNLABEL-OFF (DEFN FIND-LABELP (X LST) (IF (NLISTP LST) F (IF (AND (LABELLEDP (CAR LST)) (EQUAL X (CADR (CAR LST)))) T (FIND-LABELP X (CDR LST))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of AND, LABELLEDP, and NLISTP inform us that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, FIND-LABELP is accepted under the principle of definition. Observe that: (OR (FALSEP (FIND-LABELP X LST)) (TRUEP (FIND-LABELP X LST))) is a theorem. [ 0.0 0.0 0.0 ] FIND-LABELP (DEFN FIND-LABEL (X LST) (IF (NLISTP LST) 0 (IF (AND (LABELLEDP (CAR LST)) (EQUAL X (CADR (CAR LST)))) 0 (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 (LABEL PROGRAM) (TAG 'PC (CONS (CAR PROGRAM) (FIND-LABEL LABEL (PROGRAM-BODY PROGRAM))))) Observe that (LISTP (PC LABEL PROGRAM)) is a theorem. [ 0.0 0.0 0.0 ] PC (DEFN P-OBJECTP (X P) (AND (LISTP X) (EQUAL (CDDR X) NIL) (CASE (TYPE X) (NAT (SMALL-NATURALP (UNTAG X) (P-WORD-SIZE P))) (INT (SMALL-INTEGERP (UNTAG X) (P-WORD-SIZE P))) (BOOL (BOOLEANP (UNTAG X))) (ADDR (ADPP (UNTAG X) (P-DATA-SEGMENT P))) (PC (PCPP (UNTAG X) (P-PROG-SEGMENT P))) (SUBR (DEFINEDP (UNTAG X) (P-PROG-SEGMENT P))) (OTHERWISE F)))) Note that (OR (FALSEP (P-OBJECTP X P)) (TRUEP (P-OBJECTP X P))) is a theorem. [ 0.0 0.0 0.0 ] P-OBJECTP (DEFN P-OBJECTP-TYPE (TYPE X P) (AND (EQUAL (TYPE X) TYPE) (P-OBJECTP X P))) Observe that: (OR (FALSEP (P-OBJECTP-TYPE TYPE X P)) (TRUEP (P-OBJECTP-TYPE TYPE X P))) is a theorem. [ 0.0 0.0 0.0 ] P-OBJECTP-TYPE (DEFN ADD1-P-PC (P) (ADD1-ADDR (P-PC P))) From the definition we can conclude that (LISTP (ADD1-P-PC P)) is a theorem. [ 0.0 0.0 0.0 ] ADD1-P-PC (DEFN P-CURRENT-PROGRAM (P) (DEFINITION (AREA-NAME (P-PC P)) (P-PROG-SEGMENT P))) [ 0.0 0.0 0.0 ] P-CURRENT-PROGRAM (DEFN P-CURRENT-INSTRUCTION (P) (UNLABEL (GET (OFFSET (P-PC P)) (PROGRAM-BODY (P-CURRENT-PROGRAM P))))) [ 0.0 0.0 0.0 ] P-CURRENT-INSTRUCTION (DEFN P-FRAME (BINDINGS RET-PC) (LIST BINDINGS RET-PC)) From the definition we can conclude that: (LISTP (P-FRAME BINDINGS RET-PC)) is a theorem. [ 0.0 0.0 0.0 ] P-FRAME (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 (PROVE-LEMMA BINDINGS-FRAME (REWRITE) (AND (EQUAL (BINDINGS (CONS X Y)) X) (EQUAL (BINDINGS (P-FRAME X Y)) X))) WARNING: Note that the rewrite rule BINDINGS-FRAME will be stored so as to apply only to terms with the nonrecursive function symbol BINDINGS. WARNING: Note that the rewrite rule BINDINGS-FRAME will be stored so as to apply only to terms with the nonrecursive function symbol BINDINGS. WARNING: Note that the proposed lemma BINDINGS-FRAME is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviations AND, P-FRAME, CAR-CONS, and BINDINGS, to: (EQUAL X X), which simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] BINDINGS-FRAME (PROVE-LEMMA RET-PC-FRAME (REWRITE) (AND (EQUAL (RET-PC (LIST X Y)) Y) (EQUAL (RET-PC (P-FRAME X Y)) Y))) WARNING: Note that the rewrite rule RET-PC-FRAME will be stored so as to apply only to terms with the nonrecursive function symbol RET-PC. WARNING: Note that the rewrite rule RET-PC-FRAME will be stored so as to apply only to terms with the nonrecursive function symbol RET-PC. WARNING: Note that the proposed lemma RET-PC-FRAME is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This conjecture can be simplified, using the abbreviations AND, P-FRAME, CAR-CONS, CDR-CONS, and RET-PC, to the goal: (EQUAL Y Y). This simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RET-PC-FRAME (DISABLE P-FRAME) [ 0.0 0.0 0.0 ] P-FRAME-OFF (DISABLE BINDINGS) [ 0.0 0.0 0.0 ] BINDINGS-OFF (DISABLE RET-PC) [ 0.0 0.0 0.0 ] RET-PC-OFF (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 (DISABLE P-FRAME-SIZE) [ 0.0 0.0 0.0 ] P-FRAME-SIZE-OFF (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 LOCAL-VAR-VALUE (VAR CTRL-STK) (VALUE VAR (BINDINGS (TOP CTRL-STK)))) [ 0.0 0.0 0.0 ] LOCAL-VAR-VALUE (DEFN SET-LOCAL-VAR-VALUE (VAL VAR CTRL-STK) (PUSH (P-FRAME (PUT-VALUE VAL VAR (BINDINGS (TOP CTRL-STK))) (RET-PC (TOP CTRL-STK))) (POP CTRL-STK))) Note that (LISTP (SET-LOCAL-VAR-VALUE VAL VAR CTRL-STK)) is a theorem. [ 0.0 0.0 0.0 ] SET-LOCAL-VAR-VALUE (DEFN FIRST-N (N X) (IF (ZEROP N) NIL (CONS (CAR X) (FIRST-N (SUB1 N) (CDR X))))) 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, FIRST-N is accepted under the definitional principle. Note that: (OR (LITATOM (FIRST-N N X)) (LISTP (FIRST-N N X))) is a theorem. [ 0.0 0.0 0.0 ] FIRST-N (PROVE-LEMMA FIRST-N-ADD1 (REWRITE) (AND (EQUAL (FIRST-N (ADD1 N) (PUSH X Y)) (CONS X (FIRST-N N Y))) (EQUAL (FIRST-N (ADD1 N) (CONS X Y)) (CONS X (FIRST-N N Y))) (EQUAL (FIRST-N 0 Y) NIL))) WARNING: Note that the proposed lemma FIRST-N-ADD1 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and three replacement rules. This conjecture can be simplified, using the abbreviation AND, to three new formulas: Case 3. (EQUAL (FIRST-N (ADD1 N) (PUSH X Y)) (CONS X (FIRST-N N Y))), which simplifies, rewriting with SUB1-ADD1, CAR-CDR-PUSH, CAR-CONS, CDR-CONS, and APPEND-CONS-REWRITE2, and expanding the definition of FIRST-N, to: (IMPLIES (NOT (NUMBERP N)) (EQUAL (FIRST-N 0 Y) (FIRST-N N Y))), which again simplifies, unfolding the functions EQUAL and FIRST-N, to: T. Case 2. (EQUAL (FIRST-N (ADD1 N) (CONS X Y)) (CONS X (FIRST-N N Y))), which simplifies, rewriting with the lemmas CDR-CONS, SUB1-ADD1, CAR-CONS, and APPEND-CONS-REWRITE2, and unfolding the function FIRST-N, to: (IMPLIES (NOT (NUMBERP N)) (EQUAL (FIRST-N 0 Y) (FIRST-N N Y))). However this again simplifies, unfolding the definitions of EQUAL and FIRST-N, to: T. Case 1. (EQUAL (FIRST-N 0 Y) NIL), which simplifies, expanding the functions EQUAL and FIRST-N, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FIRST-N-ADD1 (PROVE-LEMMA FIRST-N-PLUS-APPEND (REWRITE) (IMPLIES (EQUAL N (LENGTH LST1)) (EQUAL (FIRST-N (PLUS N M) (APPEND LST1 LST2)) (APPEND LST1 (FIRST-N M LST2))))) Call the conjecture *1. We will try to prove it by induction. The recursive terms in the conjecture suggest four inductions. They merge into two likely candidate inductions, both of which are unflawed. However, one of these is more likely than the other. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP LST1) (p (CDR LST1) M LST2)) (p LST1 M LST2)) (IMPLIES (NOT (LISTP LST1)) (p LST1 M LST2))). Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT LST1) 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 goals: Case 2. (IMPLIES (AND (LISTP LST1) (EQUAL (FIRST-N (PLUS (LENGTH (CDR LST1)) M) (APPEND (CDR LST1) LST2)) (APPEND (CDR LST1) (FIRST-N M LST2)))) (EQUAL (FIRST-N (PLUS (LENGTH LST1) M) (APPEND LST1 LST2)) (APPEND LST1 (FIRST-N M LST2)))). This simplifies, applying the lemmas SUB1-ADD1 and FIRST-N-ADD1, and expanding the functions LENGTH, PLUS, and APPEND, to: T. Case 1. (IMPLIES (NOT (LISTP LST1)) (EQUAL (FIRST-N (PLUS (LENGTH LST1) M) (APPEND LST1 LST2)) (APPEND LST1 (FIRST-N M LST2)))). This simplifies, expanding LENGTH, EQUAL, PLUS, and APPEND, to the new formula: (IMPLIES (AND (NOT (LISTP LST1)) (NOT (NUMBERP M))) (EQUAL (FIRST-N 0 LST2) (FIRST-N M LST2))), which again simplifies, rewriting with the lemma FIRST-N-ADD1, and expanding the functions FIRST-N and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] FIRST-N-PLUS-APPEND (DISABLE FIRST-N-PLUS-APPEND) [ 0.0 0.0 0.0 ] FIRST-N-PLUS-APPEND-OFF (PROVE-LEMMA FIRST-N-APPEND2 (REWRITE) (IMPLIES (AND (PLISTP LST1) (EQUAL N (LENGTH LST1))) (EQUAL (FIRST-N N (APPEND LST1 LST2)) LST1))) Name the conjecture *1. We will try to prove it by induction. Three 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 LST1) (p LST1 LST2)) (IMPLIES (AND (NOT (NLISTP LST1)) (p (CDR LST1) LST2)) (p LST1 LST2))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT LST1) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates three new conjectures: Case 3. (IMPLIES (AND (NLISTP LST1) (PLISTP LST1)) (EQUAL (FIRST-N (LENGTH LST1) (APPEND LST1 LST2)) LST1)), which simplifies, rewriting with the lemmas PLISTP-ATOM, APPEND-NIL-LEMMA, and FIRST-N-ADD1, and unfolding the functions NLISTP, LENGTH, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP LST1)) (NOT (PLISTP (CDR LST1))) (PLISTP LST1)) (EQUAL (FIRST-N (LENGTH LST1) (APPEND LST1 LST2)) LST1)), which simplifies, expanding the functions NLISTP and PLISTP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP LST1)) (EQUAL (FIRST-N (LENGTH (CDR LST1)) (APPEND (CDR LST1) LST2)) (CDR LST1)) (PLISTP LST1)) (EQUAL (FIRST-N (LENGTH LST1) (APPEND LST1 LST2)) LST1)), which simplifies, applying CONS-CAR-CDR and FIRST-N-ADD1, and opening up the definitions of NLISTP, PLISTP, LENGTH, and APPEND, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] FIRST-N-APPEND2 (DISABLE FIRST-N-APPEND2) [ 0.0 0.0 0.0 ] FIRST-N-APPEND2-OFF (DEFN PAIRLIST (LST1 LST2) (IF (NLISTP LST1) NIL (CONS (CONS (CAR LST1) (CAR LST2)) (PAIRLIST (CDR LST1) (CDR LST2))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT LST1) decreases according to the well-founded relation LESSP in each recursive call. Hence, PAIRLIST is accepted under the definitional principle. Observe that: (OR (LITATOM (PAIRLIST LST1 LST2)) (LISTP (PAIRLIST LST1 LST2))) is a theorem. [ 0.0 0.0 0.0 ] PAIRLIST (PROVE-LEMMA PAIRLIST-PLISTP (REWRITE) (PLISTP (PAIRLIST X Y)) ((ENABLE PLISTP PAIRLIST))) Name the conjecture *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP X) (p X Y)) (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X) (CDR Y))) (p X Y))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show 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 Y. The above induction scheme leads to two new goals: Case 2. (IMPLIES (NLISTP X) (PLISTP (PAIRLIST X Y))), which simplifies, unfolding the definitions of NLISTP, PAIRLIST, and PLISTP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (PLISTP (PAIRLIST (CDR X) (CDR Y)))) (PLISTP (PAIRLIST X Y))), which simplifies, rewriting with the lemma PLISTP-CONS, and expanding NLISTP and PAIRLIST, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PAIRLIST-PLISTP (PROVE-LEMMA LENGTH-PAIRLIST (REWRITE) (EQUAL (LENGTH (PAIRLIST X Y)) (LENGTH X))) Call the conjecture *1. We will try to 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 (NLISTP X) (p X Y)) (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X) (CDR Y))) (p X Y))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to 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 Y. The above induction scheme generates the following two new formulas: Case 2. (IMPLIES (NLISTP X) (EQUAL (LENGTH (PAIRLIST X Y)) (LENGTH X))). This simplifies, expanding the definitions of NLISTP, PAIRLIST, LENGTH, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (EQUAL (LENGTH (PAIRLIST (CDR X) (CDR Y))) (LENGTH (CDR X)))) (EQUAL (LENGTH (PAIRLIST X Y)) (LENGTH X))). This simplifies, appealing to the lemma CDR-CONS, and opening up NLISTP, PAIRLIST, and LENGTH, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-PAIRLIST (PROVE-LEMMA PAIRLIST-DISTRIBUTES (REWRITE) (IMPLIES (EQUAL (LENGTH LST1) (LENGTH LST3)) (EQUAL (PAIRLIST (APPEND LST1 LST2) (APPEND LST3 LST4)) (APPEND (PAIRLIST LST1 LST3) (PAIRLIST LST2 LST4)))) ((ENABLE PAIRLIST))) Give the conjecture the name *1. Perhaps we can prove it by induction. There are six 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 LST1) (p (CDR LST1) LST2 (CDR LST3) LST4)) (p LST1 LST2 LST3 LST4)) (IMPLIES (NOT (LISTP LST1)) (p LST1 LST2 LST3 LST4))). Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure (COUNT LST1) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for LST3. The above induction scheme generates three new conjectures: Case 3. (IMPLIES (AND (LISTP LST1) (NOT (EQUAL (LENGTH (CDR LST1)) (LENGTH (CDR LST3)))) (EQUAL (LENGTH LST1) (LENGTH LST3))) (EQUAL (PAIRLIST (APPEND LST1 LST2) (APPEND LST3 LST4)) (APPEND (PAIRLIST LST1 LST3) (PAIRLIST LST2 LST4)))), which simplifies, rewriting with CDR-CONS, CAR-CONS, CAR-NLISTP, APPEND-CONS-REWRITE, APPEND-CONS-REWRITE2, and CONS-EQUAL, and expanding the definitions of LENGTH, APPEND, and PAIRLIST, to the following three new formulas: Case 3.3. (IMPLIES (AND (LISTP LST1) (NOT (EQUAL (LENGTH (CDR LST1)) (LENGTH (CDR LST3)))) (NOT (LISTP LST3)) (EQUAL (ADD1 (LENGTH (CDR LST1))) 0)) (EQUAL (CAR LST4) 0)). This again simplifies, using linear arithmetic, to: T. Case 3.2. (IMPLIES (AND (LISTP LST1) (NOT (EQUAL (LENGTH (CDR LST1)) (LENGTH (CDR LST3)))) (NOT (LISTP LST3)) (EQUAL (ADD1 (LENGTH (CDR LST1))) 0)) (EQUAL (PAIRLIST (APPEND (CDR LST1) LST2) (CDR LST4)) (APPEND (PAIRLIST (CDR LST1) (CDR LST3)) (PAIRLIST LST2 LST4)))), which again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (LISTP LST1) (NOT (EQUAL (LENGTH (CDR LST1)) (LENGTH (CDR LST3)))) (LISTP LST3) (EQUAL (ADD1 (LENGTH (CDR LST1))) (ADD1 (LENGTH (CDR LST3))))) (EQUAL (PAIRLIST (APPEND (CDR LST1) LST2) (APPEND (CDR LST3) LST4)) (APPEND (PAIRLIST (CDR LST1) (CDR LST3)) (PAIRLIST LST2 LST4)))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (LISTP LST1) (EQUAL (PAIRLIST (APPEND (CDR LST1) LST2) (APPEND (CDR LST3) LST4)) (APPEND (PAIRLIST (CDR LST1) (CDR LST3)) (PAIRLIST LST2 LST4))) (EQUAL (LENGTH LST1) (LENGTH LST3))) (EQUAL (PAIRLIST (APPEND LST1 LST2) (APPEND LST3 LST4)) (APPEND (PAIRLIST LST1 LST3) (PAIRLIST LST2 LST4)))), which simplifies, appealing to the lemmas CDR-CONS, CAR-CONS, CAR-NLISTP, APPEND-CONS-REWRITE, APPEND-CONS-REWRITE2, and CONS-EQUAL, and unfolding the functions LENGTH, APPEND, and PAIRLIST, to two new goals: Case 2.2. (IMPLIES (AND (LISTP LST1) (EQUAL (PAIRLIST (APPEND (CDR LST1) LST2) (APPEND (CDR LST3) LST4)) (APPEND (PAIRLIST (CDR LST1) (CDR LST3)) (PAIRLIST LST2 LST4))) (NOT (LISTP LST3)) (EQUAL (ADD1 (LENGTH (CDR LST1))) 0)) (EQUAL (CAR LST4) 0)), which again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (LISTP LST1) (EQUAL (PAIRLIST (APPEND (CDR LST1) LST2) (APPEND (CDR LST3) LST4)) (APPEND (PAIRLIST (CDR LST1) (CDR LST3)) (PAIRLIST LST2 LST4))) (NOT (LISTP LST3)) (EQUAL (ADD1 (LENGTH (CDR LST1))) 0)) (EQUAL (PAIRLIST (APPEND (CDR LST1) LST2) (CDR LST4)) (APPEND (PAIRLIST (CDR LST1) (CDR LST3)) (PAIRLIST LST2 LST4)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (LISTP LST1)) (EQUAL (LENGTH LST1) (LENGTH LST3))) (EQUAL (PAIRLIST (APPEND LST1 LST2) (APPEND LST3 LST4)) (APPEND (PAIRLIST LST1 LST3) (PAIRLIST LST2 LST4)))), which simplifies, applying APPEND-NIL-LEMMA, and unfolding the definitions of LENGTH, APPEND, and PAIRLIST, to: (IMPLIES (AND (NOT (LISTP LST1)) (EQUAL 0 (ADD1 (LENGTH (CDR LST3)))) (LISTP LST3)) (EQUAL (PAIRLIST LST2 (CONS (CAR LST3) (APPEND (CDR LST3) LST4))) (PAIRLIST LST2 LST4))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PAIRLIST-DISTRIBUTES (DISABLE PAIRLIST-DISTRIBUTES) [ 0.0 0.0 0.0 ] PAIRLIST-DISTRIBUTES-OFF (DEFN PAIR-FORMAL-VARS-WITH-ACTUALS (FORMAL-VARS TEMP-STK) (PAIRLIST FORMAL-VARS (REVERSE (FIRST-N (LENGTH FORMAL-VARS) TEMP-STK)))) Note that: (OR (LITATOM (PAIR-FORMAL-VARS-WITH-ACTUALS FORMAL-VARS TEMP-STK)) (LISTP (PAIR-FORMAL-VARS-WITH-ACTUALS FORMAL-VARS TEMP-STK))) is a theorem. [ 0.0 0.0 0.0 ] PAIR-FORMAL-VARS-WITH-ACTUALS (DEFN PAIR-TEMPS-WITH-INITIAL-VALUES (TEMP-VAR-DCLS) (IF (NLISTP TEMP-VAR-DCLS) NIL (CONS (CONS (CAAR TEMP-VAR-DCLS) (CADAR TEMP-VAR-DCLS)) (PAIR-TEMPS-WITH-INITIAL-VALUES (CDR TEMP-VAR-DCLS))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT TEMP-VAR-DCLS) decreases according to the well-founded relation LESSP in each recursive call. Hence, PAIR-TEMPS-WITH-INITIAL-VALUES is accepted under the principle of definition. Note that: (OR (LITATOM (PAIR-TEMPS-WITH-INITIAL-VALUES TEMP-VAR-DCLS)) (LISTP (PAIR-TEMPS-WITH-INITIAL-VALUES TEMP-VAR-DCLS))) is a theorem. [ 0.0 0.0 0.0 ] PAIR-TEMPS-WITH-INITIAL-VALUES (PROVE-LEMMA LENGTH-PAIR-TEMPS-WITH-INITIAL-VALUES (REWRITE) (EQUAL (LENGTH (PAIR-TEMPS-WITH-INITIAL-VALUES LST)) (LENGTH LST)) ((ENABLE PAIR-TEMPS-WITH-INITIAL-VALUES))) 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 LST) (p LST)) (IMPLIES (AND (NOT (NLISTP LST)) (p (CDR LST))) (p 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 induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (NLISTP LST) (EQUAL (LENGTH (PAIR-TEMPS-WITH-INITIAL-VALUES LST)) (LENGTH LST))). This simplifies, expanding the functions NLISTP, PAIR-TEMPS-WITH-INITIAL-VALUES, LENGTH, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP LST)) (EQUAL (LENGTH (PAIR-TEMPS-WITH-INITIAL-VALUES (CDR LST))) (LENGTH (CDR LST)))) (EQUAL (LENGTH (PAIR-TEMPS-WITH-INITIAL-VALUES LST)) (LENGTH LST))). This simplifies, rewriting with the lemma CDR-CONS, and opening up NLISTP, PAIR-TEMPS-WITH-INITIAL-VALUES, and LENGTH, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-PAIR-TEMPS-WITH-INITIAL-VALUES (DEFN MAKE-P-CALL-FRAME (FORMAL-VARS TEMP-STK TEMP-VAR-DCLS RET-PC) (P-FRAME (APPEND (PAIR-FORMAL-VARS-WITH-ACTUALS FORMAL-VARS TEMP-STK) (PAIR-TEMPS-WITH-INITIAL-VALUES TEMP-VAR-DCLS)) RET-PC)) Note that: (LISTP (MAKE-P-CALL-FRAME FORMAL-VARS TEMP-STK TEMP-VAR-DCLS RET-PC)) is a theorem. [ 0.0 0.0 0.0 ] MAKE-P-CALL-FRAME (DEFN P-CALL-OKP (INS P) (AND (NOT (LESSP (P-MAX-CTRL-STK-SIZE P) (P-CTRL-STK-SIZE (PUSH (MAKE-P-CALL-FRAME (FORMAL-VARS (DEFINITION (CADR INS) (P-PROG-SEGMENT P))) (P-TEMP-STK P) (TEMP-VAR-DCLS (DEFINITION (CADR INS) (P-PROG-SEGMENT P))) (ADD1-ADDR (P-PC P))) (P-CTRL-STK P))))) (NOT (LESSP (LENGTH (P-TEMP-STK P)) (LENGTH (FORMAL-VARS (DEFINITION (CADR INS) (P-PROG-SEGMENT P)))))))) From the definition we can conclude that: (OR (FALSEP (P-CALL-OKP INS P)) (TRUEP (P-CALL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-CALL-OKP (DEFN P-CALL-STEP (INS P) (P-STATE (TAG 'PC (CONS (CADR INS) 0)) (PUSH (MAKE-P-CALL-FRAME (FORMAL-VARS (DEFINITION (CADR INS) (P-PROG-SEGMENT P))) (P-TEMP-STK P) (TEMP-VAR-DCLS (DEFINITION (CADR INS) (P-PROG-SEGMENT P))) (ADD1-ADDR (P-PC P))) (P-CTRL-STK P)) (POPN (LENGTH (FORMAL-VARS (DEFINITION (CADR INS) (P-PROG-SEGMENT P)))) (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) From the definition we can conclude that (P-STATEP (P-CALL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-CALL-STEP (DEFN P-RET-OKP (INS P) T) WARNING: INS and P are in the arglist but not in the body of the definition of P-RET-OKP. Note that (TRUEP (P-RET-OKP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-RET-OKP (DEFN P-RET-STEP (INS P) (IF (LISTP (POP (P-CTRL-STK P))) (P-STATE (RET-PC (TOP (P-CTRL-STK P))) (POP (P-CTRL-STK P)) (P-TEMP-STK P) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN) (P-HALT P 'HALT))) WARNING: INS is in the arglist but not in the body of the definition of P-RET-STEP. Note that (P-STATEP (P-RET-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-RET-STEP (DEFN P-PUSH-CONSTANT-OKP (INS P) (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P))) WARNING: INS is in the arglist but not in the body of the definition of P-PUSH-CONSTANT-OKP. Observe that: (OR (FALSEP (P-PUSH-CONSTANT-OKP INS P)) (TRUEP (P-PUSH-CONSTANT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-CONSTANT-OKP (DEFN UNABBREVIATE-CONSTANT (C P) (IF (EQUAL C 'PC) (ADD1-P-PC P) (IF (NLISTP C) (PC C (P-CURRENT-PROGRAM P)) C))) From the definition we can conclude that: (LISTP (UNABBREVIATE-CONSTANT C P)) is a theorem. [ 0.0 0.0 0.0 ] UNABBREVIATE-CONSTANT (DEFN P-PUSH-CONSTANT-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (UNABBREVIATE-CONSTANT (CADR INS) P) (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Note that (P-STATEP (P-PUSH-CONSTANT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-CONSTANT-STEP (DEFN P-PUSH-LOCAL-OKP (INS P) (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P))) WARNING: INS is in the arglist but not in the body of the definition of P-PUSH-LOCAL-OKP. Observe that: (OR (FALSEP (P-PUSH-LOCAL-OKP INS P)) (TRUEP (P-PUSH-LOCAL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-LOCAL-OKP (DEFN P-PUSH-LOCAL-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (LOCAL-VAR-VALUE (CADR INS) (P-CTRL-STK P)) (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Observe that (P-STATEP (P-PUSH-LOCAL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-LOCAL-STEP (DEFN P-PUSH-GLOBAL-OKP (INS P) (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P))) WARNING: INS is in the arglist but not in the body of the definition of P-PUSH-GLOBAL-OKP. Observe that: (OR (FALSEP (P-PUSH-GLOBAL-OKP INS P)) (TRUEP (P-PUSH-GLOBAL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-GLOBAL-OKP (DEFN P-PUSH-GLOBAL-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (FETCH (TAG 'ADDR (CONS (CADR INS) 0)) (P-DATA-SEGMENT P)) (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) From the definition we can conclude that: (P-STATEP (P-PUSH-GLOBAL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-GLOBAL-STEP (DEFN P-PUSH-TEMP-STK-INDEX-OKP (INS P) (AND (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P)) (LESSP (CADR INS) (LENGTH (P-TEMP-STK P))))) Observe that: (OR (FALSEP (P-PUSH-TEMP-STK-INDEX-OKP INS P)) (TRUEP (P-PUSH-TEMP-STK-INDEX-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-TEMP-STK-INDEX-OKP (DEFN P-PUSH-TEMP-STK-INDEX-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'NAT (SUB1 (DIFFERENCE (LENGTH (P-TEMP-STK P)) (CADR INS)))) (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Note that (P-STATEP (P-PUSH-TEMP-STK-INDEX-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-PUSH-TEMP-STK-INDEX-STEP (DEFN P-POP-OKP (INS P) (LISTP (P-TEMP-STK P))) WARNING: INS is in the arglist but not in the body of the definition of P-POP-OKP. Observe that (OR (FALSEP (P-POP-OKP INS P)) (TRUEP (P-POP-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-POP-OKP (DEFN P-POP-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (POP (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-POP-STEP. Note that (P-STATEP (P-POP-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-POP-STEP (DEFN P-POP*-OKP (INS P) (NOT (LESSP (LENGTH (P-TEMP-STK P)) (CADR INS)))) Note that (OR (FALSEP (P-POP*-OKP INS P)) (TRUEP (P-POP*-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-POP*-OKP (DEFN P-POP*-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (POPN (CADR INS) (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Note that (P-STATEP (P-POP*-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-POP*-STEP (DEFN P-POP-LOCAL-OKP (INS P) (LISTP (P-TEMP-STK P))) WARNING: INS is in the arglist but not in the body of the definition of P-POP-LOCAL-OKP. Observe that: (OR (FALSEP (P-POP-LOCAL-OKP INS P)) (TRUEP (P-POP-LOCAL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-POP-LOCAL-OKP (DEFN P-POP-LOCAL-STEP (INS P) (P-STATE (ADD1-P-PC P) (SET-LOCAL-VAR-VALUE (TOP (P-TEMP-STK P)) (CADR INS) (P-CTRL-STK P)) (POP (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) From the definition we can conclude that: (P-STATEP (P-POP-LOCAL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-POP-LOCAL-STEP (DEFN P-POP-GLOBAL-OKP (INS P) (LISTP (P-TEMP-STK P))) WARNING: INS is in the arglist but not in the body of the definition of P-POP-GLOBAL-OKP. Observe that: (OR (FALSEP (P-POP-GLOBAL-OKP INS P)) (TRUEP (P-POP-GLOBAL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-POP-GLOBAL-OKP (DEFN P-POP-GLOBAL-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (POP (P-TEMP-STK P)) (P-PROG-SEGMENT P) (DEPOSIT (TOP (P-TEMP-STK P)) (TAG 'ADDR (CONS (CADR INS) 0)) (P-DATA-SEGMENT P)) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Note that (P-STATEP (P-POP-GLOBAL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-POP-GLOBAL-STEP (DEFN P-FETCH-TEMP-STK-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE 'NAT (TOP (P-TEMP-STK P)) P) (LESSP (UNTAG (TOP (P-TEMP-STK P))) (LENGTH (P-TEMP-STK P))))) WARNING: INS is in the arglist but not in the body of the definition of P-FETCH-TEMP-STK-OKP. From the definition we can conclude that: (OR (FALSEP (P-FETCH-TEMP-STK-OKP INS P)) (TRUEP (P-FETCH-TEMP-STK-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-FETCH-TEMP-STK-OKP (DEFN P-FETCH-TEMP-STK-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (RGET (UNTAG (TOP (P-TEMP-STK P))) (P-TEMP-STK P)) (POP (P-TEMP-STK P))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-FETCH-TEMP-STK-STEP. From the definition we can conclude that: (P-STATEP (P-FETCH-TEMP-STK-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-FETCH-TEMP-STK-STEP (DEFN P-DEPOSIT-TEMP-STK-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'NAT (TOP (P-TEMP-STK P)) P) (LESSP (UNTAG (TOP (P-TEMP-STK P))) (LENGTH (POP (POP (P-TEMP-STK P))))))) WARNING: INS is in the arglist but not in the body of the definition of P-DEPOSIT-TEMP-STK-OKP. Note that: (OR (FALSEP (P-DEPOSIT-TEMP-STK-OKP INS P)) (TRUEP (P-DEPOSIT-TEMP-STK-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-DEPOSIT-TEMP-STK-OKP (DEFN P-DEPOSIT-TEMP-STK-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (RPUT (TOP1 (P-TEMP-STK P)) (UNTAG (TOP (P-TEMP-STK P))) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-DEPOSIT-TEMP-STK-STEP. Note that (P-STATEP (P-DEPOSIT-TEMP-STK-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-DEPOSIT-TEMP-STK-STEP (DEFN P-JUMP-OKP (INS P) T) WARNING: INS and P are in the arglist but not in the body of the definition of P-JUMP-OKP. Note that (TRUEP (P-JUMP-OKP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-JUMP-OKP (DEFN P-JUMP-STEP (INS P) (P-STATE (PC (CADR INS) (P-CURRENT-PROGRAM P)) (P-CTRL-STK P) (P-TEMP-STK P) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Note that (P-STATEP (P-JUMP-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-JUMP-STEP (DEFN P-JUMP-CASE-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE 'NAT (TOP (P-TEMP-STK P)) P) (LESSP (UNTAG (TOP (P-TEMP-STK P))) (LENGTH (CDR INS))))) From the definition we can conclude that: (OR (FALSEP (P-JUMP-CASE-OKP INS P)) (TRUEP (P-JUMP-CASE-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-JUMP-CASE-OKP (DEFN P-JUMP-CASE-STEP (INS P) (P-STATE (PC (GET (UNTAG (TOP (P-TEMP-STK P))) (CDR INS)) (P-CURRENT-PROGRAM P)) (P-CTRL-STK P) (POP (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) From the definition we can conclude that: (P-STATEP (P-JUMP-CASE-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-JUMP-CASE-STEP (DEFN P-SET-LOCAL-OKP (INS P) (LISTP (P-TEMP-STK P))) WARNING: INS is in the arglist but not in the body of the definition of P-SET-LOCAL-OKP. Observe that: (OR (FALSEP (P-SET-LOCAL-OKP INS P)) (TRUEP (P-SET-LOCAL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-SET-LOCAL-OKP (DEFN P-SET-LOCAL-STEP (INS P) (P-STATE (ADD1-P-PC P) (SET-LOCAL-VAR-VALUE (TOP (P-TEMP-STK P)) (CADR INS) (P-CTRL-STK P)) (P-TEMP-STK P) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) Observe that (P-STATEP (P-SET-LOCAL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-SET-LOCAL-STEP (DEFN P-TEST-AND-JUMP-OKP (INS TYPE TEST P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE TYPE (TOP (P-TEMP-STK P)) P))) WARNING: INS and TEST are in the arglist but not in the body of the definition of P-TEST-AND-JUMP-OKP. From the definition we can conclude that: (OR (FALSEP (P-TEST-AND-JUMP-OKP INS TYPE TEST P)) (TRUEP (P-TEST-AND-JUMP-OKP INS TYPE TEST P))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-AND-JUMP-OKP (DEFN P-TEST-AND-JUMP-STEP (TEST LAB P) (IF TEST (P-STATE (PC LAB (P-CURRENT-PROGRAM P)) (P-CTRL-STK P) (POP (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (POP (P-TEMP-STK P)) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN))) Observe that (P-STATEP (P-TEST-AND-JUMP-STEP TEST LAB P)) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-AND-JUMP-STEP (DEFN P-TEST-NATP (FLG X) (CASE FLG (ZERO (EQUAL X 0)) (OTHERWISE (NOT (EQUAL X 0))))) Note that (OR (FALSEP (P-TEST-NATP FLG X)) (TRUEP (P-TEST-NATP FLG X))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-NATP (DEFN P-TEST-NAT-AND-JUMP-OKP (INS P) (P-TEST-AND-JUMP-OKP INS 'NAT (P-TEST-NATP (CADR INS) (UNTAG (TOP (P-TEMP-STK P)))) P)) Observe that: (OR (FALSEP (P-TEST-NAT-AND-JUMP-OKP INS P)) (TRUEP (P-TEST-NAT-AND-JUMP-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-NAT-AND-JUMP-OKP (DEFN P-TEST-NAT-AND-JUMP-STEP (INS P) (P-TEST-AND-JUMP-STEP (P-TEST-NATP (CADR INS) (UNTAG (TOP (P-TEMP-STK P)))) (CADDR INS) P)) Observe that (P-STATEP (P-TEST-NAT-AND-JUMP-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-NAT-AND-JUMP-STEP (DEFN P-TEST-INTP (FLG X) (CASE FLG (ZERO (EQUAL X 0)) (NOT-ZERO (NOT (EQUAL X 0))) (NEG (NEGATIVEP X)) (NOT-NEG (NOT (NEGATIVEP X))) (POS (AND (NUMBERP X) (NOT (EQUAL X 0)))) (OTHERWISE (OR (EQUAL X 0) (NEGATIVEP X))))) Note that (OR (FALSEP (P-TEST-INTP FLG X)) (TRUEP (P-TEST-INTP FLG X))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-INTP (DEFN P-TEST-INT-AND-JUMP-OKP (INS P) (P-TEST-AND-JUMP-OKP INS 'INT (P-TEST-INTP (CADR INS) (UNTAG (TOP (P-TEMP-STK P)))) P)) Observe that: (OR (FALSEP (P-TEST-INT-AND-JUMP-OKP INS P)) (TRUEP (P-TEST-INT-AND-JUMP-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-INT-AND-JUMP-OKP (DEFN P-TEST-INT-AND-JUMP-STEP (INS P) (P-TEST-AND-JUMP-STEP (P-TEST-INTP (CADR INS) (UNTAG (TOP (P-TEMP-STK P)))) (CADDR INS) P)) Observe that (P-STATEP (P-TEST-INT-AND-JUMP-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-INT-AND-JUMP-STEP (DEFN P-TEST-BOOLP (FLG X) (CASE FLG (T (EQUAL X 'T)) (OTHERWISE (EQUAL X 'F)))) From the definition we can conclude that: (OR (FALSEP (P-TEST-BOOLP FLG X)) (TRUEP (P-TEST-BOOLP FLG X))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-BOOLP (DEFN P-TEST-BOOL-AND-JUMP-OKP (INS P) (P-TEST-AND-JUMP-OKP INS 'BOOL (P-TEST-BOOLP (CADR INS) (UNTAG (TOP (P-TEMP-STK P)))) P)) Observe that: (OR (FALSEP (P-TEST-BOOL-AND-JUMP-OKP INS P)) (TRUEP (P-TEST-BOOL-AND-JUMP-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-BOOL-AND-JUMP-OKP (DEFN P-TEST-BOOL-AND-JUMP-STEP (INS P) (P-TEST-AND-JUMP-STEP (P-TEST-BOOLP (CADR INS) (UNTAG (TOP (P-TEMP-STK P)))) (CADDR INS) P)) Observe that (P-STATEP (P-TEST-BOOL-AND-JUMP-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-TEST-BOOL-AND-JUMP-STEP (DEFN P-NO-OP-OKP (INS P) T) WARNING: INS and P are in the arglist but not in the body of the definition of P-NO-OP-OKP. Note that (TRUEP (P-NO-OP-OKP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-NO-OP-OKP (DEFN P-NO-OP-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (P-TEMP-STK P) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-NO-OP-STEP. From the definition we can conclude that (P-STATEP (P-NO-OP-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-NO-OP-STEP (DEFN P-EQ-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (EQUAL (TYPE (TOP (P-TEMP-STK P))) (TYPE (TOP1 (P-TEMP-STK P)))))) WARNING: INS is in the arglist but not in the body of the definition of P-EQ-OKP. Observe that (OR (FALSEP (P-EQ-OKP INS P)) (TRUEP (P-EQ-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-EQ-OKP (DEFN P-EQ-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (BOOL (EQUAL (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-EQ-STEP. Note that (P-STATEP (P-EQ-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-EQ-STEP (DEFN P-ADD-INT-WITH-CARRY-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (LISTP (POP (POP (P-TEMP-STK P)))) (P-OBJECTP-TYPE 'INT (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'INT (TOP1 (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'BOOL (TOP2 (P-TEMP-STK P)) P))) WARNING: INS is in the arglist but not in the body of the definition of P-ADD-INT-WITH-CARRY-OKP. Note that: (OR (FALSEP (P-ADD-INT-WITH-CARRY-OKP INS P)) (TRUEP (P-ADD-INT-WITH-CARRY-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-ADD-INT-WITH-CARRY-OKP (DEFN P-ADD-INT-WITH-CARRY-STEP (INS P) (LET ((SUM (IPLUS (BOOL-TO-NAT (UNTAG (TOP2 (P-TEMP-STK P)))) (IPLUS (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))))) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'INT (FIX-SMALL-INTEGER SUM (P-WORD-SIZE P))) (PUSH (BOOL (NOT (SMALL-INTEGERP SUM (P-WORD-SIZE P)))) (POP (POP (POP (P-TEMP-STK P)))))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN))) WARNING: INS is in the arglist but not in the body of the definition of: P-ADD-INT-WITH-CARRY-STEP. From the definition we can conclude that: (P-STATEP (P-ADD-INT-WITH-CARRY-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-ADD-INT-WITH-CARRY-STEP (DEFN P-SUB-INT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'INT (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'INT (TOP1 (P-TEMP-STK P)) P) (SMALL-INTEGERP (IDIFFERENCE (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P)))) (P-WORD-SIZE P)))) WARNING: INS is in the arglist but not in the body of the definition of P-SUB-INT-OKP. Observe that: (OR (FALSEP (P-SUB-INT-OKP INS P)) (TRUEP (P-SUB-INT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-SUB-INT-OKP (DEFN P-SUB-INT-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'INT (IDIFFERENCE (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-SUB-INT-STEP. Note that (P-STATEP (P-SUB-INT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-SUB-INT-STEP (DEFN P-SUB-INT-WITH-CARRY-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (LISTP (POP (POP (P-TEMP-STK P)))) (P-OBJECTP-TYPE 'INT (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'INT (TOP1 (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'BOOL (TOP2 (P-TEMP-STK P)) P))) WARNING: INS is in the arglist but not in the body of the definition of P-SUB-INT-WITH-CARRY-OKP. Note that: (OR (FALSEP (P-SUB-INT-WITH-CARRY-OKP INS P)) (TRUEP (P-SUB-INT-WITH-CARRY-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-SUB-INT-WITH-CARRY-OKP (DEFN P-SUB-INT-WITH-CARRY-STEP (INS P) (LET ((DIFF (IDIFFERENCE (UNTAG (TOP1 (P-TEMP-STK P))) (IPLUS (UNTAG (TOP (P-TEMP-STK P))) (BOOL-TO-NAT (UNTAG (TOP2 (P-TEMP-STK P)))))))) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'INT (FIX-SMALL-INTEGER DIFF (P-WORD-SIZE P))) (PUSH (BOOL (NOT (SMALL-INTEGERP DIFF (P-WORD-SIZE P)))) (POP (POP (POP (P-TEMP-STK P)))))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN))) WARNING: INS is in the arglist but not in the body of the definition of: P-SUB-INT-WITH-CARRY-STEP. From the definition we can conclude that: (P-STATEP (P-SUB-INT-WITH-CARRY-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-SUB-INT-WITH-CARRY-STEP (DEFN P-NEG-INT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE 'INT (TOP (P-TEMP-STK P)) P) (SMALL-INTEGERP (INEGATE (UNTAG (TOP (P-TEMP-STK P)))) (P-WORD-SIZE P)))) WARNING: INS is in the arglist but not in the body of the definition of P-NEG-INT-OKP. From the definition we can conclude that: (OR (FALSEP (P-NEG-INT-OKP INS P)) (TRUEP (P-NEG-INT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-NEG-INT-OKP (DEFN P-NEG-INT-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'INT (INEGATE (UNTAG (TOP (P-TEMP-STK P))))) (POP (P-TEMP-STK P))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-NEG-INT-STEP. Note that (P-STATEP (P-NEG-INT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-NEG-INT-STEP (DEFN P-LT-INT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'INT (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'INT (TOP1 (P-TEMP-STK P)) P))) WARNING: INS is in the arglist but not in the body of the definition of P-LT-INT-OKP. From the definition we can conclude that: (OR (FALSEP (P-LT-INT-OKP INS P)) (TRUEP (P-LT-INT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-LT-INT-OKP (DEFN P-LT-INT-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (BOOL (ILESSP (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-LT-INT-STEP. Note that (P-STATEP (P-LT-INT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-LT-INT-STEP (DEFN P-INT-TO-NAT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE 'INT (TOP (P-TEMP-STK P)) P) (NOT (NEGATIVEP (UNTAG (TOP (P-TEMP-STK P))))))) WARNING: INS is in the arglist but not in the body of the definition of P-INT-TO-NAT-OKP. Note that: (OR (FALSEP (P-INT-TO-NAT-OKP INS P)) (TRUEP (P-INT-TO-NAT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-INT-TO-NAT-OKP (DEFN P-INT-TO-NAT-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'NAT (UNTAG (TOP (P-TEMP-STK P)))) (POP (P-TEMP-STK P))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-INT-TO-NAT-STEP. From the definition we can conclude that: (P-STATEP (P-INT-TO-NAT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-INT-TO-NAT-STEP (DEFN P-ADD-NAT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'NAT (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'NAT (TOP1 (P-TEMP-STK P)) P) (SMALL-NATURALP (PLUS (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P)))) (P-WORD-SIZE P)))) WARNING: INS is in the arglist but not in the body of the definition of P-ADD-NAT-OKP. Observe that: (OR (FALSEP (P-ADD-NAT-OKP INS P)) (TRUEP (P-ADD-NAT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-ADD-NAT-OKP (DEFN P-ADD-NAT-STEP (INS P) (LET ((SUM (PLUS (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P)))))) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'NAT SUM) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN))) WARNING: INS is in the arglist but not in the body of the definition of P-ADD-NAT-STEP. Note that (P-STATEP (P-ADD-NAT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-ADD-NAT-STEP (DEFN P-SUB-NAT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'NAT (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'NAT (TOP1 (P-TEMP-STK P)) P) (NOT (LESSP (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))))) WARNING: INS is in the arglist but not in the body of the definition of P-SUB-NAT-OKP. Observe that: (OR (FALSEP (P-SUB-NAT-OKP INS P)) (TRUEP (P-SUB-NAT-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-SUB-NAT-OKP (DEFN P-SUB-NAT-STEP (INS P) (LET ((Y (UNTAG (TOP (P-TEMP-STK P)))) (X (UNTAG (TOP1 (P-TEMP-STK P))))) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'NAT (DIFFERENCE X Y)) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN))) WARNING: INS is in the arglist but not in the body of the definition of P-SUB-NAT-STEP. Note that (P-STATEP (P-SUB-NAT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-SUB-NAT-STEP (DEFN P-SUB1-NAT-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE 'NAT (TOP (P-TEMP-STK P)) P) (NOT (ZEROP (UNTAG (TOP (P-TEMP-STK P))))))) WARNING: INS is in the arglist but not in the body of the definition of P-SUB1-NAT-OKP. Note that: (OR (FALSEP (P-SUB1-NAT-OKP INS P)) (TRUEP (P-SUB1-NAT-OKP INS P))) is a theorem. [ 0.1 0.0 0.0 ] P-SUB1-NAT-OKP (DEFN P-SUB1-NAT-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'NAT (SUB1 (UNTAG (TOP (P-TEMP-STK P))))) (POP (P-TEMP-STK P))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-SUB1-NAT-STEP. Note that (P-STATEP (P-SUB1-NAT-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-SUB1-NAT-STEP (DEFN P-OR-BOOL-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'BOOL (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'BOOL (TOP1 (P-TEMP-STK P)) P))) WARNING: INS is in the arglist but not in the body of the definition of P-OR-BOOL-OKP. From the definition we can conclude that: (OR (FALSEP (P-OR-BOOL-OKP INS P)) (TRUEP (P-OR-BOOL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-OR-BOOL-OKP (DEFN P-OR-BOOL-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'BOOL (OR-BOOL (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-OR-BOOL-STEP. Note that (P-STATEP (P-OR-BOOL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-OR-BOOL-STEP (DEFN P-AND-BOOL-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (LISTP (POP (P-TEMP-STK P))) (P-OBJECTP-TYPE 'BOOL (TOP (P-TEMP-STK P)) P) (P-OBJECTP-TYPE 'BOOL (TOP1 (P-TEMP-STK P)) P))) WARNING: INS is in the arglist but not in the body of the definition of P-AND-BOOL-OKP. From the definition we can conclude that: (OR (FALSEP (P-AND-BOOL-OKP INS P)) (TRUEP (P-AND-BOOL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-AND-BOOL-OKP (DEFN P-AND-BOOL-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'BOOL (AND-BOOL (UNTAG (TOP1 (P-TEMP-STK P))) (UNTAG (TOP (P-TEMP-STK P))))) (POP (POP (P-TEMP-STK P)))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-AND-BOOL-STEP. Note that (P-STATEP (P-AND-BOOL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-AND-BOOL-STEP (DEFN P-NOT-BOOL-OKP (INS P) (AND (LISTP (P-TEMP-STK P)) (P-OBJECTP-TYPE 'BOOL (TOP (P-TEMP-STK P)) P))) WARNING: INS is in the arglist but not in the body of the definition of P-NOT-BOOL-OKP. From the definition we can conclude that: (OR (FALSEP (P-NOT-BOOL-OKP INS P)) (TRUEP (P-NOT-BOOL-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-NOT-BOOL-OKP (DEFN P-NOT-BOOL-STEP (INS P) (P-STATE (ADD1-P-PC P) (P-CTRL-STK P) (PUSH (TAG 'BOOL (NOT-BOOL (UNTAG (TOP (P-TEMP-STK P))))) (POP (P-TEMP-STK P))) (P-PROG-SEGMENT P) (P-DATA-SEGMENT P) (P-MAX-CTRL-STK-SIZE P) (P-MAX-TEMP-STK-SIZE P) (P-WORD-SIZE P) 'RUN)) WARNING: INS is in the arglist but not in the body of the definition of P-NOT-BOOL-STEP. Note that (P-STATEP (P-NOT-BOOL-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-NOT-BOOL-STEP (DEFN X-Y-ERROR-MSG (X Y) (PACK (APPEND (UNPACK 'ILLEGAL-) (APPEND (UNPACK Y) (CDR (UNPACK 'G-INSTRUCTION)))))) WARNING: X is in the arglist but not in the body of the definition of X-Y-ERROR-MSG. Observe that (LITATOM (X-Y-ERROR-MSG X Y)) is a theorem. [ 0.0 0.0 0.0 ] X-Y-ERROR-MSG (DEFN P-INS-OKP (INS P) (CASE (CAR INS) (CALL (P-CALL-OKP INS P)) (RET (P-RET-OKP INS P)) (PUSH-CONSTANT (P-PUSH-CONSTANT-OKP INS P)) (PUSH-LOCAL (P-PUSH-LOCAL-OKP INS P)) (PUSH-GLOBAL (P-PUSH-GLOBAL-OKP INS P)) (PUSH-TEMP-STK-INDEX (P-PUSH-TEMP-STK-INDEX-OKP INS P)) (POP (P-POP-OKP INS P)) (POP* (P-POP*-OKP INS P)) (POP-LOCAL (P-POP-LOCAL-OKP INS P)) (POP-GLOBAL (P-POP-GLOBAL-OKP INS P)) (FETCH-TEMP-STK (P-FETCH-TEMP-STK-OKP INS P)) (DEPOSIT-TEMP-STK (P-DEPOSIT-TEMP-STK-OKP INS P)) (JUMP (P-JUMP-OKP INS P)) (JUMP-CASE (P-JUMP-CASE-OKP INS P)) (SET-LOCAL (P-SET-LOCAL-OKP INS P)) (TEST-NAT-AND-JUMP (P-TEST-NAT-AND-JUMP-OKP INS P)) (TEST-INT-AND-JUMP (P-TEST-INT-AND-JUMP-OKP INS P)) (TEST-BOOL-AND-JUMP (P-TEST-BOOL-AND-JUMP-OKP INS P)) (NO-OP (P-NO-OP-OKP INS P)) (EQ (P-EQ-OKP INS P)) (ADD-INT-WITH-CARRY (P-ADD-INT-WITH-CARRY-OKP INS P)) (SUB-INT (P-SUB-INT-OKP INS P)) (SUB-INT-WITH-CARRY (P-SUB-INT-WITH-CARRY-OKP INS P)) (NEG-INT (P-NEG-INT-OKP INS P)) (LT-INT (P-LT-INT-OKP INS P)) (INT-TO-NAT (P-INT-TO-NAT-OKP INS P)) (ADD-NAT (P-ADD-NAT-OKP INS P)) (SUB-NAT (P-SUB-NAT-OKP INS P)) (SUB1-NAT (P-SUB1-NAT-OKP INS P)) (OR-BOOL (P-OR-BOOL-OKP INS P)) (AND-BOOL (P-AND-BOOL-OKP INS P)) (NOT-BOOL (P-NOT-BOOL-OKP INS P)) (OTHERWISE F))) Note that (OR (FALSEP (P-INS-OKP INS P)) (TRUEP (P-INS-OKP INS P))) is a theorem. [ 0.0 0.0 0.0 ] P-INS-OKP (DEFN P-INS-STEP (INS P) (CASE (CAR INS) (CALL (P-CALL-STEP INS P)) (RET (P-RET-STEP INS P)) (PUSH-CONSTANT (P-PUSH-CONSTANT-STEP INS P)) (PUSH-LOCAL (P-PUSH-LOCAL-STEP INS P)) (PUSH-GLOBAL (P-PUSH-GLOBAL-STEP INS P)) (PUSH-TEMP-STK-INDEX (P-PUSH-TEMP-STK-INDEX-STEP INS P)) (POP (P-POP-STEP INS P)) (POP* (P-POP*-STEP INS P)) (POP-LOCAL (P-POP-LOCAL-STEP INS P)) (POP-GLOBAL (P-POP-GLOBAL-STEP INS P)) (FETCH-TEMP-STK (P-FETCH-TEMP-STK-STEP INS P)) (DEPOSIT-TEMP-STK (P-DEPOSIT-TEMP-STK-STEP INS P)) (JUMP (P-JUMP-STEP INS P)) (JUMP-CASE (P-JUMP-CASE-STEP INS P)) (SET-LOCAL (P-SET-LOCAL-STEP INS P)) (TEST-NAT-AND-JUMP (P-TEST-NAT-AND-JUMP-STEP INS P)) (TEST-INT-AND-JUMP (P-TEST-INT-AND-JUMP-STEP INS P)) (TEST-BOOL-AND-JUMP (P-TEST-BOOL-AND-JUMP-STEP INS P)) (NO-OP (P-NO-OP-STEP INS P)) (EQ (P-EQ-STEP INS P)) (ADD-INT-WITH-CARRY (P-ADD-INT-WITH-CARRY-STEP INS P)) (SUB-INT (P-SUB-INT-STEP INS P)) (SUB-INT-WITH-CARRY (P-SUB-INT-WITH-CARRY-STEP INS P)) (NEG-INT (P-NEG-INT-STEP INS P)) (LT-INT (P-LT-INT-STEP INS P)) (INT-TO-NAT (P-INT-TO-NAT-STEP INS P)) (ADD-NAT (P-ADD-NAT-STEP INS P)) (SUB-NAT (P-SUB-NAT-STEP INS P)) (SUB1-NAT (P-SUB1-NAT-STEP INS P)) (OR-BOOL (P-OR-BOOL-STEP INS P)) (AND-BOOL (P-AND-BOOL-STEP INS P)) (NOT-BOOL (P-NOT-BOOL-STEP INS P)) (OTHERWISE (P-HALT P 'RUN)))) Note that (P-STATEP (P-INS-STEP INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-INS-STEP (DEFN P-STEP1 (INS P) (IF (P-INS-OKP INS P) (P-INS-STEP INS P) (P-HALT P (X-Y-ERROR-MSG 'P (CAR INS))))) Observe that (P-STATEP (P-STEP1 INS P)) is a theorem. [ 0.0 0.0 0.0 ] P-STEP1 (DEFN P-STEP (P) (IF (EQUAL (P-PSW P) 'RUN) (P-STEP1 (P-CURRENT-INSTRUCTION P) P) P)) Observe that (OR (P-STATEP (P-STEP P)) (EQUAL (P-STEP P) P)) is a theorem. [ 0.0 0.0 0.0 ] P-STEP (DISABLE P-STEP) [ 0.0 0.0 0.0 ] P-STEP-OFF (DEFN P (P N) (IF (ZEROP N) P (P (P-STEP P) (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, P is accepted under the principle of definition. From the definition we can conclude that: (OR (P-STATEP (P P N)) (EQUAL (P P N) P)) is a theorem. [ 0.0 0.0 0.0 ] P (DISABLE P-STEP) [ 0.0 0.0 0.0 ] P-STEP-OFF1 (DISABLE P-HALT) [ 0.0 0.0 0.0 ] P-HALT-OFF (DISABLE P-INS-STEP) [ 0.0 0.0 0.0 ] P-INS-STEP-OFF (DISABLE P-INS-OKP) [ 0.0 0.0 0.0 ] P-INS-OKP-OFF (DISABLE P-STEP1) [ 0.0 0.0 0.0 ] P-STEP1-OFF (DISABLE X-Y-ERROR-MSG) [ 0.0 0.0 0.0 ] X-Y-ERROR-MSG-OFF (PROVE-LEMMA P-STEP-EXPANSION (REWRITE) (EQUAL (P-STEP (P-STATE PC CTR-STK TEMP-STK PROG-SEG DATA-SEG P-MAX-CTRL-STK-SIZE P-MAX-TEMP-STK-SIZE P-WORD-SIZE PSW)) (IF (EQUAL PSW 'RUN) (P-STEP1 (P-CURRENT-INSTRUCTION (P-STATE PC CTR-STK TEMP-STK PROG-SEG DATA-SEG P-MAX-CTRL-STK-SIZE P-MAX-TEMP-STK-SIZE P-WORD-SIZE PSW)) (P-STATE PC CTR-STK TEMP-STK PROG-SEG DATA-SEG P-MAX-CTRL-STK-SIZE P-MAX-TEMP-STK-SIZE P-WORD-SIZE PSW)) (P-STATE PC CTR-STK TEMP-STK PROG-SEG DATA-SEG P-MAX-CTRL-STK-SIZE P-MAX-TEMP-STK-SIZE P-WORD-SIZE PSW))) ((ENABLE P-STEP))) This formula simplifies, applying P-PC-P-STATE, P-PROG-SEGMENT-P-STATE, and P-PSW-P-STATE, and expanding the definitions of P-CURRENT-INSTRUCTION, OFFSET, DEFINITION, AREA-NAME, P-CURRENT-PROGRAM, PROGRAM-BODY, and P-STEP, to: (IMPLIES (EQUAL PSW 'RUN) (EQUAL (P-STEP1 (UNLABEL (GET (ADP-OFFSET (UNTAG PC)) (CDDDR (ASSOC (ADP-NAME (UNTAG PC)) PROG-SEG)))) (P-STATE PC CTR-STK TEMP-STK PROG-SEG DATA-SEG P-MAX-CTRL-STK-SIZE P-MAX-TEMP-STK-SIZE P-WORD-SIZE PSW)) (P-STEP1 (UNLABEL (GET (ADP-OFFSET (UNTAG PC)) (CDDDR (ASSOC (ADP-NAME (UNTAG PC)) PROG-SEG)))) (P-STATE PC CTR-STK TEMP-STK PROG-SEG DATA-SEG P-MAX-CTRL-STK-SIZE P-MAX-TEMP-STK-SIZE P-WORD-SIZE 'RUN)))). This again simplifies, trivially, to: T. Q.E.D. [ 0.0 0.1 0.0 ] P-STEP-EXPANSION (PROVE-LEMMA P-INS-STEP-EXPANSION (REWRITE) (EQUAL (P-INS-STEP (CONS (PACK OPR) ARGS) P) (CASE (PACK OPR) (CALL (P-CALL-STEP (CONS (PACK OPR) ARGS) P)) (RET (P-RET-STEP (CONS (PACK OPR) ARGS) P)) (PUSH-CONSTANT (P-PUSH-CONSTANT-STEP (CONS (PACK OPR) ARGS) P)) (PUSH-LOCAL (P-PUSH-LOCAL-STEP (CONS (PACK OPR) ARGS) P)) (PUSH-GLOBAL (P-PUSH-GLOBAL-STEP (CONS (PACK OPR) ARGS) P)) (PUSH-TEMP-STK-INDEX (P-PUSH-TEMP-STK-INDEX-STEP (CONS (PACK OPR) ARGS) P)) (POP (P-POP-STEP (CONS (PACK OPR) ARGS) P)) (POP* (P-POP*-STEP (CONS (PACK OPR) ARGS) P)) (POP-LOCAL (P-POP-LOCAL-STEP (CONS (PACK OPR) ARGS) P)) (POP-GLOBAL (P-POP-GLOBAL-STEP (CONS (PACK OPR) ARGS) P)) (FETCH-TEMP-STK (P-FETCH-TEMP-STK-STEP (CONS (PACK OPR) ARGS) P)) (DEPOSIT-TEMP-STK (P-DEPOSIT-TEMP-STK-STEP (CONS (PACK OPR) ARGS) P)) (JUMP (P-JUMP-STEP (CONS (PACK OPR) ARGS) P)) (JUMP-CASE (P-JUMP-CASE-STEP (CONS (PACK OPR) ARGS) P)) (SET-LOCAL (P-SET-LOCAL-STEP (CONS (PACK OPR) ARGS) P)) (TEST-NAT-AND-JUMP (P-TEST-NAT-AND-JUMP-STEP (CONS (PACK OPR) ARGS) P)) (TEST-INT-AND-JUMP (P-TEST-INT-AND-JUMP-STEP (CONS (PACK OPR) ARGS) P)) (TEST-BOOL-AND-JUMP (P-TEST-BOOL-AND-JUMP-STEP (CONS (PACK OPR) ARGS) P)) (NO-OP (P-NO-OP-STEP (CONS (PACK OPR) ARGS) P)) (EQ (P-EQ-STEP (CONS (PACK OPR) ARGS) P)) (ADD-INT-WITH-CARRY (P-ADD-INT-WITH-CARRY-STEP (CONS (PACK OPR) ARGS) P)) (SUB-INT (P-SUB-INT-STEP (CONS (PACK OPR) ARGS) P)) (SUB-INT-WITH-CARRY (P-SUB-INT-WITH-CARRY-STEP (CONS (PACK OPR) ARGS) P)) (NEG-INT (P-NEG-INT-STEP (CONS (PACK OPR) ARGS) P)) (LT-INT (P-LT-INT-STEP (CONS (PACK OPR) ARGS) P)) (INT-TO-NAT (P-INT-TO-NAT-STEP (CONS (PACK OPR) ARGS) P)) (ADD-NAT (P-ADD-NAT-STEP (CONS (PACK OPR) ARGS) P)) (SUB-NAT (P-SUB-NAT-STEP (CONS (PACK OPR) ARGS) P)) (SUB1-NAT (P-SUB1-NAT-STEP (CONS (PACK OPR) ARGS) P)) (OR-BOOL (P-OR-BOOL-STEP (CONS (PACK OPR) ARGS) P)) (AND-BOOL (P-AND-BOOL-STEP (CONS (PACK OPR) ARGS) P)) (NOT-BOOL (P-NOT-BOOL-STEP (CONS (PACK OPR) ARGS) P)) (OTHERWISE (P-HALT P 'RUN)))) ((ENABLE P-INS-STEP))) This conjecture can be simplified, using the abbreviation PACK-EQUAL, to: (EQUAL (P-INS-STEP (CONS (PACK OPR) ARGS) P) (CASE OPR ((67 65 76 76 . 0) (P-CALL-STEP (CONS (PACK OPR) ARGS) P)) ((82 69 84 . 0) (P-RET-STEP (CONS (PACK OPR) ARGS) P)) ((80 85 83 72 45 67 79 78 83 84 65 78 84 . 0) (P-PUSH-CONSTANT-STEP (CONS (PACK OPR) ARGS) P)) ((80 85 83 72 45 76 79 67 65 76 . 0) (P-PUSH-LOCAL-STEP (CONS (PACK OPR) ARGS) P)) ((80 85 83 72 45 71 76 79 66 65 76 . 0) (P-PUSH-GLOBAL-STEP (CONS (PACK OPR) ARGS) P)) ((80 85 83 72 45 84 69 77 80 45 83 84 75 45 73 78 68 69 88 . 0) (P-PUSH-TEMP-STK-INDEX-STEP (CONS (PACK OPR) ARGS) P)) ((80 79 80 . 0) (P-POP-STEP (CONS (PACK OPR) ARGS) P)) ((80 79 80 42 . 0) (P-POP*-STEP (CONS (PACK OPR) ARGS) P)) ((80 79 80 45 76 79 67 65 76 . 0) (P-POP-LOCAL-STEP (CONS (PACK OPR) ARGS) P)) ((80 79 80 45 71 76 79 66 65 76 . 0) (P-POP-GLOBAL-STEP (CONS (PACK OPR) ARGS) P)) ((70 69 84 67 72 45 84 69 77 80 45 83 84 75 . 0) (P-FETCH-TEMP-STK-STEP (CONS (PACK OPR) ARGS) P)) ((68 69 80 79 83 73 84 45 84 69 77 80 45 83 84 75 . 0) (P-DEPOSIT-TEMP-STK-STEP (CONS (PACK OPR) ARGS) P)) ((74 85 77 80 . 0) (P-JUMP-STEP (CONS (PACK OPR) ARGS) P)) ((74 85 77 80 45 67 65 83 69 . 0) (P-JUMP-CASE-STEP (CONS (PACK OPR) ARGS) P)) ((83 69 84 45 76 79 67 65 76 . 0) (P-SET-LOCAL-STEP (CONS (PACK OPR) ARGS) P)) ((84 69 83 84 45 78 65 84 45 65 78 68 45 74 85 77 80 . 0) (P-TEST-NAT-AND-JUMP-STEP (CONS (PACK OPR) ARGS) P)) ((84 69 83 84 45 73 78 84 45 65 78 68 45 74 85 77 80 . 0) (P-TEST-INT-AND-JUMP-STEP (CONS (PACK OPR) ARGS) P)) ((84 69 83 84 45 66 79 79 76 45 65 78 68 45 74 85 77 80 . 0) (P-TEST-BOOL-AND-JUMP-STEP (CONS (PACK OPR) ARGS) P)) ((78 79 45 79 80 . 0) (P-NO-OP-STEP (CONS (PACK OPR) ARGS) P)) ((69 81 . 0) (P-EQ-STEP (CONS (PACK OPR) ARGS) P)) ((65 68 68 45 73 78 84 45 87 73 84 72 45 67 65 82 82 89 . 0) (P-ADD-INT-WITH-CARRY-STEP (CONS (PACK OPR) ARGS) P)) ((83 85 66 45 73 78 84 . 0) (P-SUB-INT-STEP (CONS (PACK OPR) ARGS) P)) ((83 85 66 45 73 78 84 45 87 73 84 72 45 67 65 82 82 89 . 0) (P-SUB-INT-WITH-CARRY-STEP (CONS (PACK OPR) ARGS) P)) ((78 69 71 45 73 78 84 . 0) (P-NEG-INT-STEP (CONS (PACK OPR) ARGS) P)) ((76 84 45 73 78 84 . 0) (P-LT-INT-STEP (CONS (PACK OPR) ARGS) P)) ((73 78 84 45 84 79 45 78 65 84 . 0) (P-INT-TO-NAT-STEP (CONS (PACK OPR) ARGS) P)) ((65 68 68 45 78 65 84 . 0) (P-ADD-NAT-STEP (CONS (PACK OPR) ARGS) P)) ((83 85 66 45 78 65 84 . 0) (P-SUB-NAT-STEP (CONS (PACK OPR) ARGS) P)) ((83 85 66 49 45 78 65 84 . 0) (P-SUB1-NAT-STEP (CONS (PACK OPR) ARGS) P)) ((79 82 45 66 79 79 76 . 0) (P-OR-BOOL-STEP (CONS (PACK OPR) ARGS) P)) ((65 78 68 45 66 79 79 76 . 0) (P-AND-BOOL-STEP (CONS (PACK OPR) ARGS) P)) ((78 79 84 45 66 79 79 76 . 0) (P-NOT-BOOL-STEP (CONS (PACK OPR) ARGS) P)) (OTHERWISE (P-HALT P 'RUN)))). This simplifies, rewriting with the lemmas ADP-OFFSET-CONS, ADP-NAME-CONS, GET-CAR, UNTAG-TAG, CDR-CONS, PACK-EQUAL, UNPACK-PACK, and CAR-CONS, and expanding the definitions of P-NOT-BOOL-STEP, NOT-BOOL, P-AND-BOOL-STEP, AND-BOOL, P-OR-BOOL-STEP, OR-BOOL, P-SUB1-NAT-STEP, P-SUB-NAT-STEP, P-ADD-NAT-STEP, P-INT-TO-NAT-STEP, P-LT-INT-STEP, ILESSP, P-NEG-INT-STEP, P-SUB-INT-WITH-CARRY-STEP, P-SUB-INT-STEP, INEGATE, IDIFFERENCE, P-ADD-INT-WITH-CARRY-STEP, BOOL-TO-NAT, IPLUS, FIX-SMALL-INTEGER, P-EQ-STEP, TAG, BOOL, P-NO-OP-STEP, P-TEST-BOOL-AND-JUMP-STEP, P-TEST-BOOLP, P-TEST-INT-AND-JUMP-STEP, P-TEST-INTP, P-TEST-NAT-AND-JUMP-STEP, P-TEST-NATP, P-TEST-AND-JUMP-STEP, P-SET-LOCAL-STEP, P-JUMP-CASE-STEP, P-JUMP-STEP, P-DEPOSIT-TEMP-STK-STEP, P-FETCH-TEMP-STK-STEP, P-POP-GLOBAL-STEP, DEPOSIT-ADP, EQUAL, PUT, DEPOSIT, P-POP-LOCAL-STEP, PUT-VALUE, SET-LOCAL-VAR-VALUE, P-POP*-STEP, P-POP-STEP, P-PUSH-TEMP-STK-INDEX-STEP, P-PUSH-GLOBAL-STEP, FETCH-ADP, ZEROP, FETCH, P-PUSH-LOCAL-STEP, LOCAL-VAR-VALUE, P-PUSH-CONSTANT-STEP, ADD1-P-PC, PC, PROGRAM-BODY, P-CURRENT-PROGRAM, AREA-NAME, UNABBREVIATE-CONSTANT, P-RET-STEP, P-CALL-STEP, DEFINITION, FORMAL-VARS, TEMP-VAR-DCLS, ADD-ADDR, ADD-ADP, ADD1-ADDR, PAIR-FORMAL-VARS-WITH-ACTUALS, MAKE-P-CALL-FRAME, UNPACK, P-INS-STEP, and PACK, to: T. Q.E.D. [ 0.0 0.7 0.0 ] P-INS-STEP-EXPANSION (PROVE-LEMMA P-INS-OKP-EXPANSION (REWRITE) (EQUAL (P-INS-OKP (CONS (PACK OPR) ARGS) P) (CASE (PACK OPR) (CALL (P-CALL-OKP (CONS (PACK OPR) ARGS) P)) (RET (P-RET-OKP (CONS (PACK OPR) ARGS) P)) (PUSH-CONSTANT (P-PUSH-CONSTANT-OKP (CONS (PACK OPR) ARGS) P)) (PUSH-LOCAL (P-PUSH-LOCAL-OKP (CONS (PACK OPR) ARGS) P)) (PUSH-GLOBAL (P-PUSH-GLOBAL-OKP (CONS (PACK OPR) ARGS) P)) (PUSH-TEMP-STK-INDEX (P-PUSH-TEMP-STK-INDEX-OKP (CONS (PACK OPR) ARGS) P)) (POP (P-POP-OKP (CONS (PACK OPR) ARGS) P)) (POP* (P-POP*-OKP (CONS (PACK OPR) ARGS) P)) (POP-LOCAL (P-POP-LOCAL-OKP (CONS (PACK OPR) ARGS) P)) (POP-GLOBAL (P-POP-GLOBAL-OKP (CONS (PACK OPR) ARGS) P)) (FETCH-TEMP-STK (P-FETCH-TEMP-STK-OKP (CONS (PACK OPR) ARGS) P)) (DEPOSIT-TEMP-STK (P-DEPOSIT-TEMP-STK-OKP (CONS (PACK OPR) ARGS) P)) (JUMP (P-JUMP-OKP (CONS (PACK OPR) ARGS) P)) (JUMP-CASE (P-JUMP-CASE-OKP (CONS (PACK OPR) ARGS) P)) (SET-LOCAL (P-SET-LOCAL-OKP (CONS (PACK OPR) ARGS) P)) (TEST-NAT-AND-JUMP (P-TEST-NAT-AND-JUMP-OKP (CONS (PACK OPR) ARGS) P)) (TEST-INT-AND-JUMP (P-TEST-INT-AND-JUMP-OKP (CONS (PACK OPR) ARGS) P)) (TEST-BOOL-AND-JUMP (P-TEST-BOOL-AND-JUMP-OKP (CONS (PACK OPR) ARGS) P)) (NO-OP (P-NO-OP-OKP (CONS (PACK OPR) ARGS) P)) (EQ (P-EQ-OKP (CONS (PACK OPR) ARGS) P)) (ADD-INT-WITH-CARRY (P-ADD-INT-WITH-CARRY-OKP (CONS (PACK OPR) ARGS) P)) (SUB-INT (P-SUB-INT-OKP (CONS (PACK OPR) ARGS) P)) (SUB-INT-WITH-CARRY (P-SUB-INT-WITH-CARRY-OKP (CONS (PACK OPR) ARGS) P)) (NEG-INT (P-NEG-INT-OKP (CONS (PACK OPR) ARGS) P)) (LT-INT (P-LT-INT-OKP (CONS (PACK OPR) ARGS) P)) (INT-TO-NAT (P-INT-TO-NAT-OKP (CONS (PACK OPR) ARGS) P)) (ADD-NAT (P-ADD-NAT-OKP (CONS (PACK OPR) ARGS) P)) (SUB-NAT (P-SUB-NAT-OKP (CONS (PACK OPR) ARGS) P)) (SUB1-NAT (P-SUB1-NAT-OKP (CONS (PACK OPR) ARGS) P)) (OR-BOOL (P-OR-BOOL-OKP (CONS (PACK OPR) ARGS) P)) (AND-BOOL (P-AND-BOOL-OKP (CONS (PACK OPR) ARGS) P)) (NOT-BOOL (P-NOT-BOOL-OKP (CONS (PACK OPR) ARGS) P)) (OTHERWISE F))) ((ENABLE P-INS-OKP))) This formula can be simplified, using the abbreviations P-NO-OP-OKP, P-SET-LOCAL-OKP, P-JUMP-OKP, P-POP-GLOBAL-OKP, P-POP-LOCAL-OKP, P-POP-OKP, P-PUSH-GLOBAL-OKP, P-PUSH-LOCAL-OKP, P-PUSH-CONSTANT-OKP, P-RET-OKP, and PACK-EQUAL, to the new goal: (EQUAL (P-INS-OKP (CONS (PACK OPR) ARGS) P) (CASE OPR ((67 65 76 76 . 0) (P-CALL-OKP (CONS (PACK OPR) ARGS) P)) ((82 69 84 . 0) T) ((80 85 83 72 45 67 79 78 83 84 65 78 84 . 0) (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P))) ((80 85 83 72 45 76 79 67 65 76 . 0) (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P))) ((80 85 83 72 45 71 76 79 66 65 76 . 0) (LESSP (LENGTH (P-TEMP-STK P)) (P-MAX-TEMP-STK-SIZE P))) ((80 85 83 72 45 84 69 77 80 45 83 84 75 45 73 78 68 69 88 . 0) (P-PUSH-TEMP-STK-INDEX-OKP (CONS (PACK OPR) ARGS) P)) ((80 79 80 . 0) (LISTP (P-TEMP-STK P))) ((80 79 80 42 . 0) (P-POP*-OKP (CONS (PACK OPR) ARGS) P)) ((80 79 80 45 76 79 67 65 76 . 0) (LISTP (P-TEMP-STK P))) ((80 79 80 45 71 76 79 66 65 76 . 0) (LISTP (P-TEMP-STK P))) ((70 69 84 67 72 45 84 69 77 80 45 83 84 75 . 0) (P-FETCH-TEMP-STK-OKP (CONS (PACK OPR) ARGS) P)) ((68 69 80 79 83 73 84 45 84 69 77 80 45 83 84 75 . 0) (P-DEPOSIT-TEMP-STK-OKP (CONS (PACK OPR) ARGS) P)) ((74 85 77 80 . 0) T) ((74 85 77 80 45 67 65 83 69 . 0) (P-JUMP-CASE-OKP (CONS (PACK OPR) ARGS) P)) ((83 69 84 45 76 79 67 65 76 . 0) (LISTP (P-TEMP-STK P))) ((84 69 83 84 45 78 65 84 45 65 78 68 45 74 85 77 80 . 0) (P-TEST-NAT-AND-JUMP-OKP (CONS (PACK OPR) ARGS) P)) ((84 69 83 84 45 73 78 84 45 65 78 68 45 74 85 77 80 . 0) (P-TEST-INT-AND-JUMP-OKP (CONS (PACK OPR) ARGS) P)) ((84 69 83 84 45 66 79 79 76 45 65 78 68 45 74 85 77 80 . 0) (P-TEST-BOOL-AND-JUMP-OKP (CONS (PACK OPR) ARGS) P)) ((78 79 45 79 80 . 0) T) ((69 81 . 0) (P-EQ-OKP (CONS (PACK OPR) ARGS) P)) ((65 68 68 45 73 78 84 45 87 73 84 72 45 67 65 82 82 89 . 0) (P-ADD-INT-WITH-CARRY-OKP (CONS (PACK OPR) ARGS) P)) ((83 85 66 45 73 78 84 . 0) (P-SUB-INT-OKP (CONS (PACK OPR) ARGS) P)) ((83 85 66 45 73 78 84 45 87 73 84 72 45 67 65 82 82 89 . 0) (P-SUB-INT-WITH-CARRY-OKP (CONS (PACK OPR) ARGS) P)) ((78 69 71 45 73 78 84 . 0) (P-NEG-INT-OKP (CONS (PACK OPR) ARGS) P)) ((76 84 45 73 78 84 . 0) (P-LT-INT-OKP (CONS (PACK OPR) ARGS) P)) ((73 78 84 45 84 79 45 78 65 84 . 0) (P-INT-TO-NAT-OKP (CONS (PACK OPR) ARGS) P)) ((65 68 68 45 78 65 84 . 0) (P-ADD-NAT-OKP (CONS (PACK OPR) ARGS) P)) ((83 85 66 45 78 65 84 . 0) (P-SUB-NAT-OKP (CONS (PACK OPR) ARGS) P)) ((83 85 66 49 45 78 65 84 . 0) (P-SUB1-NAT-OKP (CONS (PACK OPR) ARGS) P)) ((79 82 45 66 79 79 76 . 0) (P-OR-BOOL-OKP (CONS (PACK OPR) ARGS) P)) ((65 78 68 45 66 79 79 76 . 0) (P-AND-BOOL-OKP (CONS (PACK OPR) ARGS) P)) ((78 79 84 45 66 79 79 76 . 0) (P-NOT-BOOL-OKP (CONS (PACK OPR) ARGS) P)) (OTHERWISE F))), which simplifies, applying CDR-CONS, CAR-CDR-PUSH, TOP-PUSH, PACK-EQUAL, UNPACK-PACK, and CAR-CONS, and opening up P-NOT-BOOL-OKP, P-AND-BOOL-OKP, P-OR-BOOL-OKP, P-SUB1-NAT-OKP, P-SUB-NAT-OKP, P-ADD-NAT-OKP, P-INT-TO-NAT-OKP, P-LT-INT-OKP, P-NEG-INT-OKP, P-SUB-INT-WITH-CARRY-OKP, P-SUB-INT-OKP, INEGATE, IDIFFERENCE, P-ADD-INT-WITH-CARRY-OKP, P-EQ-OKP, P-NO-OP-OKP, P-TEST-BOOL-AND-JUMP-OKP, P-TEST-BOOLP, BOOLEANP, P-TEST-INT-AND-JUMP-OKP, P-TEST-INTP, P-TEST-NAT-AND-JUMP-OKP, P-TEST-NATP, P-TEST-AND-JUMP-OKP, P-SET-LOCAL-OKP, P-JUMP-CASE-OKP, P-JUMP-OKP, P-DEPOSIT-TEMP-STK-OKP, P-FETCH-TEMP-STK-OKP, P-OBJECTP, EQUAL, P-OBJECTP-TYPE, P-POP-GLOBAL-OKP, P-POP-LOCAL-OKP, P-POP*-OKP, P-POP-OKP, P-PUSH-TEMP-STK-INDEX-OKP, P-PUSH-GLOBAL-OKP, P-PUSH-LOCAL-OKP, P-PUSH-CONSTANT-OKP, P-RET-OKP, P-CALL-OKP, DEFINITION, FORMAL-VARS, TEMP-VAR-DCLS, ADD-ADDR, ADD-ADP, ADD1-ADDR, PAIR-FORMAL-VARS-WITH-ACTUALS, MAKE-P-CALL-FRAME, P-CTRL-STK-SIZE, UNPACK, P-INS-OKP, and PACK, to: T. Q.E.D. [ 0.0 0.4 0.1 ] P-INS-OKP-EXPANSION (PROVE-LEMMA P-0-UNWINDING-LEMMA (REWRITE) (EQUAL (P S 0) S)) This conjecture simplifies, unfolding the definitions of EQUAL and P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-0-UNWINDING-LEMMA (PROVE-LEMMA P-PLUS-LEMMA (REWRITE) (EQUAL (P STATE (PLUS J K)) (P (P STATE J) K)) ((ENABLE P))) Call the conjecture *1. Perhaps we can prove it by induction. Three inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP J) (p STATE J K)) (IMPLIES (AND (NOT (ZEROP J)) (p (P-STEP STATE) (SUB1 J) K)) (p STATE J K))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition of ZEROP can be used to prove that the measure (COUNT J) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for STATE. The above induction scheme leads to two new goals: Case 2. (IMPLIES (ZEROP J) (EQUAL (P STATE (PLUS J K)) (P (P STATE J) K))), which simplifies, applying the lemma P-0-UNWINDING-LEMMA, and opening up the definitions of ZEROP, EQUAL, PLUS, and P, to two new formulas: Case 2.2. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K))) (EQUAL (P STATE 0) (P STATE K))), which again simplifies, applying the lemma P-0-UNWINDING-LEMMA, and opening up the function P, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (NUMBERP K))) (EQUAL (P STATE 0) (P STATE K))), which again simplifies, applying the lemma P-0-UNWINDING-LEMMA, and opening up P, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (EQUAL (P (P-STEP STATE) (PLUS (SUB1 J) K)) (P (P (P-STEP STATE) (SUB1 J)) K))) (EQUAL (P STATE (PLUS J K)) (P (P STATE J) K))), which simplifies, applying the lemma SUB1-ADD1, and opening up ZEROP, PLUS, and P, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] P-PLUS-LEMMA (PROVE-LEMMA P-ADD1 (REWRITE) (EQUAL (P STATE (ADD1 X)) (P (P STATE X) 1)) ((USE (P-PLUS-LEMMA (J X) (K 1))) (ENABLE PLUS-ADD1))) This formula can be simplified, using the abbreviation PLUS-ADD1, to: T, which simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-ADD1 (DISABLE P-ADD1) [ 0.0 0.0 0.0 ] P-ADD1-OFF (PROVE-LEMMA P-REARRANGE-TIMES-LEMMA (REWRITE) (EQUAL (P (P STATE K) J) (P (P STATE J) K)) ((INSTRUCTIONS (USE-LEMMA P-PLUS-LEMMA) (USE-LEMMA P-PLUS-LEMMA ((J K) (K J))) (= (P (P STATE K) J) (P STATE (PLUS K J)) 0) (= (P (P STATE J) K) (P STATE (PLUS J K)) 0) (= (PLUS J K) (PLUS K J) T) S (PROVE)))) *** Entering proof-checker *** (USE-LEMMA P-PLUS-LEMMA) Using P-PLUS-LEMMA. (USE-LEMMA P-PLUS-LEMMA ((J K) (K J))) Using P-PLUS-LEMMA with the substitution ((J K) (K J)). (= (P (P STATE K) J) (P STATE (PLUS K J)) 0) (= (P (P STATE J) K) (P STATE (PLUS J K)) 0) (= (PLUS J K) (PLUS K J) T) Creating 1 new subgoal, (MAIN . 1). S The proof of the current goal, MAIN, has been completed. However, the following subgoal of MAIN remains to be proved: (MAIN . 1). Now proving (MAIN . 1). PROVE ***** Now entering the theorem prover *****: This formula can be simplified, using the abbreviations AND, IMPLIES, and P-PLUS-LEMMA, to: (IMPLIES (AND (EQUAL (P (P STATE J) K) (P (P STATE J) K)) (EQUAL (P (P STATE K) J) (P (P STATE K) J))) (EQUAL (PLUS J K) (PLUS K J))), which simplifies, using linear arithmetic, to: T. Q.E.D. The current goal, (MAIN . 1), has been proved, and has no dependents. *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!* [ 0.0 0.0 0.0 ] P-REARRANGE-TIMES-LEMMA (DISABLE P-REARRANGE-TIMES-LEMMA) [ 0.0 0.0 0.0 ] P-REARRANGE-TIMES-LEMMA-OFF (PROVE-LEMMA P-ADD1-3 (REWRITE) (EQUAL (P STATE (ADD1 X)) (P (P-STEP STATE) X))) This conjecture simplifies, applying SUB1-ADD1, and unfolding the function P, to the formula: (IMPLIES (NOT (NUMBERP X)) (EQUAL (P (P-STEP STATE) 0) (P (P-STEP STATE) X))). This again simplifies, applying P-0-UNWINDING-LEMMA, and unfolding the definition of P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-ADD1-3 (PROVE-LEMMA FIND-LABEL-APPEND (REWRITE) (IMPLIES (NOT (FIND-LABELP LABEL CODE1)) (EQUAL (FIND-LABEL LABEL (APPEND CODE1 CODE2)) (PLUS (LENGTH CODE1) (FIND-LABEL LABEL CODE2))))) Give the conjecture the name *1. We will appeal to induction. Four inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (NLISTP CODE1) (p LABEL CODE1 CODE2)) (IMPLIES (AND (NOT (NLISTP CODE1)) (AND (LABELLEDP (CAR CODE1)) (EQUAL LABEL (CADAR CODE1)))) (p LABEL CODE1 CODE2)) (IMPLIES (AND (NOT (NLISTP CODE1)) (NOT (AND (LABELLEDP (CAR CODE1)) (EQUAL LABEL (CADAR CODE1)))) (p LABEL (CDR CODE1) CODE2)) (p LABEL CODE1 CODE2))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of AND, LABELLEDP, and NLISTP can be used to establish that the measure (COUNT CODE1) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to four new goals: Case 4. (IMPLIES (AND (NLISTP CODE1) (NOT (FIND-LABELP LABEL CODE1))) (EQUAL (FIND-LABEL LABEL (APPEND CODE1 CODE2)) (PLUS (LENGTH CODE1) (FIND-LABEL LABEL CODE2)))), which simplifies, unfolding the functions NLISTP, FIND-LABELP, APPEND, LENGTH, EQUAL, and PLUS, to: T. Case 3. (IMPLIES (AND (NOT (NLISTP CODE1)) (AND (LABELLEDP (CAR CODE1)) (EQUAL LABEL (CADAR CODE1))) (NOT (FIND-LABELP LABEL CODE1))) (EQUAL (FIND-LABEL LABEL (APPEND CODE1 CODE2)) (PLUS (LENGTH CODE1) (FIND-LABEL LABEL CODE2)))), which simplifies, opening up NLISTP, LABELLEDP, AND, FIND-LABELP, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP CODE1)) (NOT (AND (LABELLEDP (CAR CODE1)) (EQUAL LABEL (CADAR CODE1)))) (FIND-LABELP LABEL (CDR CODE1)) (NOT (FIND-LABELP LABEL CODE1))) (EQUAL (FIND-LABEL LABEL (APPEND CODE1 CODE2)) (PLUS (LENGTH CODE1) (FIND-LABEL LABEL CODE2)))), which simplifies, expanding NLISTP, LABELLEDP, AND, and FIND-LABELP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP CODE1)) (NOT (AND (LABELLEDP (CAR CODE1)) (EQUAL LABEL (CADAR CODE1)))) (EQUAL (FIND-LABEL LABEL (APPEND (CDR CODE1) CODE2)) (PLUS (LENGTH (CDR CODE1)) (FIND-LABEL LABEL CODE2))) (NOT (FIND-LABELP LABEL CODE1))) (EQUAL (FIND-LABEL LABEL (APPEND CODE1 CODE2)) (PLUS (LENGTH CODE1) (FIND-LABEL LABEL CODE2)))), which simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and unfolding NLISTP, LABELLEDP, AND, FIND-LABELP, APPEND, FIND-LABEL, LENGTH, and PLUS, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] FIND-LABEL-APPEND (DISABLE FIND-LABEL-APPEND) [ 0.0 0.0 0.0 ] FIND-LABEL-APPEND-OFF (PROVE-LEMMA FIND-LABELP-APPEND2 (REWRITE) (EQUAL (FIND-LABELP N (APPEND LST1 LST2)) (OR (FIND-LABELP N LST1) (FIND-LABELP N LST2))) ((ENABLE FIND-LABELP))) This simplifies, opening up the function OR, to two new conjectures: Case 2. (IMPLIES (NOT (FIND-LABELP N LST1)) (EQUAL (FIND-LABELP N (APPEND LST1 LST2)) (FIND-LABELP N LST2))), which we will name *1. Case 1. (IMPLIES (FIND-LABELP N LST1) (EQUAL (FIND-LABELP N (APPEND LST1 LST2)) T)). This again simplifies, trivially, to the new formula: (IMPLIES (FIND-LABELP N LST1) (FIND-LABELP N (APPEND LST1 LST2))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (FIND-LABELP N (APPEND LST1 LST2)) (OR (FIND-LABELP N LST1) (FIND-LABELP N LST2))). We named this *1. We will try to prove it by induction. There are three 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 LST1) (p N (CDR LST1) LST2)) (p N LST1 LST2)) (IMPLIES (NOT (LISTP LST1)) (p N LST1 LST2))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT LST1) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new conjectures: Case 2. (IMPLIES (AND (LISTP LST1) (EQUAL (FIND-LABELP N (APPEND (CDR LST1) LST2)) (OR (FIND-LABELP N (CDR LST1)) (FIND-LABELP N LST2)))) (EQUAL (FIND-LABELP N (APPEND LST1 LST2)) (OR (FIND-LABELP N LST1) (FIND-LABELP N LST2)))), which simplifies, applying CDR-CONS and CAR-CONS, and unfolding OR, APPEND, LABELLEDP, FIND-LABELP, and EQUAL, to: T. Case 1. (IMPLIES (NOT (LISTP LST1)) (EQUAL (FIND-LABELP N (APPEND LST1 LST2)) (OR (FIND-LABELP N LST1) (FIND-LABELP N LST2)))). This simplifies, expanding the functions APPEND, FIND-LABELP, and OR, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] FIND-LABELP-APPEND2 (DISABLE FIND-LABELP-APPEND2) [ 0.0 0.0 0.0 ] FIND-LABELP-APPEND2-OFF (PROVE-LEMMA RGET-INVERTS-RPUT (REWRITE) (EQUAL (RGET N (RPUT VALUE N LST)) VALUE) ((INSTRUCTIONS (S-PROP RGET RPUT) (INDUCT (GET N LST)) PROVE PROMOTE (CLAIM (NLISTP LST) 0) PROVE (DIVE 1 1 1 1) (REWRITE PUT-PRESERVES-LENGTH) TOP (DIVE 1) (REWRITE GET-INVERTS-PUT) TOP S (REWRITE DIFFERENCE-N-LEQ) PROVE))) *** Entering proof-checker *** (S-PROP RGET RPUT) (INDUCT (GET N LST)) Creating 2 new subgoals, (MAIN . 1) and (MAIN . 2). The proof of the current goal, MAIN, has been completed. However, the following subgoals of MAIN remain to be proved: (MAIN . 1) and (MAIN . 2). Now proving (MAIN . 1). PROVE ***** Now entering the theorem prover *****: This simplifies, applying LISTP-IMPLIES-NON-ZERO-LENGTH, and unfolding the functions ZEROP, EQUAL, and DIFFERENCE, to the following four new conjectures: Case 4. (IMPLIES (AND (EQUAL N 0) (NOT (EQUAL (LENGTH LST) 0))) (EQUAL (GET (SUB1 (LENGTH (PUT VALUE (SUB1 (LENGTH LST)) LST))) (PUT VALUE (SUB1 (LENGTH LST)) LST)) VALUE)). This again simplifies, using linear arithmetic and rewriting with PUT-PRESERVES-LENGTH and GET-INVERTS-PUT, to: T. Case 3. (IMPLIES (AND (EQUAL N 0) (EQUAL (LENGTH LST) 0)) (EQUAL (GET (SUB1 (LENGTH (PUT VALUE (SUB1 0) LST))) (PUT VALUE (SUB1 0) LST)) VALUE)). But this again simplifies, opening up SUB1, EQUAL, and PUT, to two new conjectures: Case 3.2. (IMPLIES (AND (EQUAL (LENGTH LST) 0) (NOT (LISTP LST))) (EQUAL (GET (SUB1 (LENGTH (LIST VALUE))) (LIST VALUE)) VALUE)), which again simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS, and GET-CAR, and expanding the definitions of LENGTH, EQUAL, ADD1, SUB1, and ZEROP, to: T. Case 3.1. (IMPLIES (AND (EQUAL (LENGTH LST) 0) (LISTP LST)) (EQUAL (GET (SUB1 (LENGTH (CONS VALUE (CDR LST)))) (CONS VALUE (CDR LST))) VALUE)), which again simplifies, applying LISTP-IMPLIES-NON-ZERO-LENGTH, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP N)) (NOT (EQUAL (LENGTH LST) 0))) (EQUAL (GET (SUB1 (LENGTH (PUT VALUE (SUB1 (LENGTH LST)) LST))) (PUT VALUE (SUB1 (LENGTH LST)) LST)) VALUE)). This again simplifies, using linear arithmetic and appealing to the lemmas PUT-PRESERVES-LENGTH and GET-INVERTS-PUT, to: T. Case 1. (IMPLIES (AND (NOT (NUMBERP N)) (EQUAL (LENGTH LST) 0)) (EQUAL (GET (SUB1 (LENGTH (PUT VALUE (SUB1 0) LST))) (PUT VALUE (SUB1 0) LST)) VALUE)), which again simplifies, expanding the functions SUB1, EQUAL, and PUT, to two new formulas: Case 1.2. (IMPLIES (AND (NOT (NUMBERP N)) (EQUAL (LENGTH LST) 0) (NOT (LISTP LST))) (EQUAL (GET (SUB1 (LENGTH (LIST VALUE))) (LIST VALUE)) VALUE)), which again simplifies, appealing to the lemmas CDR-CONS, CAR-CONS, and GET-CAR, and unfolding the definitions of LENGTH, EQUAL, ADD1, SUB1, and ZEROP, to: T. Case 1.1. (IMPLIES (AND (NOT (NUMBERP N)) (EQUAL (LENGTH LST) 0) (LISTP LST)) (EQUAL (GET (SUB1 (LENGTH (CONS VALUE (CDR LST)))) (CONS VALUE (CDR LST))) VALUE)), which again simplifies, applying LISTP-IMPLIES-NON-ZERO-LENGTH, to: T. Q.E.D. The current goal, (MAIN . 1), has been proved, and has no dependents. Now proving (MAIN . 2). PROMOTE (CLAIM (NLISTP LST) 0) Creating one new subgoal, ((MAIN . 2) . 1). PROVE ***** Now entering the theorem prover *****: This formula can be simplified, using the abbreviations NLISTP, ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (GET (SUB1 (DIFFERENCE (LENGTH (PUT VALUE (SUB1 (DIFFERENCE (LENGTH (CDR LST)) (SUB1 N))) (CDR LST))) (SUB1 N))) (PUT VALUE (SUB1 (DIFFERENCE (LENGTH (CDR LST)) (SUB1 N))) (CDR LST))) VALUE) (NOT (LISTP LST))) (EQUAL (GET (SUB1 (DIFFERENCE (LENGTH (PUT VALUE (SUB1 (DIFFERENCE (LENGTH LST) N)) LST)) N)) (PUT VALUE (SUB1 (DIFFERENCE (LENGTH LST) N)) LST)) VALUE)), which simplifies, rewriting with CDR-NLISTP, PUT-CAR-NLISTP, CDR-CONS, ADD1-SUB1-DIFFERENCE, CAR-CONS, and GET-CAR, and opening up the definitions of LENGTH, EQUAL, DIFFERENCE, SUB1, ZEROP, ADD1, and NUMBERP, to: T. Q.E.D. The proof of the current goal, (MAIN . 2), has been completed. However, the following subgoal of (MAIN . 2) remains to be proved: ((MAIN . 2) . 1). Now proving ((MAIN . 2) . 1). (DIVE 1 1 1 1) (REWRITE PUT-PRESERVES-LENGTH) Rewriting with PUT-PRESERVES-LENGTH. Creating 1 new subgoal, (((MAIN . 2) . 1) . 1). TOP (DIVE 1) (REWRITE GET-INVERTS-PUT) Rewriting with GET-INVERTS-PUT. TOP S The proof of the current goal, ((MAIN . 2) . 1), has been completed. However, the following subgoal of ((MAIN . 2) . 1) remains to be proved: (((MAIN . 2) . 1) . 1). Now proving (((MAIN . 2) . 1) . 1). (REWRITE DIFFERENCE-N-LEQ) Rewriting with DIFFERENCE-N-LEQ. Creating 1 new subgoal, ((((MAIN . 2) . 1) . 1) . 1). The proof of the current goal, (((MAIN . 2) . 1) . 1), has been completed. However, the following subgoal of (((MAIN . 2) . 1) . 1) remains to be proved: ((((MAIN . 2) . 1) . 1) . 1). Now proving ((((MAIN . 2) . 1) . 1) . 1). PROVE ***** Now entering the theorem prover *****: This formula can be simplified, using the abbreviations NLISTP, ZEROP, NOT, AND, and IMPLIES, to the new goal: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (GET (SUB1 (DIFFERENCE (LENGTH (PUT VALUE (SUB1 (DIFFERENCE (LENGTH (CDR LST)) (SUB1 N))) (CDR LST))) (SUB1 N))) (PUT VALUE (SUB1 (DIFFERENCE (LENGTH (CDR LST)) (SUB1 N))) (CDR LST))) VALUE) (LISTP LST)) (NOT (EQUAL (LENGTH LST) 0))), which simplifies, using linear arithmetic, applying PUT-PRESERVES-LENGTH and GET-INVERTS-PUT, and expanding the function LENGTH, to: T. Q.E.D. The current goal, ((((MAIN . 2) . 1) . 1) . 1), has been proved, and has no dependents. *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!* [ 0.0 0.1 0.0 ] RGET-INVERTS-RPUT (PROVE-LEMMA RPUT-SAME-VALUE-DOESNT-DISTURB-TEMP-STK (REWRITE) (IMPLIES (EQUAL N (LENGTH TEMP-STK)) (EQUAL (RPUT VALUE N (APPEND LST (CONS VALUE TEMP-STK))) (APPEND LST (CONS VALUE TEMP-STK)))) ((ENABLE RPUT PUT-LENGTH))) This conjecture simplifies, using linear arithmetic, applying PUT-LENGTH, LENGTH-DISTRIBUTES, and CDR-CONS, and opening up the definitions of LENGTH and RPUT, to two new formulas: Case 2. (IMPLIES (LESSP (PLUS (LENGTH LST) (ADD1 (LENGTH TEMP-STK))) (LENGTH TEMP-STK)) (EQUAL (RPUT VALUE (LENGTH TEMP-STK) (APPEND LST (CONS VALUE TEMP-STK))) (APPEND LST (CONS VALUE TEMP-STK)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (NOT (LESSP (LENGTH TEMP-STK) (PLUS (LENGTH LST) (ADD1 (LENGTH TEMP-STK))))) (EQUAL (RPUT VALUE (LENGTH TEMP-STK) (APPEND LST (CONS VALUE TEMP-STK))) (APPEND LST (CONS VALUE TEMP-STK)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RPUT-SAME-VALUE-DOESNT-DISTURB-TEMP-STK (DISABLE ILESSP) [ 0.0 0.0 0.0 ] ILESSP-OFF (DISABLE NOT-BOOL) [ 0.0 0.0 0.0 ] NOT-BOOL-OFF (DISABLE AND-BOOL) [ 0.0 0.0 0.0 ] AND-BOOL-OFF (DISABLE OR-BOOL) [ 0.0 0.0 0.0 ] OR-BOOL-OFF (DISABLE INEGATE) [ 0.0 0.0 0.0 ] INEGATE-OFF (DISABLE FIX-SMALL-INTEGER) [ 0.0 0.0 0.0 ] FIX-SMALL-INTEGER-OFF (DISABLE IPLUS) [ 0.0 0.0 0.0 ] IPLUS-OFF (DISABLE IDIFFERENCE) [ 0.0 0.0 0.0 ] IDIFFERENCE-OFF (MAKE-LIB "c2") Making the lib for "c2". Finished making the lib for "c2". (/stage/ftp/pub/boyer/pc-nqthm/pc-nqthm-1992/examples/mg/c2.lib /stage/ftp/pub/boyer/pc-nqthm/pc-nqthm-1992/examples/mg/c2.lisp)