==============================================================
Starting image `/u/druss/bin/acl2'
  with no arguments
  in directory `/u/druss'
  on machine `localhost'.

International Allegro CL Enterprise Edition
7.0 [Linux (x86)] (Mar 11, 2005 11:33)
Copyright (C) 1985-2004, Franz Inc., Oakland, CA, USA.  All Rights Reserved.

This dynamic runtime copy of Allegro CL was built by:
   [TC9951] Advanced Micro Devices

;; Optimization settings: safety 0, space 0, speed 3, debug 2.
;; For a complete description of all compiler switches given the current optimization settings evaluate (EXPLAIN-COMPILER-SETTINGS).

 ACL2 Version 2.9.1 built March 11, 2005  11:33:40.
 Copyright (C) 2004  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* *ACL2-APPLICATION-DISTRIBUTED-BOOKS-DIR*).
 See the documentation topic note-2-9-1 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.9.1.  Level 1.  Cbd "/u/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(ld "/u/druss/sqrt2.lisp")

ACL2 Version 2.9.1.  Level 2.  Cbd "/u/druss/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>> "ACL2"
ACL2 !>>
; Fast loading /u/acl2/v6/acl2/current/books/ordinals/ordinal-definitions.fasl
; Fast loading /u/acl2/v6/acl2/current/books/ordinals/e0-ordinal.fasl
; Fast loading /u/acl2/v6/acl2/current/books/rtl/rel4/lib/arith.fasl

Summary
Form:  ( INCLUDE-BOOK "/u/acl2/v6/acl2/current/books/rtl/rel4/lib/arith"
...)
Rules: NIL
Warnings:  None
Time:  0.70 seconds (prove: 0.00, print: 0.00, other: 0.70)
 "/u/acl2/v6/acl2/current/books/rtl/rel4/lib/arith.lisp"
ACL2 !>>
For the admission of INDUCTION-SCHEME we will use the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (+ (NFIX M) (NFIX N)).  The non-trivial part of the measure
conjecture is

Goal
(AND (O-P (+ (NFIX M) (NFIX N)))
     (IMPLIES (AND (NOT (ZP M))
                   (NOT (ZP N))
                   (= (* M M) (* 2 N N)))
              (O< (+ (NFIX (+ (* 2 N) (- M)))
                     (NFIX (+ M (- N))))
                  (+ (NFIX M) (NFIX N))))).

By the simple :definition = and the simple :rewrite rule A2 we reduce
the conjecture to the following two conjectures.

Subgoal 2
(O-P (+ (NFIX M) (NFIX N))).

But simplification reduces this to T, using the :definitions NATP,
NFIX, O-FINP and O-P and primitive type reasoning.

Subgoal 1
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N)))
         (O< (+ (NFIX (+ (* 2 N) (* -1 M)))
                (NFIX (+ M (* -1 N))))
             (+ (NFIX M) (NFIX N)))).

This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER,
the :definitions FIX, NFIX, O-FINP and O<, primitive type reasoning
and the :rewrite rules COMMUTATIVITY-OF-+, REARRANGE-NEGATIVE-COEFS-
<, UNICITY-OF-0 and UNICITY-OF-1, to the following four conjectures.

Subgoal 1.4
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (< M N)
              (< (* 2 N) M))
         (< 0 (+ M N))).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning.

Subgoal 1.3
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (<= N M)
              (< (* 2 N) M))
         (< (+ (+ M (* -1 N)) 0) (+ M N))).

By the simple :rewrite rule ASSOCIATIVITY-OF-+ we reduce the conjecture
to

Subgoal 1.3'
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (<= N M)
              (< (* 2 N) M))
         (< (+ M (* -1 N) 0) (+ M N))).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER and linear arithmetic.

Subgoal 1.2
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (< M N)
              (<= M (* 2 N)))
         (< (+ 0 (* -1 M) (* 2 N)) (+ M N))).

By the simple :rewrite rule UNICITY-OF-0 we reduce the conjecture to

Subgoal 1.2'
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (< M N)
              (<= M (* 2 N)))
         (< (FIX (+ (* -1 M) (* 2 N))) (+ M N))).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning,
the :forward-chaining rule *-STRONGLY-MONOTONIC and the :type-prescription
rule NONNEGATIVE-PRODUCT.

Subgoal 1.1
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (<= N M)
              (<= M (* 2 N)))
         (< (+ (+ M (* -1 N)) (* -1 M) (* 2 N))
            (+ M N))).

By the simple :rewrite rule ASSOCIATIVITY-OF-+ we reduce the conjecture
to

Subgoal 1.1'
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N))
              (<= N M)
              (<= M (* 2 N)))
         (< (+ M (* -1 N) (* -1 M) (* 2 N))
            (+ M N))).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER and linear arithmetic.

Q.E.D.

That completes the proof of the measure theorem for INDUCTION-SCHEME.
Thus, we admit this function under the principle of definition. We
observe that the type of INDUCTION-SCHEME is described by the theorem
(INDUCTION-SCHEME M N).  

Summary
Form:  ( DEFUN INDUCTION-SCHEME ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIX)
        (:DEFINITION NATP)
        (:DEFINITION NFIX)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING *-STRONGLY-MONOTONIC . 2)
        (:FORWARD-CHAINING *-STRONGLY-MONOTONIC . 1)
        (:REWRITE A2)
        (:REWRITE ASSOCIATIVITY-OF-+)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE REARRANGE-NEGATIVE-COEFS-<)
        (:REWRITE UNICITY-OF-0)
        (:REWRITE UNICITY-OF-1)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Warnings:  None
Time:  0.08 seconds (prove: 0.04, print: 0.04, other: 0.00)
 INDUCTION-SCHEME
ACL2 !>>
ACL2 Warning [Non-rec] in ( DEFTHM LEMMA-1 ...):  The :REWRITE rule
generated from LEMMA-1 will be triggered only by terms containing the
non-recursive function symbol =.  Unless this function is disabled,
LEMMA-1 is unlikely ever to be used.


ACL2 Warning [Subsume] in ( DEFTHM LEMMA-1 ...):  The previously added
rule = subsumes the newly proposed :REWRITE rule LEMMA-1, 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!]

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 (INDUCTION-SCHEME M N).
This suggestion was produced using the :induction rule INDUCTION-SCHEME.
If we let  (:P M N) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (AND (NOT (ZP M))
                        (NOT (ZP N))
                        (= (* M M) (* 2 N N))))
              (:P M N))
     (IMPLIES (AND (AND (NOT (ZP M))
                        (NOT (ZP N))
                        (= (* M M) (* 2 N N)))
                   (:P (+ (* 2 N) (- M)) (+ M (- N))))
              (:P M N))).
This induction is justified by the same argument used to admit INDUCTION-
SCHEME, namely, the measure (BINARY-+ (NFIX M) (NFIX N)) is decreasing
according to the relation O< (which is known to be well-founded on
the domain recognized by O-P).  When applied to the goal at hand the
above induction scheme produces one nontautological subgoal.

Subgoal *1/
(IMPLIES (AND (AND (NOT (ZP M))
                   (NOT (ZP N))
                   (= (* M M) (* 2 N N)))
              (IMPLIES (AND (NOT (ZP (+ (* 2 N) (- M))))
                            (NOT (ZP (+ M (- N)))))
                       (NOT (= (* (+ (* 2 N) (- M)) (+ (* 2 N) (- M)))
                               (* 2 (+ M (- N)) (+ M (- N)))))))
         (IMPLIES (AND (NOT (ZP M)) (NOT (ZP N)))
                  (NOT (= (* M M) (* 2 N N))))).

By the simple :definition = and the simple :rewrite rule A2 we reduce
the conjecture to

Subgoal *1/'
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N)))
         (NOT (IMPLIES (AND (NOT (ZP (+ (* 2 N) (* -1 M))))
                            (NOT (ZP (+ M (* -1 N)))))
                       (NOT (EQUAL (* (+ (* 2 N) (* -1 M))
                                      (+ (* 2 N) (* -1 M)))
                                   (* 2 (+ M (* -1 N))
                                      (+ M (* -1 N)))))))).

By case analysis we reduce the conjecture to

Subgoal *1/''
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N)))
         (NOT (OR (NOT (AND (NOT (ZP (+ (* 2 N) (* -1 M))))
                            (NOT (ZP (+ M (* -1 N))))))
                  (NOT (EQUAL (* (+ (* 2 N) (* -1 M))
                                 (+ (* 2 N) (* -1 M)))
                              (* 2 (+ M (* -1 N))
                                 (+ M (* -1 N)))))))).

This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER,
the :definitions FIX, NOT and SYNP, the :executable-counterparts of
BINARY-*, BINARY-+ and NOT, primitive type reasoning, the :rewrite
rules A1, A3, A5, A9, COMMUTATIVITY-OF-*, COMMUTATIVITY-OF-+, REARRANGE-
NEGATIVE-COEFS-<, UNICITY-OF-0, UNICITY-OF-1 and ZP-OPEN and the :type-
prescription rule NONNEGATIVE-PRODUCT, to the following two conjectures.

Subgoal *1/2
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N)))
         (< M (* 2 N))).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning,
the :linear rule *-WEAKLY-MONOTONIC, the :rewrite rules A9 and COMMUTATIVITY-
OF-* and the :type-prescription rule NONNEGATIVE-PRODUCT.

Subgoal *1/1
(IMPLIES (AND (NOT (ZP M))
              (NOT (ZP N))
              (EQUAL (* M M) (* 2 N N)))
         (< N M)).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning,
the :forward-chaining rule *-WEAKLY-MONOTONIC and the :type-prescription
rule NONNEGATIVE-PRODUCT.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( DEFTHM LEMMA-1 ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING *-WEAKLY-MONOTONIC . 2)
        (:FORWARD-CHAINING *-WEAKLY-MONOTONIC . 1)
        (:INDUCTION INDUCTION-SCHEME)
        (:LINEAR *-WEAKLY-MONOTONIC . 2)
        (:REWRITE A1)
        (:REWRITE A2)
        (:REWRITE A3)
        (:REWRITE A5)
        (:REWRITE A9)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE REARRANGE-NEGATIVE-COEFS-<)
        (:REWRITE UNICITY-OF-0)
        (:REWRITE UNICITY-OF-1)
        (:REWRITE ZP-OPEN)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Warnings:  Subsume and Non-rec
Time:  0.06 seconds (prove: 0.03, print: 0.03, other: 0.00)
 LEMMA-1
ACL2 !>>
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.


[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

ACL2 Warning [Use] in ( DEFTHM LEMMA-2 ...):  It is unusual to :USE
an enabled :REWRITE or :DEFINITION rule, so you may want to consider
disabling (:REWRITE LEMMA-1).


We now augment the goal above by adding the hypotheses indicated by
the :USE hint.  These hypotheses can be derived from LEMMA-1 and CANCEL-
EQUAL-* via instantiation.  The augmented goal is shown below.

Goal'
(IMPLIES (AND (IMPLIES (AND (NOT (ZP M)) (NOT (ZP N)))
                       (NOT (= (* M M) (* 2 N N))))
              (IMPLIES (AND (NOT (ZP (- M))) (NOT (ZP N)))
                       (NOT (= (* (- M) (- M)) (* 2 N N))))
              (IMPLIES (AND (RATIONALP (* M M (/ N) (/ N)))
                            (RATIONALP (* N N))
                            (NOT (EQUAL (* N N) 0)))
                       (EQUAL (EQUAL (* (* N N) M M (/ N) (/ N))
                                     (* (* N N) 2))
                              (EQUAL (* M M (/ N) (/ N)) 2))))
         (IMPLIES (AND (INTEGERP M) (NOT (ZP N)))
                  (NOT (= (* (* M (/ N)) M (/ N)) 2)))).

By the simple :definition = and the simple :rewrite rules A2 and ASSOCIATIVITY\
-OF-* we reduce the conjecture to

Goal''
(IMPLIES (AND (IMPLIES (AND (NOT (ZP M)) (NOT (ZP N)))
                       (NOT (EQUAL (* M M) (* 2 N N))))
              (IMPLIES (AND (NOT (ZP (* -1 M))) (NOT (ZP N)))
                       (NOT (EQUAL (* -1 M -1 M) (* 2 N N))))
              (IMPLIES (AND (RATIONALP (* M M (/ N) (/ N)))
                            (RATIONALP (* N N))
                            (NOT (EQUAL (* N N) 0)))
                       (EQUAL (EQUAL (* N N M M (/ N) (/ N))
                                     (* N N 2))
                              (EQUAL (* M M (/ N) (/ N)) 2)))
              (INTEGERP M)
              (NOT (ZP N)))
         (NOT (EQUAL (* M (/ N) M (/ N)) 2))).

This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER,
the :definitions FIX, NOT and SYNP, the :executable-counterparts of
BINARY-*, EQUAL and NOT, primitive type reasoning, the :rewrite rules
A5, A8, A9, COMMUTATIVITY-OF-*, UNICITY-OF-1 and ZP-OPEN and the :type-
prescription rule NONNEGATIVE-PRODUCT, to

Goal'''
(IMPLIES (AND (ZP M)
              (<= (* -1 M) 0)
              (EQUAL (* M M) (* 2 N N))
              (EQUAL (EQUAL (* M M (/ N) (/ N)) 2) T)
              (INTEGERP M))
         (ZP N)).

This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER,
the :executable-counterparts of <, BINARY-*, INTEGERP, NOT and ZP and
linear arithmetic, to

Goal'4'
(IMPLIES (AND (EQUAL 0 (* 2 N N))
              (EQUAL (EQUAL (* 0 0 (/ N) (/ N)) 2) T))
         (ZP N)).

But we reduce the conjecture to T, by the :executable-counterparts
of BINARY-* and EQUAL and the simple :rewrite rule A9.

Q.E.D.

Summary
Form:  ( DEFTHM LEMMA-2 ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART BINARY-*)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE A2)
        (:REWRITE A5)
        (:REWRITE A8)
        (:REWRITE A9)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE UNICITY-OF-1)
        (:REWRITE ZP-OPEN)
        (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
Warnings:  Use, Subsume and Non-rec
Time:  0.04 seconds (prove: 0.01, print: 0.02, other: 0.01)
 LEMMA-2
ACL2 !>>
ACL2 Warning [Non-rec] in ( DEFTHM SQRT2-IRRATIONAL ...):  The :REWRITE
rule generated from SQRT2-IRRATIONAL will be triggered only by terms
containing the non-recursive function symbol =.  Unless this function
is disabled, SQRT2-IRRATIONAL is unlikely ever to be used.


ACL2 Warning [Subsume] in ( DEFTHM SQRT2-IRRATIONAL ...):  The previously
added rule = subsumes the newly proposed :REWRITE rule SQRT2-IRRATIONAL,
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!]

ACL2 Warning [Use] in ( DEFTHM SQRT2-IRRATIONAL ...):  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 hypothesis indicated by
the :USE hint.  The hypothesis can be derived from LEMMA-2 via instantiation.
The augmented goal is shown below.

Goal'
(IMPLIES (IMPLIES (AND (INTEGERP (NUMERATOR X))
                       (NOT (ZP (DENOMINATOR X))))
                  (NOT (= (* (* (NUMERATOR X) (/ (DENOMINATOR X)))
                             (NUMERATOR X)
                             (/ (DENOMINATOR X)))
                          2)))
         (IMPLIES (RATIONALP X)
                  (NOT (= (* X X) 2)))).

By the simple :definition = and the simple :rewrite rule ASSOCIATIVITY-
OF-* we reduce the conjecture to

Goal''
(IMPLIES (AND (IMPLIES (AND (INTEGERP (NUMERATOR X))
                            (NOT (ZP (DENOMINATOR X))))
                       (NOT (EQUAL (* (NUMERATOR X)
                                      (/ (DENOMINATOR X))
                                      (NUMERATOR X)
                                      (/ (DENOMINATOR X)))
                                   2)))
              (RATIONALP X))
         (NOT (EQUAL (* X X) 2))).

But simplification reduces this to T, using the :compound-recognizer
rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of EQUAL
and NOT, primitive type reasoning and the :rewrite rules A9, COMMUTATIVITY-
OF-* and RATIONAL-IMPLIES2.

Q.E.D.

Summary
Form:  ( DEFTHM SQRT2-IRRATIONAL ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION =)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE A9)
        (:REWRITE ASSOCIATIVITY-OF-*)
        (:REWRITE COMMUTATIVITY-OF-*)
        (:REWRITE RATIONAL-IMPLIES2))
Warnings:  Use, Subsume and Non-rec
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
 SQRT2-IRRATIONAL
ACL2 !>>Bye.
 :EOF
ACL2 !>