gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

RE: [Gcl-devel] 2.6.2.....


From: Mike Thomas
Subject: RE: [Gcl-devel] 2.6.2.....
Date: Tue, 15 Jun 2004 14:25:06 +1000

Hi Matt.

| Perhaps the failure was just some weird Windows glitch, which
| would go away in
| a re-run?

Further to this I cd'ed to the ivy-sources directory and managed to get an
error message about the name natp already being in use - below (don't know
why the out file was empty in the main certification build, but there you
go).  I removed the natp definition, which fixed that first problem until a
further error in alls.out (also below).

So my gut feeling is that there is a problem in the way this particular test
is set up rather than with GCL - may be wrong though as I'm skimming.

Cheers

Mike Thomas.



===================================================================
GCL (GNU Common Lisp)  2.6.2 CLtL1   Jun  7 2004 13:26:07
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License:  GPL due to GPL'ed components: (UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter

Use (help) to get some basic information on how to use GCL.

 ACL2 Version 2.8 built June 7, 2004  14:49:49.
 Copyright (C) 2004  University of Texas at Austin
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the GNU General Public License.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* T
                      NIL NIL).
 See the documentation topic note-2-8 for recent changes.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc;
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

ACL2 Version 2.8.  Level 1.  Cbd
"c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sou
rces/".

Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
ACL2>
#<"ACL2" package>

ACL2>
ACL2 Version 2.8.  Level 1.  Cbd
"c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sou
rces/".

Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
ACL2 !>
Loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/sets.o
start address -T 104ead90 Finished loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/sets.o

Summary
Form:  ( INCLUDE-BOOK "sets" ...)
Rules: NIL
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)
"c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sou
rces/sets.lisp"


ACL2 Error in ( DEFMACRO NATP ...):  The name NATP is in use as a function.
The redefinition feature is currently off.  See :DOC ld-redefinition-
action.


Summary
Form:  ( DEFMACRO NATP ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

******** FAILED ********  See :DOC failure  ******** FAILED ********

Summary
Form:  (CERTIFY-BOOK "base" ...)
Rules: NIL
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>

====================================================================
GCL (GNU Common Lisp)  2.6.2 CLtL1   Jun  7 2004 13:26:07
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License:  GPL due to GPL'ed components: (UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter

Use (help) to get some basic information on how to use GCL.

 ACL2 Version 2.8 built June 7, 2004  14:49:49.
 Copyright (C) 2004  University of Texas at Austin
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the GNU General Public License.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* T
                      NIL NIL).
 See the documentation topic note-2-8 for recent changes.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc;
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

ACL2 Version 2.8.  Level 1.  Cbd
"c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sou
rces/".

Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
ACL2>
#<"ACL2" package>

ACL2>
ACL2 Version 2.8.  Level 1.  Cbd
"c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sou
rces/".

Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
ACL2 !>
Loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/sets.o
start address -T 104ead90 Finished loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/sets.o
[GC for 500 RELOCATABLE-BLOCKS pages..(T=10).GC finished]
Loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/base.o
start address -T 10656000 Finished loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/base.o
[GC for 500 RELOCATABLE-BLOCKS pages..(T=7).GC finished]
Loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/variables.o
start address -T 104616b0 Finished loading
c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sour
ces/variables.o

Summary
Form:  ( INCLUDE-BOOK "variables" ...)
Rules: NIL
Warnings:  None
Time:  0.55 seconds (prove: 0.00, print: 0.00, other: 0.55)
"c:/lang/source/gcl/acl2-sources-2.8/books/workshops/1999/ivy/ivy-v2/ivy-sou
rces/variables.lisp"

Summary
Form:  ( DEFUN ALLS ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION NOT)
        (:DEFINITION VAR-LIST)
        (:DEFINITION VARIABLE-TERM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALLS

Summary
Form:  ( DEFTHM ALLS-VARS-F-WFF ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION VAR-LIST)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFATOM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFF)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:INDUCTION VAR-LIST)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION WFF))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
ALLS-VARS-F-WFF

Summary
Form:  ( DEFTHM SUBST-ALLS-COMMUTE ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION SUBST-FREE)
        (:DEFINITION VAR-LIST)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:INDUCTION MEMBER-EQUAL)
        (:INDUCTION VAR-LIST)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
SUBST-ALLS-COMMUTE

Summary
Form:  ( DEFTHM REMOVE-VARS-ALLS ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:REWRITE SUBST-ALLS-COMMUTE)
        (:TYPE-PRESCRIPTION DOMAIN-TERM)
        (:TYPE-PRESCRIPTION FREE-VARS-TYPE)
        (:TYPE-PRESCRIPTION VAR-LIST))
Warnings:  None
Time:  0.05 seconds (prove: 0.05, print: 0.00, other: 0.00)
REMOVE-VARS-ALLS

Summary
Form:  ( DEFTHM ALLS-PRESERVES-CLOSEDNESS ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION FREE-VARS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION REMOVE-EQUAL)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFATOMTOP)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.05 seconds (prove: 0.05, print: 0.00, other: 0.00)
ALLS-PRESERVES-CLOSEDNESS

Summary
Form:  ( DEFTHM ALLS-ALL ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION VAR-LIST)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:INDUCTION VAR-LIST)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION WFALL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALLS-ALL

Summary
Form:  ( DEFTHM ALLS-QUANT ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION VAR-LIST)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:INDUCTION VAR-LIST)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION WFQUANT))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
ALLS-QUANT

Summary
Form:  ( DEFUN REMOVE-LEADING-ALLS ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION FIX)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:DEFINITION WFATOM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFF)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REMOVE-LEADING-ALLS

Summary
Form:  ( DEFTHM REMOVE-LEADING-ALLS-PRESERVES-WFF ...)
Rules: ((:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION LOGIC-SYMBOLP)
        (:DEFINITION NOT)
        (:DEFINITION RELATION-SYMBOL)
        (:DEFINITION REMOVE-LEADING-ALLS)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:DEFINITION WFATOM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFF)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:DEFINITION WFT-LIST)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART LIST2P)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:EXECUTABLE-COUNTERPART REMOVE-LEADING-ALLS)
        (:EXECUTABLE-COUNTERPART WFF)
        (:EXECUTABLE-COUNTERPART WFT-LIST)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION REMOVE-LEADING-ALLS)
        (:INDUCTION WFF)
        (:TYPE-PRESCRIPTION WFF)
        (:TYPE-PRESCRIPTION WFT-LIST))
Warnings:  None
Time:  0.15 seconds (prove: 0.15, print: 0.00, other: 0.00)
REMOVE-LEADING-ALLS-PRESERVES-WFF

Summary
Form:  ( DEFUN LEADING-ALLS ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION FIX)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:DEFINITION WFATOM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFF)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEADING-ALLS

Summary
Form:  ( DEFTHM LEAD-ALLS-VAR-LIST ...)
Rules: ((:DEFINITION LEADING-ALLS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION VAR-LIST)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART VAR-LIST)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEADING-ALLS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION LEADING-ALLS)
        (:TYPE-PRESCRIPTION VAR-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEAD-ALLS-VAR-LIST

Summary
Form:  ( DEFTHM ALLS-LEAD-REMOVE-F-IS-F ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION LEADING-ALLS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION REMOVE-LEADING-ALLS)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEADING-ALLS)
        (:INDUCTION REMOVE-LEADING-ALLS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION LEADING-ALLS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALLS-LEAD-REMOVE-F-IS-F

Summary
Form:  ( DEFUN REMOVE-LEADING-QUANTS ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION FIX)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION LOGIC-SYMBOLP)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION RELATION-SYMBOL)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFATOM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFF)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION WFT-LIST))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
REMOVE-LEADING-QUANTS

Summary
Form:  ( DEFUN LEADING-QUANTS ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION FIX)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION LOGIC-SYMBOLP)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION RELATION-SYMBOL)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFATOM)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFF)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION WFT-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEADING-QUANTS

Summary
Form:  ( DEFTHM LEADING-ALL-IS-QUANTIFIED-VAR ...)
Rules: ((:DEFINITION LEADING-ALLS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION QUANTIFIED-VARS)
        (:DEFINITION SUBSETP-EQUAL)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEADING-ALLS)
        (:INDUCTION QUANTIFIED-VARS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE MEMBER-APPEND-LEFT)
        (:REWRITE MEMBER-APPEND-RIGHT)
        (:REWRITE NOT-MEMBER-SUBSET)
        (:REWRITE SUBSET-REFLEXIVE)
        (:TYPE-PRESCRIPTION LEADING-ALLS)
        (:TYPE-PRESCRIPTION MEMBER-EQUAL))
Warnings:  None
Time:  0.12 seconds (prove: 0.10, print: 0.00, other: 0.02)
LEADING-ALL-IS-QUANTIFIED-VAR
[GC for 5152 CONS pages..(T=7).GC finished]

Summary
Form:  ( DEFTHM SETP-QVARS-LEADING-ALLS ...)
Rules: ((:DEFINITION LEADING-ALLS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION QUANTIFIED-VARS)
        (:DEFINITION SETP)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFALL)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEADING-ALLS)
        (:INDUCTION QUANTIFIED-VARS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE LEADING-ALL-IS-QUANTIFIED-VAR)
        (:REWRITE SETP-APPEND-1)
        (:REWRITE SETP-APPEND-2)
        (:TYPE-PRESCRIPTION LEADING-ALLS)
        (:TYPE-PRESCRIPTION SETP))
Warnings:  None
Time:  0.17 seconds (prove: 0.17, print: 0.00, other: 0.00)
SETP-QVARS-LEADING-ALLS

Summary
Form:  ( DEFTHM VARSET-QVARS-LEADING-ALLS ...)
Rules: ((:REWRITE LEAD-ALLS-VAR-LIST)
        (:REWRITE SETP-QVARS-LEADING-ALLS)
        (:REWRITE VAR-LIST-QUANTIFIED-VARS)
        (:TYPE-PRESCRIPTION SETP)
        (:TYPE-PRESCRIPTION VAR-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
VARSET-QVARS-LEADING-ALLS

Summary
Form:  ( DEFTHM ALLS-ELIMINATES-FREE-VARS ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION FREE-VARS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION MEMBER-EQUAL)
        (:DEFINITION NOT)
        (:DEFINITION SUBSETP-EQUAL)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFATOMTOP)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:INDUCTION MEMBER-EQUAL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE NOT-MEMBER-NOT-MEMBER-REMOVE)
        (:REWRITE NOT-MEMBER-SUBSET)
        (:REWRITE REMOVED-ELEMENT-IS-NOT-MEMBER))
Warnings:  None
Time:  0.25 seconds (prove: 0.25, print: 0.00, other: 0.00)
ALLS-ELIMINATES-FREE-VARS

Summary
Form:  ( DEFTHM ALLS-DOESNT-INTRODUCE-FREE-VARS ...)
Rules: ((:DEFINITION ALLS)
        (:DEFINITION ATOM)
        (:DEFINITION FREE-VARS)
        (:DEFINITION LIST2P)
        (:DEFINITION LIST3P)
        (:DEFINITION NOT)
        (:DEFINITION SUBSETP-EQUAL)
        (:DEFINITION VARIABLE-TERM)
        (:DEFINITION WFATOMTOP)
        (:DEFINITION WFBINARY)
        (:DEFINITION WFNOT)
        (:DEFINITION WFQUANT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART RELATION-SYMBOL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALLS)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE NOT-MEMBER-NOT-MEMBER-REMOVE)
        (:REWRITE NOT-MEMBER-SUBSET)
        (:REWRITE SUBSET-REFLEXIVE))
Warnings:  None
Time:  0.20 seconds (prove: 0.20, print: 0.00, other: 0.00)
ALLS-DOESNT-INTRODUCE-FREE-VARS

Summary
Form:  ( DEFTHM UNIVERSAL-CLOSURE-IS-CLOSED-ALMOST-IN-FINAL-FORM ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UNIVERSAL-CLOSURE-IS-CLOSED-ALMOST-IN-FINAL-FORM

Summary
Form:  ( DEFMACRO UNIVERSAL-CLOSURE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UNIVERSAL-CLOSURE

Summary
Form:  ( DEFTHM UNIVERSAL-CLOSURE-IS-CLOSED ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE UNIVERSAL-CLOSURE-IS-CLOSED-ALMOST-IN-FINAL-FORM)
        (:TYPE-PRESCRIPTION FREE-VARS-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UNIVERSAL-CLOSURE-IS-CLOSED

Summary
Form:  ( DEFUN VAR-INDUCT ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)

******** FAILED ********  See :DOC failure  ******** FAILED ********

Summary
Form:  (CERTIFY-BOOK "alls" ...)
Rules: NIL
Warnings:  None
Time:  1.62 seconds (prove: 1.03, print: 0.00, other: 0.58)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>
====================================================================


Cheers

Mike Thomas.





reply via email to

[Prev in Thread] Current Thread [Next in Thread]