ACL2 Version 2.5. Level 1. Cbd "/v/hank/v92/moore/demo/flying-demo/". Type :help for help. ACL2 !>(+ 3 4) 7 ACL2 !>(equal (car (cons 1 '(2 3 4))) 1) T ACL2 !>(thm (equal (car (cons x y)) x)) By the simple :rewrite rule CAR-CONS we reduce the conjecture to Goal' (EQUAL X X). But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( THM ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) Proof succeeded. ACL2 !>(endp nil) T ACL2 !>(endp '(1 2 3 4)) NIL ACL2 !>(thm (implies (and (not (endp x)) (endp (cdr x)) (integerp n) (<= 0 n) (rationalp u)) (< (* (len x) u) (+ u n 3)))) By the simple :definition ENDP we reduce the conjecture to Goal' (IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))) (INTEGERP N) (<= 0 N) (RATIONALP U)) (< (* (LEN X) U) (+ U N 3))). This simplifies, using the :definitions FIX and LEN, the :executable- counterpart of BINARY-+ and the :rewrite rules COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+ and UNICITY-OF-1, to Goal'' (IMPLIES (AND (CONSP X) (NOT (CONSP (CDR X))) (INTEGERP N) (<= 0 N) (RATIONALP U)) (< U (+ 3 N U))). But simplification reduces this to T, using linear arithmetic. Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION ENDP) (:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION LEN) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-LINEAR NIL) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-1)) Warnings: None Time: 0.05 seconds (prove: 0.02, print: 0.01, other: 0.02) Proof succeeded. ACL2 !>(defun insert (e x) (cond ((endp x) (cons e x)) ((< e (car x)) (cons e x)) (t (cons (car x) (insert e (cdr x)))))) The admission of INSERT is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of INSERT is described by the theorem (CONSP (INSERT E X)). We used primitive type reasoning. Summary Form: ( DEFUN INSERT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INSERT ACL2 !>(insert 3 '(1 2 4 5)) (1 2 3 4 5) ACL2 !>(defun isort (x) (if (endp x) nil (insert (car x) (isort (cdr x))))) The admission of ISORT is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of ISORT is described by the theorem (OR (CONSP (ISORT X)) (EQUAL (ISORT X) NIL)). We used the :type-prescription rule INSERT. Summary Form: ( DEFUN ISORT ...) Rules: ((:TYPE-PRESCRIPTION INSERT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ISORT ACL2 !>(isort '(5 4 6 7 2 1 0 3)) (0 1 2 3 4 5 6 7) ACL2 !>(defun ordered (x) (cond ((endp x) t) ((endp (cdr x)) t) (t (and (<= (car x) (car (cdr x))) (ordered (cdr x)))))) The admission of ORDERED is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of ORDERED is described by the theorem (OR (EQUAL (ORDERED X) T) (EQUAL (ORDERED X) NIL)). Summary Form: ( DEFUN ORDERED ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) ORDERED ACL2 !>(ordered '(1 2 3 4)) T ACL2 !>(ordered '(1 2 3 3 4)) T ACL2 !>(ordered '(1 3 2 4)) NIL ACL2 !>(defthm ordered-isort (ordered (isort x))) Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (ISORT X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit ISORT, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (ORDERED (ISORT (CDR X)))) (ORDERED (ISORT X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (ORDERED (ISORT (CDR X)))) (ORDERED (ISORT X))). This simplifies, using the :definition ISORT, to Subgoal *1/2'' (IMPLIES (AND (CONSP X) (ORDERED (ISORT (CDR X)))) (ORDERED (INSERT (CAR X) (ISORT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/2''' (IMPLIES (AND (CONSP (CONS X1 X2)) (ORDERED (ISORT X2))) (ORDERED (INSERT X1 (ISORT X2)))). This simplifies, using primitive type reasoning, to Subgoal *1/2'4' (IMPLIES (ORDERED (ISORT X2)) (ORDERED (INSERT X1 (ISORT X2)))). We generalize this conjecture, replacing (ISORT X2) by IT. This produces Subgoal *1/2'5' (IMPLIES (ORDERED IT) (ORDERED (INSERT X1 IT))). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (ENDP X) (ORDERED (ISORT X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (ORDERED (ISORT X))). But simplification reduces this to T, using the :definition ISORT and the :executable-counterpart of ORDERED. So we now return to *1.1, which is (IMPLIES (ORDERED IT) (ORDERED (INSERT X1 IT))). Perhaps we can prove *1.1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (INSERT X1 IT). If we let (:P IT X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP IT)) (<= (CAR IT) X1) (:P (CDR IT) X1)) (:P IT X1)) (IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT))) (:P IT X1)) (IMPLIES (ENDP IT) (:P IT X1))). This induction is justified by the same argument used to admit INSERT, namely, the measure (ACL2-COUNT IT) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following four nontautological subgoals. Subgoal *1.1/4 (IMPLIES (AND (NOT (ENDP IT)) (<= (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/4' (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type- prescription rules INSERT and ORDERED, to the following two conjectures. Subgoal *1.1/4.2 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (NOT (CONSP (CDR IT)))) (<= (CAR IT) (CAR (INSERT X1 (CDR IT))))). But simplification reduces this to T, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.1/4.1 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (ORDERED (INSERT X1 (CDR IT))) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT))) (<= (CAR IT) (CAR (INSERT X1 (CDR IT))))). The destructor terms (CAR IT) and (CDR IT) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace IT by (CONS IT1 IT2), generalizing (CAR IT) to IT1 and (CDR IT) to IT2. (2) Use CAR-CDR- ELIM, again, to replace IT2 by (CONS IT3 IT4), generalizing (CAR IT2) to IT3 and (CDR IT2) to IT4. These steps produce the following two goals. Subgoal *1.1/4.1.2 (IMPLIES (AND (NOT (CONSP IT2)) (CONSP (CONS IT1 IT2)) (<= IT1 X1) (ORDERED (INSERT X1 IT2)) (<= IT1 (CAR IT2)) (ORDERED IT2)) (<= IT1 (CAR (INSERT X1 IT2)))). But simplification reduces this to T, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, DEFAULT-<-1 and DEFAULT-CAR. Subgoal *1.1/4.1.1 (IMPLIES (AND (CONSP (CONS IT3 IT4)) (CONSP (LIST* IT1 IT3 IT4)) (<= IT1 X1) (ORDERED (INSERT X1 (CONS IT3 IT4))) (<= IT1 IT3) (ORDERED (CONS IT3 IT4))) (<= IT1 (CAR (INSERT X1 (CONS IT3 IT4))))). But simplification reduces this to T, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP IT)) (<= (CAR IT) X1) (NOT (ORDERED (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (NOT (ORDERED (CDR IT))) (ORDERED IT)) (ORDERED (INSERT X1 IT))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type- prescription rule INSERT, to the following two conjectures. Subgoal *1.1/3.2 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (NOT (ORDERED (CDR IT))) (NOT (CONSP (CDR IT)))) (<= (CAR IT) (CAR (INSERT X1 (CDR IT))))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.1/3.1 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (NOT (ORDERED (CDR IT))) (NOT (CONSP (CDR IT)))) (ORDERED (INSERT X1 (CDR IT)))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT)) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP IT) (< X1 (CAR IT)) (ORDERED IT)) (ORDERED (INSERT X1 IT))). This simplifies, using the :definitions INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type- prescription rule ORDERED, to the following two conjectures. Subgoal *1.1/2.2 (IMPLIES (AND (CONSP IT) (< X1 (CAR IT)) (NOT (CONSP (CDR IT)))) (<= X1 (CAR IT))). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/2.1 (IMPLIES (AND (CONSP IT) (< X1 (CAR IT)) (<= (CAR IT) (CADR IT)) (ORDERED (CDR IT))) (<= X1 (CAR IT))). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/1 (IMPLIES (AND (ENDP IT) (ORDERED IT)) (ORDERED (INSERT X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (AND (NOT (CONSP IT)) (ORDERED IT)) (ORDERED (INSERT X1 IT))). But simplification reduces this to T, using the :definitions INSERT and ORDERED, primitive type reasoning and the :rewrite rule CDR-CONS. That completes the proofs of *1.1 and *1. Q.E.D. The storage of ORDERED-ISORT depends upon the :type-prescription rule ORDERED. Summary Form: ( DEFTHM ORDERED-ISORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION NOT) (:DEFINITION ORDERED) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ORDERED) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-<-1) (:REWRITE DEFAULT-CAR) (:TYPE-PRESCRIPTION INSERT) (:TYPE-PRESCRIPTION ORDERED)) Warnings: None Time: 0.37 seconds (prove: 0.23, print: 0.12, other: 0.02) ORDERED-ISORT ACL2 !>(pe 'perm) d 2 (INCLUDE-BOOK "isort") \ >L (DEFUN PERM (X Y) (IF (CONSP X) (AND (MEM (CAR X) Y) (PERM (CDR X) (DEL (CAR X) Y))) (NOT (CONSP Y)))) ACL2 !>(perm '(1 2 3 3 4) '(4 3 1 2 3)) T ACL2 !>(perm '(1 2 3 3 4) '(4 3 1 2 2)) NIL ACL2 !>(defthm perm-isort (perm (isort x) x)) Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (ISORT X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit ISORT, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (PERM (ISORT (CDR X)) (CDR X))) (PERM (ISORT X) X)). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (PERM (ISORT (CDR X)) (CDR X))) (PERM (ISORT X) X)). This simplifies, using the :definition ISORT, to Subgoal *1/2'' (IMPLIES (AND (CONSP X) (PERM (ISORT (CDR X)) (CDR X))) (PERM (INSERT (CAR X) (ISORT (CDR X))) X)). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/2''' (IMPLIES (AND (CONSP (CONS X1 X2)) (PERM (ISORT X2) X2)) (PERM (INSERT X1 (ISORT X2)) (CONS X1 X2))). This simplifies, using primitive type reasoning, to Subgoal *1/2'4' (IMPLIES (PERM (ISORT X2) X2) (PERM (INSERT X1 (ISORT X2)) (CONS X1 X2))). We generalize this conjecture, replacing (ISORT X2) by IT. This produces Subgoal *1/2'5' (IMPLIES (PERM IT X2) (PERM (INSERT X1 IT) (CONS X1 X2))). This simplifies, using the :congruence rule PERM-IMPLIES-PERM-CONS- 2, to Subgoal *1/2'6' (PERM (INSERT X1 IT) (CONS X1 IT)). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (ENDP X) (PERM (ISORT X) X)). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (PERM (ISORT X) X)). But simplification reduces this to T, using the :definitions ISORT and PERM and the :executable-counterpart of CONSP. So we now return to *1.1, which is (PERM (INSERT X1 IT) (CONS X1 IT)). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (INSERT X1 IT). If we let (:P IT X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP IT)) (<= (CAR IT) X1) (:P (CDR IT) X1)) (:P IT X1)) (IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT))) (:P IT X1)) (IMPLIES (ENDP IT) (:P IT X1))). This induction is justified by the same argument used to admit INSERT, namely, the measure (ACL2-COUNT IT) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP IT)) (<= (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT)))) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT)))) (PERM (INSERT X1 IT) (CONS X1 IT))). This simplifies, using the :congruence rule PERM-IMPLIES-PERM-CONS- 2, the :definitions DEL, INSERT, MEM and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following four conjectures. Subgoal *1.1/3.4 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (EQUAL (CAR IT) X1)) (MEM X1 IT)). But simplification reduces this to T, using the :definition MEM, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM. Subgoal *1.1/3.3 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (EQUAL (CAR IT) X1)) (PERM (CDR IT) (DEL X1 IT))). But simplification reduces this to T, using the :definitions DEL, MEM and PERM, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM. Subgoal *1.1/3.2 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (NOT (EQUAL (CAR IT) X1))) (MEM X1 (CONS X1 (CDR IT)))). But simplification reduces this to T, using the :definition MEM, primitive type reasoning and the :rewrite rule CAR-CONS. Subgoal *1.1/3.1 (IMPLIES (AND (CONSP IT) (<= (CAR IT) X1) (PERM (INSERT X1 (CDR IT)) (CONS X1 (CDR IT))) (NOT (EQUAL (CAR IT) X1))) (PERM (CDR IT) (DEL X1 (CONS X1 (CDR IT))))). But simplification reduces this to T, using the :definitions DEL, MEM and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP IT)) (< X1 (CAR IT))) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP IT) (< X1 (CAR IT))) (PERM (INSERT X1 IT) (CONS X1 IT))). But simplification reduces this to T, using the :definitions DEL, INSERT, MEM and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.1/1 (IMPLIES (ENDP IT) (PERM (INSERT X1 IT) (CONS X1 IT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (NOT (CONSP IT)) (PERM (INSERT X1 IT) (CONS X1 IT))). But simplification reduces this to T, using the :definitions DEL, INSERT, MEM and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proofs of *1.1 and *1. Q.E.D. Summary Form: ( DEFTHM PERM-ISORT ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION DEL) (:DEFINITION ENDP) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION MEM) (:DEFINITION NOT) (:DEFINITION PERM) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CDR-ELIM) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.30 seconds (prove: 0.22, print: 0.07, other: 0.01) PERM-ISORT ACL2 !>(defun buggy-insert (e x) (cond ((endp x) x) ((< e (car x)) (cons e x)) (t (cons (car x) (buggy-insert e (cdr x)))))) The admission of BUGGY-INSERT is trivial, using the relation E0-ORD- < (which is known to be well-founded on the domain recognized by E0- ORDINALP) and the measure (ACL2-COUNT X). We could deduce no constraints on the type of BUGGY-INSERT. Summary Form: ( DEFUN BUGGY-INSERT ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) BUGGY-INSERT ACL2 !>(buggy-insert 3 '(1 2 4 5)) (1 2 3 4 5) ACL2 !>(buggy-insert 3 '(1 2)) (1 2) ACL2 !>(defun buggy-isort (x) (if (endp x) nil (buggy-insert (car x) (buggy-isort (cdr x))))) The admission of BUGGY-ISORT is trivial, using the relation E0-ORD- < (which is known to be well-founded on the domain recognized by E0- ORDINALP) and the measure (ACL2-COUNT X). We could deduce no constraints on the type of BUGGY-ISORT. Summary Form: ( DEFUN BUGGY-ISORT ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) BUGGY-ISORT ACL2 !>(defthm ordered-buggy-isort (ordered (buggy-isort x))) Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (BUGGY-ISORT X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit BUGGY- ISORT, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (ORDERED (BUGGY-ISORT (CDR X)))) (ORDERED (BUGGY-ISORT X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (ORDERED (BUGGY-ISORT (CDR X)))) (ORDERED (BUGGY-ISORT X))). This simplifies, using the :definition BUGGY-ISORT, to Subgoal *1/2'' (IMPLIES (AND (CONSP X) (ORDERED (BUGGY-ISORT (CDR X)))) (ORDERED (BUGGY-INSERT (CAR X) (BUGGY-ISORT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/2''' (IMPLIES (AND (CONSP (CONS X1 X2)) (ORDERED (BUGGY-ISORT X2))) (ORDERED (BUGGY-INSERT X1 (BUGGY-ISORT X2)))). This simplifies, using primitive type reasoning, to Subgoal *1/2'4' (IMPLIES (ORDERED (BUGGY-ISORT X2)) (ORDERED (BUGGY-INSERT X1 (BUGGY-ISORT X2)))). We generalize this conjecture, replacing (BUGGY-ISORT X2) by BIT. This produces Subgoal *1/2'5' (IMPLIES (ORDERED BIT) (ORDERED (BUGGY-INSERT X1 BIT))). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (ENDP X) (ORDERED (BUGGY-ISORT X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (ORDERED (BUGGY-ISORT X))). But simplification reduces this to T, using the :definition BUGGY-ISORT and the :executable-counterpart of ORDERED. So we now return to *1.1, which is (IMPLIES (ORDERED BIT) (ORDERED (BUGGY-INSERT X1 BIT))). Perhaps we can prove *1.1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (BUGGY-INSERT X1 BIT). If we let (:P BIT X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP BIT)) (<= (CAR BIT) X1) (:P (CDR BIT) X1)) (:P BIT X1)) (IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT))) (:P BIT X1)) (IMPLIES (ENDP BIT) (:P BIT X1))). This induction is justified by the same argument used to admit BUGGY- INSERT, namely, the measure (ACL2-COUNT BIT) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following four nontautological subgoals. Subgoal *1.1/4 (IMPLIES (AND (NOT (ENDP BIT)) (<= (CAR BIT) X1) (ORDERED (BUGGY-INSERT X1 (CDR BIT))) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/4' (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (ORDERED (BUGGY-INSERT X1 (CDR BIT))) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). This simplifies, using the :definitions BUGGY-INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type- prescription rule ORDERED, to the following two conjectures. Subgoal *1.1/4.2 (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (ORDERED (BUGGY-INSERT X1 (CDR BIT))) (NOT (CONSP (CDR BIT))) (CONSP (BUGGY-INSERT X1 (CDR BIT)))) (<= (CAR BIT) (CAR (BUGGY-INSERT X1 (CDR BIT))))). But simplification reduces this to T, using the :definitions BUGGY- INSERT and ORDERED. Subgoal *1.1/4.1 (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (ORDERED (BUGGY-INSERT X1 (CDR BIT))) (<= (CAR BIT) (CADR BIT)) (ORDERED (CDR BIT)) (CONSP (BUGGY-INSERT X1 (CDR BIT)))) (<= (CAR BIT) (CAR (BUGGY-INSERT X1 (CDR BIT))))). The destructor terms (CAR BIT) and (CDR BIT) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace BIT by (CONS BIT1 BIT2), generalizing (CAR BIT) to BIT1 and (CDR BIT) to BIT2. (2) Use CAR- CDR-ELIM, again, to replace BIT2 by (CONS BIT3 BIT4), generalizing (CAR BIT2) to BIT3 and (CDR BIT2) to BIT4. These steps produce the following two goals. Subgoal *1.1/4.1.2 (IMPLIES (AND (NOT (CONSP BIT2)) (CONSP (CONS BIT1 BIT2)) (<= BIT1 X1) (ORDERED (BUGGY-INSERT X1 BIT2)) (<= BIT1 (CAR BIT2)) (ORDERED BIT2) (CONSP (BUGGY-INSERT X1 BIT2))) (<= BIT1 (CAR (BUGGY-INSERT X1 BIT2)))). But simplification reduces this to T, using the :definitions BUGGY- INSERT and ORDERED, primitive type reasoning and the :rewrite rules DEFAULT-<-1 and DEFAULT-CAR. Subgoal *1.1/4.1.1 (IMPLIES (AND (CONSP (CONS BIT3 BIT4)) (CONSP (LIST* BIT1 BIT3 BIT4)) (<= BIT1 X1) (ORDERED (BUGGY-INSERT X1 (CONS BIT3 BIT4))) (<= BIT1 BIT3) (ORDERED (CONS BIT3 BIT4)) (CONSP (BUGGY-INSERT X1 (CONS BIT3 BIT4)))) (<= BIT1 (CAR (BUGGY-INSERT X1 (CONS BIT3 BIT4))))). But simplification reduces this to T, using the :definitions BUGGY- INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP BIT)) (<= (CAR BIT) X1) (NOT (ORDERED (CDR BIT))) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (NOT (ORDERED (CDR BIT))) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). This simplifies, using the :definitions BUGGY-INSERT and ORDERED, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following two conjectures. Subgoal *1.1/3.2 (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (NOT (ORDERED (CDR BIT))) (NOT (CONSP (CDR BIT))) (CONSP (BUGGY-INSERT X1 (CDR BIT)))) (<= (CAR BIT) (CAR (BUGGY-INSERT X1 (CDR BIT))))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.1/3.1 (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (NOT (ORDERED (CDR BIT))) (NOT (CONSP (CDR BIT))) (CONSP (BUGGY-INSERT X1 (CDR BIT)))) (ORDERED (BUGGY-INSERT X1 (CDR BIT)))). But simplification reduces this to T, using the :definition ORDERED. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT)) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP BIT) (< X1 (CAR BIT)) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). This simplifies, using the :definitions BUGGY-INSERT and ORDERED, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type- prescription rule ORDERED, to the following two conjectures. Subgoal *1.1/2.2 (IMPLIES (AND (CONSP BIT) (< X1 (CAR BIT)) (NOT (CONSP (CDR BIT)))) (<= X1 (CAR BIT))). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/2.1 (IMPLIES (AND (CONSP BIT) (< X1 (CAR BIT)) (<= (CAR BIT) (CADR BIT)) (ORDERED (CDR BIT))) (<= X1 (CAR BIT))). But simplification reduces this to T, using linear arithmetic. Subgoal *1.1/1 (IMPLIES (AND (ENDP BIT) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (AND (NOT (CONSP BIT)) (ORDERED BIT)) (ORDERED (BUGGY-INSERT X1 BIT))). But simplification reduces this to T, using the :definitions BUGGY- INSERT and ORDERED. That completes the proofs of *1.1 and *1. Q.E.D. The storage of ORDERED-BUGGY-ISORT depends upon the :type-prescription rule ORDERED. Summary Form: ( DEFTHM ORDERED-BUGGY-ISORT ...) Rules: ((:DEFINITION BUGGY-INSERT) (:DEFINITION BUGGY-ISORT) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION ORDERED) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ORDERED) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-<-1) (:REWRITE DEFAULT-CAR) (:TYPE-PRESCRIPTION ORDERED)) Warnings: None Time: 0.55 seconds (prove: 0.49, print: 0.04, other: 0.02) ORDERED-BUGGY-ISORT ACL2 !>(defthm perm-buggy-isort (perm (buggy-isort x) x)) Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (BUGGY-ISORT X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit BUGGY- ISORT, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (PERM (BUGGY-ISORT (CDR X)) (CDR X))) (PERM (BUGGY-ISORT X) X)). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (PERM (BUGGY-ISORT (CDR X)) (CDR X))) (PERM (BUGGY-ISORT X) X)). This simplifies, using the :definition BUGGY-ISORT, to Subgoal *1/2'' (IMPLIES (AND (CONSP X) (PERM (BUGGY-ISORT (CDR X)) (CDR X))) (PERM (BUGGY-INSERT (CAR X) (BUGGY-ISORT (CDR X))) X)). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/2''' (IMPLIES (AND (CONSP (CONS X1 X2)) (PERM (BUGGY-ISORT X2) X2)) (PERM (BUGGY-INSERT X1 (BUGGY-ISORT X2)) (CONS X1 X2))). This simplifies, using primitive type reasoning, to Subgoal *1/2'4' (IMPLIES (PERM (BUGGY-ISORT X2) X2) (PERM (BUGGY-INSERT X1 (BUGGY-ISORT X2)) (CONS X1 X2))). We generalize this conjecture, replacing (BUGGY-ISORT X2) by BIT. This produces Subgoal *1/2'5' (IMPLIES (PERM BIT X2) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 X2))). This simplifies, using the :congruence rule PERM-IMPLIES-PERM-CONS- 2, to Subgoal *1/2'6' (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT)). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (ENDP X) (PERM (BUGGY-ISORT X) X)). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (PERM (BUGGY-ISORT X) X)). But simplification reduces this to T, using the :definitions BUGGY- ISORT and PERM and the :executable-counterpart of CONSP. So we now return to *1.1, which is (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT)). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (BUGGY-INSERT X1 BIT). If we let (:P BIT X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP BIT)) (<= (CAR BIT) X1) (:P (CDR BIT) X1)) (:P BIT X1)) (IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT))) (:P BIT X1)) (IMPLIES (ENDP BIT) (:P BIT X1))). This induction is justified by the same argument used to admit BUGGY- INSERT, namely, the measure (ACL2-COUNT BIT) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP BIT)) (<= (CAR BIT) X1) (PERM (BUGGY-INSERT X1 (CDR BIT)) (CONS X1 (CDR BIT)))) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (PERM (BUGGY-INSERT X1 (CDR BIT)) (CONS X1 (CDR BIT)))) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT))). This simplifies, using the :definitions BUGGY-INSERT, DEL, MEM and PERM, the :equivalence rule PERM-IS-AN-EQUIVALENCE, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to the following two conjectures. Subgoal *1.1/3.2 (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (PERM (BUGGY-INSERT X1 (CDR BIT)) (CONS X1 (CDR BIT))) (EQUAL (CAR BIT) X1)) (PERM (BUGGY-INSERT X1 (CDR BIT)) BIT)). But simplification reduces this to T, using the :rewrite rule CAR-CDR- ELIM. Subgoal *1.1/3.1 (IMPLIES (AND (CONSP BIT) (<= (CAR BIT) X1) (PERM (BUGGY-INSERT X1 (CDR BIT)) (CONS X1 (CDR BIT))) (NOT (EQUAL (CAR BIT) X1))) (PERM (BUGGY-INSERT X1 (CDR BIT)) (BUGGY-INSERT X1 (CDR BIT)))). But simplification reduces this to T, using primitive type reasoning. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP BIT)) (< X1 (CAR BIT))) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP BIT) (< X1 (CAR BIT))) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT))). But simplification reduces this to T, using the :definitions BUGGY- INSERT, DEL, MEM and PERM, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1.1/1 (IMPLIES (ENDP BIT) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (NOT (CONSP BIT)) (PERM (BUGGY-INSERT X1 BIT) (CONS X1 BIT))). This simplifies, using the :definitions BUGGY-INSERT and PERM and primitive type reasoning, to Subgoal *1.1/1'' (CONSP BIT). We suspect that this conjecture is not a theorem. We might as well be trying to prove Subgoal *1.1/1''' NIL. Obviously, the proof attempt has failed. Summary Form: ( DEFTHM PERM-BUGGY-ISORT ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION BUGGY-INSERT) (:DEFINITION BUGGY-ISORT) (:DEFINITION DEL) (:DEFINITION ENDP) (:DEFINITION MEM) (:DEFINITION NOT) (:DEFINITION PERM) (:ELIM CAR-CDR-ELIM) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CDR-ELIM) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.24 seconds (prove: 0.18, print: 0.05, other: 0.01) ******** FAILED ******** See :DOC failure ******** FAILED ******** ACL2 !>(defthm buggy-isort-is-nil (equal (buggy-isort x) nil)) By case analysis we reduce the conjecture to Goal' (NOT (BUGGY-ISORT X)). Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (BUGGY-ISORT X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit BUGGY- ISORT, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (NOT (BUGGY-ISORT (CDR X)))) (NOT (BUGGY-ISORT X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (NOT (BUGGY-ISORT (CDR X)))) (NOT (BUGGY-ISORT X))). But simplification reduces this to T, using the :definitions BUGGY- INSERT and BUGGY-ISORT and the :executable-counterpart of CONSP. Subgoal *1/1 (IMPLIES (ENDP X) (NOT (BUGGY-ISORT X))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (NOT (BUGGY-ISORT X))). But simplification reduces this to T, using the :definition BUGGY-ISORT. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM BUGGY-ISORT-IS-NIL ...) Rules: ((:DEFINITION BUGGY-INSERT) (:DEFINITION BUGGY-ISORT) (:DEFINITION ENDP) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART CONSP)) Warnings: None Time: 0.03 seconds (prove: 0.01, print: 0.01, other: 0.01) BUGGY-ISORT-IS-NIL ACL2 !>(defun full-adder (p q c) (mv (xor p (xor q c)) (maj p q c))) Since FULL-ADDER is non-recursive, its admission is trivial. We observe that the type of FULL-ADDER is described by the theorem (AND (CONSP (FULL-ADDER P Q C)) (TRUE-LISTP (FULL-ADDER P Q C))). We used primitive type reasoning. (FULL-ADDER * * *) => (MV * *). Summary Form: ( DEFUN FULL-ADDER ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) FULL-ADDER ACL2 !>(full-adder t t nil) (NIL T) ACL2 !>(full-adder nil nil t) (T NIL) ACL2 !>(defun serial-adder (a b c) (declare (xargs :measure (+ (acl2-count a) (acl2-count b)))) (if (and (endp a) (endp b)) (list c) (mv-let (sum cout) (full-adder (car a) (car b) c) (cons sum (serial-adder (cdr a) (cdr b) cout))))) For the admission of SERIAL-ADDER we will use the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (+ (ACL2-COUNT A) (ACL2-COUNT B)). The non-trivial part of the measure conjecture is Goal (AND (E0-ORDINALP (+ (ACL2-COUNT A) (ACL2-COUNT B))) (IMPLIES (NOT (AND (ENDP A) (ENDP B))) (E0-ORD-< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT (CDR B))) (+ (ACL2-COUNT A) (ACL2-COUNT B))))). By case analysis we reduce the conjecture to the following two conjectures. Subgoal 2 (E0-ORDINALP (+ (ACL2-COUNT A) (ACL2-COUNT B))). But simplification reduces this to T, using the :definition E0-ORDINALP, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (NOT (AND (ENDP A) (ENDP B))) (E0-ORD-< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT (CDR B))) (+ (ACL2-COUNT A) (ACL2-COUNT B)))). This simplifies, using the :definitions E0-ORD-< and ENDP, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to the following two conjectures. Subgoal 1.2 (IMPLIES (CONSP A) (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT (CDR B))) (+ (ACL2-COUNT A) (ACL2-COUNT B)))). The destructor terms (CAR B) and (CDR B) can be eliminated by using CAR-CDR-ELIM to replace B by (CONS B1 B2), generalizing (CAR B) to B1 and (CDR B) to B2. This produces the following two goals. Subgoal 1.2.2 (IMPLIES (AND (NOT (CONSP B)) (CONSP A)) (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT (CDR B))) (+ (ACL2-COUNT A) (ACL2-COUNT B)))). This simplifies, using the :definition FIX, the :executable-counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+, DEFAULT-CDR and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 1.2.2' (IMPLIES (AND (NOT (CONSP B)) (CONSP A)) (< (ACL2-COUNT (CDR A)) (+ (ACL2-COUNT A) (ACL2-COUNT B)))). The destructor terms (CAR A) and (CDR A) can be eliminated by using CAR-CDR-ELIM to replace A by (CONS A1 A2), generalizing (CAR A) to A1 and (CDR A) to A2. This produces the following goal. Subgoal 1.2.2'' (IMPLIES (AND (CONSP (CONS A1 A2)) (NOT (CONSP B))) (< (ACL2-COUNT A2) (+ (ACL2-COUNT (CONS A1 A2)) (ACL2-COUNT B)))). This simplifies, using the :definition ACL2-COUNT, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-OF-+, to Subgoal 1.2.2''' (IMPLIES (NOT (CONSP B)) (< (ACL2-COUNT A2) (+ 1 (ACL2-COUNT A1) (ACL2-COUNT A2) (ACL2-COUNT B)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 1.2.1 (IMPLIES (AND (CONSP (CONS B1 B2)) (CONSP A)) (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT B2)) (+ (ACL2-COUNT A) (ACL2-COUNT (CONS B1 B2))))). This simplifies, using the :definition ACL2-COUNT, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-OF-+, to Subgoal 1.2.1' (IMPLIES (CONSP A) (< (+ (ACL2-COUNT B2) (ACL2-COUNT (CDR A))) (+ 1 (ACL2-COUNT A) (ACL2-COUNT B1) (ACL2-COUNT B2)))). The destructor terms (CAR A) and (CDR A) can be eliminated by using CAR-CDR-ELIM to replace A by (CONS A1 A2), generalizing (CAR A) to A1 and (CDR A) to A2. This produces the following goal. Subgoal 1.2.1'' (IMPLIES (CONSP (CONS A1 A2)) (< (+ (ACL2-COUNT B2) (ACL2-COUNT A2)) (+ 1 (ACL2-COUNT (CONS A1 A2)) (ACL2-COUNT B1) (ACL2-COUNT B2)))). This simplifies, using the :definitions ACL2-COUNT and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- 2-OF-+, COMMUTATIVITY-OF-+ and FOLD-CONSTS-IN-+, to Subgoal 1.2.1''' (< (+ (ACL2-COUNT A2) (ACL2-COUNT B2)) (+ 2 (ACL2-COUNT A1) (ACL2-COUNT A2) (ACL2-COUNT B1) (ACL2-COUNT B2))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 1.1 (IMPLIES (CONSP B) (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT (CDR B))) (+ (ACL2-COUNT A) (ACL2-COUNT B)))). The destructor terms (CAR B) and (CDR B) can be eliminated by using CAR-CDR-ELIM to replace B by (CONS B1 B2), generalizing (CAR B) to B1 and (CDR B) to B2. This produces the following goal. Subgoal 1.1' (IMPLIES (CONSP (CONS B1 B2)) (< (+ (ACL2-COUNT (CDR A)) (ACL2-COUNT B2)) (+ (ACL2-COUNT A) (ACL2-COUNT (CONS B1 B2))))). This simplifies, using the :definition ACL2-COUNT, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-OF-+, to Subgoal 1.1'' (< (+ (ACL2-COUNT B2) (ACL2-COUNT (CDR A))) (+ 1 (ACL2-COUNT A) (ACL2-COUNT B1) (ACL2-COUNT B2))). The destructor terms (CAR A) and (CDR A) can be eliminated by using CAR-CDR-ELIM to replace A by (CONS A1 A2), generalizing (CAR A) to A1 and (CDR A) to A2. This produces the following two goals. Subgoal 1.1.2 (IMPLIES (NOT (CONSP A)) (< (+ (ACL2-COUNT B2) (ACL2-COUNT (CDR A))) (+ 1 (ACL2-COUNT A) (ACL2-COUNT B1) (ACL2-COUNT B2)))). This simplifies, using the :definition FIX, the :executable-counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+, DEFAULT-CDR and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 1.1.2' (IMPLIES (NOT (CONSP A)) (< (ACL2-COUNT B2) (+ 1 (ACL2-COUNT A) (ACL2-COUNT B1) (ACL2-COUNT B2)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 1.1.1 (IMPLIES (CONSP (CONS A1 A2)) (< (+ (ACL2-COUNT B2) (ACL2-COUNT A2)) (+ 1 (ACL2-COUNT (CONS A1 A2)) (ACL2-COUNT B1) (ACL2-COUNT B2)))). This simplifies, using the :definitions ACL2-COUNT and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- 2-OF-+, COMMUTATIVITY-OF-+ and FOLD-CONSTS-IN-+, to Subgoal 1.1.1' (< (+ (ACL2-COUNT A2) (ACL2-COUNT B2)) (+ 2 (ACL2-COUNT A1) (ACL2-COUNT A2) (ACL2-COUNT B1) (ACL2-COUNT B2))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for SERIAL-ADDER. Thus, we admit this function under the principle of definition. We observe that the type of SERIAL-ADDER is described by the theorem (AND (CONSP (SERIAL-ADDER A B C)) (TRUE-LISTP (SERIAL-ADDER A B C))). We used primitive type reasoning. Summary Form: ( DEFUN SERIAL-ADDER ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION ENDP) (:DEFINITION FIX) (:DEFINITION SYNTAXP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DEFAULT-CDR) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.64 seconds (prove: 0.58, print: 0.02, other: 0.04) SERIAL-ADDER ACL2 !>(serial-adder '(t t nil) '(t nil t) nil) (NIL NIL NIL T) ACL2 !>(serial-adder '(t t nil) '(t nil t) t) (T NIL NIL T) ACL2 !>(serial-adder '(t t nil) '() t) (NIL NIL T NIL) ACL2 !>(defconst *a* '(t nil nil t t t t t nil t t t nil t nil t nil t nil t t t t t t t t t t t nil nil nil nil nil t t t t t nil t t t nil t nil t t t nil t t t t t nil t nil t t nil nil t t nil nil t t t t t nil t nil t nil t t t nil t nil t t t t t nil t nil t nil t nil nil t nil nil t t t t t t t t t t t nil nil nil nil nil t t t t t t t t t nil t nil t nil nil nil nil t t t t t t nil t nil nil t t)) Summary Form: ( DEFCONST *A* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *A* ACL2 !>(defconst *b* '(t t t t t t t t t t nil t nil t nil t t nil t t t t t t t t t t nil nil nil nil nil nil nil t t t t t nil t nil t t t t t t nil nil t t t t t t t t t t nil t nil t nil t nil t t t t t t t t t nil nil nil nil t t t t t t t nil t nil t t t t nil t nil t nil t t t t nil t nil t t nil nil t nil nil nil t t t t t nil t nil t nil t nil nil nil t t t t t t t t t t t nil t nil t)) Summary Form: ( DEFCONST *B* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *B* ACL2 !>(serial-adder *a* *b* nil) (NIL NIL NIL T T T T T NIL T NIL T T NIL T NIL NIL NIL NIL T T T T T T T T T NIL NIL T NIL NIL NIL NIL NIL T T T T T NIL NIL T NIL T NIL T T NIL T NIL T T T T NIL T NIL T T T T T NIL T T T NIL T T T NIL T NIL T NIL NIL NIL NIL T NIL NIL T T T T T T NIL T NIL NIL T NIL T NIL T T T NIL T T T NIL T NIL T T NIL T T NIL NIL NIL NIL T T T T NIL T NIL T T NIL T T NIL T T T NIL T T T T T NIL T T T T NIL T) ACL2 !>(defun n (v) (cond ((endp v) 0) ((car v) (+ 1 (* 2 (n (cdr v))))) (t (* 2 (n (cdr v)))))) The admission of N is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT V). We observe that the type of N is described by the theorem (AND (INTEGERP (N V)) (<= 0 (N V))). We used primitive type reasoning. Summary Form: ( DEFUN N ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) N ACL2 !>(n '(t t nil)) 3 ACL2 !>(n *a*) 17765695716094771496618484167493975784730361 ACL2 !>(n *b*) 15331138877664345459150421522004660157524991 ACL2 !>(+ (n *a*) (n *b*)) 33096834593759116955768905689498635942255352 ACL2 !>(n (serial-adder *a* *b* nil)) 33096834593759116955768905689498635942255352 ACL2 !>(defthm serial-adder-correct (equal (n (serial-adder x y c)) (+ (n x) (n y) (if c 1 0)))) This simplifies, using trivial observations, to the following two conjectures. Subgoal 2 (IMPLIES C (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) 1))). This simplifies, using the :rewrite rules COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-OF-+, to Subgoal 2' (IMPLIES C (EQUAL (N (SERIAL-ADDER X Y C)) (+ 1 (N X) (N Y)))). Name the formula above *1. Subgoal 1 (IMPLIES (NOT C) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (N X) (N Y) 0))). This simplifies, using the :definition FIX, the :rewrite rules COMMUTATIVITY- OF-+ and UNICITY-OF-0 and the :type-prescription rule N, to Subgoal 1' (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (N X) (N Y))). Normally we would attempt to prove this formula by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (N Y), but modified to accommodate (N X) and (SERIAL-ADDER X Y C). If we let (:P C X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP Y)) (NOT (CAR Y)) (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) (CDR X) (CDR Y))) (:P C X Y)) (IMPLIES (AND (NOT (ENDP Y)) (CAR Y) (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) (CDR X) (CDR Y))) (:P C X Y)) (IMPLIES (ENDP Y) (:P C X Y))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT Y) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variables C and X are being instantiated. When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ENDP Y)) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+, CONS, MV-NTH, XOR and ZP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+ and UNICITY- OF-0 and the :type-prescription rule N, to the following nine conjectures. Subgoal *1/3.9 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) C) (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (+ 1 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). This simplifies, using the :definitions FIX and N, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION- FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL- ADDER, to Subgoal *1/3.9' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)))) (CONSP X) C) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (+ (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ and XOR, the :executable-counterparts of CONS, MV-NTH and XOR, primitive type reasoning and the :rewrite rule DISTRIBUTIVITY. Subgoal *1/3.8 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X)) C) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX and N, the :executable- counterparts of EQUAL and FIX, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION-FOR- *, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/3.8' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X)) C) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ and XOR, the :executable-counterparts of CONS, MV-NTH, N and XOR, the :rewrite rules DEFAULT-CAR, DEFAULT-CDR and UNICITY-OF- 0 and the :type-prescription rule N. Subgoal *1/3.7 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (+ 0 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/3.7' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (FIX (+ (* 2 (N (CDR Y))) (* 2 (N (CDR X))))))). But simplification reduces this to T, using the :definitions FIX and N, the :executable-counterparts of FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/3.6 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 0 (* 2 (N (CDR Y))) 0))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/3.6' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL))) (FIX (+ (* 2 (N (CDR Y))) 0)))). This simplifies, using the :definitions FIX and N, the :executable- counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT- CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/3.6'' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definition FIX, the :executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/3.5 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (CAR X) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 1 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N and SYNTAXP, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/3.5' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (CAR X) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 2 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY- + and ZP, primitive type reasoning and the :rewrite rules CDR-CONS and DISTRIBUTIVITY. Subgoal *1/3.4 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (CAR X) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X))) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 (* 2 (N (CDR Y))) 0))). But simplification reduces this to T, using trivial observations. Subgoal *1/3.3 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX, N and SERIAL-ADDER, the :executable-counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY- OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/3.3' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definition FIX, the :executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/3.2 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (CAR X)) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/3.1 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (NOT (CAR X))) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX, N and SERIAL-ADDER, the :executable-counterparts of FULL-ADDER and MV- NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type- prescription rules N and SERIAL-ADDER. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP Y)) (CAR Y) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP Y) (CAR Y) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). This simplifies, using the :definitions FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY- +, CAR, CONSP, EQ, IF, XOR and ZP, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+, to the following nine conjectures. Subgoal *1/2.9 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) C) (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 1 1 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N and SYNTAXP, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/2.9' (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X) C) (EQUAL (+ 1 (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))) (+ 3 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY- *, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+. Subgoal *1/2.8 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X)) C) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C))) (+ 1 1 (* 2 (N (CDR Y))) 0))). But simplification reduces this to T, using trivial observations. Subgoal *1/2.7 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 1 0 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/2.7' (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 1 (FIX (+ (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, MV-NTH, N, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+, DISTRIBUTIVITY and FOLD-CONSTS-IN-+ and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/2.6 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 0 (* 2 (N (CDR Y))) 0))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/2.6' (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 (FIX (+ (* 2 (N (CDR Y))) 0))))). But we reduce the conjecture to T, by case analysis. Subgoal *1/2.5 (IMPLIES (AND (CONSP Y) (CAR Y) (NOT (CAR X)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X)) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ 1 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY- OF-0 and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/2.4 (IMPLIES (AND (CONSP Y) (CAR Y) (NOT (CAR X)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ 1 (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, N, SERIAL- ADDER and XOR, the :executable-counterparts of CONS, EQUAL, FIX, MV- NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION- FOR-*, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/2.4' (IMPLIES (AND (CONSP Y) (CAR Y) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definition FIX, the :executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/2.3 (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X))) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C))) (+ 2 (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX and N, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL- ADDER, to Subgoal *1/2.3' (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (* 2 (N (SERIAL-ADDER NIL (CDR Y) C))) (+ 2 (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY- *, BINARY-+, N, XOR and ZP, primitive type reasoning, the :rewrite rules CDR-CONS, DEFAULT-CAR, DEFAULT-CDR, DISTRIBUTIVITY and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/2.2 (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (CAR X)) (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 2 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N and SYNTAXP, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/2.2' (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X) (CAR X)) (EQUAL (+ 1 (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))) (+ 3 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY- *, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+. Subgoal *1/2.1 (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (NOT (CAR X))) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 2 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). This simplifies, using the :definition N, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY- OF-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/2.1' (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X) (NOT (CAR X))) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 2 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY- +, XOR and ZP, primitive type reasoning and the :rewrite rules CDR- CONS and DISTRIBUTIVITY. Subgoal *1/1 (IMPLIES (ENDP Y) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP Y)) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+, CONS, EQUAL, N and ZP, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR and UNICITY-OF-0, to the following five conjectures. Subgoal *1/1.5 (IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C) (EQUAL (N (LIST C)) (+ 1 0))). By the :executable-counterpart of BINARY-+ we reduce the conjecture to Subgoal *1/1.5' (IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C) (EQUAL (N (LIST C)) 1)). But simplification reduces this to T, using the :definition N, the :executable-counterparts of BINARY-*, BINARY-+, EQUAL and N, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1/1.4 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) C (CAR X)) (EQUAL (N (CONS (XOR (CAR X) T) (SERIAL-ADDER (CDR X) NIL C))) (+ 1 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N, SYNTAXP and XOR, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/1.4' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) C (CAR X)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) NIL C))) (+ 2 (* 2 (N (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/1.4'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (CONSP Y)) C X1) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/1.4''' (IMPLIES (AND (NOT (CONSP Y)) C X1) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). This simplifies, using trivial observations, to Subgoal *1/1.4'4' (IMPLIES (AND (NOT (CONSP Y)) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/1.4'5' (IMPLIES C (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). Name the formula above *1.1. Subgoal *1/1.3 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (CAR X)) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (+ 0 1 (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/1.3' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (CAR X)) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (FIX (+ 1 (* 2 (N (CDR X))))))). This simplifies, using the :definitions FIX, N and XOR, the :executable- counterparts of EQUAL and FIX, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, LEFT-CANCELLATION-FOR-* and LEFT-CANCELLATION- FOR-+ and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/1.3'' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X)))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/1.3''' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (CONSP Y)) X1) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). This simplifies, using primitive type reasoning, to Subgoal *1/1.3'4' (IMPLIES (AND (NOT (CONSP Y)) X1) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). This simplifies, using trivial observations, to Subgoal *1/1.3'5' (IMPLIES (NOT (CONSP Y)) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/1.3'6' (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2)). Name the formula above *1.2. Subgoal *1/1.2 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) C (NOT (CAR X))) (EQUAL (N (CONS (XOR (CAR X) T) (SERIAL-ADDER (CDR X) NIL NIL))) (+ 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions FIX and N, the :executable- counterparts of EQUAL, FIX and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, LEFT-CANCELLATION-FOR-* and LEFT-CANCELLATION- FOR-+ and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/1.2' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT (CAR X))) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X)))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/1.2'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (CONSP Y)) (NOT X1)) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). This simplifies, using primitive type reasoning, to Subgoal *1/1.2''' (IMPLIES (NOT (CONSP Y)) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/1.2'4' (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2)). Name the formula above *1.3. Subgoal *1/1.1 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (NOT (CAR X))) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (+ 0 (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/1.1' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (NOT (CAR X))) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (FIX (* 2 (N (CDR X)))))). This simplifies, using the :definitions FIX and N, the :executable- counterparts of EQUAL, FIX and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and LEFT-CANCELLATION-FOR-* and the :type- prescription rules N and SERIAL-ADDER, to Subgoal *1/1.1'' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT (CAR X))) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X)))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/1.1''' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (CONSP Y)) (NOT X1)) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). This simplifies, using primitive type reasoning, to Subgoal *1/1.1'4' (IMPLIES (NOT (CONSP Y)) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/1.1'5' (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2)). Name the formula above *1.4. But this formula is subsumed by *1.3, which we'll try to prove later. We therefore regard *1.4 as proved (pending the proof of the more general *1.3). We next consider *1.3, which is (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2)). But this formula is subsumed by *1.2, which we'll try to prove later. We therefore regard *1.3 as proved (pending the proof of the more general *1.2). We next consider *1.2, which is (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2)). Perhaps we can prove *1.2 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (N X2). If we let (:P X2) denote *1.2 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X2)) (NOT (CAR X2)) (:P (CDR X2))) (:P X2)) (IMPLIES (AND (NOT (ENDP X2)) (CAR X2) (:P (CDR X2))) (:P X2)) (IMPLIES (ENDP X2) (:P X2))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT X2) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1.2/3 (IMPLIES (AND (NOT (ENDP X2)) (NOT (CAR X2)) (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL)) (N (CDR X2)))) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/3' (IMPLIES (AND (CONSP X2) (NOT (CAR X2)) (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL)) (N (CDR X2)))) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). But simplification reduces this to T, using the :definitions N and SERIAL-ADDER, the :executable-counterparts of CAR, CDR, FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rule SERIAL-ADDER. Subgoal *1.2/2 (IMPLIES (AND (NOT (ENDP X2)) (CAR X2) (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL)) (N (CDR X2)))) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/2' (IMPLIES (AND (CONSP X2) (CAR X2) (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL)) (N (CDR X2)))) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of CAR, CDR, CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rule SERIAL-ADDER. Subgoal *1.2/1 (IMPLIES (ENDP X2) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.2/1' (IMPLIES (NOT (CONSP X2)) (EQUAL (N (SERIAL-ADDER X2 NIL NIL)) (N X2))). But simplification reduces this to T, using the :definitions N and SERIAL-ADDER and the :executable-counterparts of CONS, CONSP, EQUAL and N. That completes the proof of *1.2. We therefore turn our attention to *1.1, which is (IMPLIES C (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (N X2). If we let (:P C X2) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X2)) (NOT (CAR X2)) (:P C (CDR X2))) (:P C X2)) (IMPLIES (AND (NOT (ENDP X2)) (CAR X2) (:P C (CDR X2))) (:P C X2)) (IMPLIES (ENDP X2) (:P C X2))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT X2) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP X2)) (NOT (CAR X2)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP X2) (NOT (CAR X2)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, N, SERIAL- ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, CAR, CDR, CONS, CONSP, EQ, EQUAL, FIX, IF, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVITY, FOLD- CONSTS-IN-*, LEFT-CANCELLATION-FOR-* and LEFT-CANCELLATION-FOR-+ and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1.1/3'' (IMPLIES (AND (CONSP X2) (NOT (CAR X2)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (N (SERIAL-ADDER (CDR X2) NIL NIL)) (N (CDR X2)))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. This produces the following goal. Subgoal *1.1/3''' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT X3) (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C))) (+ 2 (* 2 (N X4)))) C) (EQUAL (N (SERIAL-ADDER X4 NIL NIL)) (N X4))). This simplifies, using primitive type reasoning, to Subgoal *1.1/3'4' (IMPLIES (AND (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C))) (+ 2 (* 2 (N X4)))) C) (EQUAL (N (SERIAL-ADDER X4 NIL NIL)) (N X4))). We generalize this conjecture, replacing (N X4) by I and restricting the type of the new variable I to be that of the term it replaces, as established by N. This produces Subgoal *1.1/3'5' (IMPLIES (AND (INTEGERP I) (<= 0 I) (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C))) (+ 2 (* 2 I))) C) (EQUAL (N (SERIAL-ADDER X4 NIL NIL)) I)). Name the formula above *1.1.1. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP X2)) (CAR X2) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP X2) (CAR X2) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CDR, CONSP, EQ, IF and ZP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVITY, FOLD- CONSTS-IN-* and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL- ADDER. Subgoal *1.1/1 (IMPLIES (AND (ENDP X2) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (AND (NOT (CONSP X2)) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). But simplification reduces this to T, using the :definitions N and SERIAL-ADDER, the :executable-counterparts of BINARY-*, BINARY-+, CONSP, EQUAL and N, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. So we now return to *1.1.1, which is (IMPLIES (AND (INTEGERP I) (<= 0 I) (EQUAL (* 2 (N (SERIAL-ADDER X4 NIL C))) (+ 2 (* 2 I))) C) (EQUAL (N (SERIAL-ADDER X4 NIL NIL)) I)). No induction schemes are suggested by *1.1.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM SERIAL-ADDER-CORRECT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION FIX) (:DEFINITION FULL-ADDER) (:DEFINITION MAJ) (:DEFINITION MV-NTH) (:DEFINITION N) (:DEFINITION NOT) (:DEFINITION SERIAL-ADDER) (:DEFINITION SYNTAXP) (:DEFINITION XOR) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART FULL-ADDER) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART MV-NTH) (:EXECUTABLE-COUNTERPART N) (:EXECUTABLE-COUNTERPART XOR) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DEFAULT-CAR) (:REWRITE DEFAULT-CDR) (:REWRITE DISTRIBUTIVITY) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE LEFT-CANCELLATION-FOR-*) (:REWRITE LEFT-CANCELLATION-FOR-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION N) (:TYPE-PRESCRIPTION SERIAL-ADDER)) Warnings: None Time: 2.64 seconds (prove: 2.16, print: 0.47, other: 0.01) ******** FAILED ******** See :DOC failure ******** FAILED ******** ACL2 !>(defthm serial-adder-special-case (and (equal (n (serial-adder x nil t)) (+ 1 (n x))) (equal (n (serial-adder x nil nil)) (n x)))) By case analysis we reduce the conjecture to the following two conjectures. Subgoal 2 (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))). Name the formula above *1. Subgoal 1 (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)). Normally we would attempt to prove this formula by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (N X). If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (CAR X)) (:P (CDR X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (CAR X) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ENDP X)) (NOT (CAR X)) (AND (EQUAL (N (SERIAL-ADDER (CDR X) NIL T)) (+ 1 (N (CDR X)))) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X))))) (AND (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))) (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP X) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) NIL T)) (+ 1 (N (CDR X)))) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X)))) (AND (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))) (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)))). But simplification reduces this to T, using the :definitions N and SERIAL-ADDER, the :executable-counterparts of CAR, CDR, FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rule SERIAL-ADDER. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (CAR X) (AND (EQUAL (N (SERIAL-ADDER (CDR X) NIL T)) (+ 1 (N (CDR X)))) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X))))) (AND (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))) (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) NIL T)) (+ 1 (N (CDR X)))) (EQUAL (N (SERIAL-ADDER (CDR X) NIL NIL)) (N (CDR X)))) (AND (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))) (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CDR, CONS, CONSP, EQ, IF, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVIT\ Y and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER. Subgoal *1/1 (IMPLIES (ENDP X) (AND (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))) (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (AND (EQUAL (N (SERIAL-ADDER X NIL T)) (+ 1 (N X))) (EQUAL (N (SERIAL-ADDER X NIL NIL)) (N X)))). But simplification reduces this to T, using the :definitions N and SERIAL-ADDER and the :executable-counterparts of BINARY-+, CONS, CONSP, EQUAL and N. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM SERIAL-ADDER-SPECIAL-CASE ...) Rules: ((:DEFINITION ENDP) (:DEFINITION FULL-ADDER) (:DEFINITION MAJ) (:DEFINITION N) (:DEFINITION NOT) (:DEFINITION SERIAL-ADDER) (:DEFINITION SYNTAXP) (:DEFINITION XOR) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FULL-ADDER) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART MV-NTH) (:EXECUTABLE-COUNTERPART N) (:EXECUTABLE-COUNTERPART XOR) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DISTRIBUTIVITY) (:REWRITE FOLD-CONSTS-IN-+) (:TYPE-PRESCRIPTION SERIAL-ADDER)) Warnings: None Time: 0.37 seconds (prove: 0.32, print: 0.04, other: 0.01) SERIAL-ADDER-SPECIAL-CASE ACL2 !>(defthm serial-adder-correct (equal (n (serial-adder x y c)) (+ (n x) (n y) (if c 1 0)))) ACL2 Warning [Subsume] in ( DEFTHM SERIAL-ADDER-CORRECT ...): The newly proposed :REWRITE rule SERIAL-ADDER-CORRECT probably subsumes the previously added :REWRITE rules SERIAL-ADDER-SPECIAL-CASE and SERIAL- ADDER-SPECIAL-CASE, in the sense that SERIAL-ADDER-CORRECT will now probably be applied whenever the old rules would have been. This simplifies, using trivial observations, to the following two conjectures. Subgoal 2 (IMPLIES C (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) 1))). This simplifies, using the :rewrite rules COMMUTATIVITY-2-OF-+ and COMMUTATIVITY-OF-+, to Subgoal 2' (IMPLIES C (EQUAL (N (SERIAL-ADDER X Y C)) (+ 1 (N X) (N Y)))). Name the formula above *1. Subgoal 1 (IMPLIES (NOT C) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (N X) (N Y) 0))). This simplifies, using the :definition FIX, the :rewrite rules COMMUTATIVITY- OF-+ and UNICITY-OF-0 and the :type-prescription rule N, to Subgoal 1' (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (N X) (N Y))). Normally we would attempt to prove this formula by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (N Y), but modified to accommodate (N X) and (SERIAL-ADDER X Y C). If we let (:P C X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP Y)) (NOT (CAR Y)) (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) (CDR X) (CDR Y))) (:P C X Y)) (IMPLIES (AND (NOT (ENDP Y)) (CAR Y) (:P (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) (CDR X) (CDR Y))) (:P C X Y)) (IMPLIES (ENDP Y) (:P C X Y))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT Y) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variables C and X are being instantiated. When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ENDP Y)) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+, CONS, MV-NTH, XOR and ZP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+ and UNICITY- OF-0 and the :type-prescription rule N, to the following nine conjectures. Subgoal *1/3.9 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) C) (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (+ 1 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). This simplifies, using the :definitions FIX and N, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION- FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL- ADDER, to Subgoal *1/3.9' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)))) (CONSP X) C) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (+ (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ and XOR, the :executable-counterparts of CONS, MV-NTH and XOR, primitive type reasoning and the :rewrite rule DISTRIBUTIVITY. Subgoal *1/3.8 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X)) C) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX and N, the :executable- counterparts of EQUAL and FIX, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, LEFT-CANCELLATION-FOR- *, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/3.8' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X)) C) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ and XOR, the :executable-counterparts of CONS, MV-NTH, N and XOR, the :rewrite rules DEFAULT-CAR, DEFAULT-CDR and UNICITY-OF- 0 and the :type-prescription rule N. Subgoal *1/3.7 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (+ 0 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/3.7' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) NIL))) (FIX (+ (* 2 (N (CDR Y))) (* 2 (N (CDR X))))))). But simplification reduces this to T, using the :definitions FIX and N, the :executable-counterparts of FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/3.6 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 0 (* 2 (N (CDR Y))) 0))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/3.6' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT (CAR X)) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) NIL))) (FIX (+ (* 2 (N (CDR Y))) 0)))). This simplifies, using the :definitions FIX and N, the :executable- counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT- CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/3.6'' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definition FIX, the :executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/3.5 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (CAR X) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 1 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N and SYNTAXP, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/3.5' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (CAR X) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 2 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY- + and ZP, primitive type reasoning and the :rewrite rules CDR-CONS and DISTRIBUTIVITY. Subgoal *1/3.4 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (CAR X) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X))) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 (* 2 (N (CDR Y))) 0))). But simplification reduces this to T, using trivial observations. Subgoal *1/3.3 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX, N and SERIAL-ADDER, the :executable-counterparts of EQUAL, FIX, FULL-ADDER and MV-NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION-FOR-* and UNICITY- OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/3.3' (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definition FIX, the :executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/3.2 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (CAR X)) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/3.1 (IMPLIES (AND (CONSP Y) (NOT (CAR Y)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X) (NOT (CAR X))) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX, N and SERIAL-ADDER, the :executable-counterparts of FULL-ADDER and MV- NTH, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY-OF-0 and the :type- prescription rules N and SERIAL-ADDER. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP Y)) (CAR Y) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP Y) (CAR Y) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) (IF (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)) 1 0)))) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). This simplifies, using the :definitions FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY- +, CAR, CONSP, EQ, IF, XOR and ZP, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+, to the following nine conjectures. Subgoal *1/2.9 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) C) (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 1 1 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N and SYNTAXP, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/2.9' (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X) C) (EQUAL (+ 1 (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))) (+ 3 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY- *, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+. Subgoal *1/2.8 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X)) C) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C))) (+ 1 1 (* 2 (N (CDR Y))) 0))). But simplification reduces this to T, using trivial observations. Subgoal *1/2.7 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 1 0 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/2.7' (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (NOT C)) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 1 (FIX (+ (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, MV-NTH, N, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+, DISTRIBUTIVITY and FOLD-CONSTS-IN-+ and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/2.6 (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 0 (* 2 (N (CDR Y))) 0))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/2.6' (IMPLIES (AND (CONSP Y) (CAR Y) (CAR X) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X)) (NOT C)) (EQUAL (N (CONS T (SERIAL-ADDER NIL (CDR Y) NIL))) (+ 1 (FIX (+ (* 2 (N (CDR Y))) 0))))). But we reduce the conjecture to T, by case analysis. Subgoal *1/2.5 (IMPLIES (AND (CONSP Y) (CAR Y) (NOT (CAR X)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (CONSP X)) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ 1 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, N, SERIAL-ADDER and XOR, the :executable-counterparts of CONS, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DISTRIBUTIVITY and UNICITY- OF-0 and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/2.4 (IMPLIES (AND (CONSP Y) (CAR Y) (NOT (CAR X)) (NOT C) (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) NIL)))) (+ (N (CDR X)) (N (CDR Y)) 0)) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER X Y NIL)) (+ 1 (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, N, SERIAL- ADDER and XOR, the :executable-counterparts of CONS, EQUAL, FIX, MV- NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR, LEFT-CANCELLATION- FOR-*, LEFT-CANCELLATION-FOR-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL-ADDER, to Subgoal *1/2.4' (IMPLIES (AND (CONSP Y) (CAR Y) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (+ (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (N (SERIAL-ADDER NIL (CDR Y) NIL)) (N (CDR Y)))). But simplification reduces this to T, using the :definition FIX, the :executable-counterpart of N, the :rewrite rules DEFAULT-CDR and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/2.3 (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (NOT (CONSP X))) (EQUAL (N (CONS NIL (SERIAL-ADDER NIL (CDR Y) C))) (+ 2 (* 2 (N (CDR Y))) 0))). This simplifies, using the :definitions FIX and N, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and UNICITY-OF-0 and the :type-prescription rules N and SERIAL- ADDER, to Subgoal *1/2.3' (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (NOT (CONSP X))) (EQUAL (* 2 (N (SERIAL-ADDER NIL (CDR Y) C))) (+ 2 (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FIX, FULL- ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY- *, BINARY-+, N, XOR and ZP, primitive type reasoning, the :rewrite rules CDR-CONS, DEFAULT-CAR, DEFAULT-CDR, DISTRIBUTIVITY and UNICITY- OF-0 and the :type-prescription rule N. Subgoal *1/2.2 (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (CAR X)) (EQUAL (N (CONS T (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y)))) (+ 2 (* 2 (N (CDR Y))) 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N and SYNTAXP, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, COMMUTATIVITY- OF-+ and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/2.2' (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X) (CAR X)) (EQUAL (+ 1 (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) (CAR Y))))) (+ 3 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH, SYNTAXP and XOR, the :executable-counterparts of BINARY- *, BINARY-+, CAR, CONSP, EQ, IF and ZP, primitive type reasoning and the :rewrite rules CDR-CONS, DISTRIBUTIVITY and FOLD-CONSTS-IN-+. Subgoal *1/2.1 (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ (N (CDR X)) (N (CDR Y)) 1)) (CONSP X) (NOT (CAR X))) (EQUAL (N (CONS NIL (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 2 (* 2 (N (CDR Y))) (* 2 (N (CDR X)))))). This simplifies, using the :definition N, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+ and COMMUTATIVITY- OF-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/2.1' (IMPLIES (AND (CONSP Y) (CAR Y) C (EQUAL (N (SERIAL-ADDER (CDR X) (CDR Y) (MV-NTH 1 (FULL-ADDER (CAR X) (CAR Y) C)))) (+ 1 (N (CDR X)) (N (CDR Y)))) (CONSP X) (NOT (CAR X))) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) (CDR Y) C))) (+ 2 (* 2 (N (CDR X))) (* 2 (N (CDR Y)))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH and XOR, the :executable-counterparts of BINARY-*, BINARY- +, XOR and ZP, primitive type reasoning and the :rewrite rules CDR- CONS and DISTRIBUTIVITY. Subgoal *1/1 (IMPLIES (ENDP Y) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP Y)) (EQUAL (N (SERIAL-ADDER X Y C)) (+ (N X) (N Y) (IF C 1 0)))). This simplifies, using the :definitions FIX, FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER and XOR, the :executable-counterparts of BINARY-+, CONS, EQUAL, N and ZP, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, DEFAULT-CAR, DEFAULT-CDR and UNICITY-OF-0, to the following five conjectures. Subgoal *1/1.5 (IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C) (EQUAL (N (LIST C)) (+ 1 0))). By the :executable-counterpart of BINARY-+ we reduce the conjecture to Subgoal *1/1.5' (IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X)) C) (EQUAL (N (LIST C)) 1)). But simplification reduces this to T, using the :definition N, the :executable-counterparts of BINARY-*, BINARY-+, EQUAL and N, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1/1.4 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) C (CAR X)) (EQUAL (N (CONS (XOR (CAR X) T) (SERIAL-ADDER (CDR X) NIL C))) (+ 1 1 (* 2 (N (CDR X)))))). This simplifies, using the :definitions N, SYNTAXP and XOR, the :executable- counterparts of BINARY-+, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL-ADDER, to Subgoal *1/1.4' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) C (CAR X)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X) NIL C))) (+ 2 (* 2 (N (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. This produces the following goal. Subgoal *1/1.4'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (CONSP Y)) C X1) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/1.4''' (IMPLIES (AND (NOT (CONSP Y)) C X1) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). This simplifies, using trivial observations, to Subgoal *1/1.4'4' (IMPLIES (AND (NOT (CONSP Y)) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). We suspect that the term (NOT (CONSP Y)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/1.4'5' (IMPLIES C (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). Name the formula above *1.1. Subgoal *1/1.3 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (CAR X)) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (+ 0 1 (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/1.3' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (CAR X)) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (FIX (+ 1 (* 2 (N (CDR X))))))). But simplification reduces this to T, using the :definitions FIX, N and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR- CONS and SERIAL-ADDER-SPECIAL-CASE and the :type-prescription rules N and SERIAL-ADDER. Subgoal *1/1.2 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) C (NOT (CAR X))) (EQUAL (N (CONS (XOR (CAR X) T) (SERIAL-ADDER (CDR X) NIL NIL))) (+ 1 (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definition N, the :executable-counterpart of XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and SERIAL-ADDER-SPECIAL-CASE and the :type- prescription rule SERIAL-ADDER. Subgoal *1/1.1 (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (NOT (CAR X))) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (+ 0 (* 2 (N (CDR X)))))). By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to Subgoal *1/1.1' (IMPLIES (AND (NOT (CONSP Y)) (CONSP X) (NOT C) (NOT (CAR X))) (EQUAL (N (CONS (XOR (CAR X) NIL) (SERIAL-ADDER (CDR X) NIL NIL))) (FIX (* 2 (N (CDR X)))))). But simplification reduces this to T, using the :definitions FIX and N, the :executable-counterpart of XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and SERIAL-ADDER-SPECIAL-CASE and the :type-prescription rules N and SERIAL-ADDER. So we now return to *1.1, which is (IMPLIES C (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (N X2). If we let (:P C X2) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X2)) (NOT (CAR X2)) (:P C (CDR X2))) (:P C X2)) (IMPLIES (AND (NOT (ENDP X2)) (CAR X2) (:P C (CDR X2))) (:P C X2)) (IMPLIES (ENDP X2) (:P C X2))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT X2) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1.1/3 (IMPLIES (AND (NOT (ENDP X2)) (NOT (CAR X2)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (CONSP X2) (NOT (CAR X2)) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, CAR, CDR, CONS, CONSP, EQ, IF, MV-NTH and XOR, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVITY, FOLD-CONSTS-IN-* and SERIAL-ADDER-SPECIAL-CASE and the :type-prescription rule SERIAL-ADDER. Subgoal *1.1/2 (IMPLIES (AND (NOT (ENDP X2)) (CAR X2) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (CONSP X2) (CAR X2) (EQUAL (* 2 (N (SERIAL-ADDER (CDR X2) NIL C))) (+ 2 (* 2 (N (CDR X2))))) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). But simplification reduces this to T, using the :definitions FULL-ADDER, MAJ, MV-NTH, N, SERIAL-ADDER, SYNTAXP and XOR, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CDR, CONSP, EQ, IF and ZP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, DISTRIBUTIVITY, FOLD- CONSTS-IN-* and FOLD-CONSTS-IN-+ and the :type-prescription rule SERIAL- ADDER. Subgoal *1.1/1 (IMPLIES (AND (ENDP X2) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (AND (NOT (CONSP X2)) C) (EQUAL (* 2 (N (SERIAL-ADDER X2 NIL C))) (+ 2 (* 2 (N X2))))). But simplification reduces this to T, using the :definitions N and SERIAL-ADDER, the :executable-counterparts of BINARY-*, BINARY-+, CONSP, EQUAL and N, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proofs of *1.1 and *1. Q.E.D. Summary Form: ( DEFTHM SERIAL-ADDER-CORRECT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION FIX) (:DEFINITION FULL-ADDER) (:DEFINITION MAJ) (:DEFINITION MV-NTH) (:DEFINITION N) (:DEFINITION NOT) (:DEFINITION SERIAL-ADDER) (:DEFINITION SYNTAXP) (:DEFINITION XOR) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART FULL-ADDER) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART MV-NTH) (:EXECUTABLE-COUNTERPART N) (:EXECUTABLE-COUNTERPART XOR) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DEFAULT-CAR) (:REWRITE DEFAULT-CDR) (:REWRITE DISTRIBUTIVITY) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE LEFT-CANCELLATION-FOR-*) (:REWRITE LEFT-CANCELLATION-FOR-+) (:REWRITE SERIAL-ADDER-SPECIAL-CASE) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION N) (:TYPE-PRESCRIPTION SERIAL-ADDER)) Warnings: Subsume Time: 2.19 seconds (prove: 1.83, print: 0.33, other: 0.03) SERIAL-ADDER-CORRECT ACL2 !>(defun multiplier (x y p) (if (endp x) p (multiplier (cdr x) (cons nil y) (if (car x) (serial-adder y p nil) p)))) The admission of MULTIPLIER is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). We observe that the type of MULTIPLIER is described by the theorem (OR (AND (CONSP (MULTIPLIER X Y P)) (TRUE-LISTP (MULTIPLIER X Y P))) (EQUAL (MULTIPLIER X Y P) P)). We used the :type-prescription rule SERIAL-ADDER. Summary Form: ( DEFUN MULTIPLIER ...) Rules: ((:TYPE-PRESCRIPTION SERIAL-ADDER)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) MULTIPLIER ACL2 !>(n '(nil nil nil t nil t t t t t)) 1000 ACL2 !>(n (multiplier '(nil nil nil t nil t t t t t) '(nil nil nil t nil t t t t t) nil)) 1000000 ACL2 !>(defthm multiplier-correct (equal (n (multiplier x y p)) (+ (* (n x) (n y)) (n p)))) This simplifies, using the :rewrite rule COMMUTATIVITY-OF-+, to Goal' (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y)))). Name the formula above *1. Perhaps we can prove *1 by induction. Four induction schemes are suggested by this conjecture. These merge into three derived induction schemes. However, two of these are flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (N X), but modified to accommodate (MULTIPLIER X Y P). If we let (:P P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (CAR X)) (:P (IF (CAR X) (SERIAL-ADDER Y P NIL) P) (CDR X) (CONS NIL Y))) (:P P X Y)) (IMPLIES (AND (NOT (ENDP X)) (CAR X) (:P (IF (CAR X) (SERIAL-ADDER Y P NIL) P) (CDR X) (CONS NIL Y))) (:P P X Y)) (IMPLIES (ENDP X) (:P P X Y))). This induction is justified by the same argument used to admit N, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variables Y and P are being instantiated. When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ENDP X)) (NOT (CAR X)) (EQUAL (N (MULTIPLIER (CDR X) (CONS NIL Y) (IF (CAR X) (SERIAL-ADDER Y P NIL) P))) (+ (N (IF (CAR X) (SERIAL-ADDER Y P NIL) P)) (* (N (CDR X)) (N (CONS NIL Y)))))) (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP X) (NOT (CAR X)) (EQUAL (N (MULTIPLIER (CDR X) (CONS NIL Y) (IF (CAR X) (SERIAL-ADDER Y P NIL) P))) (+ (N (IF (CAR X) (SERIAL-ADDER Y P NIL) P)) (* (N (CDR X)) (N (CONS NIL Y)))))) (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y))))). But simplification reduces this to T, using the :definitions MULTIPLIER and N, primitive type reasoning and the :rewrite rules CAR-CONS, CDR- CONS, COMMUTATIVITY-2-OF-* and COMMUTATIVITY-OF-*. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (CAR X) (EQUAL (N (MULTIPLIER (CDR X) (CONS NIL Y) (IF (CAR X) (SERIAL-ADDER Y P NIL) P))) (+ (N (IF (CAR X) (SERIAL-ADDER Y P NIL) P)) (* (N (CDR X)) (N (CONS NIL Y)))))) (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (CAR X) (EQUAL (N (MULTIPLIER (CDR X) (CONS NIL Y) (IF (CAR X) (SERIAL-ADDER Y P NIL) P))) (+ (N (IF (CAR X) (SERIAL-ADDER Y P NIL) P)) (* (N (CDR X)) (N (CONS NIL Y)))))) (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y))))). But simplification reduces this to T, using the :definitions FIX, MULTIPLIER and N, primitive type reasoning, the :rewrite rules ASSOCIATIVITY-OF- +, CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-*, COMMUTATIVITY-OF-*, COMMUTATIVITY\ -OF-+, DISTRIBUTIVITY, SERIAL-ADDER-CORRECT, UNICITY-OF-0 and UNICITY- OF-1 and the :type-prescription rule N. Subgoal *1/1 (IMPLIES (ENDP X) (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (EQUAL (N (MULTIPLIER X Y P)) (+ (N P) (* (N X) (N Y))))). But simplification reduces this to T, using the :definitions FIX, MULTIPLIER and N, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF- +, TIMES-ZERO and UNICITY-OF-0 and the :type-prescription rule N. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM MULTIPLIER-CORRECT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION FIX) (:DEFINITION MULTIPLIER) (:DEFINITION N) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE SERIAL-ADDER-CORRECT) (:REWRITE TIMES-ZERO) (:REWRITE UNICITY-OF-0) (:REWRITE UNICITY-OF-1) (:TYPE-PRESCRIPTION N)) Warnings: None Time: 0.19 seconds (prove: 0.11, print: 0.06, other: 0.02) MULTIPLIER-CORRECT ACL2 !>(defun adder-net (a b c i) (cond ((endp a) `((,i ,c *))) (t `((,i (xor ,(car b) ,c)) (,(+ i 1) (xor ,(car a) ,i) *) (,(+ i 2) (maj ,(car a) ,(car b) ,c)) ,@(adder-net (cdr a) (cdr b) (+ i 2) (+ i 3)))))) The admission of ADDER-NET is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT A). We observe that the type of ADDER- NET is described by the theorem (CONSP (ADDER-NET A B C I)). We used primitive type reasoning. Summary Form: ( DEFUN ADDER-NET ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ADDER-NET ACL2 !>(adder-net '(a0 a1 a2) '(b0 b1 b2) 'c 0) ((0 (XOR B0 C)) (1 (XOR A0 0) *) (2 (MAJ A0 B0 C)) (3 (XOR B1 2)) (4 (XOR A1 3) *) (5 (MAJ A1 B1 2)) (6 (XOR B2 5)) (7 (XOR A2 6) *) (8 (MAJ A2 B2 5)) (9 8 *)) ACL2 !>(defun net-val (netlist alist) (cond ((endp netlist) nil) (t (let* ((wire-name (car (car netlist))) (gate-expr (cadr (car netlist))) (output-flag (caddr (car netlist))) (val (evaluate-gate gate-expr alist)) (ans (net-val (cdr netlist) (bind wire-name val alist)))) (cond ((eq output-flag '*) (cons val ans)) (t ans)))))) The admission of NET-VAL is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT NETLIST). We observe that the type of NET-VAL is described by the theorem (TRUE-LISTP (NET-VAL NETLIST ALIST)). We used primitive type reasoning. Summary Form: ( DEFUN NET-VAL ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) NET-VAL ACL2 !>(net-val '((0 (xor a1 b1)) (1 (xor c 0) *)) '((a1 . t) (b1 . nil) (c . nil))) (T) ACL2 !>(defthm true-listp-adder-net (true-listp (adder-net a b c i))) Name the formula above *1. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (ADDER-NET A B C I). If we let (:P A B C I) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) (CDR B) (+ I 2) (+ I 3))) (:P A B C I)) (IMPLIES (ENDP A) (:P A B C I))). This induction is justified by the same argument used to admit ADDER- NET, namely, the measure (ACL2-COUNT A) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variables B, C and I are being instantiated. When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP A)) (TRUE-LISTP (ADDER-NET (CDR A) (CDR B) (+ I 2) (+ I 3)))) (TRUE-LISTP (ADDER-NET A B C I))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP A) (TRUE-LISTP (ADDER-NET (CDR A) (CDR B) (+ I 2) (+ I 3)))) (TRUE-LISTP (ADDER-NET A B C I))). But simplification reduces this to T, using the :definition ADDER-NET, primitive type reasoning, the :rewrite rules APPEND-RIGHT-ID and COMMUTATIVITY\ -OF-+ and the :type-prescription rule ADDER-NET. Subgoal *1/1 (IMPLIES (ENDP A) (TRUE-LISTP (ADDER-NET A B C I))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (TRUE-LISTP (ADDER-NET A B C I))). But simplification reduces this to T, using the :definition ADDER-NET and primitive type reasoning. That completes the proof of *1. Q.E.D. The storage of TRUE-LISTP-ADDER-NET depends upon the :type-prescription rule TRUE-LISTP. Summary Form: ( DEFTHM TRUE-LISTP-ADDER-NET ...) Rules: ((:DEFINITION ADDER-NET) (:DEFINITION ENDP) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE APPEND-RIGHT-ID) (:REWRITE COMMUTATIVITY-OF-+) (:TYPE-PRESCRIPTION ADDER-NET) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.05 seconds (prove: 0.01, print: 0.02, other: 0.02) TRUE-LISTP-ADDER-NET ACL2 !>(defthm adder-net-is-serial-adder (implies (and (symbol-listp a) (symbol-listp b) (equal (len a) (len b)) (integerp i) (or (symbolp c) (and (integerp c) (< c i)))) (equal (net-val (adder-net a b c i) alist) (serial-adder (lookup-all a alist) (lookup-all b alist) (lookup c alist)))) :hints (("Goal" :induct (net-val-hint a b c i alist) :in-theory (disable xor maj)))) [Note: A hint was supplied for our processing of the goal above. Thanks!] Name the formula above *1. We have been told to use induction. One induction scheme is suggested by the induction hint. We will induct according to a scheme suggested by (NET-VAL-HINT A B C I ALIST). If we let (:P A ALIST B C I) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST) (CDR B) (+ I 2) (+ I 3))) (:P A ALIST B C I)) (IMPLIES (ENDP A) (:P A ALIST B C I))). This induction is justified by the same argument used to admit NET- VAL-HINT, namely, the measure (ACL2-COUNT A) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variables B, C, I and ALIST are being instantiated. When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP A)) (IMPLIES (AND (SYMBOL-LISTP (CDR A)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP (+ I 3)) (OR (SYMBOLP (+ I 2)) (AND (INTEGERP (+ I 2)) (< (+ I 2) (+ I 3))))) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ I 2) (+ I 3)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (LOOKUP-ALL (CDR B) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (LOOKUP (+ I 2) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)))))) (IMPLIES (AND (SYMBOL-LISTP A) (SYMBOL-LISTP B) (EQUAL (LEN A) (LEN B)) (INTEGERP I) (OR (SYMBOLP C) (AND (INTEGERP C) (< C I)))) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (SERIAL-ADDER (LOOKUP-ALL A ALIST) (LOOKUP-ALL B ALIST) (LOOKUP C ALIST))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP A) (OR (NOT (AND (SYMBOL-LISTP (CDR A)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP (+ I 3)) (OR (SYMBOLP (+ I 2)) (AND (INTEGERP (+ I 2)) (< (+ I 2) (+ I 3)))))) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ I 2) (+ I 3)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (LOOKUP-ALL (CDR B) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (LOOKUP (+ I 2) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST))))) (SYMBOL-LISTP A) (SYMBOL-LISTP B) (EQUAL (LEN A) (LEN B)) (INTEGERP I) (OR (SYMBOLP C) (AND (INTEGERP C) (< C I)))) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (SERIAL-ADDER (LOOKUP-ALL A ALIST) (LOOKUP-ALL B ALIST) (LOOKUP C ALIST)))). This simplifies, using the :definitions FIX, FULL-ADDER, LEN, LOOKUP, LOOKUP-ALL, MV-NTH, SERIAL-ADDER and SYMBOL-LISTP, the :executable- counterparts of BINARY-+, CAR, CDR, CONSP, LEN, SYMBOL-LISTP and ZP, primitive type reasoning, the :forward-chaining rule SYMBOL-LISTP-FORWARD- TO-TRUE-LISTP, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- OF-+ and LEFT-CANCELLATION-FOR-+ and the :type-prescription rules LEN, LOOKUP-ALL and SYMBOL-LISTP, to the following four conjectures. Subgoal *1/2.4 (IMPLIES (AND (CONSP A) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ 2 I) (+ 3 I)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (LOOKUP-ALL (CDR B) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (SYMBOLP (CAR A)) (SYMBOL-LISTP (CDR A)) (CONSP B) (SYMBOLP (CAR B)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP I) (SYMBOLP C)) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (CONS (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))))). But simplification reduces this to T, using the :definitions ADDER- NET, BIND, EVALUATE-GATE, LOOKUP and NET-VAL, the :executable-counterparts of CAR and EQUAL, primitive type reasoning, the :rewrite rules APPEND- RIGHT-ID, CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, INPUT-LOOKUP-ALL- NOT-CHANGED and TRUE-LISTP-ADDER-NET and the :type-prescription rule SYMBOL-LISTP. Subgoal *1/2.3 (IMPLIES (AND (CONSP A) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ 2 I) (+ 3 I)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (LOOKUP-ALL (CDR B) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (SYMBOLP (CAR A)) (SYMBOL-LISTP (CDR A)) (CONSP B) (SYMBOLP (CAR B)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP I) (INTEGERP C) (< C I)) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (CONS (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))))). This simplifies, using the :definitions ADDER-NET, BIND, EVALUATE-GATE, LOOKUP and NET-VAL, the :executable-counterparts of CAR and EQUAL, primitive type reasoning, the :rewrite rules APPEND-RIGHT-ID, CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-+, CONS-EQUAL, INPUT-LOOKUP-ALL-NOT-CHANGED and TRUE-LISTP-ADDER-NET and the :type-prescription rule SYMBOL-LISTP, to the following two conjectures. Subgoal *1/2.3.2 (IMPLIES (AND (CONSP A) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ 2 I) (+ 3 I)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (SYMBOLP (CAR A)) (SYMBOL-LISTP (CDR A)) (CONSP B) (SYMBOLP (CAR B)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP I) (INTEGERP C) (< C I) (EQUAL C (+ 1 I))) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ 2 I) (+ 3 I)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Subgoal *1/2.3.1 (IMPLIES (AND (CONSP A) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ 2 I) (+ 3 I)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (SYMBOLP (CAR A)) (SYMBOL-LISTP (CDR A)) (CONSP B) (SYMBOLP (CAR B)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP I) (INTEGERP C) (< C I) (NOT (EQUAL C (+ 1 I))) (EQUAL C I)) (EQUAL (NET-VAL (ADDER-NET (CDR A) (CDR B) (+ 2 I) (+ 3 I)) (LIST* (CONS (+ 2 I) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS (+ 1 I) (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))) (CONS I (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) ALIST)) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.2 (IMPLIES (AND (CONSP A) (<= (+ 3 I) (+ 2 I)) (SYMBOLP (CAR A)) (SYMBOL-LISTP (CDR A)) (CONSP B) (SYMBOLP (CAR B)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP I) (SYMBOLP C)) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (CONS (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.1 (IMPLIES (AND (CONSP A) (<= (+ 3 I) (+ 2 I)) (SYMBOLP (CAR A)) (SYMBOL-LISTP (CDR A)) (CONSP B) (SYMBOLP (CAR B)) (SYMBOL-LISTP (CDR B)) (EQUAL (LEN (CDR A)) (LEN (CDR B))) (INTEGERP I) (INTEGERP C) (< C I)) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (CONS (XOR (LOOKUP (CAR A) ALIST) (XOR (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST))) (SERIAL-ADDER (LOOKUP-ALL (CDR A) ALIST) (LOOKUP-ALL (CDR B) ALIST) (MAJ (LOOKUP (CAR A) ALIST) (LOOKUP (CAR B) ALIST) (LOOKUP C ALIST)))))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/1 (IMPLIES (ENDP A) (IMPLIES (AND (SYMBOL-LISTP A) (SYMBOL-LISTP B) (EQUAL (LEN A) (LEN B)) (INTEGERP I) (OR (SYMBOLP C) (AND (INTEGERP C) (< C I)))) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (SERIAL-ADDER (LOOKUP-ALL A ALIST) (LOOKUP-ALL B ALIST) (LOOKUP C ALIST))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (AND (NOT (CONSP A)) (SYMBOL-LISTP A) (SYMBOL-LISTP B) (EQUAL (LEN A) (LEN B)) (INTEGERP I) (OR (SYMBOLP C) (AND (INTEGERP C) (< C I)))) (EQUAL (NET-VAL (ADDER-NET A B C I) ALIST) (SERIAL-ADDER (LOOKUP-ALL A ALIST) (LOOKUP-ALL B ALIST) (LOOKUP C ALIST)))). But simplification reduces this to T, using the :definitions ADDER- NET, ATOM, BIND, EVALUATE-GATE, LOOKUP-ALL, NET-VAL, SERIAL-ADDER and SYMBOL-LISTP, the :executable-counterparts of CAR, CONSP, EQUAL and LEN, primitive type reasoning, the :forward-chaining rule SYMBOL-LISTP- FORWARD-TO-TRUE-LISTP, the :rewrite rules CAR-CONS, CDR-CONS and EQUAL- LEN-0 and the :type-prescription rule SYMBOL-LISTP. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM ADDER-NET-IS-SERIAL-ADDER ...) Rules: ((:DEFINITION ADDER-NET) (:DEFINITION ATOM) (:DEFINITION BIND) (:DEFINITION ENDP) (:DEFINITION EVALUATE-GATE) (:DEFINITION FIX) (:DEFINITION FULL-ADDER) (:DEFINITION IMPLIES) (:DEFINITION LEN) (:DEFINITION LOOKUP) (:DEFINITION LOOKUP-ALL) (:DEFINITION MV-NTH) (:DEFINITION NET-VAL) (:DEFINITION NOT) (:DEFINITION SERIAL-ADDER) (:DEFINITION SYMBOL-LISTP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART SYMBOL-LISTP) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP) (:REWRITE APPEND-RIGHT-ID) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE CONS-EQUAL) (:REWRITE EQUAL-LEN-0) (:REWRITE INPUT-LOOKUP-ALL-NOT-CHANGED) (:REWRITE LEFT-CANCELLATION-FOR-+) (:REWRITE TRUE-LISTP-ADDER-NET) (:TYPE-PRESCRIPTION LEN) (:TYPE-PRESCRIPTION LOOKUP-ALL) (:TYPE-PRESCRIPTION SYMBOL-LISTP)) Warnings: None Time: 5.47 seconds (prove: 5.28, print: 0.13, other: 0.06) ADDER-NET-IS-SERIAL-ADDER ACL2 !>(defthm adder-net-is-correct (implies (and (symbol-listp a) (symbol-listp b) (equal (len a) (len b)) (integerp i) (or (symbolp c) (and (integerp c) (< c i)))) (equal (n (net-val (adder-net a b c i) alist)) (+ (n (lookup-all a alist)) (n (lookup-all b alist)) (if (lookup c alist) 1 0))))) But simplification reduces this to T, using primitive type reasoning, the :rewrite rules ADDER-NET-IS-SERIAL-ADDER and SERIAL-ADDER-CORRECT and the :type-prescription rule SYMBOL-LISTP. Q.E.D. Summary Form: ( DEFTHM ADDER-NET-IS-CORRECT ...) Rules: ((:DEFINITION IMPLIES) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ADDER-NET-IS-SERIAL-ADDER) (:REWRITE SERIAL-ADDER-CORRECT) (:TYPE-PRESCRIPTION SYMBOL-LISTP)) Warnings: None Time: 0.13 seconds (prove: 0.12, print: 0.00, other: 0.01) ADDER-NET-IS-CORRECT ACL2 !>(adder-net '(a00 a01 a02 a03 a04 a05 a06 a07 a08 a09 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a35 a36 a37 a38 a39 a40 a41 a42 a43 a44 a45 a46 a47 a48 a49 a50 a51 a52 a53 a54 a55 a56 a57 a58 a59 a60 a61 a62 a63 a64 a65 a66 a67 a68 a69 a70 a71 a72 a73 a74 a75 a76 a77 a78 a79 a80 a81 a82 a83 a84 a85 a86 a87 a88 a89 a90 a91 a92 a93 a94 a95 a96 a97 a98 a99) '(b00 b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 b32 b33 b34 b35 b36 b37 b38 b39 b40 b41 b42 b43 b44 b45 b46 b47 b48 b49 b50 b51 b52 b53 b54 b55 b56 b57 b58 b59 b60 b61 b62 b63 b64 b65 b66 b67 b68 b69 b70 b71 b72 b73 b74 b75 b76 b77 b78 b79 b80 b81 b82 b83 b84 b85 b86 b87 b88 b89 b90 b91 b92 b93 b94 b95 b96 b97 b98 b99) 'c 0) ((0 (XOR B00 C)) (1 (XOR A00 0) *) (2 (MAJ A00 B00 C)) (3 (XOR B01 2)) (4 (XOR A01 3) *) (5 (MAJ A01 B01 2)) (6 (XOR B02 5)) (7 (XOR A02 6) *) (8 (MAJ A02 B02 5)) (9 (XOR B03 8)) (10 (XOR A03 9) *) (11 (MAJ A03 B03 8)) (12 (XOR B04 11)) (13 (XOR A04 12) *) (14 (MAJ A04 B04 11)) (15 (XOR B05 14)) (16 (XOR A05 15) *) (17 (MAJ A05 B05 14)) (18 (XOR B06 17)) (19 (XOR A06 18) *) (20 (MAJ A06 B06 17)) (21 (XOR B07 20)) (22 (XOR A07 21) *) (23 (MAJ A07 B07 20)) (24 (XOR B08 23)) (25 (XOR A08 24) *) (26 (MAJ A08 B08 23)) (27 (XOR B09 26)) (28 (XOR A09 27) *) (29 (MAJ A09 B09 26)) (30 (XOR B10 29)) (31 (XOR A10 30) *) (32 (MAJ A10 B10 29)) (33 (XOR B11 32)) (34 (XOR A11 33) *) (35 (MAJ A11 B11 32)) (36 (XOR B12 35)) (37 (XOR A12 36) *) (38 (MAJ A12 B12 35)) (39 (XOR B13 38)) (40 (XOR A13 39) *) (41 (MAJ A13 B13 38)) (42 (XOR B14 41)) (43 (XOR A14 42) *) (44 (MAJ A14 B14 41)) (45 (XOR B15 44)) (46 (XOR A15 45) *) (47 (MAJ A15 B15 44)) (48 (XOR B16 47)) (49 (XOR A16 48) *) (50 (MAJ A16 B16 47)) (51 (XOR B17 50)) (52 (XOR A17 51) *) (53 (MAJ A17 B17 50)) (54 (XOR B18 53)) (55 (XOR A18 54) *) (56 (MAJ A18 B18 53)) (57 (XOR B19 56)) (58 (XOR A19 57) *) (59 (MAJ A19 B19 56)) (60 (XOR B20 59)) (61 (XOR A20 60) *) (62 (MAJ A20 B20 59)) (63 (XOR B21 62)) (64 (XOR A21 63) *) (65 (MAJ A21 B21 62)) (66 (XOR B22 65)) (67 (XOR A22 66) *) (68 (MAJ A22 B22 65)) (69 (XOR B23 68)) (70 (XOR A23 69) *) (71 (MAJ A23 B23 68)) (72 (XOR B24 71)) (73 (XOR A24 72) *) (74 (MAJ A24 B24 71)) (75 (XOR B25 74)) (76 (XOR A25 75) *) (77 (MAJ A25 B25 74)) (78 (XOR B26 77)) (79 (XOR A26 78) *) (80 (MAJ A26 B26 77)) (81 (XOR B27 80)) (82 (XOR A27 81) *) (83 (MAJ A27 B27 80)) (84 (XOR B28 83)) (85 (XOR A28 84) *) (86 (MAJ A28 B28 83)) (87 (XOR B29 86)) (88 (XOR A29 87) *) (89 (MAJ A29 B29 86)) (90 (XOR B30 89)) (91 (XOR A30 90) *) (92 (MAJ A30 B30 89)) (93 (XOR B31 92)) (94 (XOR A31 93) *) (95 (MAJ A31 B31 92)) (96 (XOR B32 95)) (97 (XOR A32 96) *) (98 (MAJ A32 B32 95)) (99 (XOR B33 98)) (100 (XOR A33 99) *) (101 (MAJ A33 B33 98)) (102 (XOR B34 101)) (103 (XOR A34 102) *) (104 (MAJ A34 B34 101)) (105 (XOR B35 104)) (106 (XOR A35 105) *) (107 (MAJ A35 B35 104)) (108 (XOR B36 107)) (109 (XOR A36 108) *) (110 (MAJ A36 B36 107)) (111 (XOR B37 110)) (112 (XOR A37 111) *) (113 (MAJ A37 B37 110)) (114 (XOR B38 113)) (115 (XOR A38 114) *) (116 (MAJ A38 B38 113)) (117 (XOR B39 116)) (118 (XOR A39 117) *) (119 (MAJ A39 B39 116)) (120 (XOR B40 119)) (121 (XOR A40 120) *) (122 (MAJ A40 B40 119)) (123 (XOR B41 122)) (124 (XOR A41 123) *) (125 (MAJ A41 B41 122)) (126 (XOR B42 125)) (127 (XOR A42 126) *) (128 (MAJ A42 B42 125)) (129 (XOR B43 128)) (130 (XOR A43 129) *) (131 (MAJ A43 B43 128)) (132 (XOR B44 131)) (133 (XOR A44 132) *) (134 (MAJ A44 B44 131)) (135 (XOR B45 134)) (136 (XOR A45 135) *) (137 (MAJ A45 B45 134)) (138 (XOR B46 137)) (139 (XOR A46 138) *) (140 (MAJ A46 B46 137)) (141 (XOR B47 140)) (142 (XOR A47 141) *) (143 (MAJ A47 B47 140)) (144 (XOR B48 143)) (145 (XOR A48 144) *) (146 (MAJ A48 B48 143)) (147 (XOR B49 146)) (148 (XOR A49 147) *) (149 (MAJ A49 B49 146)) (150 (XOR B50 149)) (151 (XOR A50 150) *) (152 (MAJ A50 B50 149)) (153 (XOR B51 152)) (154 (XOR A51 153) *) (155 (MAJ A51 B51 152)) (156 (XOR B52 155)) (157 (XOR A52 156) *) (158 (MAJ A52 B52 155)) (159 (XOR B53 158)) (160 (XOR A53 159) *) (161 (MAJ A53 B53 158)) (162 (XOR B54 161)) (163 (XOR A54 162) *) (164 (MAJ A54 B54 161)) (165 (XOR B55 164)) (166 (XOR A55 165) *) (167 (MAJ A55 B55 164)) (168 (XOR B56 167)) (169 (XOR A56 168) *) (170 (MAJ A56 B56 167)) (171 (XOR B57 170)) (172 (XOR A57 171) *) (173 (MAJ A57 B57 170)) (174 (XOR B58 173)) (175 (XOR A58 174) *) (176 (MAJ A58 B58 173)) (177 (XOR B59 176)) (178 (XOR A59 177) *) (179 (MAJ A59 B59 176)) (180 (XOR B60 179)) (181 (XOR A60 180) *) (182 (MAJ A60 B60 179)) (183 (XOR B61 182)) (184 (XOR A61 183) *) (185 (MAJ A61 B61 182)) (186 (XOR B62 185)) (187 (XOR A62 186) *) (188 (MAJ A62 B62 185)) (189 (XOR B63 188)) (190 (XOR A63 189) *) (191 (MAJ A63 B63 188)) (192 (XOR B64 191)) (193 (XOR A64 192) *) (194 (MAJ A64 B64 191)) (195 (XOR B65 194)) (196 (XOR A65 195) *) (197 (MAJ A65 B65 194)) (198 (XOR B66 197)) (199 (XOR A66 198) *) (200 (MAJ A66 B66 197)) (201 (XOR B67 200)) (202 (XOR A67 201) *) (203 (MAJ A67 B67 200)) (204 (XOR B68 203)) (205 (XOR A68 204) *) (206 (MAJ A68 B68 203)) (207 (XOR B69 206)) (208 (XOR A69 207) *) (209 (MAJ A69 B69 206)) (210 (XOR B70 209)) (211 (XOR A70 210) *) (212 (MAJ A70 B70 209)) (213 (XOR B71 212)) (214 (XOR A71 213) *) (215 (MAJ A71 B71 212)) (216 (XOR B72 215)) (217 (XOR A72 216) *) (218 (MAJ A72 B72 215)) (219 (XOR B73 218)) (220 (XOR A73 219) *) (221 (MAJ A73 B73 218)) (222 (XOR B74 221)) (223 (XOR A74 222) *) (224 (MAJ A74 B74 221)) (225 (XOR B75 224)) (226 (XOR A75 225) *) (227 (MAJ A75 B75 224)) (228 (XOR B76 227)) (229 (XOR A76 228) *) (230 (MAJ A76 B76 227)) (231 (XOR B77 230)) (232 (XOR A77 231) *) (233 (MAJ A77 B77 230)) (234 (XOR B78 233)) (235 (XOR A78 234) *) (236 (MAJ A78 B78 233)) (237 (XOR B79 236)) (238 (XOR A79 237) *) (239 (MAJ A79 B79 236)) (240 (XOR B80 239)) (241 (XOR A80 240) *) (242 (MAJ A80 B80 239)) (243 (XOR B81 242)) (244 (XOR A81 243) *) (245 (MAJ A81 B81 242)) (246 (XOR B82 245)) (247 (XOR A82 246) *) (248 (MAJ A82 B82 245)) (249 (XOR B83 248)) (250 (XOR A83 249) *) (251 (MAJ A83 B83 248)) (252 (XOR B84 251)) (253 (XOR A84 252) *) (254 (MAJ A84 B84 251)) (255 (XOR B85 254)) (256 (XOR A85 255) *) (257 (MAJ A85 B85 254)) (258 (XOR B86 257)) (259 (XOR A86 258) *) (260 (MAJ A86 B86 257)) (261 (XOR B87 260)) (262 (XOR A87 261) *) (263 (MAJ A87 B87 260)) (264 (XOR B88 263)) (265 (XOR A88 264) *) (266 (MAJ A88 B88 263)) (267 (XOR B89 266)) (268 (XOR A89 267) *) (269 (MAJ A89 B89 266)) (270 (XOR B90 269)) (271 (XOR A90 270) *) (272 (MAJ A90 B90 269)) (273 (XOR B91 272)) (274 (XOR A91 273) *) (275 (MAJ A91 B91 272)) (276 (XOR B92 275)) (277 (XOR A92 276) *) (278 (MAJ A92 B92 275)) (279 (XOR B93 278)) (280 (XOR A93 279) *) (281 (MAJ A93 B93 278)) (282 (XOR B94 281)) (283 (XOR A94 282) *) (284 (MAJ A94 B94 281)) (285 (XOR B95 284)) (286 (XOR A95 285) *) (287 (MAJ A95 B95 284)) (288 (XOR B96 287)) (289 (XOR A96 288) *) (290 (MAJ A96 B96 287)) (291 (XOR B97 290)) (292 (XOR A97 291) *) (293 (MAJ A97 B97 290)) (294 (XOR B98 293)) (295 (XOR A98 294) *) (296 (MAJ A98 B98 293)) (297 (XOR B99 296)) (298 (XOR A99 297) *) (299 (MAJ A99 B99 296)) (300 299 *)) ACL2 !>(defun execute (instr alist stk) (let ((op (car instr))) (cond ((equal op 'load) (push-stack (lookup (cadr instr) alist) stk)) ((equal op 'push) (push-stack (cadr instr) stk)) ((equal op 'dup) (push-stack (top-stack stk) stk)) ((equal op 'add) (push-stack (+ (top-stack (pop-stack stk)) (top-stack stk)) (pop-stack (pop-stack stk)))) ((equal op 'mul) (push-stack (* (top-stack (pop-stack stk)) (top-stack stk)) (pop-stack (pop-stack stk)))) (t stk)))) Since EXECUTE is non-recursive, its admission is trivial. We observe that the type of EXECUTE is described by the theorem (OR (CONSP (EXECUTE INSTR ALIST STK)) (EQUAL (EXECUTE INSTR ALIST STK) STK)). We used the :type-prescription rule PUSH-STACK. Summary Form: ( DEFUN EXECUTE ...) Rules: ((:TYPE-PRESCRIPTION PUSH-STACK)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) EXECUTE ACL2 !>(execute '(LOAD A) '((A . 7) (B . 4)) '(3 2 1)) (7 3 2 1) ACL2 !>(execute '(PUSH A) '((A . 7) (B . 4)) '(3 2 1)) (A 3 2 1) ACL2 !>(execute '(DUP) '((A . 7) (B . 4)) '(3 2 1)) (3 3 2 1) ACL2 !>(execute '(ADD) '((A . 7) (B . 4)) '(3 2 1)) (5 1) ACL2 !>(execute '(MUL) '((A . 7) (B . 4)) '(3 2 1)) (6 1) ACL2 !>(defun m (program alist stk) (cond ((endp program) stk) ((m (cdr program) alist (execute (car program) alist stk))))) The admission of M is trivial, using the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT PROGRAM). We could deduce no constraints on the type of M. Summary Form: ( DEFUN M ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) M ACL2 !>(m '((LOAD A) (DUP) (ADD)) '((A . 7) (B . 4)) '(0 0 0)) (14 0 0 0) ACL2 !>(defun evaluate (x alist) (cond ((atom x) (cond ((symbolp x) (lookup x alist)) (t x))) ((equal (len x) 2) (cond ((equal (car x) 'inc) (+ 1 (evaluate (cadr x) alist))) ((equal (car x) 'sq) (* (evaluate (cadr x) alist) (evaluate (cadr x) alist))) (t 0))) ((equal (cadr x) '+) (+ (evaluate (car x) alist) (evaluate (caddr x) alist))) ((equal (cadr x) '*) (* (evaluate (car x) alist) (evaluate (caddr x) alist))) (t 0))) For the admission of EVALUATE we will use the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (AND (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'SQ)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '+)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '*)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'INC)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X)))). By the simple :definition ATOM we reduce the conjecture to the following four conjectures. Subgoal 4 (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'SQ)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, FIX and LEN, the :executable-counterpart of ACL2-COUNT, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2- COUNT, to Subgoal 4' (IMPLIES (AND (CONSP X) (EQUAL (+ 1 (LEN (CDR X))) 2) (EQUAL (CAR X) 'SQ)) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2 and restricting the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. These steps produce the following two goals. Subgoal 4.2 (IMPLIES (AND (NOT (CONSP X2)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (CONS X1 X2)) (EQUAL (+ 1 (LEN X2)) 2) (EQUAL X1 'SQ)) (< (ACL2-COUNT (CAR X2)) (+ 1 (ACL2-COUNT X2)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 4.1 (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL (+ 1 (LEN (CONS X3 X4))) 2) (EQUAL X1 'SQ)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definitions ACL2-COUNT, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR- CONS, CDR-CONS and FOLD-CONSTS-IN-+, to Subgoal 4.1' (IMPLIES (EQUAL (+ 2 (LEN X4)) 2) (< (ACL2-COUNT X3) (+ 2 (ACL2-COUNT X3) (ACL2-COUNT X4)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 3 (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '+)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions E0-ORD-< and LEN, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to Subgoal 3' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definition SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF and the :rewrite rule FOLD-CONSTS- IN-+, to Subgoal 3'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4 and restricting the type of the new variable X3 to be that of the term it replaces. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), generalizing (CAR X4) to X5 and (CDR X4) to X6. These steps produce the following two goals. Subgoal 3.2 (IMPLIES (AND (NOT (CONSP X4)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (CONS X3 X4)) (CONSP (LIST* X1 X3 X4)) (NOT (EQUAL (+ 2 (LEN X4)) 2)) (EQUAL X3 '+)) (< (ACL2-COUNT (CAR X4)) (ACL2-COUNT (LIST* X1 X3 X4)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 3.1 (IMPLIES (AND (CONSP (CONS X5 X6)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (LIST* X3 X5 X6)) (CONSP (LIST* X1 X3 X5 X6)) (NOT (EQUAL (+ 2 (LEN (CONS X5 X6))) 2)) (EQUAL X3 '+)) (< (ACL2-COUNT X5) (ACL2-COUNT (LIST* X1 X3 X5 X6)))). This simplifies, using the :definitions ACL2-COUNT, FIX, LEN and SYNTAXP, the :executable-counterparts of ACL2-COUNT, BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, FOLD-CONSTS-IN-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 3.1' (IMPLIES (NOT (EQUAL (+ 3 (LEN X6)) 2)) (< (ACL2-COUNT X5) (+ 3 (ACL2-COUNT X1) (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 2 (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '*)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions E0-ORD-< and LEN, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to Subgoal 2' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definition SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF and the :rewrite rule FOLD-CONSTS- IN-+, to Subgoal 2'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4 and restricting the type of the new variable X3 to be that of the term it replaces. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), generalizing (CAR X4) to X5 and (CDR X4) to X6. These steps produce the following two goals. Subgoal 2.2 (IMPLIES (AND (NOT (CONSP X4)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (CONS X3 X4)) (CONSP (LIST* X1 X3 X4)) (NOT (EQUAL (+ 2 (LEN X4)) 2)) (EQUAL X3 '*)) (< (ACL2-COUNT (CAR X4)) (ACL2-COUNT (LIST* X1 X3 X4)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 2.1 (IMPLIES (AND (CONSP (CONS X5 X6)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (LIST* X3 X5 X6)) (CONSP (LIST* X1 X3 X5 X6)) (NOT (EQUAL (+ 2 (LEN (CONS X5 X6))) 2)) (EQUAL X3 '*)) (< (ACL2-COUNT X5) (ACL2-COUNT (LIST* X1 X3 X5 X6)))). This simplifies, using the :definitions ACL2-COUNT, FIX, LEN and SYNTAXP, the :executable-counterparts of ACL2-COUNT, BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, FOLD-CONSTS-IN-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2.1' (IMPLIES (NOT (EQUAL (+ 3 (LEN X6)) 2)) (< (ACL2-COUNT X5) (+ 3 (ACL2-COUNT X1) (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'INC)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, FIX and LEN, the :executable-counterpart of ACL2-COUNT, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2- COUNT, to Subgoal 1' (IMPLIES (AND (CONSP X) (EQUAL (+ 1 (LEN (CDR X))) 2) (EQUAL (CAR X) 'INC)) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2 and restricting the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. These steps produce the following two goals. Subgoal 1.2 (IMPLIES (AND (NOT (CONSP X2)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (CONS X1 X2)) (EQUAL (+ 1 (LEN X2)) 2) (EQUAL X1 'INC)) (< (ACL2-COUNT (CAR X2)) (+ 1 (ACL2-COUNT X2)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 1.1 (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL (+ 1 (LEN (CONS X3 X4))) 2) (EQUAL X1 'INC)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definitions ACL2-COUNT, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR- CONS, CDR-CONS and FOLD-CONSTS-IN-+, to Subgoal 1.1' (IMPLIES (EQUAL (+ 2 (LEN X4)) 2) (< (ACL2-COUNT X3) (+ 2 (ACL2-COUNT X3) (ACL2-COUNT X4)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for EVALUATE. Thus, we admit this function under the principle of definition. We could deduce no constraints on the type of EVALUATE. Summary Form: ( DEFUN EVALUATE ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION ATOM) (:DEFINITION E0-ORD-<) (:DEFINITION FIX) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 1.07 seconds (prove: 0.89, print: 0.13, other: 0.05) EVALUATE ACL2 !>(evaluate '((3 * b) + a) '((a . 7) (b . 4))) 19 ACL2 !>(m '((PUSH 3) (LOAD B) (MUL) (LOAD A) (ADD)) '((a . 7) (b . 4)) nil) (19) ACL2 !>(defun compile-expression (x) (cond ((atom x) (cond ((symbolp x) (list (list 'load x))) (t (list (list 'push x))))) ((equal (len x) 2) (cond ((eq (car x) 'inc) (append (compile-expression (cadr x)) '((push 1) (add)))) ((eq (car x) 'sq) (append (compile-expression (cadr x)) '((dup) (mul)))) (t (list (list 'push 0))))) ((eq (cadr x) '+) (append (compile-expression (car x)) (compile-expression (caddr x)) '((add)))) ((eq (cadr x) '*) (append (compile-expression (car x)) (compile-expression (caddr x)) '((mul)))) (t (list (list 'push 0))))) For the admission of COMPILE-EXPRESSION we will use the relation E0- ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (AND (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQ (CAR X) 'SQ)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQ (CADR X) '+)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQ (CADR X) '*)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQ (CAR X) 'INC)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X)))). By the simple :definitions ATOM and EQ we reduce the conjecture to the following four conjectures. Subgoal 4 (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'SQ)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, FIX and LEN, the :executable-counterpart of ACL2-COUNT, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2- COUNT, to Subgoal 4' (IMPLIES (AND (CONSP X) (EQUAL (+ 1 (LEN (CDR X))) 2) (EQUAL (CAR X) 'SQ)) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2 and restricting the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. These steps produce the following two goals. Subgoal 4.2 (IMPLIES (AND (NOT (CONSP X2)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (CONS X1 X2)) (EQUAL (+ 1 (LEN X2)) 2) (EQUAL X1 'SQ)) (< (ACL2-COUNT (CAR X2)) (+ 1 (ACL2-COUNT X2)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 4.1 (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL (+ 1 (LEN (CONS X3 X4))) 2) (EQUAL X1 'SQ)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definitions ACL2-COUNT, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR- CONS, CDR-CONS and FOLD-CONSTS-IN-+, to Subgoal 4.1' (IMPLIES (EQUAL (+ 2 (LEN X4)) 2) (< (ACL2-COUNT X3) (+ 2 (ACL2-COUNT X3) (ACL2-COUNT X4)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 3 (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '+)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions E0-ORD-< and LEN, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to Subgoal 3' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definition SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF and the :rewrite rule FOLD-CONSTS- IN-+, to Subgoal 3'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4 and restricting the type of the new variable X3 to be that of the term it replaces. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), generalizing (CAR X4) to X5 and (CDR X4) to X6. These steps produce the following two goals. Subgoal 3.2 (IMPLIES (AND (NOT (CONSP X4)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (CONS X3 X4)) (CONSP (LIST* X1 X3 X4)) (NOT (EQUAL (+ 2 (LEN X4)) 2)) (EQUAL X3 '+)) (< (ACL2-COUNT (CAR X4)) (ACL2-COUNT (LIST* X1 X3 X4)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 3.1 (IMPLIES (AND (CONSP (CONS X5 X6)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (LIST* X3 X5 X6)) (CONSP (LIST* X1 X3 X5 X6)) (NOT (EQUAL (+ 2 (LEN (CONS X5 X6))) 2)) (EQUAL X3 '+)) (< (ACL2-COUNT X5) (ACL2-COUNT (LIST* X1 X3 X5 X6)))). This simplifies, using the :definitions ACL2-COUNT, FIX, LEN and SYNTAXP, the :executable-counterparts of ACL2-COUNT, BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, FOLD-CONSTS-IN-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 3.1' (IMPLIES (NOT (EQUAL (+ 3 (LEN X6)) 2)) (< (ACL2-COUNT X5) (+ 3 (ACL2-COUNT X1) (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 2 (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '*)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions E0-ORD-< and LEN, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to Subgoal 2' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definition SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF and the :rewrite rule FOLD-CONSTS- IN-+, to Subgoal 2'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4 and restricting the type of the new variable X3 to be that of the term it replaces. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), generalizing (CAR X4) to X5 and (CDR X4) to X6. These steps produce the following two goals. Subgoal 2.2 (IMPLIES (AND (NOT (CONSP X4)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (CONS X3 X4)) (CONSP (LIST* X1 X3 X4)) (NOT (EQUAL (+ 2 (LEN X4)) 2)) (EQUAL X3 '*)) (< (ACL2-COUNT (CAR X4)) (ACL2-COUNT (LIST* X1 X3 X4)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 2.1 (IMPLIES (AND (CONSP (CONS X5 X6)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (LIST* X3 X5 X6)) (CONSP (LIST* X1 X3 X5 X6)) (NOT (EQUAL (+ 2 (LEN (CONS X5 X6))) 2)) (EQUAL X3 '*)) (< (ACL2-COUNT X5) (ACL2-COUNT (LIST* X1 X3 X5 X6)))). This simplifies, using the :definitions ACL2-COUNT, FIX, LEN and SYNTAXP, the :executable-counterparts of ACL2-COUNT, BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, FOLD-CONSTS-IN-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2.1' (IMPLIES (NOT (EQUAL (+ 3 (LEN X6)) 2)) (< (ACL2-COUNT X5) (+ 3 (ACL2-COUNT X1) (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'INC)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, FIX and LEN, the :executable-counterpart of ACL2-COUNT, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2- COUNT, to Subgoal 1' (IMPLIES (AND (CONSP X) (EQUAL (+ 1 (LEN (CDR X))) 2) (EQUAL (CAR X) 'INC)) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2 and restricting the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. These steps produce the following two goals. Subgoal 1.2 (IMPLIES (AND (NOT (CONSP X2)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (CONS X1 X2)) (EQUAL (+ 1 (LEN X2)) 2) (EQUAL X1 'INC)) (< (ACL2-COUNT (CAR X2)) (+ 1 (ACL2-COUNT X2)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 1.1 (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL (+ 1 (LEN (CONS X3 X4))) 2) (EQUAL X1 'INC)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definitions ACL2-COUNT, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR- CONS, CDR-CONS and FOLD-CONSTS-IN-+, to Subgoal 1.1' (IMPLIES (EQUAL (+ 2 (LEN X4)) 2) (< (ACL2-COUNT X3) (+ 2 (ACL2-COUNT X3) (ACL2-COUNT X4)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for COMPILE-EXPRESSION. Thus, we admit this function under the principle of definition. We observe that the type of COMPILE-EXPRESSION is described by the theorem (CONSP (COMPILE-EXPRESSION X)). We used primitive type reasoning and the :type-prescription rule BINARY-APPEND. Summary Form: ( DEFUN COMPILE-EXPRESSION ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION ATOM) (:DEFINITION E0-ORD-<) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION BINARY-APPEND)) Warnings: None Time: 0.70 seconds (prove: 0.52, print: 0.12, other: 0.06) COMPILE-EXPRESSION ACL2 !>(compile-expression '(SQ (INC (A + (3 * B))))) ((LOAD A) (PUSH 3) (LOAD B) (MUL) (ADD) (PUSH 1) (ADD) (DUP) (MUL)) ACL2 !>(defthm sequential-execution (equal (m (append x y) a s) (m y a (m x a s)))) Name the formula above *1. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into two derived induction schemes. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (M X A S), but modified to accommodate (APPEND X Y). If we let (:P A S X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (:P A (EXECUTE (CAR X) A S) (CDR X) Y)) (:P A S X Y)) (IMPLIES (AND (NOT (ENDP X)) (M (CDR X) A (EXECUTE (CAR X) A S)) (:P A (EXECUTE (CAR X) A S) (CDR X) Y)) (:P A S X Y)) (IMPLIES (ENDP X) (:P A S X Y))). This induction is justified by the same argument used to admit M, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variable S is being instantiated. When applied to the goal at hand the above induction scheme produces the following three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ENDP X)) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (M (APPEND (CDR X) Y) A (EXECUTE (CAR X) A S)) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND X Y) A S) (M Y A (M X A S)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (M (APPEND (CDR X) Y) A (EXECUTE (CAR X) A S)) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND X Y) A S) (M Y A (M X A S)))). This simplifies, using the :definitions BINARY-APPEND, EXECUTE, FIX, M, POP-STACK, PUSH-STACK and TOP-STACK, the :executable-counterparts of BINARY-*, BINARY-+, EQUAL, POP-STACK, PUSH-STACK and TOP-STACK, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+, DEFAULT-CDR, TIMES-ZERO and UNICITY-OF-0, to the following five conjectures. Subgoal *1/3.5 (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'ADD) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))) (M Y A NIL)) (ACL2-NUMBERP (CAR S))) (EQUAL (M (APPEND (CDR X) Y) A (LIST (CAR S))) (M Y A NIL))). But simplification reduces this to T, using the :definition FIX and the :rewrite rules COMMUTATIVITY-OF-+, DEFAULT-CDR and UNICITY-OF-0. Subgoal *1/3.4 (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'ADD) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))) (M Y A NIL)) (NOT (ACL2-NUMBERP (CAR S)))) (EQUAL (M (APPEND (CDR X) Y) A (LIST 0)) (M Y A NIL))). By the :executable-counterpart of CONS we reduce the conjecture to Subgoal *1/3.4' (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'ADD) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))) (M Y A NIL)) (NOT (ACL2-NUMBERP (CAR S)))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M Y A NIL))). But simplification reduces this to T, using the :executable-counterparts of CONS and FIX and the :rewrite rules DEFAULT-+-1 and DEFAULT-CDR. Subgoal *1/3.3 (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'ADD) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ 0 0) (CDDR S))) (M Y A NIL))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M Y A NIL))). By the :executable-counterpart of BINARY-+ we reduce the conjecture to Subgoal *1/3.3' (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'ADD) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS 0 (CDDR S))) (M Y A NIL))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M Y A NIL))). But simplification reduces this to T, using the :executable-counterparts of CDR and CONS, primitive type reasoning and the :rewrite rule DEFAULT- CDR. Subgoal *1/3.2 (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'MUL) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (* (CAR S) 0) (CDDR S))) (M Y A NIL))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M Y A NIL))). But simplification reduces this to T, using the :executable-counterpart of CONS and the :rewrite rules COMMUTATIVITY-OF-*, DEFAULT-CDR and TIMES-ZERO. Subgoal *1/3.1 (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'MUL) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (* 0 0) (CDDR S))) (M Y A NIL))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M Y A NIL))). By the :executable-counterpart of BINARY-* we reduce the conjecture to Subgoal *1/3.1' (IMPLIES (AND (CONSP X) (NOT (M (CDR X) A (EXECUTE (CAR X) A S))) (EQUAL (CAAR X) 'MUL) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS 0 (CDDR S))) (M Y A NIL))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M Y A NIL))). But simplification reduces this to T, using the :executable-counterparts of CDR and CONS, primitive type reasoning and the :rewrite rule DEFAULT- CDR. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (M (APPEND (CDR X) Y) A (EXECUTE (CAR X) A S)) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND X Y) A S) (M Y A (M X A S)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (M (APPEND (CDR X) Y) A (EXECUTE (CAR X) A S)) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND X Y) A S) (M Y A (M X A S)))). This simplifies, using the :definitions BINARY-APPEND, EXECUTE, FIX, M, POP-STACK, PUSH-STACK and TOP-STACK, the :executable-counterparts of BINARY-*, BINARY-+, EQUAL, POP-STACK, PUSH-STACK and TOP-STACK, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+, DEFAULT-CDR, TIMES-ZERO and UNICITY-OF-0, to the following five conjectures. Subgoal *1/2.5 (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'ADD) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S)))) (ACL2-NUMBERP (CAR S))) (EQUAL (M (APPEND (CDR X) Y) A (LIST (CAR S))) (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))))). But simplification reduces this to T, using the :definition FIX, primitive type reasoning and the :rewrite rules COMMUTATIVITY-OF-+, DEFAULT-CDR and UNICITY-OF-0. Subgoal *1/2.4 (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'ADD) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S)))) (NOT (ACL2-NUMBERP (CAR S)))) (EQUAL (M (APPEND (CDR X) Y) A (LIST 0)) (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))))). By the :executable-counterpart of CONS we reduce the conjecture to Subgoal *1/2.4' (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'ADD) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S)))) (NOT (ACL2-NUMBERP (CAR S)))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M (APPEND (CDR X) Y) A (CONS (+ (CAR S) 0) (CDDR S))))). But simplification reduces this to T, using the :executable-counterparts of CONS and FIX, primitive type reasoning and the :rewrite rules DEFAULT- +-1 and DEFAULT-CDR. Subgoal *1/2.3 (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'ADD) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (+ 0 0) (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M (APPEND (CDR X) Y) A (CONS (+ 0 0) (CDDR S))))). By the :executable-counterpart of BINARY-+ we reduce the conjecture to Subgoal *1/2.3' (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'ADD) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS 0 (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M (APPEND (CDR X) Y) A (CONS 0 (CDDR S))))). But simplification reduces this to T, using the :executable-counterparts of CDR and CONS, primitive type reasoning and the :rewrite rule DEFAULT- CDR. Subgoal *1/2.2 (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'MUL) (CONSP S) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (* (CAR S) 0) (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M (APPEND (CDR X) Y) A (CONS (* (CAR S) 0) (CDDR S))))). But simplification reduces this to T, using the :executable-counterpart of CONS, primitive type reasoning and the :rewrite rules COMMUTATIVITY- OF-*, DEFAULT-CDR and TIMES-ZERO. Subgoal *1/2.1 (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'MUL) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS (* 0 0) (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M (APPEND (CDR X) Y) A (CONS (* 0 0) (CDDR S))))). By the :executable-counterpart of BINARY-* we reduce the conjecture to Subgoal *1/2.1' (IMPLIES (AND (CONSP X) (M (CDR X) A (EXECUTE (CAR X) A S)) (EQUAL (CAAR X) 'MUL) (NOT (CONSP S)) (NOT (CONSP (CDR S))) (EQUAL (M (APPEND (CDR X) Y) A (CONS 0 (CDDR S))) (M Y A (M (CDR X) A (EXECUTE (CAR X) A S))))) (EQUAL (M (APPEND (CDR X) Y) A '(0)) (M (APPEND (CDR X) Y) A (CONS 0 (CDDR S))))). But simplification reduces this to T, using the :executable-counterparts of CDR and CONS, primitive type reasoning and the :rewrite rule DEFAULT- CDR. Subgoal *1/1 (IMPLIES (ENDP X) (EQUAL (M (APPEND X Y) A S) (M Y A (M X A S)))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (EQUAL (M (APPEND X Y) A S) (M Y A (M X A S)))). But simplification reduces this to T, using the :definitions BINARY- APPEND and M and primitive type reasoning. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM SEQUENTIAL-EXECUTION ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION EXECUTE) (:DEFINITION FIX) (:DEFINITION M) (:DEFINITION NOT) (:DEFINITION POP-STACK) (:DEFINITION PUSH-STACK) (:DEFINITION TOP-STACK) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART POP-STACK) (:EXECUTABLE-COUNTERPART PUSH-STACK) (:EXECUTABLE-COUNTERPART TOP-STACK) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DEFAULT-+-1) (:REWRITE DEFAULT-CDR) (:REWRITE TIMES-ZERO) (:REWRITE UNICITY-OF-0)) Warnings: None Time: 1.94 seconds (prove: 1.77, print: 0.16, other: 0.01) SEQUENTIAL-EXECUTION ACL2 !>(defun hintfn (x a s) (cond ((atom x) (list x a s)) ((equal (len x) 2) (cond ((eq (car x) 'inc) (hintfn (cadr x) a s)) ((eq (car x) 'sq) (hintfn (cadr x) a s)) (t (list x a s)))) ((eq (cadr x) '+) (cons (hintfn (car x) a s) (hintfn (caddr x) a (push-stack (evaluate (car x) a) s)))) ((eq (cadr x) '*) (cons (hintfn (car x) a s) (hintfn (caddr x) a (push-stack (evaluate (car x) a) s)))) (t (list x a s)))) For the admission of HINTFN we will use the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (AND (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQ (CAR X) 'SQ)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQ (CADR X) '+)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQ (CADR X) '*)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQ (CAR X) 'INC)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X)))). By the simple :definitions ATOM and EQ we reduce the conjecture to the following four conjectures. Subgoal 4 (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'SQ)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, FIX and LEN, the :executable-counterpart of ACL2-COUNT, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2- COUNT, to Subgoal 4' (IMPLIES (AND (CONSP X) (EQUAL (+ 1 (LEN (CDR X))) 2) (EQUAL (CAR X) 'SQ)) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2 and restricting the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. These steps produce the following two goals. Subgoal 4.2 (IMPLIES (AND (NOT (CONSP X2)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (CONS X1 X2)) (EQUAL (+ 1 (LEN X2)) 2) (EQUAL X1 'SQ)) (< (ACL2-COUNT (CAR X2)) (+ 1 (ACL2-COUNT X2)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 4.1 (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL (+ 1 (LEN (CONS X3 X4))) 2) (EQUAL X1 'SQ)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definitions ACL2-COUNT, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR- CONS, CDR-CONS and FOLD-CONSTS-IN-+, to Subgoal 4.1' (IMPLIES (EQUAL (+ 2 (LEN X4)) 2) (< (ACL2-COUNT X3) (+ 2 (ACL2-COUNT X3) (ACL2-COUNT X4)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 3 (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '+)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions E0-ORD-< and LEN, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to Subgoal 3' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definition SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF and the :rewrite rule FOLD-CONSTS- IN-+, to Subgoal 3'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4 and restricting the type of the new variable X3 to be that of the term it replaces. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), generalizing (CAR X4) to X5 and (CDR X4) to X6. These steps produce the following two goals. Subgoal 3.2 (IMPLIES (AND (NOT (CONSP X4)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (CONS X3 X4)) (CONSP (LIST* X1 X3 X4)) (NOT (EQUAL (+ 2 (LEN X4)) 2)) (EQUAL X3 '+)) (< (ACL2-COUNT (CAR X4)) (ACL2-COUNT (LIST* X1 X3 X4)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 3.1 (IMPLIES (AND (CONSP (CONS X5 X6)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (LIST* X3 X5 X6)) (CONSP (LIST* X1 X3 X5 X6)) (NOT (EQUAL (+ 2 (LEN (CONS X5 X6))) 2)) (EQUAL X3 '+)) (< (ACL2-COUNT X5) (ACL2-COUNT (LIST* X1 X3 X5 X6)))). This simplifies, using the :definitions ACL2-COUNT, FIX, LEN and SYNTAXP, the :executable-counterparts of ACL2-COUNT, BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, FOLD-CONSTS-IN-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 3.1' (IMPLIES (NOT (EQUAL (+ 3 (LEN X6)) 2)) (< (ACL2-COUNT X5) (+ 3 (ACL2-COUNT X1) (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 2 (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '*)) (E0-ORD-< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions E0-ORD-< and LEN, primitive type reasoning and the :type-prescription rule ACL2-COUNT, to Subgoal 2' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definition SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ and IF and the :rewrite rule FOLD-CONSTS- IN-+, to Subgoal 2'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*)) (< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4 and restricting the type of the new variable X3 to be that of the term it replaces. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), generalizing (CAR X4) to X5 and (CDR X4) to X6. These steps produce the following two goals. Subgoal 2.2 (IMPLIES (AND (NOT (CONSP X4)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (CONS X3 X4)) (CONSP (LIST* X1 X3 X4)) (NOT (EQUAL (+ 2 (LEN X4)) 2)) (EQUAL X3 '*)) (< (ACL2-COUNT (CAR X4)) (ACL2-COUNT (LIST* X1 X3 X4)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 2.1 (IMPLIES (AND (CONSP (CONS X5 X6)) (SYMBOLP X3) (NOT (EQUAL X3 T)) X3 (CONSP (LIST* X3 X5 X6)) (CONSP (LIST* X1 X3 X5 X6)) (NOT (EQUAL (+ 2 (LEN (CONS X5 X6))) 2)) (EQUAL X3 '*)) (< (ACL2-COUNT X5) (ACL2-COUNT (LIST* X1 X3 X5 X6)))). This simplifies, using the :definitions ACL2-COUNT, FIX, LEN and SYNTAXP, the :executable-counterparts of ACL2-COUNT, BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY-2-OF-+, FOLD-CONSTS-IN-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2.1' (IMPLIES (NOT (EQUAL (+ 3 (LEN X6)) 2)) (< (ACL2-COUNT X5) (+ 3 (ACL2-COUNT X1) (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'INC)) (E0-ORD-< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, FIX and LEN, the :executable-counterpart of ACL2-COUNT, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2- COUNT, to Subgoal 1' (IMPLIES (AND (CONSP X) (EQUAL (+ 1 (LEN (CDR X))) 2) (EQUAL (CAR X) 'INC)) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), generalizing (CAR X) to X1 and (CDR X) to X2 and restricting the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), generalizing (CAR X2) to X3 and (CDR X2) to X4. These steps produce the following two goals. Subgoal 1.2 (IMPLIES (AND (NOT (CONSP X2)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (CONS X1 X2)) (EQUAL (+ 1 (LEN X2)) 2) (EQUAL X1 'INC)) (< (ACL2-COUNT (CAR X2)) (+ 1 (ACL2-COUNT X2)))). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL, NOT and SYMBOLP and primitive type reasoning. Subgoal 1.1 (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL (+ 1 (LEN (CONS X3 X4))) 2) (EQUAL X1 'INC)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definitions ACL2-COUNT, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, EQUAL, IF, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR- CONS, CDR-CONS and FOLD-CONSTS-IN-+, to Subgoal 1.1' (IMPLIES (EQUAL (+ 2 (LEN X4)) 2) (< (ACL2-COUNT X3) (+ 2 (ACL2-COUNT X3) (ACL2-COUNT X4)))). But simplification reduces this to T, using linear arithmetic and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for HINTFN. Thus, we admit this function under the principle of definition. We observe that the type of HINTFN is described by the theorem (AND (CONSP (HINTFN X A S)) (TRUE-LISTP (HINTFN X A S))). We used primitive type reasoning. Summary Form: ( DEFUN HINTFN ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION ATOM) (:DEFINITION E0-ORD-<) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 1.04 seconds (prove: 0.47, print: 0.16, other: 0.41) HINTFN ACL2 !>(defthm key-compiler-lemma (equal (m (compile-expression x) a s) (push-stack (evaluate x a) s)) :hints (("Goal" :induct (hintfn x a s)))) [Note: A hint was supplied for our processing of the goal above. Thanks!] Name the formula above *1. We have been told to use induction. One induction scheme is suggested by the induction hint. We will induct according to a scheme suggested by (HINTFN X A S). If we let (:P A S X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (NOT (EQ (CADR X) '+)) (NOT (EQ (CADR X) '*))) (:P A S X)) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (NOT (EQ (CADR X) '+)) (EQ (CADR X) '*) (:P A S (CAR X)) (:P A (PUSH-STACK (EVALUATE (CAR X) A) S) (CADDR X))) (:P A S X)) (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQ (CADR X) '+) (:P A S (CAR X)) (:P A (PUSH-STACK (EVALUATE (CAR X) A) S) (CADDR X))) (:P A S X)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (NOT (EQ (CAR X) 'INC)) (NOT (EQ (CAR X) 'SQ))) (:P A S X)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (NOT (EQ (CAR X) 'INC)) (EQ (CAR X) 'SQ) (:P A S (CADR X))) (:P A S X)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQ (CAR X) 'INC) (:P A S (CADR X))) (:P A S X)) (IMPLIES (ATOM X) (:P A S X))). This induction is justified by the same argument used to admit HINTFN, namely, the measure (ACL2-COUNT X) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). Note, however, that the unmeasured variable S is being instantiated. When applied to the goal at hand the above induction scheme produces the following seven nontautological subgoals. Subgoal *1/7 (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (NOT (EQ (CADR X) '+)) (NOT (EQ (CADR X) '*))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM, EQ and PUSH-STACK we reduce the conjecture to Subgoal *1/7' (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (NOT (EQUAL (CADR X) '+)) (NOT (EQUAL (CADR X) '*))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). But simplification reduces this to T, using the :definitions COMPILE- EXPRESSION, EVALUATE, EXECUTE, LEN, M and PUSH-STACK, the :executable- counterparts of CAR, CDR, CONSP and EQUAL and primitive type reasoning. Subgoal *1/6 (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (NOT (EQ (CADR X) '+)) (EQ (CADR X) '*) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (PUSH-STACK (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (PUSH-STACK (EVALUATE (CAR X) A) S)) (PUSH-STACK (EVALUATE (CADDR X) A) (PUSH-STACK (EVALUATE (CAR X) A) S)))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM, EQ and PUSH-STACK we reduce the conjecture to Subgoal *1/6' (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (NOT (EQUAL (CADR X) '+)) (EQUAL (CADR X) '*) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (CONS (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE (CAR X) A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE (CAR X) A) S))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). This simplifies, using the :definitions COMPILE-EXPRESSION, EVALUATE, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, BINARY-APPEND, CAR, COMPILE-EXPRESSION, CONSP, EQ, EQUAL, IF and SYMBOLP, primitive type reasoning and the :rewrite rule FOLD-CONSTS-IN-+, to the following four conjectures. Subgoal *1/6.4 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (CONS (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE (CAR X) A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE (CAR X) A) S)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2))) (EQUAL (M (APPEND (COMPILE-EXPRESSION (CAR X)) (COMPILE-EXPRESSION (CADDR X)) '((MUL))) A S) (CONS (* (EVALUATE (CAR X) A) (EVALUATE (CADDR X) A)) S))). But simplification reduces this to T, using the :definitions EXECUTE, M, POP-STACK, PUSH-STACK, SYNTAXP and TOP-STACK, the :executable-counterparts of BINARY-+, CAR, CDR, CONSP, EQ, EQUAL and IF, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, FOLD-CONSTS-IN-+ and SEQUENTIAL- EXECUTION. Subgoal *1/6.3 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*) (EQUAL (M '((LOAD INC)) A S) (CONS (EVALUATE 'INC A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE 'INC A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE 'INC A) S)) (EQUAL (+ 2 (LEN (CDDR X))) 2) (EQUAL (CAR X) 'INC)) (EQUAL (M '((LOAD *) (PUSH 1) (ADD)) A S) (CONS (+ 1 (LOOKUP '* A)) S))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1/6.2 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (CONS (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE (CAR X) A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE (CAR X) A) S)) (EQUAL (+ 2 (LEN (CDDR X))) 2) (NOT (EQUAL (CAR X) 'INC)) (NOT (EQUAL (CAR X) 'SQ))) (EQUAL (M '((PUSH 0)) A S) (CONS 0 S))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1/6.1 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '*) (EQUAL (M '((LOAD SQ)) A S) (CONS (EVALUATE 'SQ A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE 'SQ A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE 'SQ A) S)) (EQUAL (+ 2 (LEN (CDDR X))) 2) (EQUAL (CAR X) 'SQ)) (EQUAL (M '((LOAD *) (DUP) (MUL)) A S) (CONS (* (LOOKUP '* A) (LOOKUP '* A)) S))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1/5 (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL (LEN X) 2)) (EQ (CADR X) '+) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (PUSH-STACK (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (PUSH-STACK (EVALUATE (CAR X) A) S)) (PUSH-STACK (EVALUATE (CADDR X) A) (PUSH-STACK (EVALUATE (CAR X) A) S)))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM, EQ and PUSH-STACK we reduce the conjecture to Subgoal *1/5' (IMPLIES (AND (CONSP X) (NOT (EQUAL (LEN X) 2)) (EQUAL (CADR X) '+) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (CONS (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE (CAR X) A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE (CAR X) A) S))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). This simplifies, using the :definitions COMPILE-EXPRESSION, EVALUATE, LEN and SYNTAXP, the :executable-counterparts of BINARY-+, BINARY-APPEND, CAR, COMPILE-EXPRESSION, CONSP, EQ, EQUAL, IF and SYMBOLP, primitive type reasoning and the :rewrite rule FOLD-CONSTS-IN-+, to the following four conjectures. Subgoal *1/5.4 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (CONS (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE (CAR X) A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE (CAR X) A) S)) (NOT (EQUAL (+ 2 (LEN (CDDR X))) 2))) (EQUAL (M (APPEND (COMPILE-EXPRESSION (CAR X)) (COMPILE-EXPRESSION (CADDR X)) '((ADD))) A S) (CONS (+ (EVALUATE (CAR X) A) (EVALUATE (CADDR X) A)) S))). But simplification reduces this to T, using the :definitions EXECUTE, M, POP-STACK, PUSH-STACK, SYNTAXP and TOP-STACK, the :executable-counterparts of BINARY-+, CAR, CDR, CONSP, EQ, EQUAL and IF, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, FOLD-CONSTS-IN-+ and SEQUENTIAL- EXECUTION. Subgoal *1/5.3 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+) (EQUAL (M '((LOAD INC)) A S) (CONS (EVALUATE 'INC A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE 'INC A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE 'INC A) S)) (EQUAL (+ 2 (LEN (CDDR X))) 2) (EQUAL (CAR X) 'INC)) (EQUAL (M '((LOAD +) (PUSH 1) (ADD)) A S) (CONS (+ 1 (LOOKUP '+ A)) S))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1/5.2 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+) (EQUAL (M (COMPILE-EXPRESSION (CAR X)) A S) (CONS (EVALUATE (CAR X) A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE (CAR X) A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE (CAR X) A) S)) (EQUAL (+ 2 (LEN (CDDR X))) 2) (NOT (EQUAL (CAR X) 'INC)) (NOT (EQUAL (CAR X) 'SQ))) (EQUAL (M '((PUSH 0)) A S) (CONS 0 S))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1/5.1 (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (NOT (EQUAL (+ 1 1 (LEN (CDDR X))) 2)) (EQUAL (CADR X) '+) (EQUAL (M '((LOAD SQ)) A S) (CONS (EVALUATE 'SQ A) S)) (EQUAL (M (COMPILE-EXPRESSION (CADDR X)) A (CONS (EVALUATE 'SQ A) S)) (LIST* (EVALUATE (CADDR X) A) (EVALUATE 'SQ A) S)) (EQUAL (+ 2 (LEN (CDDR X))) 2) (EQUAL (CAR X) 'SQ)) (EQUAL (M '((LOAD +) (DUP) (MUL)) A S) (CONS (* (LOOKUP '+ A) (LOOKUP '+ A)) S))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1/4 (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (NOT (EQ (CAR X) 'INC)) (NOT (EQ (CAR X) 'SQ))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM, EQ and PUSH-STACK we reduce the conjecture to Subgoal *1/4' (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (NOT (EQUAL (CAR X) 'INC)) (NOT (EQUAL (CAR X) 'SQ))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). But simplification reduces this to T, using the :definitions COMPILE- EXPRESSION, EVALUATE, EXECUTE, M and PUSH-STACK, the :executable-counterparts of CAR, CDR, CONSP and EQUAL and primitive type reasoning. Subgoal *1/3 (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (NOT (EQ (CAR X) 'INC)) (EQ (CAR X) 'SQ) (EQUAL (M (COMPILE-EXPRESSION (CADR X)) A S) (PUSH-STACK (EVALUATE (CADR X) A) S))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM, EQ and PUSH-STACK we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (NOT (EQUAL (CAR X) 'INC)) (EQUAL (CAR X) 'SQ) (EQUAL (M (COMPILE-EXPRESSION (CADR X)) A S) (CONS (EVALUATE (CADR X) A) S))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). But simplification reduces this to T, using the :definitions COMPILE- EXPRESSION, EVALUATE, EXECUTE, LEN, M, POP-STACK, PUSH-STACK and TOP- STACK, the :executable-counterparts of CAR, CDR, CONSP and EQUAL, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS and SEQUENTIAL- EXECUTION. Subgoal *1/2 (IMPLIES (AND (NOT (ATOM X)) (EQUAL (LEN X) 2) (EQ (CAR X) 'INC) (EQUAL (M (COMPILE-EXPRESSION (CADR X)) A S) (PUSH-STACK (EVALUATE (CADR X) A) S))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM, EQ and PUSH-STACK we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (LEN X) 2) (EQUAL (CAR X) 'INC) (EQUAL (M (COMPILE-EXPRESSION (CADR X)) A S) (CONS (EVALUATE (CADR X) A) S))) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). But simplification reduces this to T, using the :definitions COMPILE- EXPRESSION, EVALUATE, EXECUTE, LEN, M, POP-STACK, PUSH-STACK and TOP- STACK, the :executable-counterparts of CAR, CDR, CONSP and EQUAL, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, COMMUTATIVITY- OF-+ and SEQUENTIAL-EXECUTION. Subgoal *1/1 (IMPLIES (ATOM X) (EQUAL (M (COMPILE-EXPRESSION X) A S) (PUSH-STACK (EVALUATE X A) S))). By the simple :definitions ATOM and PUSH-STACK we reduce the conjecture to Subgoal *1/1' (IMPLIES (NOT (CONSP X)) (EQUAL (M (COMPILE-EXPRESSION X) A S) (CONS (EVALUATE X A) S))). This simplifies, using the :definitions COMPILE-EXPRESSION and EVALUATE, to the following two conjectures. Subgoal *1/1.2 (IMPLIES (AND (NOT (CONSP X)) (SYMBOLP X)) (EQUAL (M (LIST (LIST 'LOAD X)) A S) (CONS (LOOKUP X A) S))). But simplification reduces this to T, using the :definitions EXECUTE, M and PUSH-STACK, the :executable-counterparts of CONSP and EQUAL, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal *1/1.1 (IMPLIES (AND (NOT (CONSP X)) (NOT (SYMBOLP X))) (EQUAL (M (LIST (LIST 'PUSH X)) A S) (CONS X S))). But simplification reduces this to T, using the :definitions EXECUTE, M and PUSH-STACK, the :executable-counterparts of CONSP and EQUAL, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM KEY-COMPILER-LEMMA ...) Rules: ((:DEFINITION ATOM) (:DEFINITION COMPILE-EXPRESSION) (:DEFINITION EQ) (:DEFINITION EVALUATE) (:DEFINITION EXECUTE) (:DEFINITION LEN) (:DEFINITION M) (:DEFINITION NOT) (:DEFINITION POP-STACK) (:DEFINITION PUSH-STACK) (:DEFINITION SYNTAXP) (:DEFINITION TOP-STACK) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART BINARY-APPEND) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART COMPILE-EXPRESSION) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE SEQUENTIAL-EXECUTION) (:TYPE-PRESCRIPTION LEN)) Warnings: None Time: 1.95 seconds (prove: 1.80, print: 0.13, other: 0.02) KEY-COMPILER-LEMMA ACL2 !>(defthm main-compiler-thm (equal (top-stack (m (compile-expression x) a s)) (evaluate x a)) :rule-classes nil) By the simple :definition PUSH-STACK and the simple :rewrite rule KEY- COMPILER-LEMMA we reduce the conjecture to Goal' (EQUAL (TOP-STACK (CONS (EVALUATE X A) S)) (EVALUATE X A)). But simplification reduces this to T, using the :definition TOP-STACK, primitive type reasoning and the :rewrite rule CAR-CONS. Q.E.D. Summary Form: ( DEFTHM MAIN-COMPILER-THM ...) Rules: ((:DEFINITION PUSH-STACK) (:DEFINITION TOP-STACK) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE KEY-COMPILER-LEMMA)) Warnings: None Time: 0.05 seconds (prove: 0.03, print: 0.00, other: 0.02) MAIN-COMPILER-THM ACL2 !>(in-package "TJVM") "TJVM" TJVM !>(pe 'step) d 2 (INCLUDE-BOOK "isort") \ >L d (DEFUN STEP (S) (DO-INST (NEXT-INST S) S)) TJVM !>(pe 'next-inst) d 2 (INCLUDE-BOOK "isort") \ >L (DEFUN NEXT-INST (S) (NTH (PC (TOP-FRAME S)) (PROGRAM (TOP-FRAME S)))) TJVM !>(pe 'do-inst) d 2 (INCLUDE-BOOK "isort") \ >L (DEFUN DO-INST (INST S) (CASE (OP-CODE INST) (PUSH (EXECUTE-PUSH INST S)) (POP (EXECUTE-POP INST S)) (LOAD (EXECUTE-LOAD INST S)) (STORE (EXECUTE-STORE INST S)) (ADD (EXECUTE-ADD INST S)) (SUB (EXECUTE-SUB INST S)) (MUL (EXECUTE-MUL INST S)) (GOTO (EXECUTE-GOTO INST S)) (IFEQ (EXECUTE-IFEQ INST S)) (IFGT (EXECUTE-IFGT INST S)) (IFLE (EXECUTE-IFLE INST S)) (INVOKEVIRTUAL (EXECUTE-INVOKEVIRTUAL INST S)) (INVOKESTATIC (EXECUTE-INVOKESTATIC INST S)) (RETURN (EXECUTE-RETURN INST S)) (XRETURN (EXECUTE-XRETURN INST S)) (NEW (EXECUTE-NEW INST S)) (GETFIELD (EXECUTE-GETFIELD INST S)) (PUTFIELD (EXECUTE-PUTFIELD INST S)) (INSTANCEOF (EXECUTE-INSTANCEOF INST S)) (HALT S) (OTHERWISE S))) TJVM !>(pe 'execute-load) d 2 (INCLUDE-BOOK "isort") \ >L (DEFUN EXECUTE-LOAD (INST S) (MAKE-STATE (PUSH (MAKE-FRAME (+ 1 (PC (TOP-FRAME S))) (LOCALS (TOP-FRAME S)) (PUSH (BINDING (ARG1 INST) (LOCALS (TOP-FRAME S))) (STACK (TOP-FRAME S))) (PROGRAM (TOP-FRAME S))) (POP (CALL-STACK S))) (HEAP S) (CLASS-TABLE S))) TJVM !>(pe 'execute-invokevirtual) d 2 (INCLUDE-BOOK "isort") \ >L (DEFUN EXECUTE-INVOKEVIRTUAL (INST S) (LET* ((METHOD-NAME (ARG2 INST)) (NFORMALS (ARG3 INST)) (OBJ-REF (TOP (POPN NFORMALS (STACK (TOP-FRAME S))))) (OBJ-CLASS-NAME (CLASS-NAME-OF-REF OBJ-REF (HEAP S))) (CLOSEST-METHOD (LOOKUP-METHOD METHOD-NAME OBJ-CLASS-NAME (CLASS-TABLE S))) (VARS (CONS 'THIS (METHOD-FORMALS CLOSEST-METHOD))) (PROG (METHOD-PROGRAM CLOSEST-METHOD))) (MAKE-STATE (PUSH (MAKE-FRAME 0 (REVERSE (BIND-FORMALS (REVERSE VARS) (STACK (TOP-FRAME S)))) NIL PROG) (PUSH (MAKE-FRAME (+ 1 (PC (TOP-FRAME S))) (LOCALS (TOP-FRAME S)) (POPN (LEN VARS) (STACK (TOP-FRAME S))) (PROGRAM (TOP-FRAME S))) (POP (CALL-STACK S)))) (HEAP S) (CLASS-TABLE S)))) TJVM !>(pe 'tjvm) d 2 (INCLUDE-BOOK "isort") \ >L d (DEFUN TJVM (S N) (IF (ZP N) S (TJVM (STEP S) (- N 1)))) TJVM !>(cons-class) ("Cons" ("Object") ("car" "cdr") (("cons" (X Y) (NEW "Cons") (STORE TEMP) (LOAD TEMP) (LOAD X) (PUTFIELD "Cons" "car") (LOAD TEMP) (LOAD Y) (PUTFIELD "Cons" "cdr") (LOAD TEMP) (XRETURN)) ("insert" (E X) (LOAD X) (IFEQ 18) (LOAD X) (GETFIELD "Cons" "car") (LOAD E) (SUB) (IFLE 5) (LOAD E) (LOAD X) (INVOKESTATIC "Cons" "cons" 2) (XRETURN) (LOAD X) (GETFIELD "Cons" "car") (LOAD E) (LOAD X) (GETFIELD "Cons" "cdr") (INVOKESTATIC "Cons" "insert" 2) (INVOKESTATIC "Cons" "cons" 2) (XRETURN) (LOAD E) (LOAD X) (INVOKESTATIC "Cons" "cons" 2) (XRETURN)) ("isort" (X) (LOAD X) (IFEQ 8) (LOAD X) (GETFIELD "Cons" "car") (LOAD X) (GETFIELD "Cons" "cdr") (INVOKESTATIC "Cons" "isort" 1) (INVOKESTATIC "Cons" "insert" 2) (XRETURN) (LOAD X) (XRETURN)))) TJVM !>(defconst *s0* (make-state (push ; activation stack (make-frame 1 ; pc '((x . (REF 4))) ; local vars '((REF 4)) ; stack '((load x) ; byte code (invokestatic "Cons" "isort" 1); for most (halt))) ; recent method nil) '((0 ("Cons" ("car" . 5) ("cdr" . 0)) ; heap ("Object")) (1 ("Cons" ("car" . 1) ("cdr" REF 0)) ("Object")) (2 ("Cons" ("car" . 4) ("cdr" REF 1)) ("Object")) (3 ("Cons" ("car" . 2) ("cdr" REF 2)) ("Object")) (4 ("Cons" ("car" . 3) ("cdr" REF 3)) ("Object"))) (list (cons-class) ; class table (object-class)))) Summary Form: ( DEFCONST *S0* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *S0* TJVM !>(deref* (top (stack (top-frame *s0*))) (heap *s0*)) (3 2 4 1 5) TJVM !>(defconst *s1* (tjvm *s0* 250)) Summary Form: ( DEFCONST *S1* ...) Rules: NIL Warnings: None Time: 1.32 seconds (prove: 0.00, print: 0.00, other: 1.32) *S1* TJVM !>(deref* (top (stack (top-frame *s1*))) (heap *s1*)) (1 2 3 4 5) TJVM !>(pe 'isort-spec) d 2 (INCLUDE-BOOK "isort") \ > (DEFTHM ISORT-SPEC (IMPLIES (AND (STANDARD-HYPS S0) (EQUAL (NEXT-INST S0) '(INVOKESTATIC "Cons" "isort" 1))) (LET* ((X0 (TOP (STACK (TOP-FRAME S0)))) (HEAP0 (HEAP S0)) (N0 (ISORT-CLOCK X0 HEAP0)) (S1 (TJVM S0 N0)) (X1 (TOP (STACK (TOP-FRAME S1)))) (HEAP1 (HEAP S1))) (IMPLIES (OK-REFP X0 HEAP0) (LET ((LIST0 (DEREF* X0 HEAP0)) (LIST1 (DEREF* X1 HEAP1))) (AND (ORDERED LIST1) (PERM LIST1 LIST0))))))) TJVM !>(pe 'tjvm-isort-lemma) d 2 (INCLUDE-BOOK "isort") \ > (DEFTHM TJVM-ISORT-LEMMA (IMPLIES (AND (STANDARD-HYPS S0) (EQUAL (NEXT-INST S0) '(INVOKESTATIC "Cons" "isort" 1))) (LET* ((X0 (TOP (STACK (TOP-FRAME S0)))) (HEAP0 (HEAP S0)) (N0 (ISORT-CLOCK X0 HEAP0)) (S1 (TJVM S0 N0)) (X1 (TOP (STACK (TOP-FRAME S1)))) (HEAP1 (HEAP S1))) (IMPLIES (OK-REFP X0 HEAP0) (EQUAL (DEREF* X1 HEAP1) (ISORT (DEREF* X0 HEAP0))))))) TJVM !>(quote "The End") "The End" TJVM !>