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 !>
Summary
Form:  ( DEFPKG "LABEL" ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 "LABEL"
ACL2 !>
Summary
Form:  ( DEFPKG "JVM" ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 "JVM"
ACL2 !>
Summary
Form:  ( DEFPKG "M5" ...)
Rules: NIL
Warnings:  None
Time:  0.10 seconds (prove: 0.00, print: 0.00, other: 0.10)
 "M5"
ACL2 !>
Summary
Form:  ( DEFUN PUSH ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PUSH

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

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

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

Summary
Form:  ( DEFUN BOUND? ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BOUND?

Summary
Form:  ( DEFUN BIND ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
BIND

Summary
Form:  ( DEFUN BINDING ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
BINDING

Summary
Form:  ( DEFUN OP-CODE ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
OP-CODE

Summary
Form:  ( DEFUN ARG1 ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ARG1

Summary
Form:  ( DEFUN ARG2 ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ARG2

Summary
Form:  ( DEFUN ARG3 ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ARG3

Summary
Form:  ( DEFUN NULLREFP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
NULLREFP

Summary
Form:  ( DEFUN REVERSE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BINARY-APPEND))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
REVERSE

Summary
Form:  ( DEFCONST *LARGEST-INTEGER-VALUE* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*LARGEST-INTEGER-VALUE*

Summary
Form:  ( DEFCONST *LARGEST-LONG-VALUE* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*LARGEST-LONG-VALUE*

Summary
Form:  ( DEFCONST *MOST-NEGATIVE-INTEGER* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*MOST-NEGATIVE-INTEGER*

Summary
Form:  ( DEFCONST *MOST-NEGATIVE-LONG* ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
*MOST-NEGATIVE-LONG*

Summary
Form:  ( DEFUN U-FIX ...)
Rules: ((:TYPE-PRESCRIPTION MOD))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
U-FIX

Summary
Form:  ( DEFUN S-FIX ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION MOD))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
S-FIX

Summary
Form:  ( DEFUN BYTE-FIX ...)
Rules: ((:TYPE-PRESCRIPTION S-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BYTE-FIX

Summary
Form:  ( DEFUN UBYTE-FIX ...)
Rules: ((:TYPE-PRESCRIPTION U-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UBYTE-FIX

Summary
Form:  ( DEFUN SHORT-FIX ...)
Rules: ((:TYPE-PRESCRIPTION S-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SHORT-FIX

Summary
Form:  ( DEFUN INT-FIX ...)
Rules: ((:TYPE-PRESCRIPTION S-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INT-FIX

Summary
Form:  ( DEFUN UINT-FIX ...)
Rules: ((:TYPE-PRESCRIPTION U-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UINT-FIX

Summary
Form:  ( DEFUN LONG-FIX ...)
Rules: ((:TYPE-PRESCRIPTION S-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LONG-FIX

Summary
Form:  ( DEFUN ULONG-FIX ...)
Rules: ((:TYPE-PRESCRIPTION U-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ULONG-FIX

Summary
Form:  ( DEFUN CHAR-FIX ...)
Rules: ((:TYPE-PRESCRIPTION U-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CHAR-FIX

Summary
Form:  ( DEFUN |6-BIT-FIX| ...)
Rules: ((:TYPE-PRESCRIPTION U-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
|6-BIT-FIX|

Summary
Form:  ( DEFUN |5-BIT-FIX| ...)
Rules: ((:TYPE-PRESCRIPTION U-FIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
|5-BIT-FIX|

Summary
Form:  ( DEFUN EXPT2 ...)
Rules: ((:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE)
        (:TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EXPT2

Summary
Form:  ( DEFUN SHL ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
SHL

Summary
Form:  ( DEFUN SHR ...)
Rules: ((:TYPE-PRESCRIPTION FLOOR))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
SHR

Summary
Form:  ( DEFUN MAKE-STATE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAKE-STATE

Summary
Form:  ( DEFUN THREAD-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
THREAD-TABLE

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

Summary
Form:  ( DEFUN CLASS-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-TABLE

Summary
Form:  ( DEFUN MAKE-THREAD ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAKE-THREAD

Summary
Form:  ( DEFUN CALL-STACK ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CALL-STACK

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

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

Summary
Form:  ( DEFUN MAKE-CLASS-DECL ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAKE-CLASS-DECL

Summary
Form:  ( DEFUN CLASS-DECL-NAME ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-NAME

Summary
Form:  ( DEFUN CLASS-DECL-SUPERCLASSES ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-SUPERCLASSES

Summary
Form:  ( DEFUN CLASS-DECL-FIELDS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-FIELDS

Summary
Form:  ( DEFUN CLASS-DECL-SFIELDS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-SFIELDS

Summary
Form:  ( DEFUN CLASS-DECL-CP ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-CP

Summary
Form:  ( DEFUN CLASS-DECL-METHODS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-METHODS

Summary
Form:  ( DEFUN CLASS-DECL-HEAPREF ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CLASS-DECL-HEAPREF

Summary
Form:  ( DEFUN BASE-CLASS-DEF ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BASE-CLASS-DEF

Summary
Form:  ( DEFUN MAKE-CLASS-DEF ...)
Rules: ((:TYPE-PRESCRIPTION BINARY-APPEND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAKE-CLASS-DEF

Summary
Form:  ( DEFUN CP-MAKE-INT-ENTRY ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CP-MAKE-INT-ENTRY

Summary
Form:  ( DEFUN CP-MAKE-STRING-ENTRY ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CP-MAKE-STRING-ENTRY

Summary
Form:  ( DEFUN CP-STRING-RESOLVED? ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
CP-STRING-RESOLVED?

Summary
Form:  ( DEFUN RETRIEVE-CP ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
RETRIEVE-CP

Summary
Form:  ( DEFUN UPDATE-CT-STRING-REF ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UPDATE-CT-STRING-REF

Summary
Form:  ( DEFUN MAKE-TT ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAKE-TT

Summary
Form:  ( DEFUN ADDTO-TT ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ADDTO-TT

Summary
Form:  ( DEFUN MOD-THREAD-SCHEDULING ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MOD-THREAD-SCHEDULING

Summary
Form:  ( DEFUN SCHEDULE-THREAD ...)
Rules: ((:TYPE-PRESCRIPTION MOD-THREAD-SCHEDULING))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SCHEDULE-THREAD

Summary
Form:  ( DEFUN UNSCHEDULE-THREAD ...)
Rules: ((:TYPE-PRESCRIPTION MOD-THREAD-SCHEDULING))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
UNSCHEDULE-THREAD

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

Summary
Form:  ( DEFUN IN-LIST ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-LIST

Summary
Form:  ( DEFUN ISTHREADOBJECT? ...)
Rules: ((:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ISTHREADOBJECT?

Summary
Form:  ( DEFUN LOCK-OBJECT ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LOCK-OBJECT

Summary
Form:  ( DEFUN UNLOCK-OBJECT ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
UNLOCK-OBJECT

Summary
Form:  ( DEFUN OBJECTLOCKABLE? ...)
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)
OBJECTLOCKABLE?

Summary
Form:  ( DEFUN OBJECTUNLOCKABLE? ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
OBJECTUNLOCKABLE?

Summary
Form:  ( DEFUN MAKE-FRAME ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MAKE-FRAME

Summary
Form:  ( DEFUN TOP-FRAME ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TOP-FRAME

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

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

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

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

Summary
Form:  ( DEFUN SYNC-FLG ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SYNC-FLG

Summary
Form:  ( DEFUN CUR-CLASS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CUR-CLASS

Summary
Form:  ( DEFUN METHOD-NAME ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
METHOD-NAME

Summary
Form:  ( DEFUN METHOD-FORMALS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
METHOD-FORMALS

Summary
Form:  ( DEFUN METHOD-SYNC ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
METHOD-SYNC

Summary
Form:  ( DEFUN METHOD-PROGRAM ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
METHOD-PROGRAM

Summary
Form:  ( DEFUN METHOD-ISNATIVE? ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
METHOD-ISNATIVE?

Summary
Form:  ( DEFUN SUPPLIEDP ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
SUPPLIEDP

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

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

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

Summary
Form:  ( DEFUN FIELD-VALUE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FIELD-VALUE

Summary
Form:  ( DEFUN BUILD-CLASS-FIELD-BINDINGS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-CLASS-FIELD-BINDINGS
[SGC for 618 CONS pages..(3097 writable)..(T=10).GC finished]

Summary
Form:  ( DEFUN BUILD-CLASS-OBJECT-FIELD-BINDINGS ...)
Rules: NIL
Warnings:  None
Time:  0.10 seconds (prove: 0.00, print: 0.00, other: 0.10)
BUILD-CLASS-OBJECT-FIELD-BINDINGS

Summary
Form:  ( DEFUN BUILD-IMMEDIATE-INSTANCE-DATA ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BUILD-CLASS-FIELD-BINDINGS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-IMMEDIATE-INSTANCE-DATA

Summary
Form:  ( DEFUN BUILD-AN-INSTANCE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-AN-INSTANCE

Summary
Form:  ( DEFUN BUILD-CLASS-DATA ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BUILD-CLASS-FIELD-BINDINGS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-CLASS-DATA

Summary
Form:  ( DEFUN BUILD-A-CLASS-INSTANCE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-A-CLASS-INSTANCE

Summary
Form:  ( DEFUN VALUE-OF ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
VALUE-OF

Summary
Form:  ( DEFUN SUPERCLASSES-OF ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUPERCLASSES-OF

Summary
Form:  ( DEFUN ARRAY-CONTENT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ARRAY-CONTENT

Summary
Form:  ( DEFUN ARRAY-TYPE ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ARRAY-TYPE

Summary
Form:  ( DEFUN ARRAY-BOUND ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ARRAY-BOUND

Summary
Form:  ( DEFUN ARRAY-DATA ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ARRAY-DATA

Summary
Form:  ( DEFUN ELEMENT-AT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ELEMENT-AT

Summary
Form:  ( DEFUN MAKEARRAY ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION BUILD-AN-INSTANCE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAKEARRAY

Summary
Form:  ( DEFUN SET-ELEMENT-AT ...)
Rules: ((:TYPE-PRESCRIPTION MAKEARRAY))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SET-ELEMENT-AT

Summary
Form:  ( DEFUN PRIMITIVE-TYPE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PRIMITIVE-TYPE

Summary
Form:  ( DEFUN ATYPE-TO-IDENTIFIER ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ATYPE-TO-IDENTIFIER

Summary
Form:  ( DEFUN IDENTIFIER-TO-ATYPE ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
IDENTIFIER-TO-ATYPE

Summary
Form:  ( DEFUN DEFAULT-VALUE1 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
DEFAULT-VALUE1

Summary
Form:  ( DEFUN INIT-ARRAY ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INIT-ARRAY

Summary
Form:  ( DEFUN NATURAL-SUM ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION NFIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NATURAL-SUM

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN MAKEMULTIARRAY2 ...) ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION E0-ORD-<)
        (:DEFINITION E0-ORDINALP)
        (:DEFINITION LEN)
        (:DEFINITION NATURAL-SUM)
        (:DEFINITION NFIX)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CDR-ELIM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:TYPE-PRESCRIPTION E0-ORDINALP)
        (:TYPE-PRESCRIPTION LEN)
        (:TYPE-PRESCRIPTION NATURAL-SUM))
Warnings:  None
Time:  0.10 seconds (prove: 0.06, print: 0.00, other: 0.04)
(MAKEMULTIARRAY2 MAKEMULTIARRAY)
[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=10).GC finished]

Summary
Form:  ( DEFUN INST-LENGTH ...)
Rules: NIL
Warnings:  None
Time:  0.97 seconds (prove: 0.00, print: 0.00, other: 0.97)
INST-LENGTH

Summary
Form:  ( DEFUN EXECUTE-AALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-AALOAD

Summary
Form:  ( DEFUN EXECUTE-AASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-AASTORE

Summary
Form:  ( DEFUN EXECUTE-ACONST_NULL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-ACONST_NULL

Summary
Form:  ( DEFUN EXECUTE-ALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ALOAD

Summary
Form:  ( DEFUN EXECUTE-ALOAD_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-ALOAD_X

Summary
Form:  ( DEFUN EXECUTE-ANEWARRAY ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ANEWARRAY

Summary
Form:  ( DEFUN EXECUTE-ARETURN ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
EXECUTE-ARETURN

Summary
Form:  ( DEFUN EXECUTE-ARRAYLENGTH ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-ARRAYLENGTH

Summary
Form:  ( DEFUN EXECUTE-ASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ASTORE

Summary
Form:  ( DEFUN EXECUTE-ASTORE_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ASTORE_X
[SGC for 618 CONS pages..(3102 writable)..(T=9).GC finished]

Summary
Form:  ( DEFUN EXECUTE-BALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.11 seconds (prove: 0.00, print: 0.00, other: 0.11)
EXECUTE-BALOAD

Summary
Form:  ( DEFUN EXECUTE-BASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-BASTORE

Summary
Form:  ( DEFUN EXECUTE-BIPUSH ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-BIPUSH

Summary
Form:  ( DEFUN EXECUTE-CALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-CALOAD

Summary
Form:  ( DEFUN EXECUTE-CASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-CASTORE

Summary
Form:  ( DEFUN EXECUTE-DUP ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-DUP

Summary
Form:  ( DEFUN EXECUTE-DUP_X1 ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-DUP_X1

Summary
Form:  ( DEFUN EXECUTE-DUP_X2 ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-DUP_X2

Summary
Form:  ( DEFUN EXECUTE-DUP2 ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-DUP2

Summary
Form:  ( DEFUN EXECUTE-DUP2_X1 ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-DUP2_X1

Summary
Form:  ( DEFUN EXECUTE-DUP2_X2 ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-DUP2_X2

Summary
Form:  ( DEFUN EXECUTE-GETFIELD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-GETFIELD

Summary
Form:  ( DEFUN STATIC-FIELD-VALUE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
STATIC-FIELD-VALUE

Summary
Form:  ( DEFUN EXECUTE-GETSTATIC ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-GETSTATIC

Summary
Form:  ( DEFUN EXECUTE-GOTO ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-GOTO

Summary
Form:  ( DEFUN EXECUTE-GOTO_W ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-GOTO_W

Summary
Form:  ( DEFUN EXECUTE-I2B ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-I2B

Summary
Form:  ( DEFUN EXECUTE-I2C ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-I2C

Summary
Form:  ( DEFUN EXECUTE-I2L ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-I2L
[SGC for 618 CONS pages..(3103 writable)..(T=10).GC finished]

Summary
Form:  ( DEFUN EXECUTE-I2S ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)
EXECUTE-I2S

Summary
Form:  ( DEFUN EXECUTE-IADD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IADD

Summary
Form:  ( DEFUN EXECUTE-IALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IALOAD

Summary
Form:  ( DEFUN EXECUTE-IAND ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IAND

Summary
Form:  ( DEFUN EXECUTE-IASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IASTORE

Summary
Form:  ( DEFUN EXECUTE-ICONST_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ICONST_X

Summary
Form:  ( DEFUN EXECUTE-IDIV ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IDIV

Summary
Form:  ( DEFUN EXECUTE-IF_ACMPEQ ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IF_ACMPEQ

Summary
Form:  ( DEFUN EXECUTE-IF_ACMPNE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IF_ACMPNE

Summary
Form:  ( DEFUN EXECUTE-IF_ICMPEQ ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IF_ICMPEQ

Summary
Form:  ( DEFUN EXECUTE-IF_ICMPGE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IF_ICMPGE

Summary
Form:  ( DEFUN EXECUTE-IF_ICMPGT ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IF_ICMPGT

Summary
Form:  ( DEFUN EXECUTE-IF_ICMPLT ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IF_ICMPLT

Summary
Form:  ( DEFUN EXECUTE-IF_ICMPLE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IF_ICMPLE

Summary
Form:  ( DEFUN EXECUTE-IF_ICMPNE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IF_ICMPNE

Summary
Form:  ( DEFUN EXECUTE-IFEQ ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IFEQ
[SGC for 618 CONS pages..(3104 writable)..(T=10).GC finished]

Summary
Form:  ( DEFUN EXECUTE-IFGE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.11 seconds (prove: 0.00, print: 0.00, other: 0.11)
EXECUTE-IFGE

Summary
Form:  ( DEFUN EXECUTE-IFGT ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IFGT

Summary
Form:  ( DEFUN EXECUTE-IFLE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IFLE

Summary
Form:  ( DEFUN EXECUTE-IFLT ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IFLT

Summary
Form:  ( DEFUN EXECUTE-IFNE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IFNE

Summary
Form:  ( DEFUN EXECUTE-IFNONNULL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IFNONNULL

Summary
Form:  ( DEFUN EXECUTE-IFNULL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IFNULL

Summary
Form:  ( DEFUN EXECUTE-IINC ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IINC

Summary
Form:  ( DEFUN EXECUTE-ILOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ILOAD

Summary
Form:  ( DEFUN EXECUTE-ILOAD_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-ILOAD_X

Summary
Form:  ( DEFUN EXECUTE-IMUL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IMUL

Summary
Form:  ( DEFUN EXECUTE-INEG ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-INEG

Summary
Form:  ( DEFUN EXECUTE-INSTANCEOF ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-INSTANCEOF

Summary
Form:  ( DEFUN EXECUTE-IOR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IOR

Summary
Form:  ( DEFUN EXECUTE-IREM ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IREM
[SGC for 618 CONS pages..(3105 writable)..(T=10).GC finished]

Summary
Form:  ( DEFUN EXECUTE-IRETURN ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)
EXECUTE-IRETURN

Summary
Form:  ( DEFUN EXECUTE-ISHL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-ISHL

Summary
Form:  ( DEFUN EXECUTE-ISHR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ISHR

Summary
Form:  ( DEFUN EXECUTE-ISTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ISTORE

Summary
Form:  ( DEFUN EXECUTE-ISTORE_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-ISTORE_X

Summary
Form:  ( DEFUN EXECUTE-ISUB ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-ISUB

Summary
Form:  ( DEFUN EXECUTE-IUSHR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-IUSHR

Summary
Form:  ( DEFUN EXECUTE-IXOR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-IXOR

Summary
Form:  ( DEFUN EXECUTE-JSR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-JSR

Summary
Form:  ( DEFUN EXECUTE-JSR_W ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-JSR_W

Summary
Form:  ( DEFUN CLASS-NAME-OF-REF ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
CLASS-NAME-OF-REF

Summary
Form:  ( DEFUN BIND-FORMALS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BIND-FORMALS

Summary
Form:  ( DEFUN LOOKUP-METHOD-IN-SUPERCLASSES ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LOOKUP-METHOD-IN-SUPERCLASSES

Summary
Form:  ( DEFUN LOOKUP-METHOD ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LOOKUP-METHOD
[SGC for 618 CONS pages..(3106 writable)..(T=9).GC finished]

Summary
Form:  ( DEFUN EXECUTE-INVOKESPECIAL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.14 seconds (prove: 0.00, print: 0.00, other: 0.14)
EXECUTE-INVOKESPECIAL

Summary
Form:  ( DEFUN EXECUTE-INVOKESTATIC ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
EXECUTE-INVOKESTATIC

Summary
Form:  ( DEFUN EXECUTE-INVOKEVIRTUAL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.05 seconds (prove: 0.00, print: 0.00, other: 0.05)
EXECUTE-INVOKEVIRTUAL

Summary
Form:  ( DEFUN EXECUTE-L2I ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-L2I

Summary
Form:  ( DEFUN EXECUTE-LADD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LADD

Summary
Form:  ( DEFUN EXECUTE-LALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LALOAD

Summary
Form:  ( DEFUN EXECUTE-LAND ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LAND

Summary
Form:  ( DEFUN EXECUTE-LASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LASTORE

Summary
Form:  ( DEFUN EXECUTE-LCMP ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LCMP

Summary
Form:  ( DEFUN EXECUTE-LCONST_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LCONST_X

Summary
Form:  ( DEFUN SET-INSTANCE-FIELD ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SET-INSTANCE-FIELD
[SGC for 618 CONS pages..(3106 writable)..(T=10).GC finished]

Summary
Form:  ( DEFUN EXECUTE-LDC ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)
EXECUTE-LDC

Summary
Form:  ( DEFUN EXECUTE-LDC2_W ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LDC2_W

Summary
Form:  ( DEFUN EXECUTE-LDIV ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LDIV

Summary
Form:  ( DEFUN EXECUTE-LLOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LLOAD

Summary
Form:  ( DEFUN EXECUTE-LLOAD_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LLOAD_X

Summary
Form:  ( DEFUN EXECUTE-LMUL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LMUL

Summary
Form:  ( DEFUN EXECUTE-LNEG ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LNEG

Summary
Form:  ( DEFUN EXECUTE-LOR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LOR

Summary
Form:  ( DEFUN EXECUTE-LREM ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LREM

Summary
Form:  ( DEFUN EXECUTE-LRETURN ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
EXECUTE-LRETURN

Summary
Form:  ( DEFUN EXECUTE-LSHL ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LSHL
[SGC for 618 CONS pages..(3107 writable)..(T=11).GC finished]

Summary
Form:  ( DEFUN EXECUTE-LSHR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)
EXECUTE-LSHR

Summary
Form:  ( DEFUN EXECUTE-LSTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LSTORE

Summary
Form:  ( DEFUN EXECUTE-LSTORE_X ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LSTORE_X

Summary
Form:  ( DEFUN EXECUTE-LSUB ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-LSUB

Summary
Form:  ( DEFUN EXECUTE-LUSHR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LUSHR

Summary
Form:  ( DEFUN EXECUTE-LXOR ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-LXOR

Summary
Form:  ( DEFUN EXECUTE-MONITORENTER ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-MONITORENTER

Summary
Form:  ( DEFUN EXECUTE-MONITOREXIT ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-MONITOREXIT

Summary
Form:  ( DEFUN EXECUTE-MULTIANEWARRAY ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-MULTIANEWARRAY
[SGC for 618 CONS pages..(3107 writable)..(T=10).GC finished]

Summary
Form:  ( DEFUN EXECUTE-NEW ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.13 seconds (prove: 0.00, print: 0.00, other: 0.13)
EXECUTE-NEW

Summary
Form:  ( DEFUN EXECUTE-NEWARRAY ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-NEWARRAY

Summary
Form:  ( DEFUN EXECUTE-NOP ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-NOP

Summary
Form:  ( DEFUN EXECUTE-POP ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-POP

Summary
Form:  ( DEFUN EXECUTE-POP2 ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-POP2

Summary
Form:  ( DEFUN EXECUTE-PUTFIELD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
EXECUTE-PUTFIELD

Summary
Form:  ( DEFUN EXECUTE-PUTSTATIC ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-PUTSTATIC

Summary
Form:  ( DEFUN EXECUTE-RET ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-RET

Summary
Form:  ( DEFUN EXECUTE-RETURN ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-RETURN
[SGC for 618 CONS pages..(3108 writable)..(T=11).GC finished]

Summary
Form:  ( DEFUN EXECUTE-SALOAD ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.12 seconds (prove: 0.00, print: 0.00, other: 0.12)
EXECUTE-SALOAD

Summary
Form:  ( DEFUN EXECUTE-SASTORE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-SASTORE

Summary
Form:  ( DEFUN EXECUTE-SIPUSH ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
EXECUTE-SIPUSH

Summary
Form:  ( DEFUN EXECUTE-SWAP ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
EXECUTE-SWAP

Summary
Form:  ( DEFUN INDEX-INTO-PROGRAM ...)
Rules: ((:DEFINITION E0-ORD-<)
        (:DEFINITION E0-ORDINALP)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION LEN))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
INDEX-INTO-PROGRAM

Summary
Form:  ( DEFUN NEXT-INST ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NEXT-INST
[SGC for 618 CONS pages..(3108 writable)..(T=11).GC finished]
[SGC for 618 CONS pages..(3108 writable)..(T=11).GC finished]
[SGC for 618 CONS pages..(3108 writable)..(T=11).GC finished]
[SGC for 618 CONS pages..(3108 writable)..(T=11).GC finished]
[SGC for 618 CONS pages..(3108 writable)..(T=12).GC finished]

Summary
Form:  ( DEFUN DO-INST ...)
Rules: ((:TYPE-PRESCRIPTION EXECUTE-AALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-AASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-ACONST_NULL)
        (:TYPE-PRESCRIPTION EXECUTE-ALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-ALOAD_X)
        (:TYPE-PRESCRIPTION EXECUTE-ANEWARRAY)
        (:TYPE-PRESCRIPTION EXECUTE-ARETURN)
        (:TYPE-PRESCRIPTION EXECUTE-ARRAYLENGTH)
        (:TYPE-PRESCRIPTION EXECUTE-ASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-ASTORE_X)
        (:TYPE-PRESCRIPTION EXECUTE-BALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-BASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-BIPUSH)
        (:TYPE-PRESCRIPTION EXECUTE-CALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-CASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-DUP)
        (:TYPE-PRESCRIPTION EXECUTE-DUP2)
        (:TYPE-PRESCRIPTION EXECUTE-DUP2_X1)
        (:TYPE-PRESCRIPTION EXECUTE-DUP2_X2)
        (:TYPE-PRESCRIPTION EXECUTE-DUP_X1)
        (:TYPE-PRESCRIPTION EXECUTE-DUP_X2)
        (:TYPE-PRESCRIPTION EXECUTE-GETFIELD)
        (:TYPE-PRESCRIPTION EXECUTE-GETSTATIC)
        (:TYPE-PRESCRIPTION EXECUTE-GOTO)
        (:TYPE-PRESCRIPTION EXECUTE-GOTO_W)
        (:TYPE-PRESCRIPTION EXECUTE-I2B)
        (:TYPE-PRESCRIPTION EXECUTE-I2C)
        (:TYPE-PRESCRIPTION EXECUTE-I2L)
        (:TYPE-PRESCRIPTION EXECUTE-I2S)
        (:TYPE-PRESCRIPTION EXECUTE-IADD)
        (:TYPE-PRESCRIPTION EXECUTE-IALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-IAND)
        (:TYPE-PRESCRIPTION EXECUTE-IASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-ICONST_X)
        (:TYPE-PRESCRIPTION EXECUTE-IDIV)
        (:TYPE-PRESCRIPTION EXECUTE-IFEQ)
        (:TYPE-PRESCRIPTION EXECUTE-IFGE)
        (:TYPE-PRESCRIPTION EXECUTE-IFGT)
        (:TYPE-PRESCRIPTION EXECUTE-IFLE)
        (:TYPE-PRESCRIPTION EXECUTE-IFLT)
        (:TYPE-PRESCRIPTION EXECUTE-IFNE)
        (:TYPE-PRESCRIPTION EXECUTE-IFNONNULL)
        (:TYPE-PRESCRIPTION EXECUTE-IFNULL)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ACMPEQ)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ACMPNE)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ICMPEQ)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ICMPGE)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ICMPGT)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ICMPLE)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ICMPLT)
        (:TYPE-PRESCRIPTION EXECUTE-IF_ICMPNE)
        (:TYPE-PRESCRIPTION EXECUTE-IINC)
        (:TYPE-PRESCRIPTION EXECUTE-ILOAD)
        (:TYPE-PRESCRIPTION EXECUTE-ILOAD_X)
        (:TYPE-PRESCRIPTION EXECUTE-IMUL)
        (:TYPE-PRESCRIPTION EXECUTE-INEG)
        (:TYPE-PRESCRIPTION EXECUTE-INSTANCEOF)
        (:TYPE-PRESCRIPTION EXECUTE-INVOKESPECIAL)
        (:TYPE-PRESCRIPTION EXECUTE-INVOKESTATIC)
        (:TYPE-PRESCRIPTION EXECUTE-INVOKEVIRTUAL)
        (:TYPE-PRESCRIPTION EXECUTE-IOR)
        (:TYPE-PRESCRIPTION EXECUTE-IREM)
        (:TYPE-PRESCRIPTION EXECUTE-IRETURN)
        (:TYPE-PRESCRIPTION EXECUTE-ISHL)
        (:TYPE-PRESCRIPTION EXECUTE-ISHR)
        (:TYPE-PRESCRIPTION EXECUTE-ISTORE)
        (:TYPE-PRESCRIPTION EXECUTE-ISTORE_X)
        (:TYPE-PRESCRIPTION EXECUTE-ISUB)
        (:TYPE-PRESCRIPTION EXECUTE-IUSHR)
        (:TYPE-PRESCRIPTION EXECUTE-IXOR)
        (:TYPE-PRESCRIPTION EXECUTE-JSR)
        (:TYPE-PRESCRIPTION EXECUTE-JSR_W)
        (:TYPE-PRESCRIPTION EXECUTE-L2I)
        (:TYPE-PRESCRIPTION EXECUTE-LADD)
        (:TYPE-PRESCRIPTION EXECUTE-LALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-LAND)
        (:TYPE-PRESCRIPTION EXECUTE-LASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-LCMP)
        (:TYPE-PRESCRIPTION EXECUTE-LCONST_X)
        (:TYPE-PRESCRIPTION EXECUTE-LDC)
        (:TYPE-PRESCRIPTION EXECUTE-LDC2_W)
        (:TYPE-PRESCRIPTION EXECUTE-LDIV)
        (:TYPE-PRESCRIPTION EXECUTE-LLOAD)
        (:TYPE-PRESCRIPTION EXECUTE-LLOAD_X)
        (:TYPE-PRESCRIPTION EXECUTE-LMUL)
        (:TYPE-PRESCRIPTION EXECUTE-LNEG)
        (:TYPE-PRESCRIPTION EXECUTE-LOR)
        (:TYPE-PRESCRIPTION EXECUTE-LREM)
        (:TYPE-PRESCRIPTION EXECUTE-LRETURN)
        (:TYPE-PRESCRIPTION EXECUTE-LSHL)
        (:TYPE-PRESCRIPTION EXECUTE-LSHR)
        (:TYPE-PRESCRIPTION EXECUTE-LSTORE)
        (:TYPE-PRESCRIPTION EXECUTE-LSTORE_X)
        (:TYPE-PRESCRIPTION EXECUTE-LSUB)
        (:TYPE-PRESCRIPTION EXECUTE-LUSHR)
        (:TYPE-PRESCRIPTION EXECUTE-LXOR)
        (:TYPE-PRESCRIPTION EXECUTE-MONITORENTER)
        (:TYPE-PRESCRIPTION EXECUTE-MONITOREXIT)
        (:TYPE-PRESCRIPTION EXECUTE-MULTIANEWARRAY)
        (:TYPE-PRESCRIPTION EXECUTE-NEW)
        (:TYPE-PRESCRIPTION EXECUTE-NEWARRAY)
        (:TYPE-PRESCRIPTION EXECUTE-NOP)
        (:TYPE-PRESCRIPTION EXECUTE-POP)
        (:TYPE-PRESCRIPTION EXECUTE-POP2)
        (:TYPE-PRESCRIPTION EXECUTE-PUTFIELD)
        (:TYPE-PRESCRIPTION EXECUTE-PUTSTATIC)
        (:TYPE-PRESCRIPTION EXECUTE-RET)
        (:TYPE-PRESCRIPTION EXECUTE-RETURN)
        (:TYPE-PRESCRIPTION EXECUTE-SALOAD)
        (:TYPE-PRESCRIPTION EXECUTE-SASTORE)
        (:TYPE-PRESCRIPTION EXECUTE-SIPUSH)
        (:TYPE-PRESCRIPTION EXECUTE-SWAP))
Warnings:  None
Time:  1.34 seconds (prove: 0.00, print: 0.00, other: 1.34)
DO-INST

Summary
Form:  ( DEFUN STEP ...)
Rules: ((:TYPE-PRESCRIPTION DO-INST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
STEP

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

Summary
Form:  ( DEFUN ACK2 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ACK2

Summary
Form:  ( DEFUN ACK0 ...)
Rules: ((:TYPE-PRESCRIPTION ACK2))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACK0
T

Summary
Form:  ( DEFUN SIM-LOOP ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
SIM-LOOP

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

Summary
Form:  ( DEFUN ISLABEL? ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ISLABEL?

Summary
Form:  ( DEFUN ISLABELEDINST? ...)
Rules: ((:TYPE-PRESCRIPTION ISLABEL?))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ISLABELEDINST?

Summary
Form:  ( DEFUN GEN_LABEL_ALIST ...)
Rules: ((:TYPE-PRESCRIPTION BIND))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
GEN_LABEL_ALIST

Summary
Form:  ( DEFUN RESOLVE_LABELS ...)
Rules: ((:TYPE-PRESCRIPTION BINARY-APPEND))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
RESOLVE_LABELS

Summary
Form:  ( DEFUN RESOLVE_BASIC_BLOCK ...)
Rules: ((:TYPE-PRESCRIPTION RESOLVE_LABELS))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
RESOLVE_BASIC_BLOCK

Summary
Form:  ( DEFUN ASSEMBLE_FRAME ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-FRAME))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ASSEMBLE_FRAME

Summary
Form:  ( DEFUN ASSEMBLE_CALL_STACK ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ASSEMBLE_CALL_STACK

Summary
Form:  ( DEFUN ASSEMBLE_THREAD ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ASSEMBLE_THREAD

Summary
Form:  ( DEFUN ASSEMBLE_THREAD_TABLE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ASSEMBLE_THREAD_TABLE

Summary
Form:  ( DEFUN ASSEMBLE_METHOD ...)
Rules: ((:TYPE-PRESCRIPTION BINARY-APPEND)
        (:TYPE-PRESCRIPTION RESOLVE_BASIC_BLOCK))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ASSEMBLE_METHOD

Summary
Form:  ( DEFUN ASSEMBLE_METHODS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ASSEMBLE_METHODS

Summary
Form:  ( DEFUN ASSEMBLE_CLASS ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-CLASS-DECL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ASSEMBLE_CLASS

Summary
Form:  ( DEFUN ASSEMBLE_CLASS_TABLE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ASSEMBLE_CLASS_TABLE

Summary
Form:  ( DEFUN ASSEMBLE_STATE ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ASSEMBLE_STATE

Summary
Form:  ( DEFUN MAKE-STRING-OBJ ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MAKE-STRING-OBJ

Summary
Form:  ( DEFUN RESOLVE-STRING-CONSTANTS ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STRING-OBJ))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
RESOLVE-STRING-CONSTANTS

Summary
Form:  ( DEFUN GEN_CLASS_OBJ ...)
Rules: ((:TYPE-PRESCRIPTION MAKE-STATE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
GEN_CLASS_OBJ

Summary
Form:  ( DEFUN LD_CLASS_LIB ...)
Rules: ((:TYPE-PRESCRIPTION GEN_CLASS_OBJ))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LD_CLASS_LIB

Summary
Form:  ( DEFUN LOAD_CLASS_LIBRARY ...)
Rules: ((:TYPE-PRESCRIPTION LD_CLASS_LIB))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LOAD_CLASS_LIBRARY

Summary
Form:  ( DEFUN M5_LOAD ...)
Rules: ((:TYPE-PRESCRIPTION ASSEMBLE_STATE)
        (:TYPE-PRESCRIPTION LOAD_CLASS_LIBRARY))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
M5_LOAD

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
[SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=44).GC finished]
[SGC on][SGC for 1258 CONS pages..(2922 writable)..(T=13).GC finished]
[SGC for 1258 CONS pages..(3022 writable)..(T=13).GC finished]
[SGC for 1258 CONS pages..(3112 writable)..(T=14).GC finished]
[SGC for 1258 CONS pages..(3193 writable)..(T=16).GC finished]
[SGC for 1258 CONS pages..(3215 writable)..(T=15).GC finished]

Summary
Form:  ( INCLUDE-BOOK "m5" ...)
Rules: NIL
Warnings:  None
Time:  5.04 seconds (prove: 0.00, print: 0.00, other: 5.04)
Compiling /v/net2/v2/users/prof/moore/publications/trecia/support/m5.lisp.
[SGC for 1258 CONS pages..(3284 writable)..(T=16).GC finished]
End of Pass 1.  

;; Note: Tail-recursive call of POPN was replaced by iteration.[SGC for 1258 CONS pages..(3334 writable)..(T=19).GC finished]

;; Note: Tail-recursive call of RREFTOTHREAD was replaced by iteration.
;; Note: Tail-recursive call of IN-LIST was replaced by iteration.
;; Note: Tail-recursive call of SUPPLIEDP was replaced by iteration.
;; Note: Tail-recursive call of ACTUAL was replaced by iteration.
;; Note: Tail-recursive call of MAKEMULTIARRAY2 was replaced by iteration.
;; Note: Tail-recursive call of LOOKUP-METHOD-IN-SUPERCLASSES was replaced by iteration.
;; Note: Tail-recursive call of INDEX-INTO-PROGRAM was replaced by iteration.
;; Note: Tail-recursive call of RUN was replaced by iteration.
;; Note: Tail-recursive call of ACK2 was replaced by iteration.
;; Note: Tail-recursive call of GEN_LABEL_ALIST was replaced by iteration.
;; Note: Tail-recursive call of RESOLVE-STRING-CONSTANTS was replaced by iteration.
;; Note: Tail-recursive call of RESOLVE-STRING-CONSTANTS was replaced by iteration.
;; Note: Tail-recursive call of LD_CLASS_LIB 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/m5.o.

"/v/net2/v2/users/prof/moore/publications/trecia/support/m5.o" 

Loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o
[SGC for 0 CONTIGUOUS-BLOCKS pages..(3421 writable)..(T=16).GC finished]
start address -T 0x9c02000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/m5.o

Summary
Form:  (CERTIFY-BOOK "m5" ...)
Rules: NIL
Warnings:  None
Time:  13.68 seconds (prove: 0.07, print: 0.00, other: 13.61)
 "/v/net2/v2/users/prof/moore/publications/trecia/support/m5.lisp"
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>