[ruben@majestic misc]$ acl2r GCL (GNU Common Lisp) Version(2.3) Mon May 29 10:34:50 CDT 2000 Licensed under GNU Library General Public License Contains Enhancements by W. Schelter ACL2 Version 2.5(r) built September 4, 2000 09:55:23. Copyright (C) 2000 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* NIL). See the documentation topic note-2-5(r) for recent changes. NOTE!! Proof trees are disabled in ACL2. To enable them in emacs, look under the ACL2 source directory in interface/emacs/README.doc; and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 command loop. Look in the ACL2 documentation under PROOF-TREE. ACL2 Version 2.5(r). Level 1. Cbd "/home/ruben/acl2-2.5r/acl2-sources/books/nonstd/misc/". Type :help for help. ACL2(r) !>(ld "no-sqrt.lisp" :ld-pre-eval-print t ) ACL2 Version 2.5(r). Level 2. Cbd "/home/ruben/acl2-2.5r/acl2-sources/books/nonstd/misc/". Type :help for help. ACL2(r) !>>(IN-PACKAGE "ACL2") "ACL2" ACL2(r) !>>(INCLUDE-BOOK "../arithmetic/top" :LOAD-COMPILED-FILE NIL) Loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/equalities.o start address -T a63bf7c Finished loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/equalities.o Loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/rational-listp.o start address -T a63ef90 Finished loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/rational-listp.o Loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/realp.o start address -T a498f54 Finished loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/realp.o Loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/real-listp.o start address -T a498f8c Finished loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/real-listp.o Loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/inequalities.o start address -T a640edc Finished loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/inequalities.o Loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/rationals-with-axioms-proved.o start address -T a640f14 Finished loading /home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/rationals-with-axioms-proved.o Summary Form: ( INCLUDE-BOOK "../arithmetic/top" ...) Rules: NIL Warnings: None Time: 1.67 seconds (prove: 0.00, print: 0.00, other: 1.67) "/home/ruben/acl2-2.5r/acl2-sources/books/nonstd/arithmetic/top.lisp" ACL2(r) !>>(ENCAPSULATE NIL (LOCAL (DEFUN EVEN-INDUCTION (X) "Induct by going two steps at a time" (IF (OR (ZP X) (EQUAL X 1)) X (1+ (EVEN-INDUCTION (1- (1- X))))))) (LOCAL (DEFTHM LEMMA-1 (IMPLIES (AND (INTEGERP P) (<= 0 P) (EVENP (* P P))) (EVENP P)) :HINTS (("Goal" :INDUCT (EVEN-INDUCTION P))) :RULE-CLASSES NIL)) (LOCAL (DEFTHM LEMMA-2 (IMPLIES (AND (INTEGERP P) (<= P 0) (EVENP (* P P))) (EVENP P)) :HINTS (("Goal" :USE (:INSTANCE LEMMA-1 (P (- P))))) :RULE-CLASSES NIL)) (LOCAL (DEFTHM LEMMA-3 (IMPLIES (AND (INTEGERP P) (EVENP P)) (EVENP (* P P))) :RULE-CLASSES NIL)) (DEFTHM EVEN-SQUARE-IMPLIES-EVEN (IMPLIES (INTEGERP P) (EQUAL (EVENP (* P P)) (EVENP P))) :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE LEMMA-2) (:INSTANCE LEMMA-3)))))) To verify that the five encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2(r) !>>>(LOCAL (DEFUN EVEN-INDUCTION (X) "Induct by going two steps at a time" (IF (OR (ZP X) (EQUAL X 1)) X (1+ (EVEN-INDUCTION (1- (1- X))))))) For the admission of EVEN-INDUCTION 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 (IMPLIES (NOT (OR (ZP X) (EQUAL X 1))) (E0-ORD-< (ACL2-COUNT (+ -1 -1 X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, E0-ORD-<, INTEGER- ABS, SYNTAXP and ZP, the :executable-counterparts of BINARY-+, CAR, CONSP, EQ, IF and UNARY--, primitive type reasoning and the :rewrite rules <-+-NEGATIVE-0-1, DISTRIBUTIVITY-OF-MINUS-OVER-+ and FOLD-CONSTS- IN-+, to the following two conjectures. Subgoal 2 (IMPLIES (AND (INTEGERP X) (< 0 X) (NOT (EQUAL X 1)) (< X 2)) (< (+ 2 (- X)) X)). But simplification reduces this to T, using linear arithmetic. Subgoal 1 (IMPLIES (AND (INTEGERP X) (< 0 X) (NOT (EQUAL X 1)) (<= 2 X)) (< (+ -2 X) X)). But simplification reduces this to T, using linear arithmetic. Q.E.D. That completes the proof of the measure theorem for EVEN-INDUCTION. Thus, we admit this function under the principle of definition. We observe that the type of EVEN-INDUCTION is described by the theorem (OR (ACL2-NUMBERP (EVEN-INDUCTION X)) (EQUAL (EVEN-INDUCTION X) X)). We used primitive type reasoning and the :type-prescription rule ZP. Summary Form: ( DEFUN EVEN-INDUCTION ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION E0-ORD-<) (:DEFINITION INTEGER-ABS) (:DEFINITION SYNTAXP) (:DEFINITION ZP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE <-+-NEGATIVE-0-1) (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE FOLD-CONSTS-IN-+) (:TYPE-PRESCRIPTION ZP)) Warnings: None Time: 0.05 seconds (prove: 0.01, print: 0.01, other: 0.03) EVEN-INDUCTION ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-1 (IMPLIES (AND (INTEGERP P) (<= 0 P) (EVENP (* P P))) (EVENP P)) :HINTS (("Goal" :INDUCT (EVEN-INDUCTION P))) :RULE-CLASSES NIL)) [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 (EVEN-INDUCTION P). If we let (:P P) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (OR (ZP P) (EQUAL P 1))) (:P (+ -1 -1 P))) (:P P)) (IMPLIES (OR (ZP P) (EQUAL P 1)) (:P P))). This induction is justified by the same argument used to admit EVEN- INDUCTION, namely, the measure (ACL2-COUNT P) 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 (OR (ZP P) (EQUAL P 1))) (IMPLIES (AND (INTEGERP (+ -1 -1 P)) (<= 0 (+ -1 -1 P)) (EVENP (* (+ -1 -1 P) (+ -1 -1 P)))) (EVENP (+ -1 -1 P)))) (IMPLIES (AND (INTEGERP P) (<= 0 P) (EVENP (* P P))) (EVENP P))). By the simple :definition EVENP and the simple :rewrite rules <-+-NEGATIVE- 0-1 and ASSOCIATIVITY-OF-* we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (NOT (OR (ZP P) (EQUAL P 1))) (OR (NOT (AND (INTEGERP (+ -1 -1 P)) (<= 1 (+ -1 P)) (INTEGERP (* (+ -1 -1 P) (+ -1 -1 P) 1/2)))) (INTEGERP (* (+ -1 -1 P) 1/2))) (INTEGERP P) (<= 0 P) (INTEGERP (* P P 1/2))) (INTEGERP (* P 1/2))). This simplifies, using the :definitions FIX, NOT, SYNTAXP and ZP, the :executable-counterparts of BINARY-*, BINARY-+, CAR, CONSP, EQ, IF, UNARY-- and ZP, primitive type reasoning, the :rewrite rules ASSOCIATIVITY- OF-+, COMMUTATIVITY-2-OF-*, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF- *, DISTRIBUTIVITY, DISTRIBUTIVITY-OF-MINUS-OVER-+, FOLD-CONSTS-IN-*, FOLD-CONSTS-IN-+, FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT and UNICITY- OF-1 and the :type-prescription rule NONNEGATIVE-PRODUCT, to the following two conjectures. Subgoal *1/2.2 (IMPLIES (AND (< 0 P) (NOT (EQUAL P 1)) (< (+ -1 P) 1) (INTEGERP P) (INTEGERP (* 1/2 P P))) (INTEGERP (* 1/2 P))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Subgoal *1/2.1 (IMPLIES (AND (< 0 P) (NOT (EQUAL P 1)) (INTEGERP (+ -1 (* 1/2 P))) (INTEGERP P) (INTEGERP (* 1/2 P P))) (INTEGERP (* 1/2 P))). But simplification reduces this to T, using primitive type reasoning. Subgoal *1/1 (IMPLIES (OR (ZP P) (EQUAL P 1)) (IMPLIES (AND (INTEGERP P) (<= 0 P) (EVENP (* P P))) (EVENP P))). By the simple :definition EVENP and the simple :rewrite rule ASSOCIATIVITY- OF-* we reduce the conjecture to Subgoal *1/1' (IMPLIES (AND (OR (ZP P) (EQUAL P 1)) (INTEGERP P) (<= 0 P) (INTEGERP (* P P 1/2))) (INTEGERP (* P 1/2))). But simplification reduces this to T, using the :definition ZP, the :executable-counterparts of <, BINARY-*, INTEGERP, NOT and ZP and primitive type reasoning. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM LEMMA-1 ...) Rules: ((:DEFINITION EVENP) (:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:DEFINITION ZP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE <-+-NEGATIVE-0-1) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE DISTRIBUTIVITY) (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE FOLD-CONSTS-IN-+) (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT) (:REWRITE UNICITY-OF-1) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: None Time: 0.09 seconds (prove: 0.05, print: 0.02, other: 0.02) LEMMA-1 ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-2 (IMPLIES (AND (INTEGERP P) (<= P 0) (EVENP (* P P))) (EVENP P)) :HINTS (("Goal" :USE (:INSTANCE LEMMA-1 (P (- P))))) :RULE-CLASSES NIL)) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be derived from LEMMA-1 via instantiation. The augmented goal is shown below. Goal' (IMPLIES (IMPLIES (AND (INTEGERP (- P)) (<= 0 (- P)) (EVENP (* (- P) (- P)))) (EVENP (- P))) (IMPLIES (AND (INTEGERP P) (<= P 0) (EVENP (* P P))) (EVENP P))). By the simple :definition EVENP and the simple :rewrite rules <-MINUS- ZERO, ASSOCIATIVITY-OF-*, FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT, FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT and FUNCTIONAL-SELF-INVERSION- OF-MINUS we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (INTEGERP (- P)) (<= P 0) (INTEGERP (* (FIX (* P P)) 1/2)))) (INTEGERP (- (* P 1/2)))) (INTEGERP P) (<= P 0) (INTEGERP (* P P 1/2))) (INTEGERP (* P 1/2))). This simplifies, using the :definition FIX, the :executable-counterpart of NOT, primitive type reasoning, the :rewrite rules COMMUTATIVITY- 2-OF-* and COMMUTATIVITY-OF-* and the :type-prescription rule NONNEGATIVE- PRODUCT, to Goal''' (IMPLIES (AND (INTEGERP (- (* 1/2 P))) (INTEGERP P) (<= P 0) (INTEGERP (* 1/2 P P))) (INTEGERP (* 1/2 P))). But simplification reduces this to T, using primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM LEMMA-2 ...) Rules: ((:DEFINITION EVENP) (:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE <-MINUS-ZERO) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT) (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT) (:REWRITE FUNCTIONAL-SELF-INVERSION-OF-MINUS) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) LEMMA-2 ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-3 (IMPLIES (AND (INTEGERP P) (EVENP P)) (EVENP (* P P))) :RULE-CLASSES NIL)) By the simple :definition EVENP and the simple :rewrite rule ASSOCIATIVITY- OF-* we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP P) (INTEGERP (* P 1/2))) (INTEGERP (* P P 1/2))). But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM LEMMA-3 ...) Rules: ((:DEFINITION EVENP) (:DEFINITION IMPLIES) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-*)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) LEMMA-3 ACL2(r) !>>>(DEFTHM EVEN-SQUARE-IMPLIES-EVEN (IMPLIES (INTEGERP P) (EQUAL (EVENP (* P P)) (EVENP P))) :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE LEMMA-2) (:INSTANCE LEMMA-3))))) ACL2 Warning [Non-rec] in ( DEFTHM EVEN-SQUARE-IMPLIES-EVEN ...): The :REWRITE rule generated from EVEN-SQUARE-IMPLIES-EVEN will be triggered only by terms containing the non-recursive function symbol EVENP. Unless this function is disabled, EVEN-SQUARE-IMPLIES-EVEN is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM EVEN-SQUARE-IMPLIES-EVEN ...): The previously added rule EVENP subsumes the newly proposed :REWRITE rule EVEN-SQUARE-IMPLIES-EVEN, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from LEMMA-1, LEMMA- 2 and LEMMA-3 via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (AND (INTEGERP P) (<= 0 P) (EVENP (* P P))) (EVENP P)) (IMPLIES (AND (INTEGERP P) (<= P 0) (EVENP (* P P))) (EVENP P)) (IMPLIES (AND (INTEGERP P) (EVENP P)) (EVENP (* P P)))) (IMPLIES (INTEGERP P) (EQUAL (EVENP (* P P)) (EVENP P)))). By the simple :definition EVENP and the simple :rewrite rule ASSOCIATIVITY- OF-* we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (INTEGERP P) (<= 0 P) (INTEGERP (* P P 1/2)))) (INTEGERP (* P 1/2))) (OR (NOT (AND (INTEGERP P) (<= P 0) (INTEGERP (* P P 1/2)))) (INTEGERP (* P 1/2))) (OR (NOT (AND (INTEGERP P) (INTEGERP (* P 1/2)))) (INTEGERP (* P P 1/2))) (INTEGERP P)) (EQUAL (INTEGERP (* P P 1/2)) (INTEGERP (* P 1/2)))). But simplification reduces this to T, using the :definition NOT, the :executable-counterpart of EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-2-OF-* and COMMUTATIVITY-OF-* and the :type-prescription rule NONNEGATIVE-PRODUCT. Q.E.D. Summary Form: ( DEFTHM EVEN-SQUARE-IMPLIES-EVEN ...) Rules: ((:DEFINITION EVENP) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: Subsume and Non-rec Time: 0.06 seconds (prove: 0.04, print: 0.00, other: 0.02) EVEN-SQUARE-IMPLIES-EVEN End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: Subsume and Non-rec Time: 0.26 seconds (prove: 0.12, print: 0.03, other: 0.11) T ACL2(r) !>>(DEFTHM EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4 (IMPLIES (AND (INTEGERP P) (EVENP (* P P))) (EVENP (* 1/2 P P))) :HINTS (("Goal" :USE ((:INSTANCE EVEN-SQUARE-IMPLIES-EVEN) (:INSTANCE (:THEOREM (IMPLIES (INTEGERP X) (INTEGERP (* X X)))) (X (* 1/2 P)))) :IN-THEORY (DISABLE EVEN-SQUARE-IMPLIES-EVEN)))) ACL2 Warning [Non-rec] in ( DEFTHM EVEN-SQUARE-IMPLIES-EVEN-SQUARE- MULTIPLE-OF-4 ...): The :REWRITE rule generated from EVEN-SQUARE-IMPLIES- EVEN-SQUARE-MULTIPLE-OF-4 will be triggered only by terms containing the non-recursive function symbol EVENP. Unless this function is disabled, EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4 is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM EVEN-SQUARE-IMPLIES-EVEN-SQUARE- MULTIPLE-OF-4 ...): The previously added rule EVENP subsumes the newly proposed :REWRITE rule EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF- 4, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from EVEN-SQUARE-IMPLIES- EVEN and (IMPLIES (INTEGERP X) (INTEGERP (* X X))) via instantiation, provided we can establish the constraint generated. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (INTEGERP P) (EQUAL (EVENP (* P P)) (EVENP P))) (IMPLIES (INTEGERP (* 1/2 P)) (INTEGERP (* (* 1/2 P) 1/2 P)))) (IMPLIES (AND (INTEGERP P) (EVENP (* P P))) (EVENP (* 1/2 P P)))). By the simple :definition EVENP and the simple :rewrite rule ASSOCIATIVITY- OF-* we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (INTEGERP P)) (EQUAL (INTEGERP (* P P 1/2)) (INTEGERP (* P 1/2)))) (OR (NOT (INTEGERP (* 1/2 P))) (INTEGERP (* 1/2 P 1/2 P))) (INTEGERP P) (INTEGERP (* P P 1/2))) (INTEGERP (* 1/2 P P 1/2))). But simplification reduces this to T, using the :definition SYNTAXP, the :executable-counterparts of BINARY-*, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules COMMUTATIVITY-2-OF-*, COMMUTATIVITY- OF-* and FOLD-CONSTS-IN-* and the :type-prescription rule NONNEGATIVE- PRODUCT. Q.E.D. The storage of EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4 depends upon the :type-prescription rule EVENP. Summary Form: ( DEFTHM EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4 ...) Rules: ((:DEFINITION EVENP) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE FOLD-CONSTS-IN-*) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: Subsume and Non-rec Time: 0.25 seconds (prove: 0.03, print: 0.01, other: 0.21) EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4 ACL2(r) !>>(DEFTHM EVENP-2X (IMPLIES (INTEGERP X) (EVENP (* 2 X)))) ACL2 Warning [Non-rec] in ( DEFTHM EVENP-2X ...): The :REWRITE rule generated from EVENP-2X will be triggered only by terms containing the non-recursive function symbol EVENP. Unless this function is disabled, EVENP-2X is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM EVENP-2X ...): The previously added rule EVENP subsumes the newly proposed :REWRITE rule EVENP-2X, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition EVENP and the simple :rewrite rule ASSOCIATIVITY- OF-* we reduce the conjecture to Goal' (IMPLIES (INTEGERP X) (INTEGERP (* 2 X 1/2))). But simplification reduces this to T, using the :definitions FIX and SYNTAXP, the :executable-counterparts of BINARY-*, CAR, CONSP, EQ and IF and the :rewrite rules COMMUTATIVITY-OF-*, FOLD-CONSTS-IN-* and UNICITY-OF-1. Q.E.D. The storage of EVENP-2X depends upon the :type-prescription rule EVENP. Summary Form: ( DEFTHM EVENP-2X ...) Rules: ((:DEFINITION EVENP) (:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION SYNTAXP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE UNICITY-OF-1) (:TYPE-PRESCRIPTION EVENP)) Warnings: Subsume and Non-rec Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) EVENP-2X ACL2(r) !>>(DEFTHM NUMERATOR-SQRT-2-IS-EVEN (IMPLIES (AND (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 (* Q Q)))) (EVENP P)) :HINTS (("Goal" :USE ((:INSTANCE EVEN-SQUARE-IMPLIES-EVEN) (:INSTANCE EVENP-2X (X (* Q Q)))) :IN-THEORY (DISABLE EVEN-SQUARE-IMPLIES-EVEN EVENP-2X EVENP)))) ACL2 Warning [Non-rec] in ( DEFTHM NUMERATOR-SQRT-2-IS-EVEN ...): The :REWRITE rule generated from NUMERATOR-SQRT-2-IS-EVEN will be triggered only by terms containing the non-recursive function symbol EVENP. Unless this function is disabled, NUMERATOR-SQRT-2-IS-EVEN is unlikely ever to be used. ACL2 Warning [Free] in ( DEFTHM NUMERATOR-SQRT-2-IS-EVEN ...): The :REWRITE rule generated from NUMERATOR-SQRT-2-IS-EVEN contains the free variable Q. This variable will be chosen by searching for an instance of (INTEGERP Q) among the hypotheses of the conjecture being rewritten. This is generally a severe restriction on the applicability of the :REWRITE rule. ACL2 Warning [Subsume] in ( DEFTHM NUMERATOR-SQRT-2-IS-EVEN ...): The previously added rule EVENP subsumes the newly proposed :REWRITE rule NUMERATOR-SQRT-2-IS-EVEN, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from EVEN-SQUARE-IMPLIES- EVEN and EVENP-2X via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (INTEGERP P) (EQUAL (EVENP (* P P)) (EVENP P))) (IMPLIES (INTEGERP (* Q Q)) (EVENP (* 2 Q Q)))) (IMPLIES (AND (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 Q Q))) (EVENP P))). By case analysis we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (INTEGERP P)) (EQUAL (EVENP (* P P)) (EVENP P))) (OR (NOT (INTEGERP (* Q Q))) (EVENP (* 2 Q Q))) (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 Q Q))) (EVENP P)). But simplification reduces this to T, using primitive type reasoning and the :type-prescription rule NONNEGATIVE-PRODUCT. Q.E.D. The storage of NUMERATOR-SQRT-2-IS-EVEN depends upon the :type-prescription rule EVENP. Summary Form: ( DEFTHM NUMERATOR-SQRT-2-IS-EVEN ...) Rules: ((:DEFINITION IMPLIES) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: Subsume, Free and Non-rec Time: 0.07 seconds (prove: 0.02, print: 0.00, other: 0.05) NUMERATOR-SQRT-2-IS-EVEN ACL2(r) !>>(DEFTHM DENOMINATOR-SQRT-2-IS-EVEN (IMPLIES (AND (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 (* Q Q)))) (EVENP Q)) :HINTS (("Goal" :USE ((:INSTANCE EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4) (:INSTANCE EVEN-SQUARE-IMPLIES-EVEN (P Q)) (:INSTANCE EVENP-2X (X (* Q Q))) (:INSTANCE EQUAL-*-/-1 (X 2) (Y (* P P)) (Z (* Q Q)))) :IN-THEORY (DISABLE EVEN-SQUARE-IMPLIES-EVEN-SQUARE-MULTIPLE-OF-4 EVEN-SQUARE-IMPLIES-EVEN EVENP-2X EVENP EQUAL-*-/-1)))) ACL2 Warning [Non-rec] in ( DEFTHM DENOMINATOR-SQRT-2-IS-EVEN ...): The :REWRITE rule generated from DENOMINATOR-SQRT-2-IS-EVEN will be triggered only by terms containing the non-recursive function symbol EVENP. Unless this function is disabled, DENOMINATOR-SQRT-2-IS-EVEN is unlikely ever to be used. ACL2 Warning [Free] in ( DEFTHM DENOMINATOR-SQRT-2-IS-EVEN ...): The :REWRITE rule generated from DENOMINATOR-SQRT-2-IS-EVEN contains the free variable P. This variable will be chosen by searching for an instance of (INTEGERP P) among the hypotheses of the conjecture being rewritten. This is generally a severe restriction on the applicability of the :REWRITE rule. ACL2 Warning [Subsume] in ( DEFTHM DENOMINATOR-SQRT-2-IS-EVEN ...): The previously added rule EVENP subsumes the newly proposed :REWRITE rule DENOMINATOR-SQRT-2-IS-EVEN, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from EVEN-SQUARE-IMPLIES- EVEN-SQUARE-MULTIPLE-OF-4, EVEN-SQUARE-IMPLIES-EVEN, EVENP-2X and EQUAL- *-/-1 via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (AND (INTEGERP P) (EVENP (* P P))) (EVENP (* 1/2 P P))) (IMPLIES (INTEGERP Q) (EQUAL (EVENP (* Q Q)) (EVENP Q))) (IMPLIES (INTEGERP (* Q Q)) (EVENP (* 2 Q Q))) (IMPLIES T (EQUAL (EQUAL (* 1/2 P P) (* Q Q)) (AND (ACL2-NUMBERP (* Q Q)) (EQUAL (FIX (* P P)) (* 2 Q Q)))))) (IMPLIES (AND (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 Q Q))) (EVENP Q))). By case analysis we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (INTEGERP P) (EVENP (* P P)))) (EVENP (* 1/2 P P))) (OR (NOT (INTEGERP Q)) (EQUAL (EVENP (* Q Q)) (EVENP Q))) (OR (NOT (INTEGERP (* Q Q))) (EVENP (* 2 Q Q))) (OR (NOT T) (EQUAL (EQUAL (* 1/2 P P) (* Q Q)) (AND (ACL2-NUMBERP (* Q Q)) (EQUAL (FIX (* P P)) (* 2 Q Q))))) (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 Q Q))) (EVENP Q)). This simplifies, using the :definition FIX, primitive type reasoning and the :type-prescription rules EVENP and NONNEGATIVE-PRODUCT, to Goal''' (IMPLIES (AND (EVENP (* 1/2 P P)) (NOT (EVENP (* Q Q))) (EVENP (* P P)) (EQUAL (* 1/2 P P) (* Q Q)) (INTEGERP P) (INTEGERP Q) (EQUAL (* P P) (* 2 Q Q))) (EVENP Q)). But simplification reduces this to T, using trivial observations. Q.E.D. The storage of DENOMINATOR-SQRT-2-IS-EVEN depends upon the :type-prescription rule EVENP. Summary Form: ( DEFTHM DENOMINATOR-SQRT-2-IS-EVEN ...) Rules: ((:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: Subsume, Free and Non-rec Time: 0.15 seconds (prove: 0.10, print: 0.00, other: 0.05) DENOMINATOR-SQRT-2-IS-EVEN ACL2(r) !>>(ENCAPSULATE NIL (LOCAL (DEFTHM LEMMA-1 (IMPLIES (RATIONALP X) (EQUAL (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X)) (NUMERATOR X) (NUMERATOR X)) (* X X))) :HINTS (("Goal" :USE ((:INSTANCE RATIONAL-IMPLIES2) (:INSTANCE *-R-DENOMINATOR-R (R X))) :IN-THEORY (DISABLE RATIONAL-IMPLIES2 *-R-DENOMINATOR-R))))) (DEFTHM SQRT-2-NOT-RATIONAL (IMPLIES (EQUAL (* X X) 2) (NOT (RATIONALP X))) :HINTS (("Goal" :USE ((:INSTANCE NUMERATOR-SQRT-2-IS-EVEN (P (NUMERATOR X)) (Q (DENOMINATOR X))) (:INSTANCE DENOMINATOR-SQRT-2-IS-EVEN (P (NUMERATOR X)) (Q (DENOMINATOR X))) (:INSTANCE LOWEST-TERMS (N 2) (R (/ (NUMERATOR X) 2)) (Q (/ (DENOMINATOR X) 2))) (:INSTANCE EQUAL-*-/-1 (X (/ (* (DENOMINATOR X) (DENOMINATOR X)))) (Y 2) (Z (* (NUMERATOR X) (NUMERATOR X))))) :IN-THEORY (DISABLE EQUAL-*-/-1 NUMERATOR-SQRT-2-IS-EVEN DENOMINATOR-SQRT-2-IS-EVEN))))) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-1 (IMPLIES (RATIONALP X) (EQUAL (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X)) (NUMERATOR X) (NUMERATOR X)) (* X X))) :HINTS (("Goal" :USE ((:INSTANCE RATIONAL-IMPLIES2) (:INSTANCE *-R-DENOMINATOR-R (R X))) :IN-THEORY (DISABLE RATIONAL-IMPLIES2 *-R-DENOMINATOR-R))))) ACL2 Warning [Subsume] in ( DEFTHM LEMMA-1 ...): The previously added rules COMMUTATIVITY-2-OF-* and COMMUTATIVITY-OF-* subsume the newly proposed :REWRITE rule LEMMA-1, in the sense that the old rules rewrite more general targets. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from RATIONAL-IMPLIES2 and *-R-DENOMINATOR-R via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (RATIONALP X) (EQUAL (* (/ (DENOMINATOR X)) (NUMERATOR X)) X)) (EQUAL (* X (DENOMINATOR X)) (IF (RATIONALP X) (NUMERATOR X) (FIX X)))) (IMPLIES (RATIONALP X) (EQUAL (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X)) (NUMERATOR X) (NUMERATOR X)) (* X X)))). By case analysis we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (RATIONALP X)) (EQUAL (* (/ (DENOMINATOR X)) (NUMERATOR X)) X)) (EQUAL (* X (DENOMINATOR X)) (IF (RATIONALP X) (NUMERATOR X) (FIX X))) (RATIONALP X)) (EQUAL (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X)) (NUMERATOR X) (NUMERATOR X)) (* X X))). This simplifies, using the :definition FIX, primitive type reasoning, the :rewrite rules COMMUTATIVITY-2-OF-*, COMMUTATIVITY-OF-* and EQUAL- *-/-1 and the :type-prescription rule NONNEGATIVE-PRODUCT, to Goal''' (IMPLIES (AND (EQUAL (NUMERATOR X) (* X (DENOMINATOR X))) (RATIONALP X)) (EQUAL (* (NUMERATOR X) (NUMERATOR X)) (* X (DENOMINATOR X) (NUMERATOR X)))). We now use the first hypothesis by substituting (* X (DENOMINATOR X)) for (NUMERATOR X) and keeping the hypothesis. This produces Goal'4' (IMPLIES (AND (EQUAL (NUMERATOR X) (* X (DENOMINATOR X))) (RATIONALP X)) (EQUAL (* (* X (DENOMINATOR X)) X (DENOMINATOR X)) (* X (DENOMINATOR X) X (DENOMINATOR X)))). By the simple :rewrite rule ASSOCIATIVITY-OF-* we reduce the conjecture to Goal'5' (IMPLIES (AND (EQUAL (NUMERATOR X) (* X (DENOMINATOR X))) (RATIONALP X)) (EQUAL (* X (DENOMINATOR X) X (DENOMINATOR X)) (* X (DENOMINATOR X) X (DENOMINATOR X)))). But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM LEMMA-1 ...) Rules: ((:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE EQUAL-*-/-1) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: Subsume Time: 0.09 seconds (prove: 0.04, print: 0.00, other: 0.05) LEMMA-1 ACL2(r) !>>>(DEFTHM SQRT-2-NOT-RATIONAL (IMPLIES (EQUAL (* X X) 2) (NOT (RATIONALP X))) :HINTS (("Goal" :USE ((:INSTANCE NUMERATOR-SQRT-2-IS-EVEN (P (NUMERATOR X)) (Q (DENOMINATOR X))) (:INSTANCE DENOMINATOR-SQRT-2-IS-EVEN (P (NUMERATOR X)) (Q (DENOMINATOR X))) (:INSTANCE LOWEST-TERMS (N 2) (R (/ (NUMERATOR X) 2)) (Q (/ (DENOMINATOR X) 2))) (:INSTANCE EQUAL-*-/-1 (X (/ (* (DENOMINATOR X) (DENOMINATOR X)))) (Y 2) (Z (* (NUMERATOR X) (NUMERATOR X))))) :IN-THEORY (DISABLE EQUAL-*-/-1 NUMERATOR-SQRT-2-IS-EVEN DENOMINATOR-SQRT-2-IS-EVEN)))) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from NUMERATOR-SQRT- 2-IS-EVEN, DENOMINATOR-SQRT-2-IS-EVEN, LOWEST-TERMS and EQUAL-*-/-1 via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (AND (INTEGERP (NUMERATOR X)) (INTEGERP (DENOMINATOR X)) (EQUAL (* (NUMERATOR X) (NUMERATOR X)) (* 2 (DENOMINATOR X) (DENOMINATOR X)))) (EVENP (NUMERATOR X))) (IMPLIES (AND (INTEGERP (NUMERATOR X)) (INTEGERP (DENOMINATOR X)) (EQUAL (* (NUMERATOR X) (NUMERATOR X)) (* 2 (DENOMINATOR X) (DENOMINATOR X)))) (EVENP (DENOMINATOR X))) (IMPLIES (AND (RATIONALP X) (INTEGERP (* (NUMERATOR X) (/ 2))) (INTEGERP (* (DENOMINATOR X) (/ 2))) (EQUAL (NUMERATOR X) (* 2 (NUMERATOR X) (/ 2))) (EQUAL (DENOMINATOR X) (* 2 (DENOMINATOR X) (/ 2)))) NIL) (IMPLIES (AND (ACL2-NUMBERP (/ (* (DENOMINATOR X) (DENOMINATOR X)))) (NOT (EQUAL (/ (* (DENOMINATOR X) (DENOMINATOR X))) 0))) (EQUAL (EQUAL (* (/ (/ (* (DENOMINATOR X) (DENOMINATOR X)))) 2) (* (NUMERATOR X) (NUMERATOR X))) (AND (ACL2-NUMBERP (* (NUMERATOR X) (NUMERATOR X))) (EQUAL (FIX 2) (* (/ (* (DENOMINATOR X) (DENOMINATOR X))) (NUMERATOR X) (NUMERATOR X))))))) (IMPLIES (EQUAL (* X X) 2) (NOT (RATIONALP X)))). By the simple :definition EVENP, the :executable-counterparts of FIX, IF and UNARY-/ and the simple :rewrite rules ASSOCIATIVITY-OF-*, DISTRIBUTIVIT\ Y-OF-/-OVER-* and FUNCTIONAL-SELF-INVERSION-OF-/ we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (INTEGERP (NUMERATOR X)) (INTEGERP (DENOMINATOR X)) (EQUAL (* (NUMERATOR X) (NUMERATOR X)) (* 2 (DENOMINATOR X) (DENOMINATOR X))))) (INTEGERP (* (NUMERATOR X) 1/2))) (OR (NOT (AND (INTEGERP (NUMERATOR X)) (INTEGERP (DENOMINATOR X)) (EQUAL (* (NUMERATOR X) (NUMERATOR X)) (* 2 (DENOMINATOR X) (DENOMINATOR X))))) (INTEGERP (* (DENOMINATOR X) 1/2))) (NOT (AND (RATIONALP X) (INTEGERP (* (NUMERATOR X) 1/2)) (INTEGERP (* (DENOMINATOR X) 1/2)) (EQUAL (NUMERATOR X) (* 2 (NUMERATOR X) 1/2)) (EQUAL (DENOMINATOR X) (* 2 (DENOMINATOR X) 1/2)))) (OR (NOT (AND (ACL2-NUMBERP (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X)))) (NOT (EQUAL (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X))) 0)))) (EQUAL (EQUAL (* (FIX (DENOMINATOR X)) (FIX (DENOMINATOR X)) 2) (* (NUMERATOR X) (NUMERATOR X))) (AND (ACL2-NUMBERP (* (NUMERATOR X) (NUMERATOR X))) (EQUAL 2 (* (/ (DENOMINATOR X)) (/ (DENOMINATOR X)) (NUMERATOR X) (NUMERATOR X)))))) (EQUAL (* X X) 2)) (NOT (RATIONALP X))). But simplification reduces this to T, using the :definitions FIX and SYNTAXP, the :executable-counterparts of BINARY-*, CAR, CONSP, EQ, EQUAL, IF and NOT, primitive type reasoning, the :rewrite rules COMMUTATIVITY- 2-OF-*, COMMUTATIVITY-OF-*, FOLD-CONSTS-IN-*, LEMMA-1 and UNICITY-OF- 1 and the :type-prescription rule NONNEGATIVE-PRODUCT. Q.E.D. Summary Form: ( DEFTHM SQRT-2-NOT-RATIONAL ...) Rules: ((:DEFINITION EVENP) (:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-*) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE DISTRIBUTIVITY-OF-/-OVER-*) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE FUNCTIONAL-SELF-INVERSION-OF-/) (:REWRITE LEMMA-1) (:REWRITE UNICITY-OF-1) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: None Time: 0.16 seconds (prove: 0.09, print: 0.02, other: 0.05) SQRT-2-NOT-RATIONAL End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: Subsume Time: 0.26 seconds (prove: 0.13, print: 0.02, other: 0.11) T ACL2(r) !>>(ENCAPSULATE NIL (LOCAL (DEFTHM LEMMA-1 (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (+ (- (* X X) (* Y Y)) (* #C(0 1) (+ (* X Y) (* X Y))))) :RULE-CLASSES NIL)) (LOCAL (DEFTHM LEMMA-2 (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (COMPLEX (- (* X X) (* Y Y)) (+ (* X Y) (* X Y))))) :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE COMPLEX-DEFINITION (X (- (* X X) (* Y Y))) (Y (+ (* X Y) (* X Y))))))) :RULE-CLASSES NIL)) (DEFTHM COMPLEX-SQUARE-DEFINITION (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (COMPLEX X Y) (COMPLEX X Y)) (COMPLEX (- (* X X) (* Y Y)) (+ (* X Y) (* X Y))))) :HINTS (("Goal" :USE ((:INSTANCE COMPLEX-DEFINITION) (:INSTANCE LEMMA-2)))) :RULE-CLASSES NIL)) To verify that the three encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-1 (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (+ (- (* X X) (* Y Y)) (* #C(0 1) (+ (* X Y) (* X Y))))) :RULE-CLASSES NIL)) By the simple :rewrite rule ASSOCIATIVITY-OF-+ we reduce the conjecture to Goal' (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (+ (* X X) (- (* Y Y)) (* #C(0 1) (+ (* X Y) (* X Y))))). But simplification reduces this to T, using the :definitions FIX and SYNTAXP, the :executable-counterparts of BINARY-*, CAR, CONSP, EQ and IF, primitive type reasoning and the :rewrite rules COMMUTATIVITY-2- OF-*, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+, DISTRIBUTIVITY, FOLD-CONSTS-IN-*, FUNCTIONAL-COMMUTATIVITY-OF-MINUS- *-LEFT and UNICITY-OF-1. Q.E.D. Summary Form: ( DEFTHM LEMMA-1 ...) Rules: ((:DEFINITION FIX) (:DEFINITION SYNTAXP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT) (:REWRITE UNICITY-OF-1)) Warnings: None Time: 0.05 seconds (prove: 0.03, print: 0.01, other: 0.01) LEMMA-1 ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-2 (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (COMPLEX (- (* X X) (* Y Y)) (+ (* X Y) (* X Y))))) :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE COMPLEX-DEFINITION (X (- (* X X) (* Y Y))) (Y (+ (* X Y) (* X Y))))))) :RULE-CLASSES NIL)) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from LEMMA-1 and COMPLEX- DEFINITION via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (+ (+ (* X X) (- (* Y Y))) (* #C(0 1) (+ (* X Y) (* X Y))))) (IMPLIES (AND (REALP (+ (* X X) (- (* Y Y)))) (REALP (+ (* X Y) (* X Y)))) (EQUAL (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y))) (+ (+ (* X X) (- (* Y Y))) (* #C(0 1) (+ (* X Y) (* X Y))))))) (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y)))))). By the simple :rewrite rule ASSOCIATIVITY-OF-+ we reduce the conjecture to Goal'' (IMPLIES (AND (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (+ (* X X) (- (* Y Y)) (* #C(0 1) (+ (* X Y) (* X Y))))) (OR (NOT (AND (REALP (+ (* X X) (- (* Y Y)))) (REALP (+ (* X Y) (* X Y))))) (EQUAL (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y))) (+ (* X X) (- (* Y Y)) (* #C(0 1) (+ (* X Y) (* X Y)))))) (REALP X) (REALP Y)) (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y))))). But simplification reduces this to T, using the :definitions FIX and SYNTAXP, the :executable-counterparts of BINARY-*, CAR, CONSP, EQ and IF, primitive type reasoning, the :rewrite rules COMMUTATIVITY-2-OF- *, COMMUTATIVITY-2-OF-+, COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+, DISTRIBUTIVIT\ Y, FOLD-CONSTS-IN-*, FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT and UNICITY- OF-1 and the :type-prescription rule NONNEGATIVE-PRODUCT. Q.E.D. Summary Form: ( DEFTHM LEMMA-2 ...) Rules: ((:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:DEFINITION SYNTAXP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQ) (:EXECUTABLE-COUNTERPART IF) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE COMMUTATIVITY-2-OF-*) (:REWRITE COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE FOLD-CONSTS-IN-*) (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT) (:REWRITE UNICITY-OF-1) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: None Time: 0.11 seconds (prove: 0.08, print: 0.00, other: 0.03) LEMMA-2 ACL2(r) !>>>(DEFTHM COMPLEX-SQUARE-DEFINITION (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (COMPLEX X Y) (COMPLEX X Y)) (COMPLEX (- (* X X) (* Y Y)) (+ (* X Y) (* X Y))))) :HINTS (("Goal" :USE ((:INSTANCE COMPLEX-DEFINITION) (:INSTANCE LEMMA-2)))) :RULE-CLASSES NIL) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from COMPLEX-DEFINITION and LEMMA-2 via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (COMPLEX X Y) (+ X (* #C(0 1) Y)))) (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y)))))) (IMPLIES (AND (REALP X) (REALP Y)) (EQUAL (* (COMPLEX X Y) (COMPLEX X Y)) (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y)))))). By case analysis we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (REALP X) (REALP Y))) (EQUAL (COMPLEX X Y) (+ X (* #C(0 1) Y)))) (OR (NOT (AND (REALP X) (REALP Y))) (EQUAL (* (+ X (* #C(0 1) Y)) (+ X (* #C(0 1) Y))) (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y))))) (REALP X) (REALP Y)) (EQUAL (* (COMPLEX X Y) (COMPLEX X Y)) (COMPLEX (+ (* X X) (- (* Y Y))) (+ (* X Y) (* X Y))))). But simplification reduces this to T, using primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM COMPLEX-SQUARE-DEFINITION ...) Rules: ((:DEFINITION IMPLIES) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.04 seconds (prove: 0.01, print: 0.01, other: 0.02) COMPLEX-SQUARE-DEFINITION End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.21 seconds (prove: 0.12, print: 0.02, other: 0.07) T ACL2(r) !>>(ENCAPSULATE NIL (LOCAL (DEFTHM LEMMA-1 (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0)) :HINTS (("Goal" :USE (:INSTANCE COMPLEX-SQUARE-DEFINITION (X (REALPART X)) (Y (IMAGPART X))))) :RULE-CLASSES NIL)) (LOCAL (DEFTHM LEMMA-2 (IMPLIES (AND (REALP X) (EQUAL (+ X X) 0)) (= X 0)))) (DEFTHM COMPLEX-SQUARES-REAL-IFF-IMAGINARY (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)) :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE LEMMA-2 (X (* (REALPART X) (IMAGPART X))))))))) To verify that the three encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-1 (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0)) :HINTS (("Goal" :USE (:INSTANCE COMPLEX-SQUARE-DEFINITION (X (REALPART X)) (Y (IMAGPART X))))) :RULE-CLASSES NIL)) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be derived from COMPLEX-SQUARE-DEFINITION via instantiation. The augmented goal is shown below. Goal' (IMPLIES (IMPLIES (AND (REALP (REALPART X)) (REALP (IMAGPART X))) (EQUAL (* (COMPLEX (REALPART X) (IMAGPART X)) (COMPLEX (REALPART X) (IMAGPART X))) (COMPLEX (+ (* (REALPART X) (REALPART X)) (- (* (IMAGPART X) (IMAGPART X)))) (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X)))))) (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0))). By case analysis we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (REALP (REALPART X)) (REALP (IMAGPART X)))) (EQUAL (* (COMPLEX (REALPART X) (IMAGPART X)) (COMPLEX (REALPART X) (IMAGPART X))) (COMPLEX (+ (* (REALPART X) (REALPART X)) (- (* (IMAGPART X) (IMAGPART X)))) (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X)))))) (COMPLEXP X) (REALP (* X X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0)). This simplifies, using primitive type reasoning and the :rewrite rules COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+ and REALPART-IMAGPART-ELIM, to Goal''' (IMPLIES (AND (EQUAL (* X X) (COMPLEX (+ (- (* (IMAGPART X) (IMAGPART X))) (* (REALPART X) (REALPART X))) (+ (* (IMAGPART X) (REALPART X)) (* (IMAGPART X) (REALPART X))))) (COMPLEXP X) (REALP (* X X))) (EQUAL (+ (* (IMAGPART X) (REALPART X)) (* (IMAGPART X) (REALPART X))) 0)). But simplification reduces this to T, using primitive type reasoning and the :type-prescription rule NONNEGATIVE-PRODUCT. Q.E.D. Summary Form: ( DEFTHM LEMMA-1 ...) Rules: ((:DEFINITION IMPLIES) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE REALPART-IMAGPART-ELIM) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: None Time: 0.04 seconds (prove: 0.01, print: 0.02, other: 0.01) LEMMA-1 ACL2(r) !>>>(LOCAL (DEFTHM LEMMA-2 (IMPLIES (AND (REALP X) (EQUAL (+ X X) 0)) (= X 0)))) ACL2 Warning [Non-rec] in ( DEFTHM LEMMA-2 ...): The :REWRITE rule generated from LEMMA-2 will be triggered only by terms containing the non-recursive function symbol =. Unless this function is disabled, LEMMA-2 is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM LEMMA-2 ...): The previously added rule = subsumes the newly proposed :REWRITE rule LEMMA-2, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition = we reduce the conjecture to Goal' (IMPLIES (AND (REALP X) (EQUAL (+ X X) 0)) (EQUAL X 0)). But simplification reduces this to T, using linear arithmetic. Q.E.D. The storage of LEMMA-2 depends upon primitive type reasoning. Summary Form: ( DEFTHM LEMMA-2 ...) Rules: ((:DEFINITION =) (:DEFINITION IMPLIES) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) LEMMA-2 ACL2(r) !>>>(DEFTHM COMPLEX-SQUARES-REAL-IFF-IMAGINARY (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)) :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE LEMMA-2 (X (* (REALPART X) (IMAGPART X)))))))) [Note: A hint was supplied for our processing of the goal above. Thanks!] ACL2 Warning [Use] in ( DEFTHM COMPLEX-SQUARES-REAL-IFF-IMAGINARY ...): It is unusual to :USE an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling (:REWRITE LEMMA-2). We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from LEMMA-1 and LEMMA- 2 via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0)) (IMPLIES (AND (REALP (* (REALPART X) (IMAGPART X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0)) (= (* (REALPART X) (IMAGPART X)) 0))) (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0))). By the simple :definition = we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (COMPLEXP X) (REALP (* X X)))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0)) (OR (NOT (AND (REALP (* (REALPART X) (IMAGPART X))) (EQUAL (+ (* (REALPART X) (IMAGPART X)) (* (REALPART X) (IMAGPART X))) 0))) (EQUAL (* (REALPART X) (IMAGPART X)) 0)) (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)). This simplifies, using the :definition FIX, the :executable-counterparts of EQUAL and FIX, primitive type reasoning and the :rewrite rules COMMUTATIVIT\ Y-OF-* and ZERO-IS-ONLY-ZERO-DIVISOR, to Goal''' (IMPLIES (AND (EQUAL (+ (* 0 (REALPART X)) (* 0 (REALPART X))) 0) (EQUAL (IMAGPART X) 0) (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)). By the :executable-counterparts of BINARY-+ and EQUAL and the simple :rewrite rule TIMES-ZERO we reduce the conjecture to Goal'4' (IMPLIES (AND (EQUAL (IMAGPART X) 0) (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)). The destructor terms (REALPART X) and (IMAGPART X) can be eliminated by using REALPART-IMAGPART-ELIM to replace X by (COMPLEX R I), generalizing (REALPART X) to R and (IMAGPART X) to I and restricting the type of the new variable R to be that of the term it replaces, as established by primitive type reasoning. This produces the following two goals. Subgoal 2 (IMPLIES (AND (NOT (ACL2-NUMBERP X)) (EQUAL (IMAGPART X) 0) (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)). But we reduce the conjecture to T, by case analysis. Subgoal 1 (IMPLIES (AND (REALP R) (NOT (EQUAL R 0)) (ACL2-NUMBERP (COMPLEX R I)) (EQUAL I 0) (COMPLEXP (COMPLEX R I))) (NOT (REALP (* (COMPLEX R I) (COMPLEX R I))))). But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM COMPLEX-SQUARES-REAL-IFF-IMAGINARY ...) Rules: ((:DEFINITION =) (:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:ELIM REALPART-IMAGPART-ELIM) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE TIMES-ZERO) (:REWRITE ZERO-IS-ONLY-ZERO-DIVISOR)) Warnings: Use Time: 0.06 seconds (prove: 0.03, print: 0.02, other: 0.01) COMPLEX-SQUARES-REAL-IFF-IMAGINARY End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: Use, Subsume and Non-rec Time: 0.12 seconds (prove: 0.04, print: 0.04, other: 0.04) T ACL2(r) !>>(DEFTHM IMAGINARY-SQUARES-ARE-NEGATIVE (IMPLIES (AND (COMPLEXP X) (EQUAL (REALPART X) 0)) (< (* X X) 0)) :HINTS (("Goal" :USE (:INSTANCE COMPLEX-SQUARE-DEFINITION (X 0) (Y (IMAGPART X)))))) [Note: A hint was supplied for our processing of the goal above. Thanks!] We now augment the goal above by adding the hypothesis indicated by the :USE hint. The hypothesis can be derived from COMPLEX-SQUARE-DEFINITION via instantiation. The augmented goal is shown below. Goal' (IMPLIES (IMPLIES (REALP (IMAGPART X)) (EQUAL (* (COMPLEX 0 (IMAGPART X)) (COMPLEX 0 (IMAGPART X))) (COMPLEX (+ 0 (- (* (IMAGPART X) (IMAGPART X)))) (+ (* 0 (IMAGPART X)) (* 0 (IMAGPART X)))))) (IMPLIES (AND (COMPLEXP X) (EQUAL (REALPART X) 0)) (< (* X X) 0))). By the :executable-counterpart of BINARY-+ and the simple :rewrite rules COMPLEX-0, TIMES-ZERO and UNICITY-OF-0 we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (REALP (IMAGPART X))) (EQUAL (* (COMPLEX 0 (IMAGPART X)) (COMPLEX 0 (IMAGPART X))) (REALFIX (FIX (- (* (IMAGPART X) (IMAGPART X))))))) (COMPLEXP X) (EQUAL (REALPART X) 0)) (< (* X X) 0)). This simplifies, using the :definitions FIX and REALFIX, primitive type reasoning and the :type-prescription rule NONNEGATIVE-PRODUCT, to Goal''' (IMPLIES (AND (EQUAL (* (COMPLEX 0 (IMAGPART X)) (COMPLEX 0 (IMAGPART X))) (- (* (IMAGPART X) (IMAGPART X)))) (COMPLEXP X) (EQUAL (REALPART X) 0)) (< (* X X) 0)). The destructor terms (REALPART X) and (IMAGPART X) can be eliminated by using REALPART-IMAGPART-ELIM to replace X by (COMPLEX I R), generalizing (REALPART X) to I and (IMAGPART X) to R and restricting the type of the new variable R to be that of the term it replaces, as established by primitive type reasoning. This produces the following two goals. Subgoal 2 (IMPLIES (AND (NOT (ACL2-NUMBERP X)) (EQUAL (* (COMPLEX 0 (IMAGPART X)) (COMPLEX 0 (IMAGPART X))) (- (* (IMAGPART X) (IMAGPART X)))) (COMPLEXP X) (EQUAL (REALPART X) 0)) (< (* X X) 0)). But we reduce the conjecture to T, by case analysis. Subgoal 1 (IMPLIES (AND (REALP R) (ACL2-NUMBERP (COMPLEX I R)) (EQUAL (* (COMPLEX 0 R) (COMPLEX 0 R)) (- (* R R))) (COMPLEXP (COMPLEX I R)) (EQUAL I 0)) (< (* (COMPLEX I R) (COMPLEX I R)) 0)). But simplification reduces this to T, using primitive type reasoning and the :type-prescription rule NONNEGATIVE-PRODUCT. Q.E.D. Summary Form: ( DEFTHM IMAGINARY-SQUARES-ARE-NEGATIVE ...) Rules: ((:DEFINITION FIX) (:DEFINITION IMPLIES) (:DEFINITION NOT) (:DEFINITION REALFIX) (:ELIM REALPART-IMAGPART-ELIM) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMPLEX-0) (:REWRITE TIMES-ZERO) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT)) Warnings: None Time: 0.08 seconds (prove: 0.02, print: 0.04, other: 0.02) IMAGINARY-SQUARES-ARE-NEGATIVE ACL2(r) !>>(DEFTHM SQRT-2-NOT-COMPLEXP (IMPLIES (COMPLEXP X) (NOT (EQUAL (* X X) 2))) :HINTS (("Goal" :USE ((:INSTANCE COMPLEX-SQUARES-REAL-IFF-IMAGINARY) (:INSTANCE IMAGINARY-SQUARES-ARE-NEGATIVE))))) [Note: A hint was supplied for our processing of the goal above. Thanks!] ACL2 Warning [Use] in ( DEFTHM SQRT-2-NOT-COMPLEXP ...): It is unusual to :USE an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling (:REWRITE COMPLEX-SQUARES-REAL-IFF-IMAGINARY) and (:REWRITE IMAGINARY-SQUARES-ARE-NEGATIVE). We now augment the goal above by adding the hypotheses indicated by the :USE hint. These hypotheses can be derived from COMPLEX-SQUARES- REAL-IFF-IMAGINARY and IMAGINARY-SQUARES-ARE-NEGATIVE via instantiation. The augmented goal is shown below. Goal' (IMPLIES (AND (IMPLIES (AND (COMPLEXP X) (REALP (* X X))) (EQUAL (REALPART X) 0)) (IMPLIES (AND (COMPLEXP X) (EQUAL (REALPART X) 0)) (< (* X X) 0))) (IMPLIES (COMPLEXP X) (NOT (EQUAL (* X X) 2)))). By case analysis we reduce the conjecture to Goal'' (IMPLIES (AND (OR (NOT (AND (COMPLEXP X) (REALP (* X X)))) (EQUAL (REALPART X) 0)) (OR (NOT (AND (COMPLEXP X) (EQUAL (REALPART X) 0))) (< (* X X) 0)) (COMPLEXP X)) (NOT (EQUAL (* X X) 2))). But simplification reduces this to T, using the :executable-counterparts of <, EQUAL and REALP, primitive type reasoning and the :rewrite rule COMPLEX-SQUARES-REAL-IFF-IMAGINARY. Q.E.D. Summary Form: ( DEFTHM SQRT-2-NOT-COMPLEXP ...) Rules: ((:DEFINITION IMPLIES) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART REALP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMPLEX-SQUARES-REAL-IFF-IMAGINARY)) Warnings: Use Time: 0.04 seconds (prove: 0.00, print: 0.01, other: 0.03) SQRT-2-NOT-COMPLEXP ACL2(r) !>>(DEFTHM IRRATIONAL-SQRT-2 (IMPLIES (EQUAL (* X X) 2) (AND (REALP X) (NOT (RATIONALP X)))) :HINTS (("Goal" :CASES ((RATIONALP X) (COMPLEXP X))))) ACL2 Warning [Subsume] in ( DEFTHM IRRATIONAL-SQRT-2 ...): The newly proposed :REWRITE rule IRRATIONAL-SQRT-2 probably subsumes the previously added :REWRITE rule SQRT-2-NOT-RATIONAL, in the sense that IRRATIONAL- SQRT-2 will now probably be applied whenever the old rule would have been. ACL2 Warning [Subsume] in ( DEFTHM IRRATIONAL-SQRT-2 ...): The previously added rule SQRT-2-NOT-RATIONAL subsumes the newly proposed :REWRITE rule IRRATIONAL-SQRT-2, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] We now split on the two terms supplied in the hint to produce three new non-trivial goals. Subgoal 3 (IMPLIES (AND (NOT (RATIONALP X)) (NOT (COMPLEXP X))) (IMPLIES (EQUAL (* X X) 2) (AND (REALP X) (NOT (RATIONALP X))))). By case analysis we reduce the conjecture to Subgoal 3' (IMPLIES (AND (NOT (RATIONALP X)) (NOT (COMPLEXP X)) (EQUAL (* X X) 2)) (AND (REALP X) (NOT (RATIONALP X)))). This simplifies, using the :executable-counterpart of NOT and the :rewrite rule SQRT-2-NOT-RATIONAL, to Subgoal 3'' (IMPLIES (AND (NOT (COMPLEXP X)) (EQUAL (* X X) 2)) (REALP X)). But simplification reduces this to T, using primitive type reasoning. Subgoal 2 (IMPLIES (RATIONALP X) (IMPLIES (EQUAL (* X X) 2) (AND (REALP X) (NOT (RATIONALP X))))). By case analysis we reduce the conjecture to Subgoal 2' (IMPLIES (AND (RATIONALP X) (EQUAL (* X X) 2)) (AND (REALP X) (NOT (RATIONALP X)))). But simplification reduces this to T, using the :rewrite rule SQRT- 2-NOT-RATIONAL. Subgoal 1 (IMPLIES (COMPLEXP X) (IMPLIES (EQUAL (* X X) 2) (AND (REALP X) (NOT (RATIONALP X))))). By case analysis we reduce the conjecture to Subgoal 1' (IMPLIES (AND (COMPLEXP X) (EQUAL (* X X) 2)) (AND (REALP X) (NOT (RATIONALP X)))). But simplification reduces this to T, using the :rewrite rule SQRT- 2-NOT-COMPLEXP. Q.E.D. Summary Form: ( DEFTHM IRRATIONAL-SQRT-2 ...) Rules: ((:DEFINITION IMPLIES) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE SQRT-2-NOT-COMPLEXP) (:REWRITE SQRT-2-NOT-RATIONAL)) Warnings: Subsume Time: 0.03 seconds (prove: 0.01, print: 0.01, other: 0.01) IRRATIONAL-SQRT-2 ACL2(r) !>>Bye. :EOF ACL2(r) !>