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=7).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=9).GC finished] [SGC for 618 CONS pages..(3101 writable)..(T=8).GC finished] [SGC for 618 CONS pages..(3102 writable)..(T=9).GC finished] [SGC for 618 CONS pages..(3103 writable)..(T=10).GC finished] [SGC for 618 CONS pages..(3103 writable)..(T=9).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=10).GC finished] [SGC for 618 CONS pages..(3105 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC for 618 CONS pages..(3106 writable)..(T=11).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=46).GC finished] [SGC on] Loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o [SGC for 0 CONTIGUOUS-BLOCKS pages..(2552 writable)..(T=7).GC finished] start address -T 0x9b3d000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o [SGC for 1122 CONS pages..(3012 writable)..(T=11).GC finished] [SGC for 1122 CONS pages..(3029 writable)..(T=12).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 0x9b5e170 Finished loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o [SGC for 1122 CONS pages..(3051 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 0x9b62790 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b624f0 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 0x9b3b500 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b3b1b0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x92fffc0 Finished loading /projects/acl2/v2-7/books/arithmetic/rationals.o Loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b614a0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o [SGC for 1122 CONS pages..(3070 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 0x92fe000 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 0x9b5d840 Finished loading /projects/acl2/v2-7/books/meta/meta-plus-lessp.o [SGC for 1122 CONS pages..(3102 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 0x9b5af20 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b59f40 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 0x9b5b5d0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9b5ca80 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 0x9b5c760 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b5cb90 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 0x9b5b7d0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9b5bc40 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b5bb60 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 0x9b5a5c0 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b58a80 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 0x9b5cd10 Finished loading /projects/acl2/v2-7/books/arithmetic/top-with-meta.o [SGC for 1122 CONS pages..(3158 writable)..(T=14).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 1122 CONS pages..(3240 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 1122 CONS pages..(3299 writable)..(T=14).GC finished] [SGC for 1122 CONS pages..(3330 writable)..(T=14).GC finished] [SGC for 1122 CONS pages..(3364 writable)..(T=14).GC finished] [SGC for 0 RELOCATABLE-BLOCKS pages..(3398 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 0x9b8c6f0 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 1122 CONS pages..(3939 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 0x9b8ade0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o Loading /projects/acl2/v2-7/books/arithmetic/rational-listp.o start address -T 0x9b79c80 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 0x9b810f0 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9c67f80 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 0x9c51760 Finished loading /projects/acl2/v2-7/books/arithmetic/equalities.o start address -T 0x9c515f0 Finished loading /projects/acl2/v2-7/books/arithmetic/inequalities.o start address -T 0x9b81250 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 0x9b8af60 Finished loading /projects/acl2/v2-7/books/meta/term-defuns.o start address -T 0x9b89f40 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 0x9b82890 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 [SGC for 1122 CONS pages..(3947 writable)..(T=17).GC finished] Loading /projects/acl2/v2-7/books/data-structures/utilities.o [SGC for 0 CONTIGUOUS-BLOCKS pages..(3952 writable)..(T=17).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 0x9c51900 Finished loading /projects/acl2/v2-7/books/ihs/ihs-theories.o start address -T 0x9b81ac0 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.76 seconds (prove: 0.00, print: 0.01, other: 13.75) "/v/net2/v2/users/prof/moore/publications/trecia/support/utilities.lisp" ACL2 !> Summary Form: ( DEFCONST *DEMO-CLASS-TABLE-IN-TAGGED-FORM* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *DEMO-CLASS-TABLE-IN-TAGGED-FORM* Summary Form: ( DEFCONST *DEMO-MAIN* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *DEMO-MAIN* Summary Form: ( DEFUN DEMO-MS ...) Rules: ((:TYPE-PRESCRIPTION MAKE-STATE)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DEMO-MS Summary Form: ( DEFUN DEMO ...) Rules: ((:TYPE-PRESCRIPTION M5_LOAD)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DEMO Summary Form: ( DEFCONST *DEMO-THREAD-TABLE* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *DEMO-THREAD-TABLE* Summary Form: ( DEFCONST *DEMO-HEAP* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *DEMO-HEAP* Summary Form: ( DEFCONST *DEMO-CLASS-TABLE* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *DEMO-CLASS-TABLE* Summary Form: ( DEFCONST *DEMO-STATE* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *DEMO-STATE* Summary Form: ( DEFTHM DEMO-STATE-IS-DEMO ...) Rules: ((:EXECUTABLE-COUNTERPART DEMO) (:EXECUTABLE-COUNTERPART EQUAL)) Warnings: None Time: 0.05 seconds (prove: 0.04, print: 0.00, other: 0.01) DEMO-STATE-IS-DEMO Summary Form: ( DEFUN FACTORIAL ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACTORIAL Summary Form: ( DEFTHM INTEGERP-FACTORIAL ...) Rules: ((:TYPE-PRESCRIPTION FACTORIAL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INTEGERP-FACTORIAL Summary Form: ( DEFUN FACT-SCHED ...) Rules: ((:TYPE-PRESCRIPTION ACL2::APPEND-TRUE-LISTP-TYPE-PRESCRIPTION) (:TYPE-PRESCRIPTION REPEAT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FACT-SCHED Summary Form: ( DEFTHM LEN-REPEAT ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIX) (:DEFINITION LEN) (:DEFINITION NFIX) (:DEFINITION REPEAT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CDR-CONS) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION REPEAT)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) LEN-REPEAT [SGC for 1122 CONS pages..(3987 writable)..(T=16).GC finished] Summary Form: ( DEFTHM LEN-APPEND ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION FIX) (:DEFINITION LEN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CDR-CONS) (:REWRITE ACL2::COMMUTATIVITY-2-OF-+) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION LEN)) Warnings: None Time: 0.19 seconds (prove: 0.01, print: 0.00, other: 0.18) LEN-APPEND Summary Form: ( DEFTHM LEN-FACT-SCHED ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (:DEFINITION BINARY-APPEND) (:DEFINITION FACT-SCHED) (:DEFINITION FIX) (:DEFINITION LEN) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION REPEAT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART BINARY-*) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DISTRIBUTIVITY) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE LEN-APPEND) (:REWRITE REPEAT-OPENER) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2::APPEND-TRUE-LISTP-TYPE-PRESCRIPTION) (:TYPE-PRESCRIPTION BINARY-APPEND) (:TYPE-PRESCRIPTION FACT-SCHED)) Warnings: None Time: 0.09 seconds (prove: 0.08, print: 0.00, other: 0.01) LEN-FACT-SCHED Summary Form: ( DEFUN MAIN-SCHED ...) Rules: ((:TYPE-PRESCRIPTION ACL2::APPEND-TRUE-LISTP-TYPE-PRESCRIPTION) (:TYPE-PRESCRIPTION FACT-SCHED) (:TYPE-PRESCRIPTION REPEAT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) MAIN-SCHED [SGC for 1122 CONS pages..(3989 writable)..(T=16).GC finished] [SGC for 1122 CONS pages..(3989 writable)..(T=16).GC finished] Summary Form: ( DEFTHM SAMPLE-EXECUTION ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART MAIN-SCHED) (:EXECUTABLE-COUNTERPART RUN) (:EXECUTABLE-COUNTERPART STATIC-FIELD-VALUE)) Warnings: None Time: 0.51 seconds (prove: 0.50, print: 0.00, other: 0.01) SAMPLE-EXECUTION Summary Form: ( DEFCONST *FACT-DEF* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *FACT-DEF* Summary Form: ( DEFUN POISED-TO-INVOKE-FACT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) POISED-TO-INVOKE-FACT Summary Form: ( DEFUN INDUCTION-HINT ...) Rules: ((:TYPE-PRESCRIPTION MAKE-STATE)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INDUCTION-HINT [SGC for 1122 CONS pages..(3990 writable)..(T=16).GC finished] [SGC for 1122 CONS pages..(3990 writable)..(T=16).GC finished] [SGC for 1122 CONS pages..(3990 writable)..(T=16).GC finished] [SGC for 1122 CONS pages..(3990 writable)..(T=15).GC finished] [SGC for 1122 CONS pages..(3990 writable)..(T=16).GC finished] [SGC for 1122 CONS pages..(3990 writable)..(T=17).GC finished] [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=52).GC finished] [SGC on][SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=52).GC finished] [SGC on] Summary Form: ( DEFTHM INDUCTION-HINT-EXPLANATION ...) Rules: ((: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-INVOKESTATIC) (:DEFINITION EXECUTE-ISUB) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION POPN) (:DEFINITION REPEAT) (:DEFINITION REVERSE) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART ARG2) (:EXECUTABLE-COUNTERPART ARG3) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART METHOD-PROGRAM) (:EXECUTABLE-COUNTERPART METHOD-SYNC) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART REVERSE) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE BIND-FORMALS-OPENER) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA3) (:REWRITE INT-LEMMA6) (:REWRITE NTH-OPENER) (:REWRITE POPN-OPENER) (:REWRITE REPEAT-OPENER) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 4.45 seconds (prove: 4.43, print: 0.00, other: 0.02) INDUCTION-HINT-EXPLANATION [SGC for 1391 CONS pages..(3044 writable)..(T=13).GC finished] [SGC for 1391 CONS pages..(3044 writable)..(T=13).GC finished] [SGC for 1391 CONS pages..(3044 writable)..(T=13).GC finished] [SGC for 1391 CONS pages..(3047 writable)..(T=14).GC finished] [SGC for 1391 CONS pages..(3047 writable)..(T=13).GC finished] [SGC for 1391 CONS pages..(3050 writable)..(T=13).GC finished] [SGC for 1391 CONS pages..(3052 writable)..(T=13).GC finished] [SGC for 1391 CONS pages..(3052 writable)..(T=11).GC finished] Summary Form: ( DEFTHM FACT-IS-CORRECT ...) Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER) (: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-SCHED) (:DEFINITION FACTORIAL) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION POPN) (:DEFINITION REPEAT) (:DEFINITION REVERSE) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART ARG1) (:EXECUTABLE-COUNTERPART ARG2) (:EXECUTABLE-COUNTERPART ARG3) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART INT-FIX) (:EXECUTABLE-COUNTERPART METHOD-PROGRAM) (:EXECUTABLE-COUNTERPART METHOD-SYNC) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART PUSH) (:EXECUTABLE-COUNTERPART REVERSE) (:EXECUTABLE-COUNTERPART TOP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE BIND-BIND) (:REWRITE BIND-FORMALS-OPENER) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA3) (:REWRITE INT-LEMMA4A) (:REWRITE INT-LEMMA6) (:REWRITE NTH-OPENER) (:REWRITE POPN-OPENER) (:REWRITE REPEAT-OPENER) (:REWRITE RUN-APPEND) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION FACTORIAL) (:TYPE-PRESCRIPTION INTEGERP-FACTORIAL) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 6.62 seconds (prove: 6.60, print: 0.00, other: 0.02) FACT-IS-CORRECT Summary Form: (IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) 2944 [SGC for 1391 CONS pages..(3068 writable)..(T=14).GC finished] Summary Form: ( DEFTHM WEAK-VERSION-OF-FACT-IS-CORRECT ...) Rules: ((:DEFINITION BINDING) (:DEFINITION BOUND?) (:DEFINITION CALL-STACK) (:DEFINITION CLASS-DECL-METHODS) (:DEFINITION CLASS-DECL-SUPERCLASSES) (:DEFINITION LOOKUP-METHOD) (:DEFINITION LOOKUP-METHOD-IN-SUPERCLASSES) (:DEFINITION MAKE-THREAD) (:DEFINITION NEXT-INST) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE ASSOC-EQUAL-BIND) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE FACT-IS-CORRECT) (:REWRITE FRAMES) (:REWRITE NTH-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 1.15 seconds (prove: 1.14, print: 0.00, other: 0.01) WEAK-VERSION-OF-FACT-IS-CORRECT [SGC for 1391 CONS pages..(3078 writable)..(T=13).GC finished] Summary Form: ( DEFTHM SYMBOLIC-COMPUTATION ...) Rules: ((:DEFINITION ASSOC-EQUAL) (:DEFINITION BIND) (:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-IADD) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION EXECUTE-IMUL) (:DEFINITION EXECUTE-ISTORE_X) (:DEFINITION FACTORIAL) (:DEFINITION FIX) (:DEFINITION MAKE-THREAD) (:DEFINITION MAKE-TT) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:DEFINITION UPDATE-NTH) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART LOOKUP-METHOD) (:EXECUTABLE-COUNTERPART NTH) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART REPEAT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FACT-IS-CORRECT) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA4A) (:REWRITE INT-LEMMA6) (:REWRITE NTH-OPENER) (:REWRITE RUN-APPEND) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE UNICITY-OF-0) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION FACTORIAL) (:TYPE-PRESCRIPTION INTEGERP-FACTORIAL) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.42 seconds (prove: 0.41, print: 0.00, other: 0.01) SYMBOLIC-COMPUTATION Summary Form: ( DEFUN ALPHA ...) Rules: ((:TYPE-PRESCRIPTION MAKE-STATE)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ALPHA Summary Form: ( DEFTHM SYMBOLIC-COMPUTATION-STEP1 ...) Rules: ((:DEFINITION ALPHA) (:DEFINITION MAKE-TT) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART REPEAT) (:REWRITE RUN-APPEND) (:REWRITE RUN-OPENER)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) SYMBOLIC-COMPUTATION-STEP1 Summary Form: ( DEFTHM SYMBOLIC-COMPUTATION-STEP2 ...) Rules: ((:DEFINITION ALPHA) (:DEFINITION ASSOC-EQUAL) (:DEFINITION BIND) (:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-IADD) (:DEFINITION EXECUTE-ICONST_X) (:DEFINITION EXECUTE-ILOAD_X) (:DEFINITION MAKE-THREAD) (:DEFINITION MAKE-TT) (:DEFINITION NEXT-INST) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART NTH) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART REPEAT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA6) (:REWRITE NTH-OPENER) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.16 seconds (prove: 0.15, print: 0.00, other: 0.01) SYMBOLIC-COMPUTATION-STEP2 Summary Form: ( DEFTHM SYMBOLIC-COMPUTATION-STEP3 ...) Rules: ((:DEFINITION ALPHA) (:DEFINITION ASSOC-EQUAL) (:DEFINITION BIND) (:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION FACTORIAL) (:DEFINITION FIX) (:DEFINITION MAKE-THREAD) (:DEFINITION MAKE-TT) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION POISED-TO-INVOKE-FACT) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART LOOKUP-METHOD) (:EXECUTABLE-COUNTERPART NTH) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE FACT-IS-CORRECT) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE FRAMES) (:REWRITE NTH-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE UNICITY-OF-0) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.06 seconds (prove: 0.05, print: 0.00, other: 0.01) SYMBOLIC-COMPUTATION-STEP3 Summary Form: ( DEFTHM SYMBOLIC-COMPUTATION-STEP4 ...) Rules: ((:DEFINITION ALPHA) (:DEFINITION ASSOC-EQUAL) (:DEFINITION BIND) (:DEFINITION BINDING) (:DEFINITION CALL-STACK) (:DEFINITION DO-INST) (:DEFINITION EXECUTE-IMUL) (:DEFINITION EXECUTE-ISTORE_X) (:DEFINITION FACTORIAL) (:DEFINITION FIX) (:DEFINITION MAKE-THREAD) (:DEFINITION MAKE-TT) (:DEFINITION NEXT-INST) (:DEFINITION NOT) (:DEFINITION RREF) (:DEFINITION STATUS) (:DEFINITION SYNP) (:DEFINITION TOP-FRAME) (:DEFINITION UPDATE-NTH) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INDEX-INTO-PROGRAM) (:EXECUTABLE-COUNTERPART INST-LENGTH) (:EXECUTABLE-COUNTERPART NTH) (:EXECUTABLE-COUNTERPART OP-CODE) (:EXECUTABLE-COUNTERPART REPEAT) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING INT-LEMMA0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE ACL2::FOLD-CONSTS-IN-+) (:REWRITE FRAMES) (:REWRITE INT-LEMMA4A) (:REWRITE NTH-OPENER) (:REWRITE RUN-OPENER) (:REWRITE STACKS) (:REWRITE STATES) (:REWRITE STEP-OPENER) (:REWRITE UNICITY-OF-0) (:REWRITE ACL2::ZP-OPEN) (:TYPE-PRESCRIPTION FACTORIAL) (:TYPE-PRESCRIPTION INTEGERP-FACTORIAL) (:TYPE-PRESCRIPTION INTP)) Warnings: None Time: 0.13 seconds (prove: 0.12, print: 0.00, other: 0.01) SYMBOLIC-COMPUTATION-STEP4 Summary Form: ( INCLUDE-BOOK "demo" ...) Rules: NIL Warnings: None Time: 0.14 seconds (prove: 0.00, print: 0.00, other: 0.14) Compiling /v/net2/v2/users/prof/moore/publications/trecia/support/demo.lisp. End of Pass 1. ;; Note: Tail-recursive call of INDUCTION-HINT 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/demo.o. "/v/net2/v2/users/prof/moore/publications/trecia/support/demo.o" Loading /v/net2/v2/users/prof/moore/publications/trecia/support/demo.o start address -T 0x9c83020 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/demo.o Summary Form: (CERTIFY-BOOK "demo" ...) Rules: NIL Warnings: None Time: 14.21 seconds (prove: 13.55, print: 0.00, other: 0.66) "/v/net2/v2/users/prof/moore/publications/trecia/support/demo.lisp" ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2>