[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] 2.6.2.....
|
From: |
Matt Kaufmann |
|
Subject: |
Re: [Gcl-devel] 2.6.2..... |
|
Date: |
Tue, 15 Jun 2004 08:23:23 -0500 |
Hi, Mike --
Thanks, that helps -- I think I know what's going on. When we release a new
version of ACL2, we also update the workshops/ books. I appears that you're
using the workshops/ books that came with the previous version of ACL2 (2.7)
rather than the current one (2.8). The current one can be obtained by way of
the installation instructions from the ACL2 home page, or directly at:
ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-8/acl2-sources/books/workshops.tar.gz
I'm really delighted and grateful that ACL2 is used in the GCL testing process.
Testing the workshops books is icing on the cake, and may not add enough to be
worth your trouble. (But since there _was_ an error, I'm glad we tracked it
down.) Anyhow, I'm a little surprised actually that there weren't massive
failures using the old workshops/.
Thanks --
-- Matt
From: "Mike Thomas" <address@hidden>
Cc: <address@hidden>, <address@hidden>
Date: Tue, 15 Jun 2004 14:25:06 +1000
Content-Type: text/plain;
charset="iso-8859-1"
X-Priority: 3 (Normal)
X-MSMail-Priority: Normal
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1409
Importance: Normal
X-SpamAssassin-Status: No, hits=-4.1 required=5.0
X-UTCS-Spam-Status: No, hits=-211 required=180
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.
- Re: [Gcl-devel] 2.6.2....., (continued)
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/08
- Re: [Gcl-devel] 2.6.2....., Matt Kaufmann, 2004/06/08
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/08
- Re: [Gcl-devel] 2.6.2....., Camm Maguire, 2004/06/12
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/14
- Re: [Gcl-devel] 2.6.2....., Matt Kaufmann, 2004/06/14
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/14
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/15
- Re: [Gcl-devel] 2.6.2.....,
Matt Kaufmann <=
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/15
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/28
- Re: [Gcl-devel] 2.6.2....., Camm Maguire, 2004/06/28
- Re: [Gcl-devel] 2.6.2....., Matt Kaufmann, 2004/06/28
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/28
- Re: [Gcl-devel] 2.6.2....., Camm Maguire, 2004/06/12
- RE: [Gcl-devel] 2.6.2....., Mike Thomas, 2004/06/14
- Re: [Gcl-devel] 2.6.2....., Camm Maguire, 2004/06/17
- Re: [Gcl-devel] 2.6.2....., Camm Maguire, 2004/06/07
Re: [Gcl-devel] 2.6.2....., Vadim V. Zhytnikov, 2004/06/07