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..(3100 writable)..(T=9).GC finished] [SGC for 618 CONS pages..(3101 writable)..(T=10).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..(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=10).GC finished] [SGC for 618 CONS pages..(3103 writable)..(T=10).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..(3105 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3105 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=41).GC finished] [SGC on] Loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o [SGC for 0 CONTIGUOUS-BLOCKS pages..(2541 writable)..(T=8).GC finished] start address -T 0x9b3d000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o [SGC for 1111 CONS pages..(3001 writable)..(T=11).GC finished] [SGC for 1111 CONS pages..(3016 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 0x9b5de90 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9b5e160 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o [SGC for 1111 CONS pages..(3039 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 0x9b625a0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b62300 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 0x9b61120 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x92fffc0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b62d80 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b3b420 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o [SGC for 1111 CONS pages..(3059 writable)..(T=12).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 0x92fefe0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b58fc0 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 0x9b5cf20 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x92ff7a0 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o [SGC for 1111 CONS pages..(3086 writable)..(T=12).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 0x9b5b740 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b5bf40 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 0x9b5a970 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9b5ac30 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 0x9b5aab0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b5ac90 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 0x9b58be0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b58a80 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b58910 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 0x9b59f40 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b5b200 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 0x9b8fea0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b57900 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 0x9b88820 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b56fc0 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 0x9b5c750 Finished loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o [SGC for 1111 CONS pages..(3147 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 1111 CONS pages..(3228 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 0x9c4c000 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 0x9b6bec0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o [SGC for 1111 CONS pages..(3288 writable)..(T=14).GC finished] [SGC for 1111 CONS pages..(3315 writable)..(T=14).GC finished] [SGC for 1111 CONS pages..(3352 writable)..(T=15).GC finished] [SGC for 0 RELOCATABLE-BLOCKS pages..(3387 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 0x9c52000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c50460 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 0x9c58000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c56460 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9b8c3c0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o start address -T 0x9b79740 Finished loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o [SGC for 1111 CONS pages..(3930 writable)..(T=15).GC finished] 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 0x9b79bd0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9c67f60 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 0x9b81250 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b79b00 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 0x9c51870 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9c51620 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b811c0 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 0x9b8a5c0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b87840 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 0x9b6a000 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b85fe0 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 0x9b81ac0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b86680 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 0x9c57db0 Finished loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o [SGC for 1111 CONS pages..(3938 writable)..(T=16).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 [SGC for 0 CONTIGUOUS-BLOCKS pages..(3943 writable)..(T=16).GC finished] start address -T 0x9c68000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c5c460 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 0x9c76000 Finished loading /projects/acl2/v2-7/books/data-structures/utilities.o start address -T 0x9c70f60 Finished loading /projects/acl2/v2-7/books/ihs/ihs-init.o start address -T 0x9b87fa0 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o start address -T 0x9b8a220 Finished loading /projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas.o start address -T 0x9b8ac90 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/utilities.o Summary Form: ( INCLUDE-BOOK "utilities" ...) Rules: NIL Warnings: None Time: 13.55 seconds (prove: 0.00, print: 0.01, other: 13.54) "/v/net2/v2/users/prof/moore/publications/trecia/support/utilities.lisp" ACL2 !>[SGC for 1111 CONS pages..(3974 writable)..(T=16).GC finished] Loading /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o start address -T 0x9c81000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o Summary Form: ( INCLUDE-BOOK "defpun" ...) Rules: NIL Warnings: None Time: 0.53 seconds (prove: 0.00, print: 0.00, other: 0.53) "/v/net2/v2/users/prof/moore/publications/trecia/support/defpun.lisp" Summary Form: ( DEFMACRO DEFPUN ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DEFPUN [SGC for 1111 CONS pages..(3977 writable)..(T=17).GC finished] Summary Form: ( DEFTHM UPDATE-NTH-OPENER ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION NOT) (:DEFINITION UPDATE-NTH) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.19 seconds (prove: 0.01, print: 0.00, other: 0.18) UPDATE-NTH-OPENER [SGC for 1111 CONS pages..(4001 writable)..(T=16).GC finished] Summary Form: ( DEFTHM INT-EVENP-INV-A ...) Rules: ((:DEFINITION EVENP) (:DEFINITION IFF) (:DEFINITION IFIX) (:DEFINITION INT-FIX) (:DEFINITION INTP) (:DEFINITION MOD) (:DEFINITION S-FIX) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ACL2::INTEGERP-I/J-INTEGERP-FORWARD . 2) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE ACL2::FOLD-CONSTS-IN-*) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE ACL2::FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION FLOOR)) Warnings: None Time: 0.58 seconds (prove: 0.50, print: 0.00, other: 0.08) INT-EVENP-INV-A Summary Form: ( DEFTHM INT-EVENP-INV-B ...) Rules: ((:DEFINITION EVENP) (:DEFINITION IFF) (:DEFINITION INTP) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE DISTRIBUTIVITY) (:TYPE-PRESCRIPTION EVENP)) Warnings: None Time: 0.10 seconds (prove: 0.02, print: 0.00, other: 0.08) INT-EVENP-INV-B [SGC for 1111 CONS pages..(4020 writable)..(T=17).GC finished] Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.22 seconds (prove: 0.00, print: 0.00, other: 0.22) 2945 Summary Form: ( DEFTHM INT-LEMMA2A ...) Rules: ((:DEFINITION INTP) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE INT-LEMMA6)) Warnings: None Time: 0.09 seconds (prove: 0.01, print: 0.00, other: 0.08) INT-LEMMA2A [SGC for 1111 CONS pages..(4021 writable)..(T=17).GC finished] Summary Form: ( DEFTHM INT-LEMMA2B ...) Rules: ((:DEFINITION INTP) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.27 seconds (prove: 0.02, print: 0.00, other: 0.25) INT-LEMMA2B Summary Form: ( DEFCONST *FLAT-PROG* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *FLAT-PROG* Summary Form: ( DEFUN HALFA ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION NFIX) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:TYPE-PRESCRIPTION INT-FIX)) Warnings: None Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.02) HALFA Summary Form: ( DEFUN FLAT-PRE-CONDITION ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FLAT-PRE-CONDITION Summary Form: ( DEFUN FLAT-LOOP-INVARIANT ...) Rules: ((:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION IFF)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FLAT-LOOP-INVARIANT Summary Form: ( DEFUN FLAT-POST-CONDITION ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FLAT-POST-CONDITION Summary Form: ( DEFUN FLAT-ASSERTION ...) Rules: ((:TYPE-PRESCRIPTION FLAT-LOOP-INVARIANT) (:TYPE-PRESCRIPTION FLAT-POST-CONDITION) (:TYPE-PRESCRIPTION FLAT-PRE-CONDITION)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) FLAT-ASSERTION T T [SGC for 1111 CONS pages..(4024 writable)..(T=17).GC finished] Summary Form: ( DEFUN |FLAT-INV-arity-1-test| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.17 seconds (prove: 0.00, print: 0.00, other: 0.17) |FLAT-INV-arity-1-test| Summary Form: ( DEFUN |FLAT-INV-arity-1-base| ...) Rules: ((:TYPE-PRESCRIPTION FLAT-ASSERTION)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |FLAT-INV-arity-1-base| Summary Form: ( DEFUN |FLAT-INV-arity-1-step| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |FLAT-INV-arity-1-step| Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2969 Summary Form: ( DEFUN |FLAT-INV-arity-1-stn| ...) Rules: ((:TYPE-PRESCRIPTION |FLAT-INV-arity-1-step|)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |FLAT-INV-arity-1-stn| Summary Form: ( DEFCHOOSE |FLAT-INV-arity-1-fch| ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |FLAT-INV-arity-1-fch| [SGC for 1111 CONS pages..(4025 writable)..(T=17).GC finished] Summary Form: ( DEFUN |FLAT-INV-arity-1-fn| ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION NFIX) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:TYPE-PRESCRIPTION |FLAT-INV-arity-1-base|)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) |FLAT-INV-arity-1-fn| Summary Form: ( DEFUN |FLAT-INV-arity-1| ...) Rules: ((:TYPE-PRESCRIPTION |FLAT-INV-arity-1-fn|)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |FLAT-INV-arity-1| Summary Form: (IN-THEORY (QUOTE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 9 Summary Form: ( DEFTHM |FLAT-INV-arity-1-DEF| ...) Rules: ((:DEFINITION |FLAT-INV-arity-1|) (:DEFINITION |FLAT-INV-arity-1-base|) (:DEFINITION |FLAT-INV-arity-1-fn|) (:DEFINITION |FLAT-INV-arity-1-step|) (:DEFINITION |FLAT-INV-arity-1-stn|) (:DEFINITION |FLAT-INV-arity-1-test|) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.07 seconds (prove: 0.04, print: 0.00, other: 0.03) |FLAT-INV-arity-1-DEF| [SGC for 1111 CONS pages..(4026 writable)..(T=17).GC finished] Summary Form: ( ENCAPSULATE ((|FLAT-INV-arity-1| ...) ...) ...) Rules: NIL Warnings: None Time: 0.18 seconds (prove: 0.05, print: 0.00, other: 0.13) T Summary Form: ( DEFUN FLAT-INV ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FLAT-INV [SGC for 1111 CONS pages..(4027 writable)..(T=18).GC finished] [SGC for 1111 CONS pages..(4027 writable)..(T=19).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=54).GC finished] [SGC on][SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=53).GC finished] [SGC on] Summary Form: ( DEFTHM FLAT-INV-DEF ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FLAT-ASSERTION) (:DEFINITION FLAT-INV) (:DEFINITION |FLAT-INV-arity-1-base|) (:DEFINITION |FLAT-INV-arity-1-step|) (:DEFINITION |FLAT-INV-arity-1-test|) (:DEFINITION FLAT-LOOP-INVARIANT) (:DEFINITION FLAT-POST-CONDITION) (:DEFINITION FLAT-PRE-CONDITION) (:DEFINITION IFF) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART IFF) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 2.58 seconds (prove: 2.57, print: 0.00, other: 0.01) FLAT-INV-DEF Summary Form: ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2::ACL2-DEFAULTS-TABLE Summary Form: ( ENCAPSULATE ((FLAT-INV ...) ...) ...) Rules: NIL Warnings: None Time: 2.99 seconds (prove: 2.62, print: 0.00, other: 0.37) T [SGC for 1297 CONS pages..(2976 writable)..(T=12).GC finished] [SGC for 1297 CONS pages..(2976 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(2976 writable)..(T=12).GC finished] Summary Form: ( DEFTHM FLAT-INV-OPENER ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FLAT-INV-DEF) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER)) Warnings: None Time: 1.88 seconds (prove: 1.86, print: 0.00, other: 0.02) FLAT-INV-OPENER Summary Form: ( DEFTHM VC1 ...) Rules: ((:DEFINITION FLAT-LOOP-INVARIANT) (:DEFINITION FLAT-PRE-CONDITION) (:EXECUTABLE-COUNTERPART IFF) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION FLAT-LOOP-INVARIANT) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) VC1 Summary Form: ( DEFTHM VC2 ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION FLAT-LOOP-INVARIANT) (:DEFINITION HALFA) (:DEFINITION IFF) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EVENP) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART IFF) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE INT-EVENP-INV-A) (:REWRITE INT-EVENP-INV-B) (:REWRITE INT-LEMMA1) (:REWRITE INT-LEMMA2A) (:REWRITE INT-LEMMA2B) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION FLAT-LOOP-INVARIANT) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.04 seconds (prove: 0.03, print: 0.00, other: 0.01) VC2 Summary Form: ( DEFTHM VC3 ...) Rules: ((:DEFINITION FLAT-LOOP-INVARIANT) (:DEFINITION FLAT-POST-CONDITION) (:DEFINITION HALFA) (:DEFINITION IFF) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART EVENP) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION FLAT-POST-CONDITION)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) VC3 Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2965 [SGC for 1297 CONS pages..(2996 writable)..(T=12).GC finished] [SGC for 1297 CONS pages..(2998 writable)..(T=11).GC finished] [SGC for 82 FIXNUM pages..(2998 writable)..(T=12).GC finished] Summary Form: ( DEFTHM FLAT-INV-STEP ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-GOTO) (:DEFINITION EXECUTE-IADD) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-IFEQ) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-ISTORE_X) (:DEFINITION EXECUTE-ISUB) (:DEFINITION FLAT-ASSERTION) (:DEFINITION FLAT-INV-DEF) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FLAT-INV-OPENER) (:REWRITE FRAMES) (:REWRITE NTH-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE UPDATE-NTH-OPENER) (:REWRITE VC1) (:REWRITE VC2) (:REWRITE VC3) (:TYPE-PRESCRIPTION FLAT-LOOP-INVARIANT) (:TYPE-PRESCRIPTION FLAT-POST-CONDITION) (:TYPE-PRESCRIPTION FLAT-PRE-CONDITION)) Warnings: None Time: 2.85 seconds (prove: 2.83, print: 0.00, other: 0.02) FLAT-INV-STEP Summary Form: ( DEFUN MONO-THREADEDP ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) MONO-THREADEDP [SGC for 1297 CONS pages..(3006 writable)..(T=12).GC finished] [SGC for 1297 CONS pages..(3006 writable)..(T=12).GC finished] Summary Form: ( DEFTHM FLAT-INV-RUN ...) Rules: ((:DEFINITION ENDP) (:DEFINITION MONO-THREADEDP) (:DEFINITION NOT) (:DEFINITION RUN) (:REWRITE FLAT-INV-STEP)) Warnings: None Time: 1.21 seconds (prove: 1.13, print: 0.00, other: 0.08) FLAT-INV-RUN Summary Form: ( DEFTHM FLAT-MAIN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FLAT-ASSERTION) (:DEFINITION FLAT-INV-DEF) (:DEFINITION FLAT-POST-CONDITION) (:DEFINITION FLAT-PRE-CONDITION) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION MONO-THREADEDP)) Warnings: None Time: 0.11 seconds (prove: 0.05, print: 0.00, other: 0.06) FLAT-MAIN Summary Form: ( DEFTHM INT-BACK ...) Rules: ((:DEFINITION INTP) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.09 seconds (prove: 0.03, print: 0.00, other: 0.06) INT-BACK Summary Form: ( DEFTHM HALFA-IS-HALF ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION EVENP) (:DEFINITION FIX) (:DEFINITION HALFA) (:DEFINITION NOT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:FORWARD-CHAINING ACL2::INTEGERP-I/J-INTEGERP-FORWARD . 2) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE INT-BACK) (:REWRITE INT-LEMMA2B) (:REWRITE INT-LEMMA6) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.16 seconds (prove: 0.11, print: 0.00, other: 0.05) HALFA-IS-HALF Summary Form: ( DEFTHM INTP-HALF-N ...) Rules: ((:DEFINITION EVENP) (:DEFINITION INTP) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART EXPT) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ACL2::INTEGERP-I/J-INTEGERP-FORWARD . 1) (:REWRITE ACL2::<-*-/-LEFT-COMMUTED) (:REWRITE COMMUTATIVITY-OF-*) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.08 seconds (prove: 0.02, print: 0.00, other: 0.06) INTP-HALF-N Summary Form: ( DEFTHM FLAT-IS-PARTIALLY-CORRECT ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::EQUAL-*-/-1) (:REWRITE HALFA-IS-HALF) (:REWRITE INTP-HALF-N) (:REWRITE NTH-OPENER) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION MONO-THREADEDP)) Warnings: None Time: 0.07 seconds (prove: 0.05, print: 0.00, other: 0.02) FLAT-IS-PARTIALLY-CORRECT Summary Form: ( DEFCONST *HALF-PROG* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *HALF-PROG* Summary Form: ( DEFUN SDEPTH ...) Rules: ((:DEFINITION ENDP) (:DEFINITION POP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.07 seconds (prove: 0.01, print: 0.00, other: 0.06) SDEPTH Summary Form: ( DEFUN HALF-ASSERTION ...) Rules: ((:TYPE-PRESCRIPTION FLAT-LOOP-INVARIANT) (:TYPE-PRESCRIPTION FLAT-POST-CONDITION) (:TYPE-PRESCRIPTION FLAT-PRE-CONDITION)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) HALF-ASSERTION T T Summary Form: ( DEFUN |HALF-INV-arity-1-test| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |HALF-INV-arity-1-test| Summary Form: ( DEFUN |HALF-INV-arity-1-base| ...) Rules: ((:TYPE-PRESCRIPTION HALF-ASSERTION)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |HALF-INV-arity-1-base| Summary Form: ( DEFUN |HALF-INV-arity-1-step| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |HALF-INV-arity-1-step| [SGC for 1297 CONS pages..(3048 writable)..(T=13).GC finished] Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2986 Summary Form: ( DEFUN |HALF-INV-arity-1-stn| ...) Rules: ((:TYPE-PRESCRIPTION |HALF-INV-arity-1-step|)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |HALF-INV-arity-1-stn| Summary Form: ( DEFCHOOSE |HALF-INV-arity-1-fch| ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |HALF-INV-arity-1-fch| Summary Form: ( DEFUN |HALF-INV-arity-1-fn| ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION NFIX) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:TYPE-PRESCRIPTION |HALF-INV-arity-1-base|)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) |HALF-INV-arity-1-fn| Summary Form: ( DEFUN |HALF-INV-arity-1| ...) Rules: ((:TYPE-PRESCRIPTION |HALF-INV-arity-1-fn|)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |HALF-INV-arity-1| Summary Form: (IN-THEORY (QUOTE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 9 Summary Form: ( DEFTHM |HALF-INV-arity-1-DEF| ...) Rules: ((:DEFINITION |HALF-INV-arity-1|) (:DEFINITION |HALF-INV-arity-1-base|) (:DEFINITION |HALF-INV-arity-1-fn|) (:DEFINITION |HALF-INV-arity-1-step|) (:DEFINITION |HALF-INV-arity-1-stn|) (:DEFINITION |HALF-INV-arity-1-test|) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.08 seconds (prove: 0.05, print: 0.00, other: 0.03) |HALF-INV-arity-1-DEF| Summary Form: ( ENCAPSULATE ((|HALF-INV-arity-1| ...) ...) ...) Rules: NIL Warnings: None Time: 0.21 seconds (prove: 0.06, print: 0.00, other: 0.15) T Summary Form: ( DEFUN HALF-INV ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) HALF-INV [SGC for 1297 CONS pages..(3085 writable)..(T=13).GC finished] Summary Form: ( DEFTHM HALF-INV-DEF ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION HALF-ASSERTION) (:DEFINITION HALF-INV) (:DEFINITION |HALF-INV-arity-1-base|) (:DEFINITION |HALF-INV-arity-1-step|) (:DEFINITION |HALF-INV-arity-1-test|) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE NTH-OPENER)) Warnings: None Time: 0.95 seconds (prove: 0.94, print: 0.00, other: 0.01) HALF-INV-DEF Summary Form: ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2::ACL2-DEFAULTS-TABLE Summary Form: ( ENCAPSULATE ((HALF-INV ...) ...) ...) Rules: NIL Warnings: None Time: 1.21 seconds (prove: 1.00, print: 0.00, other: 0.21) T [SGC for 1297 CONS pages..(3106 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3106 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3106 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3106 writable)..(T=11).GC finished] Summary Form: ( DEFTHM HALF-INV-OPENER ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION HALF-ASSERTION) (:DEFINITION HALF-INV-DEF) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER)) Warnings: None Time: 2.07 seconds (prove: 2.06, print: 0.00, other: 0.01) HALF-INV-OPENER [SGC for 1297 CONS pages..(3109 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3109 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3110 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3113 writable)..(T=14).GC finished] Summary Form: ( DEFTHM HALF-INV-STEP ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-HEAPREF) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-GOTO) (:DEFINITION EXECUTE-IADD) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-IFEQ) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-IRETURN) (:DEFINITION EXECUTE-ISTORE_X) (:DEFINITION EXECUTE-ISUB) (:DEFINITION HALF-ASSERTION) (:DEFINITION HALF-INV-DEF) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION RREF) (:DEFINITION SDEPTH) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE FRAMES) (:REWRITE HALF-INV-OPENER) (:REWRITE NTH-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE UPDATE-NTH-OPENER) (:REWRITE VC1) (:REWRITE VC2) (:REWRITE VC3) (:TYPE-PRESCRIPTION FLAT-LOOP-INVARIANT) (:TYPE-PRESCRIPTION FLAT-POST-CONDITION) (:TYPE-PRESCRIPTION FLAT-PRE-CONDITION) (:TYPE-PRESCRIPTION PUSH) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 4.47 seconds (prove: 4.41, print: 0.00, other: 0.06) HALF-INV-STEP Summary Form: ( DEFUN RUN-TO-RETURN ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) RUN-TO-RETURN [SGC for 1297 CONS pages..(3116 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3116 writable)..(T=13).GC finished] Summary Form: ( DEFTHM HALF-INV-RUN-TO-RETURN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION ENDP) (:DEFINITION MONO-THREADEDP) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE HALF-INV-STEP) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 1.24 seconds (prove: 1.19, print: 0.00, other: 0.05) HALF-INV-RUN-TO-RETURN [SGC for 1297 CONS pages..(3118 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3119 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3119 writable)..(T=13).GC finished] Summary Form: ( DEFTHM HALF-MAIN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FIX) (:DEFINITION FLAT-POST-CONDITION) (:DEFINITION FLAT-PRE-CONDITION) (:DEFINITION HALF-ASSERTION) (:DEFINITION HALF-INV-DEF) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::EQUAL-*-/-1) (:REWRITE HALFA-IS-HALF) (:REWRITE INTP-HALF-N) (:REWRITE NTH-OPENER) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION MONO-THREADEDP) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 2.34 seconds (prove: 2.28, print: 0.00, other: 0.06) HALF-MAIN [SGC for 1297 CONS pages..(3123 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3123 writable)..(T=13).GC finished] Summary Form: ( DEFTHM HALF-PARTIALLY-CORRECT ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY-/) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::EQUAL-*-/-1) (:REWRITE HALFA-IS-HALF) (:REWRITE INTP-HALF-N) (:REWRITE NTH-OPENER) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION EVENP) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION MONO-THREADEDP) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 1.29 seconds (prove: 1.28, print: 0.00, other: 0.01) HALF-PARTIALLY-CORRECT Summary Form: ( DEFCONST *SUM-PROG* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *SUM-PROG* Summary Form: ( DEFUN SUMA ...) Rules: ((:TYPE-PRESCRIPTION INT-FIX)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) SUMA Summary Form: ( DEFUN SUM-PRE-CONDITION ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) SUM-PRE-CONDITION Summary Form: ( DEFUN SUM-LOOP-INVARIANT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) SUM-LOOP-INVARIANT Summary Form: ( DEFUN SUM-POST-CONDITION ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SUM-POST-CONDITION Summary Form: ( DEFUN SUM-ASSERTION ...) Rules: ((:TYPE-PRESCRIPTION SUM-LOOP-INVARIANT) (:TYPE-PRESCRIPTION SUM-POST-CONDITION) (:TYPE-PRESCRIPTION SUM-PRE-CONDITION)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) SUM-ASSERTION T T Summary Form: ( DEFUN |SUM-INV-arity-1-test| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |SUM-INV-arity-1-test| Summary Form: ( DEFUN |SUM-INV-arity-1-base| ...) Rules: ((:TYPE-PRESCRIPTION SUM-ASSERTION)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |SUM-INV-arity-1-base| Summary Form: ( DEFUN |SUM-INV-arity-1-step| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |SUM-INV-arity-1-step| [SGC for 1297 CONS pages..(3143 writable)..(T=13).GC finished] Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 3009 Summary Form: ( DEFUN |SUM-INV-arity-1-stn| ...) Rules: ((:TYPE-PRESCRIPTION |SUM-INV-arity-1-step|)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |SUM-INV-arity-1-stn| Summary Form: ( DEFCHOOSE |SUM-INV-arity-1-fch| ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |SUM-INV-arity-1-fch| Summary Form: ( DEFUN |SUM-INV-arity-1-fn| ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION NFIX) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:TYPE-PRESCRIPTION |SUM-INV-arity-1-base|)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) |SUM-INV-arity-1-fn| Summary Form: ( DEFUN |SUM-INV-arity-1| ...) Rules: ((:TYPE-PRESCRIPTION |SUM-INV-arity-1-fn|)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |SUM-INV-arity-1| Summary Form: (IN-THEORY (QUOTE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 9 Summary Form: ( DEFTHM |SUM-INV-arity-1-DEF| ...) Rules: ((:DEFINITION |SUM-INV-arity-1|) (:DEFINITION |SUM-INV-arity-1-base|) (:DEFINITION |SUM-INV-arity-1-fn|) (:DEFINITION |SUM-INV-arity-1-step|) (:DEFINITION |SUM-INV-arity-1-stn|) (:DEFINITION |SUM-INV-arity-1-test|) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.07 seconds (prove: 0.04, print: 0.00, other: 0.03) |SUM-INV-arity-1-DEF| Summary Form: ( ENCAPSULATE ((|SUM-INV-arity-1| ...) ...) ...) Rules: NIL Warnings: None Time: 0.20 seconds (prove: 0.05, print: 0.00, other: 0.15) T Summary Form: ( DEFUN SUM-INV ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) SUM-INV [SGC for 1297 CONS pages..(3180 writable)..(T=13).GC finished] Summary Form: ( DEFTHM SUM-INV-DEF ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION NOT) (:DEFINITION SUM-ASSERTION) (:DEFINITION SUM-INV) (:DEFINITION |SUM-INV-arity-1-base|) (:DEFINITION |SUM-INV-arity-1-step|) (:DEFINITION |SUM-INV-arity-1-test|) (:DEFINITION SUM-LOOP-INVARIANT) (:DEFINITION SUM-POST-CONDITION) (:DEFINITION SUM-PRE-CONDITION) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 1.11 seconds (prove: 1.09, print: 0.00, other: 0.02) SUM-INV-DEF Summary Form: ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2::ACL2-DEFAULTS-TABLE Summary Form: ( ENCAPSULATE ((SUM-INV ...) ...) ...) Rules: NIL Warnings: None Time: 1.38 seconds (prove: 1.14, print: 0.00, other: 0.24) T [SGC for 1297 CONS pages..(3201 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3201 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3201 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3201 writable)..(T=13).GC finished] Summary Form: ( DEFTHM SUM-INV-OPENER ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION NOT) (:DEFINITION SUM-ASSERTION) (:DEFINITION SUM-INV-DEF) (:DEFINITION SUM-POST-CONDITION) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER)) Warnings: None Time: 2.09 seconds (prove: 2.08, print: 0.00, other: 0.01) SUM-INV-OPENER Summary Form: ( DEFTHM SUM-VC1 ...) Rules: ((:DEFINITION SUM-LOOP-INVARIANT) (:DEFINITION SUM-PRE-CONDITION) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION SUM-LOOP-INVARIANT)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) SUM-VC1 Summary Form: ( DEFTHM SUM-VC2 ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION NOT) (:DEFINITION SUM-LOOP-INVARIANT) (:DEFINITION SUMA) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE INT-LEMMA3) (:REWRITE INT-LEMMA6) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION SUM-LOOP-INVARIANT)) Warnings: None Time: 0.05 seconds (prove: 0.03, print: 0.00, other: 0.02) SUM-VC2 Summary Form: ( DEFTHM SUM-VC3 ...) Rules: ((:DEFINITION SUM-LOOP-INVARIANT) (:DEFINITION SUM-POST-CONDITION) (:DEFINITION SUMA) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION SUM-POST-CONDITION)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) SUM-VC3 Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 3005 [SGC for 1297 CONS pages..(3209 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3210 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3211 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3214 writable)..(T=14).GC finished] Summary Form: ( DEFTHM SUM-INV-STEP ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-HEAPREF) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-GOTO) (:DEFINITION EXECUTE-IADD) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-IFEQ) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-IRETURN) (:DEFINITION EXECUTE-ISTORE_X) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION RREF) (:DEFINITION SDEPTH) (:DEFINITION STATUS) (:DEFINITION SUM-ASSERTION) (:DEFINITION SUM-INV-DEF) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE FRAMES) (:REWRITE NTH-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE SUM-INV-OPENER) (:REWRITE SUM-VC1) (:REWRITE SUM-VC2) (:REWRITE SUM-VC3) (:REWRITE UPDATE-NTH-OPENER) (:TYPE-PRESCRIPTION PUSH) (:TYPE-PRESCRIPTION SDEPTH) (:TYPE-PRESCRIPTION SUM-LOOP-INVARIANT) (:TYPE-PRESCRIPTION SUM-POST-CONDITION) (:TYPE-PRESCRIPTION SUM-PRE-CONDITION)) Warnings: None Time: 4.43 seconds (prove: 4.41, print: 0.00, other: 0.02) SUM-INV-STEP [SGC for 1297 CONS pages..(3217 writable)..(T=12).GC finished] [SGC for 1297 CONS pages..(3217 writable)..(T=13).GC finished] Summary Form: ( DEFTHM SUM-INV-RUN-TO-RETURN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION ENDP) (:DEFINITION MONO-THREADEDP) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER) (:REWRITE SUM-INV-STEP) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 1.28 seconds (prove: 1.22, print: 0.00, other: 0.06) SUM-INV-RUN-TO-RETURN [SGC for 1297 CONS pages..(3219 writable)..(T=13).GC finished] Summary Form: ( DEFTHM SUM-MAIN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:DEFINITION SUM-ASSERTION) (:DEFINITION SUM-INV-DEF) (:DEFINITION SUM-POST-CONDITION) (:DEFINITION SUM-PRE-CONDITION) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION MONO-THREADEDP) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 0.63 seconds (prove: 0.57, print: 0.00, other: 0.06) SUM-MAIN Loading /v/net2/v2/users/prof/moore/publications/trecia/support/demo.o start address -T 0xa072000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/demo.o Summary Form: ( INCLUDE-BOOK "demo" ...) Rules: NIL Warnings: None Time: 0.15 seconds (prove: 0.00, print: 0.00, other: 0.15) "/v/net2/v2/users/prof/moore/publications/trecia/support/demo.lisp" Summary Form: ( DEFUN ! ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ! Summary Form: ( DEFCONST *FACT-DEF* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :REDUNDANT Summary Form: ( DEFUN FACT-CALLER-FRAMESP ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) FACT-CALLER-FRAMESP Summary Form: ( DEFUN FACT-ASSERTION ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) FACT-ASSERTION T T Summary Form: ( DEFUN |FACT-INV-arity-1-test| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |FACT-INV-arity-1-test| Summary Form: ( DEFUN |FACT-INV-arity-1-base| ...) Rules: ((:TYPE-PRESCRIPTION FACT-ASSERTION)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |FACT-INV-arity-1-base| Summary Form: ( DEFUN |FACT-INV-arity-1-step| ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |FACT-INV-arity-1-step| Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.06 seconds (prove: 0.00, print: 0.00, other: 0.06) 3059 Summary Form: ( DEFUN |FACT-INV-arity-1-stn| ...) Rules: ((:TYPE-PRESCRIPTION |FACT-INV-arity-1-step|)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |FACT-INV-arity-1-stn| Summary Form: ( DEFCHOOSE |FACT-INV-arity-1-fch| ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) |FACT-INV-arity-1-fch| Summary Form: ( DEFUN |FACT-INV-arity-1-fn| ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION NFIX) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:TYPE-PRESCRIPTION |FACT-INV-arity-1-base|)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) |FACT-INV-arity-1-fn| Summary Form: ( DEFUN |FACT-INV-arity-1| ...) Rules: ((:TYPE-PRESCRIPTION |FACT-INV-arity-1-fn|)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) |FACT-INV-arity-1| Summary Form: (IN-THEORY (QUOTE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 9 [SGC for 1297 CONS pages..(3295 writable)..(T=13).GC finished] Summary Form: ( DEFTHM |FACT-INV-arity-1-DEF| ...) Rules: ((:DEFINITION |FACT-INV-arity-1|) (:DEFINITION |FACT-INV-arity-1-base|) (:DEFINITION |FACT-INV-arity-1-fn|) (:DEFINITION |FACT-INV-arity-1-step|) (:DEFINITION |FACT-INV-arity-1-stn|) (:DEFINITION |FACT-INV-arity-1-test|) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.21 seconds (prove: 0.04, print: 0.00, other: 0.17) |FACT-INV-arity-1-DEF| Summary Form: ( ENCAPSULATE ((|FACT-INV-arity-1| ...) ...) ...) Rules: NIL Warnings: None Time: 0.36 seconds (prove: 0.05, print: 0.00, other: 0.31) T Summary Form: ( DEFUN FACT-INV ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FACT-INV [SGC for 1297 CONS pages..(3314 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3315 writable)..(T=11).GC finished] Summary Form: ( DEFTHM FACT-INV-DEF ...) Rules: ((:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-METHODS) (:DEFINITION CLASS-DECL-SUPERCLASSES) (:DEFINITION FACT-ASSERTION) (:DEFINITION FACT-INV) (:DEFINITION |FACT-INV-arity-1-base|) (:DEFINITION |FACT-INV-arity-1-step|) (:DEFINITION |FACT-INV-arity-1-test|) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MEMBER) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART MEMBER) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION FACT-CALLER-FRAMESP) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 2.18 seconds (prove: 2.16, print: 0.00, other: 0.02) FACT-INV-DEF Summary Form: ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2::ACL2-DEFAULTS-TABLE Summary Form: ( ENCAPSULATE ((FACT-INV ...) ...) ...) Rules: NIL Warnings: None Time: 2.61 seconds (prove: 2.21, print: 0.00, other: 0.40) T [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3336 writable)..(T=13).GC finished] Summary Form: ( DEFTHM FACT-INV-OPENER ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FACT-ASSERTION) (:DEFINITION FACT-INV-DEF) (:DEFINITION NOT) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER)) Warnings: None Time: 8.50 seconds (prove: 8.48, print: 0.00, other: 0.02) FACT-INV-OPENER Summary Form: ( DEFTHM KB-HACK1 ...) Rules: ((:DEFINITION FIX) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE ACL2::DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION FACT-CALLER-FRAMESP)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) KB-HACK1 Summary Form: ( DEFTHM KB-HACK2 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE INT-LEMMA4A) (:TYPE-PRESCRIPTION !)) Warnings: None Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.02) KB-HACK2 Summary Form: ( DEFTHM FACT-CALLER-FRAMESP-OPENER-1 ...) Rules: ((:DEFINITION FACT-CALLER-FRAMESP) (:EXECUTABLE-COUNTERPART SYNP) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE NTH-OPENER)) Warnings: None Time: 0.06 seconds (prove: 0.04, print: 0.00, other: 0.02) FACT-CALLER-FRAMESP-OPENER-1 [SGC for 1297 CONS pages..(3345 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3346 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3347 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3347 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3348 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3349 writable)..(T=15).GC finished] [SGC for 1297 CONS pages..(3352 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3355 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3357 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3358 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3359 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3360 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3361 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3362 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3363 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3364 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3366 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3367 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3367 writable)..(T=13).GC finished] Summary Form: ( DEFTHM FACT-INV-STEP ...) Rules: ((:DEFINITION !) (:DEFINITION BINARY-APPEND) (:DEFINITION BIND-FORMALS) (:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-HEAPREF) (:DEFINITION CLASS-DECL-METHODS) (:DEFINITION CLASS-DECL-SUPERCLASSES) (:DEFINITION DEREF) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-IFLE) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-IMUL) (:DEFINITION EXECUTE-INVOKESTATIC) (:DEFINITION EXECUTE-IRETURN) (:DEFINITION EXECUTE-ISUB) (:DEFINITION FACT-ASSERTION) (:DEFINITION FACT-CALLER-FRAMESP) (:DEFINITION FACT-INV-DEF) (:DEFINITION FIX) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MAKE-THREAD) (:DEFINITION MEMBER) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POPN) (:DEFINITION REVERSE) (:DEFINITION RREF) (:DEFINITION SDEPTH) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART !) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART ARG2) (:EXECUTABLE-COUNTERPART ARG3) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART INT-FIX) (:EXECUTABLE-COUNTERPART INTP) (:EXECUTABLE-COUNTERPART MEMBER) (:EXECUTABLE-COUNTERPART METHOD-PROGRAM) (:EXECUTABLE-COUNTERPART METHOD-SYNC) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART REVERSE) (:EXECUTABLE-COUNTERPART TOP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:META ACL2::CANCEL_PLUS-EQUAL-CORRECT) (:META ACL2::CANCEL_PLUS-LESSP-CORRECT) (:REWRITE ACL2::<-+-NEGATIVE-0-1) (:REWRITE ACL2::<-0-+-NEGATIVE-2) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE BIND-FORMALS-OPENER) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-*) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE ACL2::DISTRIBUTIVITY-OF-MINUS-OVER-+) (:REWRITE FACT-CALLER-FRAMESP-OPENER-1) (:REWRITE FACT-INV-OPENER) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE FRAMES) (:REWRITE ACL2::FUNCTIONAL-SELF-INVERSION-OF-MINUS) (:REWRITE INT-LEMMA0) (:REWRITE INT-LEMMA3) (:REWRITE INT-LEMMA6) (:REWRITE INVERSE-OF-+) (:REWRITE ACL2::INVERSE-OF-+-AS=0) (:REWRITE KB-HACK1) (:REWRITE KB-HACK2) (:REWRITE ACL2::MINUS-CANCELLATION-ON-LEFT) (:REWRITE NTH-OPENER) (:REWRITE POPN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE UNICITY-OF-0) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION FACT-CALLER-FRAMESP) (:TYPE-PRESCRIPTION INT-FIX) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION PUSH) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 23.21 seconds (prove: 23.20, print: 0.00, other: 0.01) FACT-INV-STEP [SGC for 1297 CONS pages..(3370 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3370 writable)..(T=14).GC finished] Summary Form: ( DEFTHM FACT-INV-RUN-TO-RETURN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION ENDP) (:DEFINITION MONO-THREADEDP) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE FACT-INV-STEP) (:REWRITE NTH-OPENER) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 1.20 seconds (prove: 1.16, print: 0.00, other: 0.04) FACT-INV-RUN-TO-RETURN [SGC for 1297 CONS pages..(3372 writable)..(T=0).GC finished] [SGC for 1297 CONS pages..(3373 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3373 writable)..(T=13).GC finished] Summary Form: ( DEFTHM FACT-MAIN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-METHODS) (:DEFINITION CLASS-DECL-SUPERCLASSES) (:DEFINITION FACT-ASSERTION) (:DEFINITION FACT-CALLER-FRAMESP) (:DEFINITION FACT-INV-DEF) (:DEFINITION FIX) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE INVERSE-OF-+) (:REWRITE NTH-OPENER) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION INTP) (:TYPE-PRESCRIPTION MONO-THREADEDP) (:TYPE-PRESCRIPTION SDEPTH)) Warnings: None Time: 2.03 seconds (prove: 2.01, print: 0.00, other: 0.02) FACT-MAIN Summary Form: ( DEFUN SCHED-TO-RETURN ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) SCHED-TO-RETURN [SGC for 1297 CONS pages..(3375 writable)..(T=15).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=13).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=14).GC finished] [SGC for 1297 CONS pages..(3375 writable)..(T=13).GC finished] Summary Form: ( DEFTHM RUN-TO-RETURN-V-RUN ...) Rules: ((:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION RUN-TO-RETURN) (:DEFINITION SCHED-TO-RETURN) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE NTH-OPENER) (:REWRITE RUN-OPENER)) Warnings: None Time: 4.28 seconds (prove: 4.26, print: 0.00, other: 0.02) RUN-TO-RETURN-V-RUN Loading /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o start address -T 0xa07c000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o [SGC for 1297 CONS pages..(3480 writable)..(T=14).GC finished] Loading /v/net2/v2/users/prof/moore/publications/trecia/support/demo.o start address -T 0xa078000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/demo.o [SGC for 1297 CONS pages..(3568 writable)..(T=15).GC finished] Summary Form: ( INCLUDE-BOOK "vcg-examples" ...) Rules: NIL Warnings: None Time: 1.08 seconds (prove: 0.00, print: 0.00, other: 1.08) Compiling /v/net2/v2/users/prof/moore/publications/trecia/support/vcg-examples.lisp. [SGC for 0 RELOCATABLE-BLOCKS pages..(3586 writable)..(T=12).GC finished] End of Pass 1. ;; Note: Tail-recursive call of HALFA was replaced by iteration. ;; Note: Tail-recursive call of MONO-THREADEDP was replaced by iteration. ;; Note: Tail-recursive call of RUN-TO-RETURN was replaced by iteration. ;; Note: Tail-recursive call of SUMA was replaced by iteration. ;; Note: Tail-recursive call of FACT-CALLER-FRAMESP was replaced by iteration. ;; Note: Tail-recursive call of SCHED-TO-RETURN was replaced by iteration. 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/vcg-examples.o. "/v/net2/v2/users/prof/moore/publications/trecia/support/vcg-examples.o" Loading /v/net2/v2/users/prof/moore/publications/trecia/support/vcg-examples.o start address -T 0xa088000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/vcg-examples.o Summary Form: (CERTIFY-BOOK "vcg-examples" ...) Rules: NIL Warnings: None Time: 77.89 seconds (prove: 72.41, print: 0.00, other: 5.48) "/v/net2/v2/users/prof/moore/publications/trecia/support/vcg-examples.lisp" ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2>