GCL (GNU Common Lisp) Version(2.5.0) Tue Aug 27 18:02:58 CDT 2002 Licensed under GNU Library General Public License Contains Enhancements by W. Schelter ACL2 Version 2.7 built November 14, 2002 10:53:25. Copyright (C) 2002 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* T). See the documentation topic note-2-7 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. Loading /v/filer1b/v0q004/moore/acl2-init.lsp Finished loading /v/filer1b/v0q004/moore/acl2-init.lsp ACL2 Version 2.7. Level 1. Cbd "/v/net2/v2/users/prof/moore/publications/trecia/support/". Type :help for help. ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT) ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2> ACL2 Version 2.7. Level 1. Cbd "/v/net2/v2/users/prof/moore/publications/trecia/support/". Type :help for help. ACL2 !>[SGC for 618 CONS pages..(3098 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3099 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3099 writable)..(T=8).GC finished] [SGC for 618 CONS pages..(3099 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3099 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3100 writable)..(T=9).GC finished] [SGC for 618 CONS pages..(3101 writable)..(T=9).GC finished] [SGC for 618 CONS pages..(3101 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3102 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3103 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3103 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3103 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3104 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3104 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3104 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3104 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3104 writable)..(T=12).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=49).GC finished] [SGC on] Loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o [SGC for 0 CONTIGUOUS-BLOCKS pages..(2548 writable)..(T=6).GC finished] start address -T 0x9b3d000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o Summary Form: ( INCLUDE-BOOK "m5" ...) Rules: NIL Warnings: None Time: 6.27 seconds (prove: 0.00, print: 0.03, other: 6.24) "/v/net2/v2/users/prof/moore/publications/trecia/support/m5.lisp" ACL2 !>[SGC for 1120 CONS pages..(3005 writable)..(T=11).GC finished] [SGC for 1120 CONS pages..(3020 writable)..(T=11).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9b678a0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9b67830 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o [SGC for 1120 CONS pages..(3043 writable)..(T=12).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9b62010 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b3cf00 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9b62e90 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b62c30 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b629e0 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b61000 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o [SGC for 1120 CONS pages..(3063 writable)..(T=13).GC finished] Loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b8f3a0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b616a0 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b5afa0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b5b8e0 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o [SGC for 1120 CONS pages..(3090 writable)..(T=13).GC finished] Loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b85000 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b85fe0 Finished loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o Loading /projects/acl2/v2-7/books/arithmetic/top.lisp Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9b5ac10 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9b5a8c0 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9b85db0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b5aab0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9b85c60 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b859d0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b858c0 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o Finished loading /projects/acl2/v2-7/books/arithmetic/top.lisp Loading /projects/acl2/v2-7/books/meta/meta.lisp Loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b64f40 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b86660 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b5cf00 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b5d820 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b8e6c0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b8a220 Finished loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Finished loading /projects/acl2/v2-7/books/meta/meta.lisp start address -T 0x9b857a0 Finished loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o Summary Form: ( INCLUDE-BOOK "/projects/acl2/v2-7/books/arithmetic/top-with-meta" ...) Rules: NIL Warnings: None Time: 2.79 seconds (prove: 0.00, print: 0.01, other: 2.78) "/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/top-with-meta.lisp" [SGC for 1120 CONS pages..(3152 writable)..(T=13).GC finished] Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9b6fec0 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9b74320 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9b6a7e0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o [SGC for 1120 CONS pages..(3234 writable)..(T=14).GC finished] Loading /projects/acl2/v2-7/books/ihs/ihs-theories.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c4a000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9b83000 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9b6bef0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o [SGC for 1120 CONS pages..(3294 writable)..(T=14).GC finished] [SGC for 1120 CONS pages..(3323 writable)..(T=14).GC finished] [SGC for 1120 CONS pages..(3359 writable)..(T=15).GC finished] [SGC for 0 RELOCATABLE-BLOCKS pages..(3394 writable)..(T=15).GC finished] Loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c50000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c4e460 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/ihs/ihs-theories.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c56000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c54460 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9b59ae0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o start address -T 0x9b79a20 Finished loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o Summary Form: ( INCLUDE-BOOK "/projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas" ...) Rules: NIL Warnings: None Time: 3.48 seconds (prove: 0.00, print: 0.01, other: 3.47) "/v/filer1b/v0q004/acl2/v2-7/books/ihs/quotient-remainder-lemmas.lisp" Summary Form: ( DEFUN INTP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION ACL2::EXPT-TYPE-PRESCRIPTION-INTEGERP) (:TYPE-PRESCRIPTION ACL2::EXPT-TYPE-PRESCRIPTION-NONZERO) (:TYPE-PRESCRIPTION ACL2::EXPT-TYPE-PRESCRIPTION-POSITIVE)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INTP Summary Form: ( DEFTHM INT-LEMMA0 ...) Rules: ((:DEFINITION INTP) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) INT-LEMMA0 [SGC for 1120 CONS pages..(3969 writable)..(T=15).GC finished] Summary Form: ( DEFTHM INT-LEMMA1 ...) Rules: ((:DEFINITION FIX) (:DEFINITION FLOOR) (:DEFINITION IFIX) (:DEFINITION INT-FIX) (:DEFINITION INTP) (:DEFINITION MOD) (:DEFINITION NOT) (:DEFINITION S-FIX) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART MOD) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ACL2::INTEGERP-I/J-INTEGERP-FORWARD . 2) (:LINEAR ACL2::NIQ-BOUNDS) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE ACL2::DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE ACL2::EQUAL-DENOMINATOR-1) (:REWRITE ACL2::FOLD-CONSTS-IN-*) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE ACL2::FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT) (:REWRITE ACL2::FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT) (:REWRITE ACL2::FUNCTIONAL-SELF-INVERSION-OF-MINUS) (:REWRITE INVERSE-OF-+) (:REWRITE ACL2::NUMERATOR-WHEN-INTEGERP) (:REWRITE RATIONAL-IMPLIES2) (:REWRITE UNICITY-OF-0) (:REWRITE UNICITY-OF-1) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT)) Warnings: None Time: 0.85 seconds (prove: 0.83, print: 0.00, other: 0.02) INT-LEMMA1 [SGC for 1120 CONS pages..(4011 writable)..(T=16).GC finished] Summary Form: (IN-THEORY (CONS ...)) Rules: NIL Warnings: None Time: 0.24 seconds (prove: 0.00, print: 0.00, other: 0.24) 2914 Summary Form: ( DEFTHM INT-LEMMA2 ...) Rules: ((:DEFINITION IFIX) (:DEFINITION INT-FIX) (:DEFINITION INTP) (:DEFINITION NOT) (:DEFINITION S-FIX) (:DEFINITION SYNP) (:DEFINITION ZP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE ACL2::MOD-X-Y-=-X . 2) (:REWRITE ACL2::RIGHT-CANCELLATION-FOR-+)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) INT-LEMMA2 Summary Form: ( DEFTHM INT-LEMMA3 ...) Rules: ((:DEFINITION INTP) (:DEFINITION NOT) (:DEFINITION ZP) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) INT-LEMMA3 [SGC for 0 CONTIGUOUS-BLOCKS pages..(4018 writable)..(T=16).GC finished] [SGC for 1120 CONS pages..(4097 writable)..(T=16).GC finished] [SGC for 1120 CONS pages..(4172 writable)..(T=17).GC finished] [SGC for 1120 CONS pages..(4241 writable)..(T=17).GC finished] [SGC for 0 CONTIGUOUS-BLOCKS pages..(4249 writable)..(T=18).GC finished] [SGC for 1120 CONS pages..(4321 writable)..(T=17).GC finished] [SGC for 0 CFUN pages..(4386 writable)..[SGC off] (doing full gc)[SGC on](T=65).GC finished] [SGC for 578 CONS pages..(2266 writable)..(T=7).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=51).GC finished] [SGC on][SGC for 568 CONS pages..(2246 writable)..(T=8).GC finished] [SGC for 0 CONTIGUOUS-BLOCKS pages..(2287 writable)..(T=7).GC finished] [SGC for 568 CONS pages..(2589 writable)..(T=8).GC finished] [SGC for 568 CONS pages..(2661 writable)..(T=8).GC finished] [SGC for 568 CONS pages..(2729 writable)..(T=9).GC finished] [SGC for 568 CONS pages..(2785 writable)..(T=9).GC finished] [SGC for 568 CONS pages..(2858 writable)..(T=9).GC finished] [SGC for 568 CONS pages..(2927 writable)..(T=10).GC finished] [SGC for 568 CONS pages..(2991 writable)..(T=10).GC finished] [SGC for 0 CFUN pages..(3010 writable)..[SGC off] (doing full gc)[SGC on](T=65).GC finished] [SGC for 0 CONTIGUOUS-BLOCKS pages..(2221 writable)..(T=7).GC finished] [SGC for 577 CONS pages..(2533 writable)..(T=7).GC finished] [SGC for 577 CONS pages..(2600 writable)..(T=8).GC finished] [SGC for 577 CONS pages..(2667 writable)..(T=9).GC finished] [SGC for 577 CONS pages..(2736 writable)..(T=8).GC finished] [SGC for 577 CONS pages..(2816 writable)..(T=10).GC finished] [SGC for 577 CONS pages..(2882 writable)..(T=9).GC finished] [SGC for 577 CONS pages..(2945 writable)..(T=10).GC finished] [SGC for 577 CONS pages..(3011 writable)..(T=10).GC finished] [SGC for 0 CFUN pages..(3028 writable)..[SGC off] (doing full gc)[SGC on](T=66).GC finished] [SGC for 548 CONS pages..(2224 writable)..(T=7).GC finished] [SGC for 548 CONS pages..(2290 writable)..(T=7).GC finished] [SGC for 548 CONS pages..(2357 writable)..(T=9).GC finished] [SGC for 0 CONTIGUOUS-BLOCKS pages..(2380 writable)..(T=9).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=52).GC finished] [SGC on][SGC for 572 CONS pages..(2249 writable)..(T=8).GC finished] [SGC for 572 CONS pages..(2317 writable)..(T=8).GC finished] Summary Form: ( DEFTHM INT-LEMMA4A ...) Rules: ((:DEFINITION FIX) (:DEFINITION FORCE) (:DEFINITION IFF) (:DEFINITION IFIX) (:DEFINITION INT-FIX) (:DEFINITION NOT) (:DEFINITION S-FIX) (:DEFINITION SYNP) (:ELIM ACL2::FLOOR-MOD-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ACL2-NUMBERP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART FORCE) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART IFF) (:EXECUTABLE-COUNTERPART IMPLIES) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART MOD) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART RATIONALP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:GENERALIZE ACL2::FLOOR-=-X/Y) (:GENERALIZE ACL2::FLOOR-BOUNDS) (:GENERALIZE ACL2::FLOOR-TYPE-1) (:GENERALIZE ACL2::FLOOR-TYPE-2) (:GENERALIZE ACL2::FLOOR-TYPE-3) (:GENERALIZE ACL2::FLOOR-TYPE-4) (:GENERALIZE ACL2::MOD-=-0) (:GENERALIZE ACL2::MOD-BOUNDS) (:GENERALIZE ACL2::MOD-TYPE) (:GENERALIZE ACL2::MOD-X-Y-=-X) (:GENERALIZE ACL2::MOD-X-Y-=-X+Y) (:META ACL2::CANCEL_PLUS-EQUAL-CORRECT) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-*-/-LEFT-COMMUTED) (:REWRITE ACL2::<-*-0) (:REWRITE ACL2::<-*-Y-X-Y) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:REWRITE ACL2::<-0-MINUS) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE ACL2::CANCEL-MOD-+) (:REWRITE ACL2::COMMUTATIVITY-2-OF-*) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE ACL2::DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE ACL2::EQUAL-CONSTANT-+) (:REWRITE ACL2::FOLD-CONSTS-IN-*) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE ACL2::FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-LEFT) (:REWRITE ACL2::FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT) (:REWRITE ACL2::LEFT-CANCELLATION-FOR-+) (:REWRITE ACL2::MOD-=-0 . 2) (:REWRITE ACL2::MOD-MINUS) (:REWRITE ACL2::TIMES-ZERO) (:REWRITE UNICITY-OF-0) (:REWRITE UNICITY-OF-1) (:REWRITE ACL2::ZERO-IS-ONLY-ZERO-DIVISOR) (:TYPE-PRESCRIPTION FLOOR) (:TYPE-PRESCRIPTION ACL2::INTEGERP-MOD) (:TYPE-PRESCRIPTION ACL2::MOD-TYPE . 4)) Warnings: None Time: 22.36 seconds (prove: 22.34, print: 0.00, other: 0.02) INT-LEMMA4A [SGC for 572 CONS pages..(2402 writable)..(T=8).GC finished] [SGC for 572 CONS pages..(2507 writable)..(T=9).GC finished] Summary Form: ( DEFTHM INT-LEMMA5A ...) Rules: ((:DEFINITION IFIX) (:DEFINITION INT-FIX) (:DEFINITION S-FIX) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::CANCEL-MOD-+) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::SIMPLIFY-MOD-+-MOD) (:TYPE-PRESCRIPTION ACL2::INTEGERP-MOD) (:TYPE-PRESCRIPTION ACL2::MOD-TYPE . 4)) Warnings: None Time: 0.87 seconds (prove: 0.85, print: 0.00, other: 0.02) INT-LEMMA5A Summary Form: ( DEFTHM INT-LEMMA5A1 ...) Rules: ((:DEFINITION INT-FIX) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOCIATIVITY-OF-+)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) INT-LEMMA5A1 [SGC for 572 CONS pages..(2591 writable)..(T=9).GC finished] Summary Form: ( DEFTHM INT-LEMMA6 ...) Rules: ((:DEFINITION FIX) (:DEFINITION FORCE) (:DEFINITION IFIX) (:DEFINITION INT-FIX) (:DEFINITION INTP) (:DEFINITION NOT) (:DEFINITION S-FIX) (:DEFINITION SYNP) (:ELIM ACL2::FLOOR-MOD-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ACL2-NUMBERP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART FIX) (:EXECUTABLE-COUNTERPART FORCE) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:GENERALIZE ACL2::FLOOR-=-X/Y) (:GENERALIZE ACL2::FLOOR-BOUNDS) (:GENERALIZE ACL2::FLOOR-TYPE-1) (:GENERALIZE ACL2::FLOOR-TYPE-2) (:GENERALIZE ACL2::FLOOR-TYPE-3) (:GENERALIZE ACL2::FLOOR-TYPE-4) (:GENERALIZE ACL2::MOD-=-0) (:GENERALIZE ACL2::MOD-BOUNDS) (:GENERALIZE ACL2::MOD-TYPE) (:GENERALIZE ACL2::MOD-X-Y-=-X) (:GENERALIZE ACL2::MOD-X-Y-=-X+Y) (:META ACL2::CANCEL_PLUS-EQUAL-CORRECT) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-*-/-LEFT-COMMUTED) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:REWRITE ACL2::<-0-MINUS) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE ACL2::DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE ACL2::EQUAL-CONSTANT-+) (:REWRITE ACL2::FOLD-CONSTS-IN-*) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE ACL2::MOD-X-Y-=-X . 1) (:REWRITE ACL2::MOD-X-Y-=-X+Y . 3) (:REWRITE UNICITY-OF-0) (:REWRITE UNICITY-OF-1) (:REWRITE ACL2::ZERO-IS-ONLY-ZERO-DIVISOR) (:TYPE-PRESCRIPTION FLOOR) (:TYPE-PRESCRIPTION ACL2::INTEGERP-MOD) (:TYPE-PRESCRIPTION ACL2::MOD-TYPE . 4)) Warnings: None Time: 0.62 seconds (prove: 0.61, print: 0.00, other: 0.01) INT-LEMMA6 Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) 2918 Summary Form: ( DEFTHM INT-LEMMA4B ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE INT-LEMMA4A)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INT-LEMMA4B Summary Form: ( DEFTHM INT-LEMMA5B ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE INT-LEMMA5A)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INT-LEMMA5B Summary Form: ( DEFTHM STATES ...) Rules: ((:DEFINITION CLASS-TABLE) (:DEFINITION HEAP) (:DEFINITION MAKE-STATE) (:DEFINITION THREAD-TABLE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-0-CONS) (:REWRITE NTH-ADD1)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) STATES [SGC for 572 CONS pages..(2652 writable)..(T=9).GC finished] Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.14 seconds (prove: 0.00, print: 0.00, other: 0.14) 2917 Summary Form: ( DEFTHM FRAMES ...) Rules: ((:DEFINITION CUR-CLASS) (:DEFINITION LOCALS) (:DEFINITION MAKE-FRAME) (:DEFINITION PC) (:DEFINITION PROGRAM) (:DEFINITION STACK) (:DEFINITION SYNC-FLG) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-0-CONS) (:REWRITE NTH-ADD1)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) FRAMES Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) 2911 Summary Form: ( DEFTHM STACKS ...) Rules: ((:DEFINITION POP) (:DEFINITION PUSH) (:DEFINITION TOP) (:EXECUTABLE-COUNTERPART IF) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) STACKS Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2909 Summary Form: ( DEFTHM ASSOC-EQUAL-BIND ...) Rules: ((:DEFINITION ASSOC-EQUAL) (:DEFINITION BIND) (:DEFINITION ENDP) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.07 seconds (prove: 0.06, print: 0.00, other: 0.01) ASSOC-EQUAL-BIND Summary Form: ( DEFTHM BIND-BIND ...) Rules: ((:DEFINITION BIND) (:DEFINITION ENDP) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) BIND-BIND Summary Form: ( DEFTHM BIND-FORMALS-OPENER ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION BIND-FORMALS) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) BIND-FORMALS-OPENER Summary Form: ( DEFTHM NTH-OPENER ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION NTH) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DEFAULT-CDR) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0)) Warnings: None Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.02) NTH-OPENER [SGC for 572 CONS pages..(2691 writable)..(T=10).GC finished] Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.15 seconds (prove: 0.00, print: 0.00, other: 0.15) 2911 Summary Form: ( DEFTHM POPN-OPENER ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION POPN) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) POPN-OPENER Summary Form: ( DEFUN REPEAT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) REPEAT Summary Form: ( DEFTHM REPEAT-OPENER ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION REPEAT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) REPEAT-OPENER Summary Form: ( DEFTHM RUN-OPENER ...) Rules: ((:DEFINITION RUN) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.05 seconds (prove: 0.01, print: 0.00, other: 0.04) RUN-OPENER [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=12).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2708 writable)..(T=11).GC finished] Summary Form: ( DEFTHM STEP-OPENER ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION NEXT-INST) (:DEFINITION STATUS) (:DEFINITION STEP) (:DEFINITION TOP-FRAME) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER)) Warnings: None Time: 1.91 seconds (prove: 1.86, print: 0.00, other: 0.05) STEP-OPENER Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2918 [SGC for 572 CONS pages..(2711 writable)..(T=12).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2711 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2712 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2712 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2712 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2712 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2712 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2712 writable)..(T=10).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=12).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=12).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=12).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=10).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=12).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=10).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=10).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] [SGC for 572 CONS pages..(2713 writable)..(T=11).GC finished] Summary Form: ( DEFTHM RUN-APPEND ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION RUN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE RUN-OPENER)) Warnings: None Time: 6.83 seconds (prove: 6.81, print: 0.00, other: 0.02) RUN-APPEND Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2917 [SGC for 572 CONS pages..(2966 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(2966 writable)..(T=13).GC finished] [SGC for 572 CONS pages..(2966 writable)..(T=13).GC finished] [SGC for 572 CONS pages..(2969 writable)..(T=13).GC finished] [SGC for 572 CONS pages..(2971 writable)..(T=13).GC finished] [SGC for 572 CONS pages..(2971 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(2972 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(2990 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3009 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3033 writable)..(T=13).GC finished] [SGC for 572 CONS pages..(3047 writable)..(T=13).GC finished] [SGC for 572 CONS pages..(3062 writable)..(T=14).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp [SGC for 572 CONS pages..(3081 writable)..(T=14).GC finished] start address -T 0x9f68b40 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9f68aa0 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o [SGC for 572 CONS pages..(3092 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3092 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3092 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3092 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3101 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3113 writable)..(T=14).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9f6f150 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9f6adc0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o [SGC for 572 CONS pages..(3123 writable)..(T=14).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9f6fe50 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9f6fbe0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9f6f9a0 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o [SGC for 572 CONS pages..(3135 writable)..(T=15).GC finished] Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f73fe0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o [SGC for 572 CONS pages..(3143 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3153 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3162 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3171 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3179 writable)..(T=14).GC finished] Loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f70000 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f74980 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o [SGC for 572 CONS pages..(3187 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3195 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3203 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3211 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3218 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3226 writable)..(T=15).GC finished] Loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f71fe0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f71840 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o [SGC for 572 CONS pages..(3234 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3240 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3247 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3253 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3260 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3266 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3272 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3278 writable)..(T=14).GC finished] [SGC for 572 CONS pages..(3284 writable)..(T=15).GC finished] [SGC for 572 CONS pages..(3290 writable)..(T=15).GC finished] Loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f76820 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f6c000 Finished loading /projects/acl2/v2-7/books/meta/meta-times-equal.o [SGC for 572 CONS pages..(3296 writable)..(T=15).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o Loading /projects/acl2/v2-7/books/arithmetic/top.lisp Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9f6ce10 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9f88f60 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9f6de20 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9f8cf90 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o [SGC for 572 CONS pages..(3313 writable)..(T=15).GC finished] Loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0x9f6ccc0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9f6dbb0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9f6dcc0 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o Finished loading /projects/acl2/v2-7/books/arithmetic/top.lisp Loading /projects/acl2/v2-7/books/meta/meta.lisp Loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f6cfe0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f75000 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f79fe0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f73000 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f7a780 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o [SGC for 572 CONS pages..(3315 writable)..(T=15).GC finished] start address -T 0x9f77940 Finished loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Finished loading /projects/acl2/v2-7/books/meta/meta.lisp start address -T 0x9f6c850 Finished loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o [SGC for 572 CONS pages..(3324 writable)..(T=14).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=56).GC finished] [SGC on]Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa12b000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa1bd000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9f877e0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=57).GC finished] [SGC on]Loading /projects/acl2/v2-7/books/ihs/ihs-theories.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa1c2000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa133f60 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9f79890 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=54).GC finished] [SGC on]Loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa28c000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9f7b000 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/ihs/ihs-theories.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa462000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa1c6460 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9f760e0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o start address -T 0x9f75c80 Finished loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=61).GC finished] [SGC on] Summary Form: ( INCLUDE-BOOK "utilities" ...) Rules: NIL Warnings: None Time: 10.45 seconds (prove: 0.00, print: 0.00, other: 10.45) Compiling /v/net2/v2/users/prof/moore/publications/trecia/support/utilities.lisp. End of Pass 1. End of Pass 2. OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3 Finished compiling /v/net2/v2/users/prof/moore/publications/trecia/support/utilities.o. "/v/net2/v2/users/prof/moore/publications/trecia/support/utilities.o" Loading /v/net2/v2/users/prof/moore/publications/trecia/support/utilities.o Loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o Loading /projects/acl2/v2-7/books/arithmetic/top.lisp Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0xa1c75f0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9f7c3a0 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0xa12fa00 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0xa1c77f0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/arithmetic/inequalities.o Loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-asg.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-agp.lisp Finished loading /projects/acl2/v2-7/books/cowles/acl2-crg.lisp start address -T 0xa12fd40 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0xa1c7960 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0xa12fed0 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o Finished loading /projects/acl2/v2-7/books/arithmetic/top.lisp Loading /projects/acl2/v2-7/books/meta/meta.lisp Loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f87000 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0xa1c1460 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-equal.o Loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f81000 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f7e560 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o Loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9f7d8e0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0xa138000 Finished loading /projects/acl2/v2-7/books/meta/meta-times-equal.o Finished loading /projects/acl2/v2-7/books/meta/meta.lisp start address -T 0xa1c1bb0 Finished loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o Loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa468000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9f7f000 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/ihs/ihs-theories.o Loading /projects/acl2/v2-7/books/ihs/ihs-init.o Loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0xa641000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9f8b7e0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9f7eaa0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o start address -T 0xa138940 Finished loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o start address -T 0x9f7c1a0 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/utilities.o Summary Form: (CERTIFY-BOOK "utilities" ...) Rules: NIL Warnings: None Time: 51.74 seconds (prove: 33.45, print: 0.02, other: 18.27) "/v/net2/v2/users/prof/moore/publications/trecia/support/utilities.lisp" ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2>