[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) !>