File: jvm-loader-guard-verification-support-load-cp-guard%40useless-runes.lsp

package info (click to toggle)
acl2 8.6%2Bdfsg-3
links: PTS
area: main
in suites: forky, sid
size: 1,138,276 kB
sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,978; makefile: 3,840; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (2031 lines) | stat: -rw-r--r-- 88,247 bytes
parent folder | download | duplicates (2)
(JVM::WFF-CLASS-TABLE-STATE)
(JVM::WFF-HEAP-STATE)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IS-AN-EQUIVALENCE
 (88323 649 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (76464 118 (:DEFINITION JVM::WFF-STATIC-CP-OK-S))
 (74104 118 (:DEFINITION JVM::WFF-STATIC-CP-ENTRY-OK-S))
 (61242 118 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARDS))
 (61198 23165 (:DEFINITION NTH))
 (59826 118 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARD))
 (45489 295 (:DEFINITION JVM::WFF-TYPE-REP))
 (41072 40918 (:REWRITE DEFAULT-CDR))
 (37288 118 (:DEFINITION JVM::VALUE-TYPE-OK))
 (32861 32751 (:REWRITE DEFAULT-CAR))
 (20178 118 (:DEFINITION JVM::WFF-TYPE-REPS))
 (15395 3079 (:DEFINITION LEN))
 (15104 118 (:DEFINITION JVM::VALUE-TYPE-OK-2))
 (12696 12696 (:REWRITE MEM-SUBSET))
 (10502 1416 (:DEFINITION JVM::ARRAY-TYPE?))
 (10384 118 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (9263 59 (:DEFINITION JVM::WFF-FIELDS-S))
 (8496 2124 (:REWRITE ZP-OPEN))
 (8282 5203 (:REWRITE DEFAULT-+-2))
 (7080 236 (:DEFINITION JVM::WFF-CODE-S))
 (6254 118 (:DEFINITION JVM::WFF-CONSTANT-POOL-S))
 (5782 118 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY-S))
 (5203 5203 (:REWRITE DEFAULT-+-1))
 (4590 4472 (:REWRITE DEFAULT-<-2))
 (4472 4472 (:REWRITE DEFAULT-<-1))
 (3960 1980 (:DEFINITION TRUE-LISTP))
 (3820 764 (:DEFINITION INT32P))
 (3658 118 (:DEFINITION JVM::WFF-METHOD-DECL-S))
 (3608 44 (:DEFINITION JVM::LOADER-INV-HELPER1))
 (3363 1121 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (3080 66 (:DEFINITION JVM::ALL-CORRECTLY-LOADED?))
 (3079 3079 (:REWRITE DEL-SET-LEN))
 (3047 44 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-IMPLIES-ALL-CORRECTLY-LOADED?))
 (2968 56 (:DEFINITION JVM::WFF-CONSTANT-POOL))
 (2744 56 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY))
 (2301 177 (:DEFINITION JVM::WFF-FIELD-S))
 (2124 708 (:DEFINITION JVM::METHOD-CODE-S))
 (2124 708 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (2006 118 (:DEFINITION JVM::WFF-FIELDS-S-X))
 (1960 56 (:DEFINITION JVM::WFF-CLASS-METHOD-DECLS))
 (1888 472 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (1770 118 (:DEFINITION JVM::WFF-LONG-CP-ENTRY-S))
 (1770 118 (:DEFINITION JVM::WFF-INT-CP-ENTRY-S))
 (1736 56 (:DEFINITION JVM::WFF-METHOD-DECL))
 (1639 66 (:REWRITE JVM::LOADER-INV-HELPER1-CORRECT-LOADED?))
 (1606 22 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (1534 118 (:DEFINITION JVM::REFERENCE-TYPE))
 (1460 292 (:DEFINITION INT64P))
 (1416 59 (:DEFINITION JVM::ALL-FIELDS-STATIC-FINAL))
 (1239 413 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (1180 118 (:DEFINITION JVM::WFF-STRING-CP-ENTRY-S))
 (1180 118 (:DEFINITION JVM::STATIC-FIELD?-S))
 (952 56 (:DEFINITION JVM::WFF-STATIC-FIELDS-X))
 (952 56 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (944 236 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (944 236 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (944 236 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (944 236 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (840 56 (:DEFINITION JVM::WFF-LONG-CP-ENTRY))
 (840 56 (:DEFINITION JVM::WFF-INT-CP-ENTRY))
 (728 56 (:DEFINITION JVM::WFF-STATIC-FIELD))
 (728 56 (:DEFINITION JVM::WFF-FIELD))
 (708 118 (:DEFINITION SHORTP))
 (708 118 (:DEFINITION JVMBOOLEANP))
 (708 118 (:DEFINITION CHARP))
 (708 118 (:DEFINITION BYTEP))
 (708 59 (:DEFINITION NODUP-SET))
 (560 56 (:DEFINITION JVM::WFF-STRING-CP-ENTRY))
 (506 22 (:REWRITE JVM::CLASS-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (472 118 (:DEFINITION JVM::METHOD-ARGS-S))
 (413 413 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REP))
 (374 22 (:DEFINITION JVM::ISCLASSTERM))
 (354 118 (:DEFINITION JVM::CPENTRY-VALUE-S))
 (354 59 (:DEFINITION JVM::COLLECT-STATIC-FIELD-NAMES))
 (308 308 (:TYPE-PRESCRIPTION JVM::ALL-CORRECTLY-LOADED?))
 (308 77 (:REWRITE JVM::INV-AND-ISASSIGNABLETO-ENV))
 (264 264 (:TYPE-PRESCRIPTION JVM::COLLECT-ASSIGNABLETONAME))
 (264 44 (:DEFINITION APP))
 (236 236 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REPS))
 (236 118 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (231 77 (:REWRITE JVM::LOADED-LORDER-INV-HELPER-IMPLIES-CORRECTLY-LOADED?))
 (209 55 (:DEFINITION JVM::CLASS-BY-NAME))
 (198 22 (:DEFINITION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (177 59 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (176 44 (:DEFINITION MV-NTH))
 (176 44 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (154 154 (:TYPE-PRESCRIPTION JVM::CLASS-LOADED?))
 (154 154 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (143 143 (:TYPE-PRESCRIPTION JVM::CORRECTLY-LOADED?))
 (132 66 (:TYPE-PRESCRIPTION APP))
 (118 118 (:TYPE-PRESCRIPTION JVM::COLLECT-STATIC-FIELD-NAMES))
 (118 118 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (118 118 (:DEFINITION JVMFLOATP))
 (118 118 (:DEFINITION DOUBLEP))
 (88 88 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (88 88 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (88 22 (:REWRITE JVM::LOADER-INV-HELPER-CORRECT-LOADED?-IMPLIES-LOADER-INV-HELPER1))
 (88 22 (:REWRITE JVM::LOADER-INV-HELPER-AND-LOADED-IMPLIES-CORRECTLY-LOADED?-2))
 (77 77 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (77 77 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (66 66 (:TYPE-PRESCRIPTION JVM::LOADER-INV-HELPER1))
 (66 66 (:TYPE-PRESCRIPTION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (32 32 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (22 22 (:TYPE-PRESCRIPTION JVM::ISCLASSTERM))
 (22 22 (:REWRITE JVM::CORRECTLY-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (22 22 (:REWRITE JVM::CORRECTLY-LOADED?-CLASSNAME-CLASS-BY-NAME))
 (11 11 (:REWRITE CDR-CONS))
 (11 11 (:REWRITE CAR-CONS))
 )
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-INSTANCE-CLASS-TABLE-1)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-ENV-1)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-WFF-STATE-1)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-WFF-CLASS-TABLE-STATE-1)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-WFF-HEAP-STATE-1)
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-LOADER-INV-1)
(JVM::WFF-CLASS-TABLE-CLASS-TABLE-NORM)
(JVM::WFF-HEAP-HEAP-NORM)
(JVM::EQUIV-TWO-TUPLE)
(JVM::EQUIV-TWO-TUPLE-IS-AN-EQUIVALENCE
 (26 26 (:REWRITE DEFAULT-CDR))
 (22 22 (:REWRITE DEFAULT-CAR))
 )
(JVM::SLOT1)
(JVM::SLOT2)
(JVM::EQUIV-TWO-TUPLE-IMPLIES-EQUAL-SLOT1-1)
(JVM::EQUIV-TWO-TUPLE-IMPLIES-EQUIV-STATE-INSTANCE-CLASS-TABLE-SLOT2-1)
(JVM::CLASS-LOADED-LOAD_CLASS_X_3
 (21 21 (:TYPE-PRESCRIPTION JVM::LOAD_CLASS_X))
 (12 3 (:DEFINITION JVM::CLASS-BY-NAME))
 (7 7 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEL-SET-LEN))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 )
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-2
 (68 4 (:DEFINITION JVM::ISCLASSTERM))
 (48 2 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (48 2 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (44 2 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (44 2 (:DEFINITION JVM::CLASS-EXISTS?))
 (34 2 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (32 32 (:TYPE-PRESCRIPTION LEN))
 (32 8 (:DEFINITION JVM::CLASS-BY-NAME))
 (30 30 (:REWRITE DEFAULT-CDR))
 (30 6 (:DEFINITION LEN))
 (26 2 (:DEFINITION JVM::WFF-FIELD))
 (20 20 (:REWRITE DEFAULT-CAR))
 (16 16 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (12 6 (:REWRITE DEFAULT-+-2))
 (8 4 (:DEFINITION NTH))
 (8 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (6 6 (:REWRITE DEL-SET-LEN))
 (6 6 (:REWRITE DEFAULT-+-1))
 (4 2 (:DEFINITION TRUE-LISTP))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 )
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IMPLIES-EQUAL-BUILD-A-JAVA-VISIBLE-INSTANCE-DATA-GUARD-2
 (10 10 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-CDR))
 )
(JVM::WFF-STATE-EQUIV-STATE-INSTANCE-CLASS-TABLE
 (100 4 (:DEFINITION JVM::COLLECT-SUPERCLASS-LIST1))
 (36 4 (:DEFINITION JVM::ISCLASSTERM))
 (34 2 (:DEFINITION JVM::COLLECT-SUPERCLASSNAME1))
 (32 30 (:REWRITE DEFAULT-CDR))
 (32 8 (:DEFINITION JVM::CLASS-BY-NAME))
 (30 28 (:REWRITE DEFAULT-CAR))
 (20 4 (:DEFINITION LEN))
 (16 4 (:DEFINITION MV-NTH))
 (16 4 (:DEFINITION JVM::CLASSSUPERCLASSNAME))
 (12 12 (:TYPE-PRESCRIPTION LEN))
 (12 12 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (12 4 (:DEFINITION JVM::SUPER))
 (12 2 (:DEFINITION JVM::BUILD-A-JAVA-VISIBLE-INSTANCE-DATA-GUARD))
 (8 4 (:REWRITE DEFAULT-+-2))
 (8 4 (:DEFINITION NTH))
 (8 2 (:DEFINITION JVM::WFF-STATIC-CLASS-TABLE))
 (8 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (8 2 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (6 6 (:REWRITE MEM-SUBSET))
 (6 6 (:DEFINITION MEM))
 (4 4 (:REWRITE DEL-SET-LEN))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP-STATIC))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP))
 (2 2 (:TYPE-PRESCRIPTION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD))
 )
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IF-WFF
 (5222 2 (:DEFINITION JVM::WFF-STATIC-CLASS-TABLE-STRONG))
 (5190 2 (:DEFINITION JVM::WFF-CLASS-REP-STATIC-STRONG))
 (2870 226 (:DEFINITION MEM))
 (2802 22 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (2400 4 (:DEFINITION JVM::WFF-STATIC-CP-OK-S))
 (2320 4 (:DEFINITION JVM::WFF-STATIC-CP-ENTRY-OK-S))
 (2076 4 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARDS))
 (2028 4 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARD))
 (1864 680 (:DEFINITION NTH))
 (1542 10 (:DEFINITION JVM::WFF-TYPE-REP))
 (1290 1262 (:REWRITE DEFAULT-CDR))
 (1212 1192 (:REWRITE DEFAULT-CAR))
 (1072 4 (:DEFINITION JVM::VALUE-TYPE-OK))
 (972 2 (:DEFINITION JVM::LOADER-INV-HELPER))
 (962 8 (:DEFINITION JVM::LOADER-INV-HELPER1))
 (866 12 (:DEFINITION JVM::ALL-CORRECTLY-LOADED?))
 (768 8 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-IMPLIES-ALL-CORRECTLY-LOADED?))
 (684 4 (:DEFINITION JVM::WFF-TYPE-REPS))
 (590 118 (:DEFINITION LEN))
 (512 4 (:DEFINITION JVM::VALUE-TYPE-OK-2))
 (430 430 (:REWRITE MEM-SUBSET))
 (420 420 (:TYPE-PRESCRIPTION LEN))
 (390 12 (:REWRITE JVM::LOADER-INV-HELPER1-CORRECT-LOADED?))
 (384 4 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (356 48 (:DEFINITION JVM::ARRAY-TYPE?))
 (352 4 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (348 14 (:REWRITE JVM::LOADED-LORDER-INV-HELPER-IMPLIES-CORRECTLY-LOADED?))
 (320 14 (:DEFINITION JVM::CLASS-LOADED?))
 (314 2 (:DEFINITION JVM::WFF-FIELDS-S))
 (308 190 (:REWRITE DEFAULT-+-2))
 (306 18 (:DEFINITION JVM::ISCLASSTERM))
 (302 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE-STRONG))
 (288 72 (:REWRITE ZP-OPEN))
 (286 2 (:DEFINITION JVM::WFF-CLASS-REP-STRONG))
 (240 8 (:DEFINITION JVM::WFF-CODE-S))
 (212 4 (:DEFINITION JVM::WFF-CONSTANT-POOL-S))
 (196 4 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY-S))
 (190 190 (:REWRITE DEFAULT-+-1))
 (156 152 (:REWRITE DEFAULT-<-2))
 (152 152 (:REWRITE DEFAULT-<-1))
 (130 26 (:DEFINITION INT32P))
 (124 4 (:DEFINITION JVM::WFF-METHOD-DECL-S))
 (118 118 (:REWRITE DEL-SET-LEN))
 (114 38 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (106 24 (:DEFINITION JVM::CLASS-BY-NAME))
 (106 2 (:DEFINITION JVM::WFF-CONSTANT-POOL))
 (104 52 (:DEFINITION TRUE-LISTP))
 (98 2 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY))
 (92 4 (:REWRITE JVM::CLASS-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (78 6 (:DEFINITION JVM::WFF-FIELD-S))
 (72 72 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (72 24 (:DEFINITION JVM::METHOD-CODE-S))
 (72 24 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (70 2 (:DEFINITION JVM::WFF-CLASS-METHOD-DECLS))
 (68 4 (:DEFINITION JVM::WFF-FIELDS-S-X))
 (64 64 (:TYPE-PRESCRIPTION JVM::COLLECT-ASSIGNABLETONAME))
 (64 16 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (62 2 (:DEFINITION JVM::WFF-METHOD-DECL))
 (60 4 (:DEFINITION JVM::WFF-LONG-CP-ENTRY-S))
 (60 4 (:DEFINITION JVM::WFF-INT-CP-ENTRY-S))
 (56 56 (:TYPE-PRESCRIPTION JVM::ALL-CORRECTLY-LOADED?))
 (56 14 (:REWRITE JVM::INV-AND-ISASSIGNABLETO-ENV))
 (52 4 (:DEFINITION JVM::REFERENCE-TYPE))
 (50 10 (:DEFINITION INT64P))
 (50 2 (:DEFINITION JVM::WFF-INTERFACE-CLASS-STATIC))
 (48 8 (:DEFINITION APP))
 (48 2 (:DEFINITION JVM::ALL-FIELDS-STATIC-FINAL))
 (46 46 (:TYPE-PRESCRIPTION MEM))
 (42 42 (:TYPE-PRESCRIPTION JVM::LOADER-INV))
 (42 14 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (40 4 (:DEFINITION JVM::WFF-STRING-CP-ENTRY-S))
 (40 4 (:DEFINITION JVM::STATIC-FIELD?-S))
 (36 4 (:DEFINITION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (34 2 (:DEFINITION JVM::WFF-STATIC-FIELDS-X))
 (34 2 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (32 8 (:DEFINITION MV-NTH))
 (32 8 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (32 8 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (32 8 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (32 8 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (32 8 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (30 2 (:DEFINITION JVM::WFF-LONG-CP-ENTRY))
 (30 2 (:DEFINITION JVM::WFF-INT-CP-ENTRY))
 (28 28 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (26 26 (:TYPE-PRESCRIPTION JVM::CORRECTLY-LOADED?))
 (26 2 (:DEFINITION JVM::WFF-STATIC-FIELD))
 (26 2 (:DEFINITION JVM::WFF-FIELD))
 (24 24 (:TYPE-PRESCRIPTION JVM::LOADER-INV-HELPER))
 (24 12 (:TYPE-PRESCRIPTION APP))
 (24 4 (:DEFINITION SHORTP))
 (24 4 (:DEFINITION JVMBOOLEANP))
 (24 4 (:DEFINITION CHARP))
 (24 4 (:DEFINITION BYTEP))
 (24 2 (:DEFINITION NODUP-SET))
 (20 2 (:DEFINITION JVM::WFF-STRING-CP-ENTRY))
 (16 16 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (16 4 (:REWRITE JVM::LOADER-INV-HELPER-CORRECT-LOADED?-IMPLIES-LOADER-INV-HELPER1))
 (16 4 (:REWRITE JVM::LOADER-INV-HELPER-AND-LOADED-IMPLIES-CORRECTLY-LOADED?-2))
 (16 4 (:DEFINITION JVM::METHOD-ARGS-S))
 (14 14 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REP))
 (14 14 (:TYPE-PRESCRIPTION JVM::CLASS-LOADED?))
 (14 14 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (14 14 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (12 12 (:TYPE-PRESCRIPTION JVM::LOADER-INV-HELPER1))
 (12 12 (:TYPE-PRESCRIPTION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (12 4 (:DEFINITION JVM::CPENTRY-VALUE-S))
 (12 2 (:DEFINITION JVM::COLLECT-STATIC-FIELD-NAMES))
 (8 8 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REPS))
 (8 8 (:TYPE-PRESCRIPTION JVM::WFF-FIELDS-S-X))
 (8 8 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL-S))
 (8 8 (:TYPE-PRESCRIPTION JVM::RUNTIME-METHOD-REP-GUARDS))
 (8 8 (:REWRITE JVM::LOADER-INV-HELPER-MEM-IMPLIES))
 (8 4 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (8 2 (:DEFINITION JVM::STATIC-FIELDS))
 (8 2 (:DEFINITION JVM::METHODS))
 (8 2 (:DEFINITION JVM::FIELDS))
 (8 2 (:DEFINITION JVM::CONSTANTPOOL))
 (6 2 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-FIELDS-X))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-CP-OK-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-FIELDS-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP-STATIC))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-METHOD-DECLS))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (4 4 (:TYPE-PRESCRIPTION NODUP-SET))
 (4 4 (:TYPE-PRESCRIPTION JVM::ISCLASSTERM))
 (4 4 (:TYPE-PRESCRIPTION JVM::COLLECT-STATIC-FIELD-NAMES))
 (4 4 (:TYPE-PRESCRIPTION JVM::ALL-FIELDS-STATIC-FINAL))
 (4 4 (:REWRITE JVM::CORRECTLY-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (4 4 (:REWRITE JVM::CORRECTLY-LOADED?-CLASSNAME-CLASS-BY-NAME))
 (4 4 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (4 4 (:DEFINITION JVMFLOATP))
 (4 4 (:DEFINITION DOUBLEP))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL))
 (2 2 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (2 2 (:REWRITE CDR-CONS))
 (2 2 (:REWRITE CAR-CONS))
 )
(JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE-IF-WFF-SPECIFIC
 (5222 2 (:DEFINITION JVM::WFF-STATIC-CLASS-TABLE-STRONG))
 (5190 2 (:DEFINITION JVM::WFF-CLASS-REP-STATIC-STRONG))
 (2870 226 (:DEFINITION MEM))
 (2802 22 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (2400 4 (:DEFINITION JVM::WFF-STATIC-CP-OK-S))
 (2320 4 (:DEFINITION JVM::WFF-STATIC-CP-ENTRY-OK-S))
 (2076 4 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARDS))
 (2028 4 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARD))
 (1864 680 (:DEFINITION NTH))
 (1542 10 (:DEFINITION JVM::WFF-TYPE-REP))
 (1290 1262 (:REWRITE DEFAULT-CDR))
 (1212 1192 (:REWRITE DEFAULT-CAR))
 (1072 4 (:DEFINITION JVM::VALUE-TYPE-OK))
 (972 2 (:DEFINITION JVM::LOADER-INV-HELPER))
 (962 8 (:DEFINITION JVM::LOADER-INV-HELPER1))
 (866 12 (:DEFINITION JVM::ALL-CORRECTLY-LOADED?))
 (768 8 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-IMPLIES-ALL-CORRECTLY-LOADED?))
 (684 4 (:DEFINITION JVM::WFF-TYPE-REPS))
 (590 118 (:DEFINITION LEN))
 (512 4 (:DEFINITION JVM::VALUE-TYPE-OK-2))
 (430 430 (:REWRITE MEM-SUBSET))
 (420 420 (:TYPE-PRESCRIPTION LEN))
 (390 12 (:REWRITE JVM::LOADER-INV-HELPER1-CORRECT-LOADED?))
 (384 4 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (356 48 (:DEFINITION JVM::ARRAY-TYPE?))
 (352 4 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (348 14 (:REWRITE JVM::LOADED-LORDER-INV-HELPER-IMPLIES-CORRECTLY-LOADED?))
 (320 14 (:DEFINITION JVM::CLASS-LOADED?))
 (314 2 (:DEFINITION JVM::WFF-FIELDS-S))
 (308 190 (:REWRITE DEFAULT-+-2))
 (306 18 (:DEFINITION JVM::ISCLASSTERM))
 (302 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE-STRONG))
 (288 72 (:REWRITE ZP-OPEN))
 (286 2 (:DEFINITION JVM::WFF-CLASS-REP-STRONG))
 (240 8 (:DEFINITION JVM::WFF-CODE-S))
 (212 4 (:DEFINITION JVM::WFF-CONSTANT-POOL-S))
 (196 4 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY-S))
 (190 190 (:REWRITE DEFAULT-+-1))
 (156 152 (:REWRITE DEFAULT-<-2))
 (152 152 (:REWRITE DEFAULT-<-1))
 (130 26 (:DEFINITION INT32P))
 (124 4 (:DEFINITION JVM::WFF-METHOD-DECL-S))
 (118 118 (:REWRITE DEL-SET-LEN))
 (114 38 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (106 24 (:DEFINITION JVM::CLASS-BY-NAME))
 (106 2 (:DEFINITION JVM::WFF-CONSTANT-POOL))
 (104 52 (:DEFINITION TRUE-LISTP))
 (98 2 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY))
 (92 4 (:REWRITE JVM::CLASS-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (78 6 (:DEFINITION JVM::WFF-FIELD-S))
 (72 72 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (72 24 (:DEFINITION JVM::METHOD-CODE-S))
 (72 24 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (70 2 (:DEFINITION JVM::WFF-CLASS-METHOD-DECLS))
 (68 4 (:DEFINITION JVM::WFF-FIELDS-S-X))
 (64 64 (:TYPE-PRESCRIPTION JVM::COLLECT-ASSIGNABLETONAME))
 (64 16 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (62 2 (:DEFINITION JVM::WFF-METHOD-DECL))
 (60 4 (:DEFINITION JVM::WFF-LONG-CP-ENTRY-S))
 (60 4 (:DEFINITION JVM::WFF-INT-CP-ENTRY-S))
 (56 56 (:TYPE-PRESCRIPTION JVM::ALL-CORRECTLY-LOADED?))
 (56 14 (:REWRITE JVM::INV-AND-ISASSIGNABLETO-ENV))
 (52 4 (:DEFINITION JVM::REFERENCE-TYPE))
 (50 10 (:DEFINITION INT64P))
 (50 2 (:DEFINITION JVM::WFF-INTERFACE-CLASS-STATIC))
 (48 8 (:DEFINITION APP))
 (48 2 (:DEFINITION JVM::ALL-FIELDS-STATIC-FINAL))
 (46 46 (:TYPE-PRESCRIPTION MEM))
 (42 42 (:TYPE-PRESCRIPTION JVM::LOADER-INV))
 (42 14 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (40 4 (:DEFINITION JVM::WFF-STRING-CP-ENTRY-S))
 (40 4 (:DEFINITION JVM::STATIC-FIELD?-S))
 (36 4 (:DEFINITION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (34 2 (:DEFINITION JVM::WFF-STATIC-FIELDS-X))
 (34 2 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (32 8 (:DEFINITION MV-NTH))
 (32 8 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (32 8 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (32 8 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (32 8 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (32 8 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (30 2 (:DEFINITION JVM::WFF-LONG-CP-ENTRY))
 (30 2 (:DEFINITION JVM::WFF-INT-CP-ENTRY))
 (28 28 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (26 26 (:TYPE-PRESCRIPTION JVM::CORRECTLY-LOADED?))
 (26 2 (:DEFINITION JVM::WFF-STATIC-FIELD))
 (26 2 (:DEFINITION JVM::WFF-FIELD))
 (24 24 (:TYPE-PRESCRIPTION JVM::LOADER-INV-HELPER))
 (24 12 (:TYPE-PRESCRIPTION APP))
 (24 4 (:DEFINITION SHORTP))
 (24 4 (:DEFINITION JVMBOOLEANP))
 (24 4 (:DEFINITION CHARP))
 (24 4 (:DEFINITION BYTEP))
 (24 2 (:DEFINITION NODUP-SET))
 (20 2 (:DEFINITION JVM::WFF-STRING-CP-ENTRY))
 (16 16 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (16 4 (:REWRITE JVM::LOADER-INV-HELPER-CORRECT-LOADED?-IMPLIES-LOADER-INV-HELPER1))
 (16 4 (:REWRITE JVM::LOADER-INV-HELPER-AND-LOADED-IMPLIES-CORRECTLY-LOADED?-2))
 (16 4 (:DEFINITION JVM::METHOD-ARGS-S))
 (14 14 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REP))
 (14 14 (:TYPE-PRESCRIPTION JVM::CLASS-LOADED?))
 (14 14 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (14 14 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (12 12 (:TYPE-PRESCRIPTION JVM::LOADER-INV-HELPER1))
 (12 12 (:TYPE-PRESCRIPTION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (12 4 (:DEFINITION JVM::CPENTRY-VALUE-S))
 (12 2 (:DEFINITION JVM::COLLECT-STATIC-FIELD-NAMES))
 (8 8 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REPS))
 (8 8 (:TYPE-PRESCRIPTION JVM::WFF-FIELDS-S-X))
 (8 8 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL-S))
 (8 8 (:TYPE-PRESCRIPTION JVM::RUNTIME-METHOD-REP-GUARDS))
 (8 8 (:REWRITE JVM::LOADER-INV-HELPER-MEM-IMPLIES))
 (8 4 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (8 2 (:DEFINITION JVM::STATIC-FIELDS))
 (8 2 (:DEFINITION JVM::METHODS))
 (8 2 (:DEFINITION JVM::FIELDS))
 (8 2 (:DEFINITION JVM::CONSTANTPOOL))
 (6 2 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-FIELDS-X))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-CP-OK-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-FIELDS-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP-STATIC))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-METHOD-DECLS))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (4 4 (:TYPE-PRESCRIPTION NODUP-SET))
 (4 4 (:TYPE-PRESCRIPTION JVM::ISCLASSTERM))
 (4 4 (:TYPE-PRESCRIPTION JVM::COLLECT-STATIC-FIELD-NAMES))
 (4 4 (:TYPE-PRESCRIPTION JVM::ALL-FIELDS-STATIC-FINAL))
 (4 4 (:REWRITE JVM::CORRECTLY-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (4 4 (:REWRITE JVM::CORRECTLY-LOADED?-CLASSNAME-CLASS-BY-NAME))
 (4 4 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (4 4 (:DEFINITION JVMFLOATP))
 (4 4 (:DEFINITION DOUBLEP))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL))
 (2 2 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (2 2 (:REWRITE CDR-CONS))
 (2 2 (:REWRITE CAR-CONS))
 )
(JVM::WFF-HEAP-STATE-LOAD_CP_ENTRY
 (5987 5629 (:REWRITE DEFAULT-CDR))
 (5014 4574 (:REWRITE DEFAULT-CAR))
 (3368 1999 (:REWRITE DEFAULT-+-2))
 (2003 1999 (:REWRITE DEFAULT-+-1))
 (1271 1271 (:REWRITE DEL-SET-LEN))
 (1176 1176 (:TYPE-PRESCRIPTION BIND))
 (1097 145 (:REWRITE DEFAULT-CHAR-CODE))
 (952 95 (:REWRITE CHARACTERP-NTH))
 (415 415 (:REWRITE DEFAULT-COERCE-2))
 (360 322 (:REWRITE DEFAULT-<-2))
 (322 322 (:REWRITE DEFAULT-<-1))
 (136 136 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (4 4 (:TYPE-PRESCRIPTION JVM::BUILD-A-JAVA-VISIBLE-INSTANCE))
 (4 4 (:TYPE-PRESCRIPTION JVM::ALLOC))
 (2 2 (:TYPE-PRESCRIPTION JVM::MAKE-ARRAY))
 (2 2 (:TYPE-PRESCRIPTION LENGTH))
 )
(JVM::WFF-HEAP-STATE-LOAD_CP_ENTRIES
 (28 6 (:DEFINITION MV-NTH))
 (27 1 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (10 6 (:REWRITE DEFAULT-CDR))
 (8 5 (:REWRITE DEFAULT-CAR))
 (7 7 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRIES))
 (6 6 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRY))
 )
(JVM::WFF-HEAP-BIND)
(JVM::WFF-HEAP-STATE-LOAD_CLASS2
 (2016 78 (:DEFINITION MEM))
 (2008 8 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (1998 37 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (1648 7 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (1585 1146 (:REWRITE DEFAULT-CDR))
 (1287 1129 (:REWRITE DEFAULT-CAR))
 (1282 1 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (1266 1 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (1200 300 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (886 1 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (883 1 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (535 1 (:DEFINITION JVM::GETCPVALUE))
 (520 1 (:REWRITE JVM::CENTRY-VALUE-NO-CHANGE-LOAD_CP_ENTRIES))
 (518 2 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (259 259 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRY))
 (252 1 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (236 1 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (148 148 (:REWRITE MEM-SUBSET))
 (108 9 (:DEFINITION JVM::ARRAY-TYPE?))
 (78 2 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (75 15 (:DEFINITION LEN))
 (72 18 (:REWRITE ZP-OPEN))
 (53 53 (:TYPE-PRESCRIPTION LEN))
 (52 2 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (48 33 (:REWRITE DEFAULT-+-2))
 (48 6 (:DEFINITION BIND))
 (33 33 (:REWRITE DEFAULT-+-1))
 (33 11 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (27 1 (:DEFINITION JVM::DEFAULT-VALUE))
 (22 22 (:TYPE-PRESCRIPTION MEM))
 (21 7 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (20 5 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (20 2 (:DEFINITION JVM::STATIC-FIELD?-S))
 (18 18 (:REWRITE DEFAULT-<-2))
 (18 18 (:REWRITE DEFAULT-<-1))
 (16 4 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (15 15 (:REWRITE DEL-SET-LEN))
 (13 1 (:DEFINITION JVM::REFERENCE-TYPE))
 (12 4 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (9 3 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (8 2 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (8 2 (:DEFINITION JVM::METHOD-ARGS-S))
 (8 2 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (8 2 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (8 2 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (8 2 (:DEFINITION JVM::CODE-INSTRS-S))
 (8 2 (:DEFINITION JVM::CODE-HANDLERS-S))
 (8 2 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (7 7 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (6 2 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (6 2 (:DEFINITION JVM::METHOD-CODE-S))
 (6 2 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (4 1 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (3 1 (:DEFINITION JVM::CPENTRY-VALUE))
 (2 2 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (2 2 (:DEFINITION JVM::MAKE-METHOD))
 (2 2 (:DEFINITION JVM::MAKE-CODE))
 (2 1 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (1 1 (:TYPE-PRESCRIPTION JVM::PRIMITIVE-TYPE?))
 (1 1 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (1 1 (:DEFINITION JVM::NO-FATAL-ERROR?))
 (1 1 (:DEFINITION JVM::MAKE-FIELD))
 )
(JVM::WFF-HEAP-STATE-LOAD_CLASS_X
 (551 527 (:REWRITE DEFAULT-CAR))
 (423 399 (:REWRITE DEFAULT-CDR))
 (378 14 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (336 84 (:DEFINITION JVM::CLASS-BY-NAME))
 (322 14 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (304 76 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (280 28 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (175 10 (:DEFINITION SUBSET))
 (92 46 (:REWRITE DEFAULT-+-2))
 (88 22 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (87 87 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (46 46 (:REWRITE DEL-SET-LEN))
 (46 46 (:REWRITE DEFAULT-+-1))
 (46 46 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (27 27 (:REWRITE SUBSET-TRANSITIVE))
 (14 14 (:REWRITE SET-EQUAL-CONS))
 (5 5 (:REWRITE CDR-CONS))
 (5 5 (:REWRITE CAR-CONS))
 )
(JVM::WFF-HEAP-STATE-IMPLIES-WFF-HEAP)
(JVM::WFF-CLASS-TABLE-STATE-LOAD_CLASS2
 (2016 78 (:DEFINITION MEM))
 (2008 8 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (1648 7 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (1282 1 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (1266 1 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (886 1 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (883 1 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (788 629 (:REWRITE DEFAULT-CDR))
 (612 153 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (572 561 (:REWRITE DEFAULT-CAR))
 (535 1 (:DEFINITION JVM::GETCPVALUE))
 (520 1 (:REWRITE JVM::CENTRY-VALUE-NO-CHANGE-LOAD_CP_ENTRIES))
 (518 2 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (252 1 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (236 1 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (148 148 (:REWRITE MEM-SUBSET))
 (108 9 (:DEFINITION JVM::ARRAY-TYPE?))
 (108 2 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (78 2 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (72 18 (:REWRITE ZP-OPEN))
 (52 2 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (50 10 (:DEFINITION LEN))
 (38 38 (:TYPE-PRESCRIPTION LEN))
 (38 28 (:REWRITE DEFAULT-+-2))
 (28 28 (:REWRITE DEFAULT-+-1))
 (27 1 (:DEFINITION JVM::DEFAULT-VALUE))
 (22 22 (:TYPE-PRESCRIPTION MEM))
 (22 11 (:DEFINITION TRUE-LISTP))
 (21 7 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (20 5 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (20 2 (:DEFINITION JVM::STATIC-FIELD?-S))
 (18 18 (:REWRITE DEFAULT-<-2))
 (18 18 (:REWRITE DEFAULT-<-1))
 (16 4 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (14 14 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRY))
 (13 1 (:DEFINITION JVM::REFERENCE-TYPE))
 (12 4 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (10 10 (:REWRITE DEL-SET-LEN))
 (9 3 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (8 2 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (8 2 (:DEFINITION JVM::METHOD-ARGS-S))
 (8 2 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (8 2 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (8 2 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (8 2 (:DEFINITION JVM::CODE-INSTRS-S))
 (8 2 (:DEFINITION JVM::CODE-HANDLERS-S))
 (8 2 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (8 1 (:DEFINITION BIND))
 (7 7 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (6 2 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (6 2 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (6 2 (:DEFINITION JVM::METHOD-CODE-S))
 (6 2 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (6 1 (:DEFINITION ALISTP))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-HEAP))
 (4 1 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (3 1 (:DEFINITION JVM::CPENTRY-VALUE))
 (2 2 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (2 2 (:DEFINITION JVM::MAKE-METHOD))
 (2 2 (:DEFINITION JVM::MAKE-CODE))
 (2 1 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (1 1 (:TYPE-PRESCRIPTION JVM::PRIMITIVE-TYPE?))
 (1 1 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (1 1 (:DEFINITION JVM::NO-FATAL-ERROR?))
 (1 1 (:DEFINITION JVM::MAKE-FIELD))
 )
(JVM::WFF-CLASS-TABLE-STATE-LOAD_CLASS_X
 (284 1 (:DEFINITION JVM::LOAD_CLASS_X))
 (72 4 (:DEFINITION JVM::CLASS-LOADED?))
 (54 2 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (53 1 (:DEFINITION JVM::LOAD_CLASS_2-INV))
 (53 1 (:DEFINITION JVM::LOAD_CLASS_1-INV))
 (52 4 (:DEFINITION JVM::ISCLASSTERM))
 (50 8 (:DEFINITION MEM))
 (48 2 (:REWRITE JVM::CLASS-LOADED-LOAD_CLASS_X_3))
 (46 2 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (43 42 (:REWRITE DEFAULT-CAR))
 (40 4 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (37 35 (:REWRITE DEFAULT-CDR))
 (28 7 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (25 7 (:DEFINITION JVM::FATALERROR))
 (24 7 (:DEFINITION MV-NTH))
 (24 6 (:DEFINITION JVM::CLASS-BY-NAME))
 (20 4 (:DEFINITION LEN))
 (18 18 (:TYPE-PRESCRIPTION MEM))
 (18 18 (:TYPE-PRESCRIPTION LEN))
 (18 7 (:DEFINITION JVM::M6-INTERNAL-ERROR))
 (16 16 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (16 16 (:REWRITE MEM-SUBSET))
 (12 12 (:TYPE-PRESCRIPTION JVM::ALL-CLASS-NAMES-S))
 (11 7 (:DEFINITION JVM::STATE-SET-ERROR-FLAG))
 (8 8 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (8 4 (:REWRITE DEFAULT-+-2))
 (8 2 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (6 6 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (6 6 (:DEFINITION JVM::NO-FATAL-ERROR?))
 (4 4 (:REWRITE DEL-SET-LEN))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 2 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (3 3 (:REWRITE JVM::LOAD_CLASS_X_ONLY_CHANGE_CLASS_TABLE_ERROR_FLAG_HEAP))
 (3 3 (:REWRITE JVM::ENV-DOES-NOT-CHANGE-LOAD_CLASS_X))
 (3 3 (:DEFINITION JVM::EXTERNAL-CLASS-TABLE))
 (2 2 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (2 2 (:TYPE-PRESCRIPTION JVM::ISINTERFACE))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-LOADED?))
 (2 2 (:REWRITE SET-EQUAL-CONS))
 )
(JVM::WFF-CLASS-TABLE-IMPLIES-WFF-CLASS-TABLE)
(JVM::WFF-INSTANCE-CLASS-TABLE-IMPLIES-WFF-INSTANCE-CLASS-TABLE)
(JVM::WFF-CLASS-REP-MAKE-RUNTIME-CLASS-REP-GENERALIZE
 (4992 47 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (4059 460 (:DEFINITION MEM))
 (4005 47 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (3012 6 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (3008 8 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (2994 6 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (2880 8 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (2230 1087 (:DEFINITION NTH))
 (1847 1844 (:REWRITE DEFAULT-CDR))
 (1572 12 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (1200 1200 (:REWRITE DEFAULT-CAR))
 (873 873 (:REWRITE MEM-SUBSET))
 (756 63 (:DEFINITION JVM::ARRAY-TYPE?))
 (620 5 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (540 5 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (468 12 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (312 12 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (216 8 (:DEFINITION JVM::DEFAULT-VALUE))
 (158 83 (:REWRITE DEFAULT-+-2))
 (141 47 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (138 69 (:DEFINITION TRUE-LISTP))
 (136 34 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (130 13 (:DEFINITION JVM::STATIC-FIELD?-S))
 (104 8 (:DEFINITION JVM::REFERENCE-TYPE))
 (104 8 (:DEFINITION JVM::GETCPVALUE))
 (96 24 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (87 29 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (83 83 (:REWRITE DEFAULT-+-1))
 (76 76 (:REWRITE DEL-SET-LEN))
 (63 21 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (48 16 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (48 12 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (48 12 (:DEFINITION JVM::METHOD-ARGS-S))
 (48 12 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (48 12 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (48 12 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (48 12 (:DEFINITION JVM::CODE-INSTRS-S))
 (48 12 (:DEFINITION JVM::CODE-HANDLERS-S))
 (48 12 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (47 47 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (37 37 (:TYPE-PRESCRIPTION MEM))
 (36 12 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (36 12 (:DEFINITION JVM::METHOD-CODE-S))
 (32 8 (:REWRITE ZP-OPEN))
 (24 8 (:DEFINITION JVM::CPENTRY-VALUE))
 (16 16 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (12 12 (:DEFINITION JVM::MAKE-METHOD))
 (12 12 (:DEFINITION JVM::MAKE-CODE))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE DEFAULT-<-1))
 (5 5 (:DEFINITION JVM::MAKE-FIELD))
 (2 2 (:LINEAR SUBSET-NODUP-SET-SIZE))
 )
(JVM::WFF-INSTANCE-CLASS-TABLE-ADD-INSTANCE-CLASS-REP
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(JVM::WFF-INSTANCE-CLASS-TABLE-PRESERVED-BY-LOAD_CLASS_X2-WEAK
 (19651 813 (:DEFINITION MEM))
 (19553 83 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (18128 77 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (11512 11 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (11336 11 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (10652 6 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (9746 11 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (9713 11 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (8741 6887 (:REWRITE DEFAULT-CDR))
 (6700 1675 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (6383 6140 (:REWRITE DEFAULT-CAR))
 (5698 22 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (3295 11 (:DEFINITION JVM::GETCPVALUE))
 (3130 11 (:REWRITE JVM::CENTRY-VALUE-NO-CHANGE-LOAD_CP_ENTRIES))
 (2808 52 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (2772 11 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (2596 11 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (1543 1543 (:REWRITE MEM-SUBSET))
 (1188 99 (:DEFINITION JVM::ARRAY-TYPE?))
 (858 22 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (572 22 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (550 110 (:DEFINITION LEN))
 (452 113 (:REWRITE ZP-OPEN))
 (364 364 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRY))
 (335 225 (:REWRITE DEFAULT-+-2))
 (297 11 (:DEFINITION JVM::DEFAULT-VALUE))
 (231 77 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (225 225 (:REWRITE DEFAULT-+-1))
 (220 55 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (220 22 (:DEFINITION JVM::STATIC-FIELD?-S))
 (176 44 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (143 11 (:DEFINITION JVM::REFERENCE-TYPE))
 (132 44 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (113 113 (:REWRITE DEFAULT-<-2))
 (113 113 (:REWRITE DEFAULT-<-1))
 (110 110 (:REWRITE DEL-SET-LEN))
 (99 33 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (88 22 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (88 22 (:DEFINITION JVM::METHOD-ARGS-S))
 (88 22 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (88 22 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (88 22 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (88 22 (:DEFINITION JVM::CODE-INSTRS-S))
 (88 22 (:DEFINITION JVM::CODE-HANDLERS-S))
 (88 22 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (77 77 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (74 12 (:DEFINITION BIND))
 (66 22 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (66 22 (:DEFINITION JVM::METHOD-CODE-S))
 (66 22 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (53 21 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (36 9 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (33 11 (:DEFINITION JVM::CPENTRY-VALUE))
 (32 32 (:TYPE-PRESCRIPTION JVM::WFF-HEAP))
 (32 8 (:DEFINITION JVM::WFF-STATIC-CLASS-TABLE))
 (32 8 (:DEFINITION ASSOC-EQUAL))
 (30 5 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (22 22 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (22 22 (:DEFINITION JVM::MAKE-METHOD))
 (22 22 (:DEFINITION JVM::MAKE-CODE))
 (12 6 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (11 11 (:TYPE-PRESCRIPTION JVM::PRIMITIVE-TYPE?))
 (11 11 (:DEFINITION JVM::MAKE-FIELD))
 (11 6 (:DEFINITION JVM::NO-FATAL-ERROR?))
 (10 5 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (6 6 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (6 6 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (5 5 (:REWRITE SET-EQUAL-CONS))
 (5 5 (:REWRITE JVM::CLASS-BY-NAME-S-FOUND-IMPLIES-EQUAL-CLASS-NAME))
 )
(JVM::WFF-INSTANCE-CLASS-TABLE-PRESERVED-BY-LOAD_CLASS_X-WEAK
 (675 651 (:REWRITE DEFAULT-CAR))
 (547 523 (:REWRITE DEFAULT-CDR))
 (378 14 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (336 84 (:DEFINITION JVM::CLASS-BY-NAME))
 (322 14 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (304 76 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (280 28 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (175 10 (:DEFINITION SUBSET))
 (92 46 (:REWRITE DEFAULT-+-2))
 (88 22 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (87 87 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (46 46 (:REWRITE DEL-SET-LEN))
 (46 46 (:REWRITE DEFAULT-+-1))
 (46 46 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (27 27 (:REWRITE SUBSET-TRANSITIVE))
 (14 14 (:REWRITE SET-EQUAL-CONS))
 (5 5 (:REWRITE CDR-CONS))
 (5 5 (:REWRITE CAR-CONS))
 )
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IS-AN-EQUIVALENCE)
(JVM::EQUIV-TUPLE-LOAD2)
(JVM::EQUIV-TUPLE-LOAD2-IS-AN-EQUIVALENCE
 (76 76 (:REWRITE DEFAULT-CDR))
 (22 22 (:REWRITE DEFAULT-CAR))
 )
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUIV-TUPLE-LOAD2-LOAD_CP_ENTRY-2
 (44980 41392 (:REWRITE DEFAULT-CDR))
 (38135 33099 (:REWRITE DEFAULT-CAR))
 (24692 14628 (:REWRITE DEFAULT-+-2))
 (15744 5248 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (14836 14628 (:REWRITE DEFAULT-+-1))
 (12192 12192 (:TYPE-PRESCRIPTION BIND))
 (10496 10496 (:TYPE-PRESCRIPTION JVM::WFF-HEAP))
 (9848 1496 (:REWRITE DEFAULT-CHAR-CODE))
 (9376 9376 (:REWRITE DEL-SET-LEN))
 (8352 816 (:REWRITE CHARACTERP-NTH))
 (4298 4298 (:REWRITE DEFAULT-COERCE-2))
 (3726 3086 (:REWRITE DEFAULT-<-2))
 (3086 3086 (:REWRITE DEFAULT-<-1))
 (1872 1872 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (1272 204 (:DEFINITION MV-NTH))
 (24 24 (:TYPE-PRESCRIPTION JVM::ALLOC))
 (12 12 (:TYPE-PRESCRIPTION JVM::MAKE-ARRAY))
 (12 12 (:TYPE-PRESCRIPTION LENGTH))
 )
(JVM::MV-TO-SLOT)
(JVM::EQUIV-TUPLE-LOAD2-IMPLIES-EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-SLOT2-TUPLE-LOAD-1)
(JVM::EQUIV-TUPLE-LOAD2-IMPLIES-EQUAL-SLOT1-TUPLE-LOAD-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-CLASS-TABLE-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-HEAP-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-ERROR-FLAG-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-ENV-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUIV-TUPLE-LOAD2-LOAD_CP_ENTRIES-2
 (28 28 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE DEFAULT-CDR))
 )
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-MAKE-STATE)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-FATALERROR-2)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUIV-TUPLE-LOAD2-BUILD-AN-INSTANCECLASS-2)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-INSTANCE-CLASS-TABLE-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-ARRAY-CLASS-TABLE-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-LOAD_CLASS2-2
 (62400 364 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (55276 3588 (:DEFINITION MEM))
 (54756 364 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (36088 52 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (35932 52 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (29536 52 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (29340 7335 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (28704 52 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (25832 25832 (:REWRITE DEFAULT-CAR))
 (23047 23047 (:REWRITE DEFAULT-CDR))
 (20280 104 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (9776 52 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (8944 52 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (7784 1112 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (6812 6812 (:REWRITE MEM-SUBSET))
 (5616 468 (:DEFINITION JVM::ARRAY-TYPE?))
 (4056 104 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (3050 610 (:DEFINITION LEN))
 (2704 104 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (2066 2066 (:TYPE-PRESCRIPTION LEN))
 (1404 52 (:DEFINITION JVM::DEFAULT-VALUE))
 (1292 682 (:REWRITE DEFAULT-+-2))
 (1092 364 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (1040 260 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (1040 104 (:DEFINITION JVM::STATIC-FIELD?-S))
 (832 208 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (682 682 (:REWRITE DEFAULT-+-1))
 (676 52 (:DEFINITION JVM::REFERENCE-TYPE))
 (676 52 (:DEFINITION JVM::GETCPVALUE))
 (624 208 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (610 610 (:REWRITE DEL-SET-LEN))
 (468 156 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (456 152 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (416 104 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (416 104 (:DEFINITION JVM::METHOD-ARGS-S))
 (416 104 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (416 104 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (416 104 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (416 104 (:DEFINITION JVM::CODE-INSTRS-S))
 (416 104 (:DEFINITION JVM::CODE-HANDLERS-S))
 (416 104 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (364 364 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (312 312 (:TYPE-PRESCRIPTION MEM))
 (312 104 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (312 104 (:DEFINITION JVM::METHOD-CODE-S))
 (312 104 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (304 304 (:TYPE-PRESCRIPTION JVM::WFF-HEAP))
 (208 52 (:REWRITE ZP-OPEN))
 (156 52 (:DEFINITION JVM::CPENTRY-VALUE))
 (104 104 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (104 104 (:DEFINITION JVM::MAKE-METHOD))
 (104 104 (:DEFINITION JVM::MAKE-CODE))
 (52 52 (:REWRITE DEFAULT-<-2))
 (52 52 (:REWRITE DEFAULT-<-1))
 (52 52 (:DEFINITION JVM::MAKE-FIELD))
 )
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-NO-FATAL-ERROR?-1)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUAL-CLASS-LOADED?-2)
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-IMPLIES-EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-LOAD_CLASS_X-2
 (2220 2220 (:REWRITE DEFAULT-CAR))
 (2200 88 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (1848 88 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (1703 1703 (:REWRITE DEFAULT-CDR))
 (1536 384 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (1468 367 (:DEFINITION JVM::CLASS-BY-NAME))
 (740 40 (:DEFINITION SUBSET))
 (426 213 (:REWRITE DEFAULT-+-2))
 (370 370 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (304 304 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (213 213 (:REWRITE DEL-SET-LEN))
 (213 213 (:REWRITE DEFAULT-+-1))
 (100 100 (:REWRITE SUBSET-TRANSITIVE))
 (88 88 (:REWRITE SET-EQUAL-CONS))
 (8 8 (:REWRITE CDR-CONS))
 (8 8 (:REWRITE CAR-CONS))
 (3 3 (:TYPE-PRESCRIPTION JVM::LOAD_CLASS_X_INDUCT))
 )
(JVM::EQUIV-STATE-EXCEPT-THREAD-AND-TRACE2-MAKE-STATE-CASE)
(JVM::CHANGE-CURRENT-THREAD-DOES-NOT-CHANGE-CLASS-TABLE)
(JVM::ALL-FOUND?)
(JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM
 (81 64 (:REWRITE DEFAULT-CAR))
 (56 14 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (26 24 (:REWRITE DEFAULT-CDR))
 )
(JVM::ALL-CORRECTLY-LOADED-IMPLIES-COLLECT-SUPERCLASS-LIST
 (505 101 (:DEFINITION JVM::CLASS-BY-NAME))
 (467 431 (:REWRITE DEFAULT-CDR))
 (448 411 (:REWRITE DEFAULT-CAR))
 (224 56 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (105 7 (:DEFINITION JVM::ALL-FOUND?))
 (68 34 (:REWRITE DEFAULT-+-2))
 (34 34 (:REWRITE DEL-SET-LEN))
 (34 34 (:REWRITE DEFAULT-+-1))
 (21 7 (:DEFINITION JVM::ALL-CLASS-NAMES))
 (18 18 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (14 14 (:TYPE-PRESCRIPTION JVM::ALL-CLASS-NAMES))
 (8 8 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (8 8 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (8 8 (:REWRITE JVM::CORRECTLY-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (8 8 (:REWRITE JVM::CORRECTLY-LOADED?-CLASSNAME-CLASS-BY-NAME))
 (4 4 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (3 3 (:REWRITE SUBSET-TRANSITIVE))
 )
(JVM::ALL-CORRECTLY-LOADED?-APP-LIST
 (28 6 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (24 24 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (24 21 (:REWRITE DEFAULT-CAR))
 (16 16 (:TYPE-PRESCRIPTION APP))
 (15 15 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (15 15 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (14 12 (:REWRITE DEFAULT-CDR))
 )
(JVM::LOADER-INV-HELPER1-IMPLIES-ALL-CORRECTLY-LOADED
 (528 8 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (510 30 (:DEFINITION JVM::ISCLASSTERM))
 (390 15 (:REWRITE JVM::CLASS-EXISTS?-IMPLIES-MEM-ALL-CLASS-NAMES))
 (375 15 (:REWRITE JVM::CLASS-BY-NAME-ALL-CLASS-NAMES))
 (360 15 (:DEFINITION JVM::CLASS-EXISTS?))
 (297 11 (:DEFINITION JVM::COLLECT-INTERFACE-X-ENV))
 (262 222 (:REWRITE DEFAULT-CAR))
 (252 214 (:REWRITE DEFAULT-CDR))
 (230 13 (:DEFINITION JVM::COLLECT-SUPERCLASSNAME1))
 (192 48 (:DEFINITION MV-NTH))
 (180 180 (:TYPE-PRESCRIPTION LEN))
 (165 33 (:DEFINITION APP))
 (158 57 (:REWRITE MEM-SUBSET))
 (150 30 (:DEFINITION LEN))
 (150 30 (:DEFINITION JVM::CLASS-BY-NAME))
 (144 144 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (120 120 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (97 3 (:DEFINITION SUBSET))
 (96 24 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (60 60 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (60 30 (:REWRITE DEFAULT-+-2))
 (60 10 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (33 33 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (30 30 (:REWRITE DEL-SET-LEN))
 (30 30 (:REWRITE DEFAULT-+-1))
 (19 19 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (19 19 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (15 15 (:TYPE-PRESCRIPTION JVM::ISCLASSTERM))
 (15 15 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 (11 11 (:TYPE-PRESCRIPTION SUBSET))
 (8 8 (:REWRITE SET-EQUAL-CONS))
 (5 5 (:REWRITE SUBSET-TRANSITIVE))
 (5 5 (:REWRITE JVM::LOADER-INV-HELPER-MEM-IMPLIES))
 )
(JVM::CLASS-LOADED-IMPLIES
 (70 1 (:DEFINITION JVM::ALL-CLASS-NAMES))
 (66 1 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (26 1 (:REWRITE JVM::CLASS-EXISTS?-IMPLIES-MEM-ALL-CLASS-NAMES))
 (25 5 (:DEFINITION JVM::CLASS-BY-NAME))
 (24 1 (:DEFINITION JVM::CLASS-EXISTS?))
 (15 15 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-CAR))
 (11 1 (:DEFINITION MEM))
 (10 10 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (10 10 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:TYPE-PRESCRIPTION JVM::ALL-CLASS-NAMES))
 (4 4 (:REWRITE DEL-SET-LEN))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE MEM-SUBSET))
 (1 1 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 (1 1 (:REWRITE SET-EQUAL-CONS))
 )
(JVM::LOADER-INV-IMPLIES
 (2611 1 (:DEFINITION JVM::WFF-STATIC-CLASS-TABLE-STRONG))
 (2595 1 (:DEFINITION JVM::WFF-CLASS-REP-STATIC-STRONG))
 (1435 113 (:DEFINITION MEM))
 (1401 11 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (1200 2 (:DEFINITION JVM::WFF-STATIC-CP-OK-S))
 (1160 2 (:DEFINITION JVM::WFF-STATIC-CP-ENTRY-OK-S))
 (1038 2 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARDS))
 (1014 2 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARD))
 (932 340 (:DEFINITION NTH))
 (771 5 (:DEFINITION JVM::WFF-TYPE-REP))
 (583 583 (:REWRITE DEFAULT-CDR))
 (548 548 (:REWRITE DEFAULT-CAR))
 (536 2 (:DEFINITION JVM::VALUE-TYPE-OK))
 (342 2 (:DEFINITION JVM::WFF-TYPE-REPS))
 (256 2 (:DEFINITION JVM::VALUE-TYPE-OK-2))
 (250 50 (:DEFINITION LEN))
 (215 215 (:REWRITE MEM-SUBSET))
 (178 24 (:DEFINITION JVM::ARRAY-TYPE?))
 (176 2 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (157 1 (:DEFINITION JVM::WFF-FIELDS-S))
 (156 156 (:TYPE-PRESCRIPTION LEN))
 (151 1 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE-STRONG))
 (144 36 (:REWRITE ZP-OPEN))
 (143 1 (:DEFINITION JVM::WFF-CLASS-REP-STRONG))
 (136 86 (:REWRITE DEFAULT-+-2))
 (120 4 (:DEFINITION JVM::WFF-CODE-S))
 (106 2 (:DEFINITION JVM::WFF-CONSTANT-POOL-S))
 (98 2 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY-S))
 (86 86 (:REWRITE DEFAULT-+-1))
 (78 76 (:REWRITE DEFAULT-<-2))
 (76 76 (:REWRITE DEFAULT-<-1))
 (65 13 (:DEFINITION INT32P))
 (62 2 (:DEFINITION JVM::WFF-METHOD-DECL-S))
 (57 19 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (53 1 (:DEFINITION JVM::WFF-CONSTANT-POOL))
 (52 26 (:DEFINITION TRUE-LISTP))
 (50 50 (:REWRITE DEL-SET-LEN))
 (49 1 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY))
 (39 3 (:DEFINITION JVM::WFF-FIELD-S))
 (36 12 (:DEFINITION JVM::METHOD-CODE-S))
 (36 12 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (35 1 (:DEFINITION JVM::WFF-CLASS-METHOD-DECLS))
 (34 2 (:DEFINITION JVM::WFF-FIELDS-S-X))
 (32 8 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (31 1 (:DEFINITION JVM::WFF-METHOD-DECL))
 (30 2 (:DEFINITION JVM::WFF-LONG-CP-ENTRY-S))
 (30 2 (:DEFINITION JVM::WFF-INT-CP-ENTRY-S))
 (26 2 (:DEFINITION JVM::REFERENCE-TYPE))
 (25 5 (:DEFINITION INT64P))
 (25 1 (:DEFINITION JVM::WFF-INTERFACE-CLASS-STATIC))
 (24 1 (:DEFINITION JVM::ALL-FIELDS-STATIC-FINAL))
 (23 23 (:TYPE-PRESCRIPTION MEM))
 (21 7 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (20 2 (:DEFINITION JVM::WFF-STRING-CP-ENTRY-S))
 (20 2 (:DEFINITION JVM::STATIC-FIELD?-S))
 (17 1 (:DEFINITION JVM::WFF-STATIC-FIELDS-X))
 (17 1 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (16 4 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (16 4 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (16 4 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (16 4 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (15 1 (:DEFINITION JVM::WFF-LONG-CP-ENTRY))
 (15 1 (:DEFINITION JVM::WFF-INT-CP-ENTRY))
 (13 1 (:DEFINITION JVM::WFF-STATIC-FIELD))
 (13 1 (:DEFINITION JVM::WFF-FIELD))
 (12 2 (:DEFINITION SHORTP))
 (12 2 (:DEFINITION JVMBOOLEANP))
 (12 2 (:DEFINITION CHARP))
 (12 2 (:DEFINITION BYTEP))
 (12 1 (:DEFINITION NODUP-SET))
 (10 1 (:DEFINITION JVM::WFF-STRING-CP-ENTRY))
 (8 2 (:DEFINITION JVM::METHOD-ARGS-S))
 (7 7 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REP))
 (6 2 (:DEFINITION JVM::CPENTRY-VALUE-S))
 (6 1 (:DEFINITION JVM::COLLECT-STATIC-FIELD-NAMES))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REPS))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-FIELDS-S-X))
 (4 4 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL-S))
 (4 4 (:TYPE-PRESCRIPTION JVM::RUNTIME-METHOD-REP-GUARDS))
 (4 2 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (4 1 (:DEFINITION JVM::STATIC-FIELDS))
 (4 1 (:DEFINITION JVM::METHODS))
 (4 1 (:DEFINITION JVM::FIELDS))
 (4 1 (:DEFINITION JVM::CONSTANTPOOL))
 (3 1 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-FIELDS-X))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-CP-OK-S))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-FIELDS-S))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP-STATIC))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-METHOD-DECLS))
 (2 2 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (2 2 (:TYPE-PRESCRIPTION NODUP-SET))
 (2 2 (:TYPE-PRESCRIPTION JVM::COLLECT-STATIC-FIELD-NAMES))
 (2 2 (:TYPE-PRESCRIPTION JVM::ALL-FIELDS-STATIC-FINAL))
 (2 2 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (2 2 (:DEFINITION JVMFLOATP))
 (2 2 (:DEFINITION DOUBLEP))
 (1 1 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL))
 )
(JVM::LOADER-INV-LOADED-CLASS-IMPLIES-ALL-CORRECTLY-LOADED
 (17 1 (:DEFINITION JVM::COLLECT-SUPERCLASSNAME1))
 (15 3 (:DEFINITION JVM::CLASS-BY-NAME))
 (11 10 (:REWRITE DEFAULT-CDR))
 (11 10 (:REWRITE DEFAULT-CAR))
 (8 2 (:DEFINITION MV-NTH))
 (6 6 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (6 6 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (6 1 (:DEFINITION JVM::ALL-CLASS-NAMES))
 (4 2 (:REWRITE DEFAULT-+-2))
 (4 1 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (2 2 (:REWRITE DEL-SET-LEN))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (2 1 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (1 1 (:REWRITE SET-EQUAL-CONS))
 (1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (1 1 (:REWRITE MEM-SUBSET))
 (1 1 (:DEFINITION MEM))
 )
(JVM::LOADER-INV-HELPER-IMPLIES-ALL-FOUND?
 (660 567 (:REWRITE DEFAULT-CAR))
 (577 491 (:REWRITE DEFAULT-CDR))
 (553 13 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (410 82 (:DEFINITION JVM::CLASS-BY-NAME))
 (392 98 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (255 51 (:DEFINITION APP))
 (164 164 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (98 49 (:DEFINITION NTH))
 (92 46 (:REWRITE DEFAULT-+-2))
 (49 49 (:TYPE-PRESCRIPTION JVM::COLLECT-SUPERCLASSNAME1))
 (49 49 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (46 46 (:REWRITE DEL-SET-LEN))
 (46 46 (:REWRITE DEFAULT-+-1))
 (34 34 (:REWRITE MEM-SUBSET))
 (34 34 (:DEFINITION MEM))
 (23 23 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (23 23 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (20 20 (:REWRITE JVM::CORRECTLY-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (20 20 (:REWRITE JVM::CORRECTLY-LOADED?-CLASSNAME-CLASS-BY-NAME))
 (20 20 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (13 13 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-ALL-CORRECTLY-LOADED))
 (10 10 (:REWRITE JVM::LOADER-INV-HELPER-MEM-IMPLIES))
 )
(JVM::LOADED-IN-A-LOADER-INV-STATE-SUPERCHAIN-IS-FIXED
 (51 3 (:DEFINITION JVM::COLLECT-SUPERCLASSNAME1))
 (24 6 (:DEFINITION MV-NTH))
 (19 16 (:REWRITE DEFAULT-CAR))
 (18 18 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (17 14 (:REWRITE DEFAULT-CDR))
 (15 3 (:DEFINITION JVM::CLASS-BY-NAME))
 (12 3 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (6 6 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE MEM-SUBSET))
 (3 3 (:DEFINITION MEM))
 (3 1 (:DEFINITION JVM::ALL-CLASS-NAMES))
 (2 2 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (2 2 (:REWRITE DEL-SET-LEN))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR SUBSET-NODUP-SET-SIZE))
 )
(JVM::COLLECT-SUPERCLASSNAME1-DOES-NOT-CHANGE)
(JVM::CLASS-LOADED?-IS-PERSERVED
 (112911 4298 (:DEFINITION MEM))
 (112553 443 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (89648 382 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (78202 61 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (77226 61 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (46462 36432 (:REWRITE DEFAULT-CDR))
 (45186 51 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (45033 51 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (37076 9269 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (34139 33147 (:REWRITE DEFAULT-CAR))
 (32635 61 (:DEFINITION JVM::GETCPVALUE))
 (31720 61 (:REWRITE JVM::CENTRY-VALUE-NO-CHANGE-LOAD_CP_ENTRIES))
 (26418 102 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (11826 219 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (11592 46 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (10856 46 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (8153 8153 (:REWRITE MEM-SUBSET))
 (6048 504 (:DEFINITION JVM::ARRAY-TYPE?))
 (4392 1098 (:REWRITE ZP-OPEN))
 (3978 102 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (2652 102 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (2410 1754 (:REWRITE DEFAULT-+-2))
 (1754 1754 (:REWRITE DEFAULT-+-1))
 (1647 61 (:DEFINITION JVM::DEFAULT-VALUE))
 (1533 1533 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRY))
 (1287 1287 (:TYPE-PRESCRIPTION MEM))
 (1146 382 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (1100 275 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (1098 1098 (:REWRITE DEFAULT-<-2))
 (1098 1098 (:REWRITE DEFAULT-<-1))
 (1070 107 (:DEFINITION JVM::STATIC-FIELD?-S))
 (816 204 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (793 61 (:DEFINITION JVM::REFERENCE-TYPE))
 (687 229 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (661 661 (:REWRITE DEL-SET-LEN))
 (504 168 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (408 102 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (408 102 (:DEFINITION JVM::METHOD-ARGS-S))
 (408 102 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (408 102 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (408 102 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (408 102 (:DEFINITION JVM::CODE-INSTRS-S))
 (408 102 (:DEFINITION JVM::CODE-HANDLERS-S))
 (408 102 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (382 382 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (366 122 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (306 102 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (306 102 (:DEFINITION JVM::METHOD-CODE-S))
 (183 61 (:DEFINITION JVM::CPENTRY-VALUE))
 (122 122 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (122 61 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (102 102 (:DEFINITION JVM::MAKE-METHOD))
 (102 102 (:DEFINITION JVM::MAKE-CODE))
 (80 80 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (61 61 (:TYPE-PRESCRIPTION JVM::PRIMITIVE-TYPE?))
 (51 17 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (48 48 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (46 46 (:DEFINITION JVM::MAKE-FIELD))
 (34 34 (:TYPE-PRESCRIPTION JVM::WFF-HEAP))
 (8 1 (:DEFINITION BIND))
 (5 5 (:REWRITE JVM::CLASS-BY-NAME-CONS))
 (4 1 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (1 1 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (1 1 (:DEFINITION JVM::NO-FATAL-ERROR?))
 )
(JVM::CLASS-LOADED-MAKE-STATE-EQUAL)
(JVM::CLASS-LOADED?-IS-PERSERVED-BY-LOAD_CLASS_X
 (378 14 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (360 344 (:REWRITE DEFAULT-CAR))
 (322 14 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (280 28 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (272 68 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (244 220 (:REWRITE DEFAULT-CDR))
 (175 10 (:DEFINITION SUBSET))
 (85 17 (:DEFINITION JVM::CLASS-BY-NAME))
 (72 18 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (67 67 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (34 34 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (26 26 (:REWRITE SUBSET-TRANSITIVE))
 (14 14 (:REWRITE SET-EQUAL-CONS))
 (5 5 (:REWRITE CDR-CONS))
 (5 5 (:REWRITE CAR-CONS))
 )
(JVM::ONCE-LOADED-SUPERCHAIN-DOES-NOT-CHANGE
 (62 2 (:DEFINITION JVM::LOAD_CLASS_X))
 (34 2 (:DEFINITION JVM::COLLECT-SUPERCLASSNAME1))
 (24 6 (:DEFINITION MV-NTH))
 (20 20 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (18 14 (:REWRITE DEFAULT-CAR))
 (16 4 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (12 4 (:DEFINITION JVM::FATALERROR))
 (10 8 (:REWRITE DEFAULT-CDR))
 (10 4 (:DEFINITION MEM))
 (8 8 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (8 4 (:DEFINITION JVM::M6-INTERNAL-ERROR))
 (6 6 (:REWRITE MEM-SUBSET))
 (6 2 (:REWRITE JVM::CLASS-LOADED-LOAD_CLASS_X_3))
 (4 4 (:DEFINITION JVM::STATE-SET-ERROR-FLAG))
 (4 2 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (2 2 (:TYPE-PRESCRIPTION MEM))
 (2 2 (:REWRITE JVM::ENV-DOES-NOT-CHANGE-LOAD_CLASS_X))
 )
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE)
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE-EXTENSION
 (68 4 (:DEFINITION JVM::ISCLASSTERM))
 (52 2 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (52 2 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (48 2 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (48 2 (:DEFINITION JVM::CLASS-EXISTS?))
 (30 30 (:REWRITE DEFAULT-CDR))
 (30 6 (:DEFINITION LEN))
 (20 20 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (20 20 (:REWRITE DEFAULT-CAR))
 (16 16 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (12 6 (:REWRITE DEFAULT-+-2))
 (8 4 (:DEFINITION NTH))
 (6 6 (:REWRITE DEL-SET-LEN))
 (6 6 (:REWRITE DEFAULT-+-1))
 (4 2 (:DEFINITION TRUE-LISTP))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 (2 2 (:REWRITE JVM::CLASS-BY-NAME-CONS))
 )
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIED-BY
 (68 4 (:DEFINITION JVM::ISCLASSTERM))
 (52 2 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (52 2 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (48 2 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (48 2 (:DEFINITION JVM::CLASS-EXISTS?))
 (40 8 (:DEFINITION JVM::CLASS-BY-NAME))
 (30 30 (:REWRITE DEFAULT-CDR))
 (30 6 (:DEFINITION LEN))
 (20 20 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (16 16 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (12 6 (:REWRITE DEFAULT-+-2))
 (8 4 (:DEFINITION NTH))
 (6 6 (:REWRITE DEL-SET-LEN))
 (6 6 (:REWRITE DEFAULT-+-1))
 (4 2 (:DEFINITION TRUE-LISTP))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 )
(JVM::CLASS-BY-NAME-LOAD_CLASS2
 (12096 468 (:DEFINITION MEM))
 (12048 48 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (9888 42 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (7692 6 (:DEFINITION JVM::RUNTIME-STATIC-FIELDS-REP1))
 (7596 6 (:DEFINITION JVM::RUNTIME-STATIC-FIELD-REP))
 (5459 4240 (:REWRITE DEFAULT-CDR))
 (5316 6 (:DEFINITION JVM::RUNTIME-METHODS-REP1))
 (5298 6 (:DEFINITION JVM::RUNTIME-METHOD-REP))
 (4280 1070 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (4076 3888 (:REWRITE DEFAULT-CAR))
 (3210 6 (:DEFINITION JVM::GETCPVALUE))
 (3120 6 (:REWRITE JVM::CENTRY-VALUE-NO-CHANGE-LOAD_CP_ENTRIES))
 (3108 12 (:DEFINITION JVM::NORMALIZE-TYPE-REPS))
 (2268 42 (:DEFINITION JVM::LOAD_CP_ENTRIES))
 (1512 6 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELDS-REP1))
 (1416 6 (:DEFINITION JVM::RUNTIME-INSTANCE-FIELD-REP))
 (888 888 (:REWRITE MEM-SUBSET))
 (648 54 (:DEFINITION JVM::ARRAY-TYPE?))
 (468 12 (:DEFINITION JVM::RUNTIME-CODE-REP))
 (432 108 (:REWRITE ZP-OPEN))
 (312 12 (:DEFINITION JVM::RUNTIME-CODE-REP0))
 (300 60 (:DEFINITION LEN))
 (294 294 (:TYPE-PRESCRIPTION JVM::LOAD_CP_ENTRY))
 (228 168 (:REWRITE DEFAULT-+-2))
 (218 218 (:TYPE-PRESCRIPTION LEN))
 (168 168 (:REWRITE DEFAULT-+-1))
 (162 6 (:DEFINITION JVM::DEFAULT-VALUE))
 (132 132 (:TYPE-PRESCRIPTION MEM))
 (126 42 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (120 30 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (120 12 (:DEFINITION JVM::STATIC-FIELD?-S))
 (108 108 (:REWRITE DEFAULT-<-2))
 (108 108 (:REWRITE DEFAULT-<-1))
 (96 24 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (78 6 (:DEFINITION JVM::REFERENCE-TYPE))
 (72 24 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (60 60 (:REWRITE DEL-SET-LEN))
 (54 18 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (48 12 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (48 12 (:DEFINITION JVM::METHOD-ARGS-S))
 (48 12 (:DEFINITION JVM::CODE-STACKMAPS-S))
 (48 12 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (48 12 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (48 12 (:DEFINITION JVM::CODE-INSTRS-S))
 (48 12 (:DEFINITION JVM::CODE-HANDLERS-S))
 (48 12 (:DEFINITION JVM::CODE-CODE-LENGTH-S))
 (42 42 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (36 12 (:DEFINITION JVM::METHOD-METHODNAME-S))
 (36 12 (:DEFINITION JVM::METHOD-CODE-S))
 (36 12 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (34 34 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (33 11 (:REWRITE JVM::WFF-HEAP-IMPLIES-ALISTP))
 (22 22 (:TYPE-PRESCRIPTION JVM::WFF-HEAP))
 (20 5 (:REWRITE JVM::CLASS-BY-NAME-CONS))
 (18 6 (:DEFINITION JVM::CPENTRY-VALUE))
 (12 12 (:DEFINITION JVM::MAKE-STATIC-FIELD))
 (12 12 (:DEFINITION JVM::MAKE-METHOD))
 (12 12 (:DEFINITION JVM::MAKE-CODE))
 (12 6 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (8 1 (:DEFINITION BIND))
 (6 6 (:TYPE-PRESCRIPTION JVM::PRIMITIVE-TYPE?))
 (6 6 (:DEFINITION JVM::MAKE-FIELD))
 (4 1 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (1 1 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (1 1 (:DEFINITION JVM::NO-FATAL-ERROR?))
 )
(JVM::LOAD_CLASS_DOES_NOT_CHANGE_LOADED_CLASS
 (1020 986 (:REWRITE DEFAULT-CAR))
 (742 718 (:REWRITE DEFAULT-CDR))
 (732 576 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (378 14 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (344 86 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (322 14 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (280 28 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (180 90 (:REWRITE DEFAULT-+-2))
 (175 10 (:DEFINITION SUBSET))
 (120 6 (:DEFINITION JVM::ALL-FOUND?))
 (114 114 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (104 26 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (91 91 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (90 90 (:REWRITE DEL-SET-LEN))
 (90 90 (:REWRITE DEFAULT-+-1))
 (30 30 (:TYPE-PRESCRIPTION JVM::ALL-FOUND?))
 (27 27 (:REWRITE SUBSET-TRANSITIVE))
 (18 18 (:TYPE-PRESCRIPTION JVM::ALL-CLASS-NAMES))
 (18 6 (:DEFINITION JVM::ALL-CLASS-NAMES))
 (14 14 (:REWRITE SET-EQUAL-CONS))
 (6 6 (:REWRITE JVM::LOADER-INV-HELPER-IMPLIES-ALL-FOUND?))
 (5 5 (:REWRITE CDR-CONS))
 (5 5 (:REWRITE CAR-CONS))
 )
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE-PERSERVED-BY-LOAD_CLASS_X
 (492 2 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (454 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE-STRONG))
 (432 2 (:DEFINITION JVM::WFF-CLASS-REP-STRONG))
 (322 1 (:DEFINITION JVM::LOAD_CLASS_X))
 (158 156 (:REWRITE DEFAULT-CDR))
 (128 2 (:DEFINITION JVM::WFF-CONSTANT-POOL))
 (124 2 (:DEFINITION JVM::WFF-CLASS-METHOD-DECLS))
 (114 2 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY))
 (110 2 (:DEFINITION JVM::WFF-METHOD-DECL))
 (95 94 (:REWRITE DEFAULT-CAR))
 (95 19 (:DEFINITION JVM::CLASS-BY-NAME))
 (64 14 (:DEFINITION TRUE-LISTP))
 (64 2 (:DEFINITION JVM::WFF-STATIC-FIELDS-X))
 (56 28 (:REWRITE DEFAULT-+-2))
 (56 28 (:DEFINITION NTH))
 (54 2 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (54 2 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (53 1 (:DEFINITION JVM::LOAD_CLASS_2-INV))
 (53 1 (:DEFINITION JVM::LOAD_CLASS_1-INV))
 (52 2 (:REWRITE JVM::CLASS-LOADED-LOAD_CLASS_X_3))
 (50 8 (:DEFINITION MEM))
 (50 2 (:DEFINITION JVM::WFF-STATIC-FIELD))
 (48 48 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (46 46 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (46 2 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (40 4 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (38 38 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (30 2 (:DEFINITION JVM::WFF-LONG-CP-ENTRY))
 (30 2 (:DEFINITION JVM::WFF-INT-CP-ENTRY))
 (30 2 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (30 2 (:DEFINITION JVM::CLASS-EXISTS?))
 (28 28 (:REWRITE DEL-SET-LEN))
 (28 28 (:REWRITE DEFAULT-+-1))
 (28 7 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (25 7 (:DEFINITION JVM::FATALERROR))
 (24 7 (:DEFINITION MV-NTH))
 (20 2 (:DEFINITION JVM::WFF-STRING-CP-ENTRY))
 (18 18 (:TYPE-PRESCRIPTION MEM))
 (18 7 (:DEFINITION JVM::M6-INTERNAL-ERROR))
 (16 16 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (16 16 (:REWRITE MEM-SUBSET))
 (16 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (12 12 (:TYPE-PRESCRIPTION JVM::WFF-STATIC-FIELDS-X))
 (12 12 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-METHOD-DECLS))
 (12 12 (:TYPE-PRESCRIPTION JVM::ALL-CLASS-NAMES-S))
 (11 7 (:DEFINITION JVM::STATE-SET-ERROR-FLAG))
 (10 10 (:TYPE-PRESCRIPTION JVM::WFF-INSTANCE-CLASS-TABLE-STRONG))
 (10 10 (:TYPE-PRESCRIPTION JVM::WFF-INSTANCE-CLASS-TABLE))
 (10 10 (:TYPE-PRESCRIPTION JVM::WFF-CONSTANT-POOL))
 (10 2 (:DEFINITION INT64P))
 (10 2 (:DEFINITION INT32P))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE DEFAULT-<-1))
 (8 2 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (8 2 (:DEFINITION JVM::STATIC-FIELDS))
 (8 2 (:DEFINITION JVM::METHODS))
 (8 2 (:DEFINITION JVM::CONSTANTPOOL))
 (6 6 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (6 6 (:DEFINITION JVM::NO-FATAL-ERROR?))
 (4 2 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (3 3 (:REWRITE JVM::LOAD_CLASS_X_ONLY_CHANGE_CLASS_TABLE_ERROR_FLAG_HEAP))
 (3 3 (:REWRITE JVM::ENV-DOES-NOT-CHANGE-LOAD_CLASS_X))
 (3 3 (:DEFINITION JVM::EXTERNAL-CLASS-TABLE))
 (2 2 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
 (2 2 (:TYPE-PRESCRIPTION JVM::ISINTERFACE))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 (2 2 (:REWRITE SET-EQUAL-CONS))
 )
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE
 (68 4 (:DEFINITION JVM::ISCLASSTERM))
 (52 2 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (52 2 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (48 2 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (48 2 (:DEFINITION JVM::CLASS-EXISTS?))
 (40 8 (:DEFINITION JVM::CLASS-BY-NAME))
 (30 6 (:DEFINITION LEN))
 (29 29 (:REWRITE DEFAULT-CDR))
 (19 19 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (16 16 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (12 6 (:REWRITE DEFAULT-+-2))
 (8 4 (:DEFINITION NTH))
 (6 6 (:REWRITE DEL-SET-LEN))
 (6 6 (:REWRITE DEFAULT-+-1))
 (4 2 (:DEFINITION TRUE-LISTP))
 (4 1 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (2 2 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 )
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE-B)
(JVM::LOADR-INV-IMPLIES-WFF-STATIC-CLASS-TABLE)
(JVM::CLASS-TABLE-CORRECT-EXTENSION-DOES-NOT-CHANGE-BUILD-IMMEDIMATE-DATA-GUARD
 (102 6 (:DEFINITION JVM::ISCLASSTERM))
 (78 3 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (78 3 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (72 3 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (72 3 (:DEFINITION JVM::CLASS-EXISTS?))
 (60 12 (:DEFINITION JVM::CLASS-BY-NAME))
 (45 45 (:REWRITE DEFAULT-CDR))
 (45 9 (:DEFINITION LEN))
 (32 32 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (30 30 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (18 9 (:REWRITE DEFAULT-+-2))
 (12 6 (:DEFINITION NTH))
 (12 3 (:DEFINITION TRUE-LISTP))
 (9 9 (:REWRITE DEL-SET-LEN))
 (9 9 (:REWRITE DEFAULT-+-1))
 (3 3 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (3 3 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 )
(JVM::ALL-LOADED?)
(JVM::CLASS-TABLE-CORRECT-EXTENSION-DOES-NOT-CHANGE-BUILD-AN-JAVA-INSTANCE-DATA-GUARD
 (2805 38 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIED-BY))
 (2648 25 (:DEFINITION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (850 50 (:DEFINITION JVM::ISCLASSTERM))
 (800 25 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (660 6 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE-PERSERVED-BY-LOAD_CLASS_X))
 (656 25 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (656 25 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (625 25 (:DEFINITION JVM::WFF-FIELD))
 (606 25 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (606 25 (:DEFINITION JVM::CLASS-EXISTS?))
 (500 500 (:TYPE-PRESCRIPTION LEN))
 (500 100 (:DEFINITION JVM::CLASS-BY-NAME))
 (375 75 (:DEFINITION LEN))
 (356 356 (:REWRITE DEFAULT-CDR))
 (300 300 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (248 248 (:REWRITE DEFAULT-CAR))
 (200 200 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (150 75 (:REWRITE DEFAULT-+-2))
 (125 25 (:DEFINITION TRUE-LISTP))
 (107 25 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE-B))
 (100 100 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (100 100 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (100 50 (:DEFINITION NTH))
 (100 25 (:DEFINITION JVM::FIELDS))
 (75 75 (:REWRITE DEL-SET-LEN))
 (75 75 (:REWRITE DEFAULT-+-1))
 (50 50 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP))
 (48 24 (:REWRITE JVM::LOAD_CLASS_DOES_NOT_CHANGE_LOADED_CLASS))
 (25 25 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (25 25 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 )
(JVM::LOADER-INV-AND-LOADED-IMPLIES-ALL-LOADED
 (270 54 (:DEFINITION JVM::CLASS-BY-NAME))
 (156 153 (:REWRITE DEFAULT-CDR))
 (136 133 (:REWRITE DEFAULT-CAR))
 (108 108 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (62 31 (:REWRITE DEFAULT-+-2))
 (31 31 (:REWRITE DEL-SET-LEN))
 (31 31 (:REWRITE DEFAULT-+-1))
 (26 26 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (24 12 (:DEFINITION NTH))
 (12 12 (:REWRITE JVM::ALL-CORRECTLY-LOADED-IMPLIES-COLLECT-SUPERCLASS-LIST))
 (1 1 (:REWRITE SUBSET-TRANSITIVE))
 )
(JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-EQUAL
 (336 3 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIED-BY))
 (228 2 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE-B))
 (208 2 (:DEFINITION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (170 10 (:DEFINITION JVM::ISCLASSTERM))
 (130 5 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (130 5 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (130 5 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (120 5 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (120 5 (:DEFINITION JVM::CLASS-EXISTS?))
 (101 5 (:DEFINITION JVM::WFF-FIELD))
 (100 20 (:DEFINITION JVM::CLASS-BY-NAME))
 (92 92 (:TYPE-PRESCRIPTION LEN))
 (75 15 (:DEFINITION LEN))
 (73 73 (:REWRITE DEFAULT-CDR))
 (52 52 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (48 48 (:REWRITE DEFAULT-CAR))
 (40 40 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (30 15 (:REWRITE DEFAULT-+-2))
 (20 10 (:DEFINITION NTH))
 (19 5 (:DEFINITION TRUE-LISTP))
 (16 3 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (15 15 (:REWRITE DEL-SET-LEN))
 (15 15 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (5 5 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (5 5 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 (2 2 (:TYPE-PRESCRIPTION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 )
(JVM::BUILD-A-JAVA-VISIBLE-INSTANCE-DATA-GUARD-EQUAL
 (902 16 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIED-BY))
 (832 8 (:DEFINITION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (272 16 (:DEFINITION JVM::ISCLASSTERM))
 (256 8 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (208 8 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (208 8 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (200 8 (:DEFINITION JVM::WFF-FIELD))
 (192 8 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (192 8 (:DEFINITION JVM::CLASS-EXISTS?))
 (160 160 (:TYPE-PRESCRIPTION LEN))
 (160 32 (:DEFINITION JVM::CLASS-BY-NAME))
 (120 24 (:DEFINITION LEN))
 (118 118 (:REWRITE DEFAULT-CDR))
 (96 96 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (84 84 (:REWRITE DEFAULT-CAR))
 (64 64 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (48 24 (:REWRITE DEFAULT-+-2))
 (40 8 (:DEFINITION TRUE-LISTP))
 (32 32 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (32 32 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (32 16 (:DEFINITION NTH))
 (32 8 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE-B))
 (32 8 (:DEFINITION JVM::FIELDS))
 (24 24 (:REWRITE DEL-SET-LEN))
 (24 24 (:REWRITE DEFAULT-+-1))
 (20 20 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-REP))
 (16 2 (:DEFINITION JVM::WFF-INSTANCE-CLASS-TABLE))
 (10 10 (:TYPE-PRESCRIPTION JVM::WFF-INSTANCE-CLASS-TABLE))
 (8 8 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (8 8 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 )
(JVM::LOADER-INV-AND-LOADED-IMPLIES-ALL-LOADED-GENERALIZE
 (34 1 (:DEFINITION JVM::COLLECT-SUPERCLASS-LIST1))
 (10 2 (:DEFINITION JVM::CLASS-BY-NAME))
 (9 1 (:DEFINITION JVM::ISCLASSTERM))
 (6 6 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 1 (:DEFINITION LEN))
 (4 4 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (4 1 (:DEFINITION MEM))
 (4 1 (:DEFINITION JVM::CLASSSUPERCLASSNAME))
 (3 3 (:TYPE-PRESCRIPTION LEN))
 (3 1 (:DEFINITION JVM::SUPER))
 (2 2 (:REWRITE MEM-SUBSET))
 (2 2 (:REWRITE JVM::ALL-CORRECTLY-LOADED-IMPLIES-COLLECT-SUPERCLASS-LIST))
 (2 1 (:REWRITE DEFAULT-+-2))
 (2 1 (:DEFINITION NTH))
 (1 1 (:TYPE-PRESCRIPTION MEM))
 (1 1 (:REWRITE DEL-SET-LEN))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(JVM::WFF-STATE-IMPLIES-INTEGERP-PC)
(JVM::LOADER-INV-EQUAL
 (23721 4 (:DEFINITION JVM::LOADER-INV-HELPER1))
 (23672 6 (:DEFINITION JVM::ALL-CORRECTLY-LOADED?))
 (23247 7 (:REWRITE JVM::INV-AND-ISASSIGNABLETO-ENV))
 (16985 4 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-IMPLIES-ALL-CORRECTLY-LOADED?))
 (15018 110 (:DEFINITION JVM::PRIMITIVE-TYPE?))
 (12714 20 (:DEFINITION JVM::WFF-STATIC-CP-OK-S))
 (12244 20 (:DEFINITION JVM::WFF-STATIC-CP-ENTRY-OK-S))
 (12046 20 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARDS))
 (11764 20 (:DEFINITION JVM::RUNTIME-METHOD-REP-GUARD))
 (9320 3400 (:DEFINITION NTH))
 (8655 50 (:DEFINITION JVM::WFF-TYPE-REP))
 (6842 6 (:REWRITE JVM::LOADER-INV-HELPER1-CORRECT-LOADED?))
 (6838 2 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-APP))
 (5893 5879 (:REWRITE DEFAULT-CDR))
 (5584 20 (:DEFINITION JVM::VALUE-TYPE-OK))
 (5540 5530 (:REWRITE DEFAULT-CAR))
 (3854 20 (:DEFINITION JVM::WFF-TYPE-REPS))
 (2784 20 (:DEFINITION JVM::VALUE-TYPE-OK-2))
 (2545 509 (:DEFINITION LEN))
 (2258 2258 (:TYPE-PRESCRIPTION LEN))
 (2228 240 (:DEFINITION JVM::ARRAY-TYPE?))
 (2151 2151 (:REWRITE MEM-SUBSET))
 (1871 10 (:DEFINITION JVM::WFF-FIELDS-S))
 (1760 20 (:DEFINITION JVM::NORMALIZE-TYPE-REP))
 (1440 360 (:REWRITE ZP-OPEN))
 (1424 40 (:DEFINITION JVM::WFF-CODE-S))
 (1378 869 (:REWRITE DEFAULT-+-2))
 (1214 20 (:DEFINITION JVM::WFF-CONSTANT-POOL-S))
 (1092 20 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY-S))
 (956 20 (:DEFINITION JVM::WFF-METHOD-DECL-S))
 (919 260 (:DEFINITION TRUE-LISTP))
 (869 869 (:REWRITE DEFAULT-+-1))
 (780 760 (:REWRITE DEFAULT-<-2))
 (760 760 (:REWRITE DEFAULT-<-1))
 (652 652 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (650 130 (:DEFINITION INT32P))
 (642 30 (:DEFINITION JVM::WFF-FIELD-S))
 (607 10 (:DEFINITION JVM::WFF-CONSTANT-POOL))
 (570 190 (:DEFINITION JVM::FIELD-FIELDTYPE-S))
 (550 20 (:DEFINITION JVM::WFF-FIELDS-S-X))
 (546 10 (:DEFINITION JVM::WFF-CONSTANT-POOL-ENTRY))
 (539 10 (:DEFINITION JVM::WFF-CLASS-METHOD-DECLS))
 (532 532 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (509 509 (:REWRITE DEL-SET-LEN))
 (478 10 (:DEFINITION JVM::WFF-METHOD-DECL))
 (428 20 (:DEFINITION JVM::REFERENCE-TYPE))
 (360 120 (:DEFINITION JVM::METHOD-CODE-S))
 (360 120 (:DEFINITION JVM::FIELD-CPINDEX-S))
 (320 80 (:DEFINITION JVM::METHOD-ACCESSFLAGS-S))
 (317 10 (:DEFINITION JVM::ALL-FIELDS-STATIC-FINAL))
 (300 20 (:DEFINITION JVM::WFF-LONG-CP-ENTRY-S))
 (300 20 (:DEFINITION JVM::WFF-INT-CP-ENTRY-S))
 (275 10 (:DEFINITION JVM::WFF-STATIC-FIELDS-X))
 (275 10 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (250 50 (:DEFINITION INT64P))
 (214 10 (:DEFINITION JVM::WFF-STATIC-FIELD))
 (214 10 (:DEFINITION JVM::WFF-FIELD))
 (210 210 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REP))
 (210 70 (:DEFINITION JVM::ARRAY-BASE-TYPE))
 (200 20 (:DEFINITION JVM::WFF-STRING-CP-ENTRY-S))
 (200 20 (:DEFINITION JVM::STATIC-FIELD?-S))
 (190 10 (:DEFINITION NODUP-SET))
 (186 7 (:REWRITE JVM::LOADED-LORDER-INV-HELPER-IMPLIES-CORRECTLY-LOADED?))
 (172 7 (:DEFINITION JVM::CLASS-LOADED?))
 (160 40 (:DEFINITION JVM::METHOD-RETURNTYPE-S))
 (160 40 (:DEFINITION JVM::FIELD-FIELDACCESSFLAGS-S))
 (160 40 (:DEFINITION JVM::CODE-MAX-STACK-S))
 (160 40 (:DEFINITION JVM::CODE-MAX-LOCAL-S))
 (153 9 (:DEFINITION JVM::ISCLASSTERM))
 (150 10 (:DEFINITION JVM::WFF-LONG-CP-ENTRY))
 (150 10 (:DEFINITION JVM::WFF-INT-CP-ENTRY))
 (120 20 (:DEFINITION SHORTP))
 (120 20 (:DEFINITION JVMBOOLEANP))
 (120 20 (:DEFINITION CHARP))
 (120 20 (:DEFINITION BYTEP))
 (100 10 (:DEFINITION JVM::WFF-STRING-CP-ENTRY))
 (96 96 (:TYPE-PRESCRIPTION JVM::WFF-TYPE-REPS))
 (80 20 (:DEFINITION JVM::METHOD-ARGS-S))
 (62 12 (:DEFINITION JVM::CLASS-BY-NAME))
 (60 20 (:DEFINITION JVM::CPENTRY-VALUE-S))
 (60 10 (:DEFINITION JVM::COLLECT-STATIC-FIELD-NAMES))
 (50 2 (:REWRITE JVM::CLASS-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (41 41 (:TYPE-PRESCRIPTION JVM::COLLECT-STATIC-FIELD-NAMES))
 (40 20 (:DEFINITION JVM::CPENTRY-TYPE-S))
 (32 32 (:TYPE-PRESCRIPTION JVM::COLLECT-ASSIGNABLETONAME))
 (30 10 (:DEFINITION JVM::FIELD-FIELDNAME-S))
 (28 28 (:TYPE-PRESCRIPTION JVM::ALL-CORRECTLY-LOADED?))
 (24 4 (:DEFINITION APP))
 (21 21 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (20 20 (:DEFINITION JVM::MAKE-ARRAY-TYPE))
 (20 20 (:DEFINITION JVMFLOATP))
 (20 20 (:DEFINITION DOUBLEP))
 (18 2 (:DEFINITION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (16 4 (:DEFINITION MV-NTH))
 (16 4 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (14 14 (:REWRITE JVM::ALL-CORRECTLY-LOADED?-SUBSET))
 (13 13 (:TYPE-PRESCRIPTION JVM::CORRECTLY-LOADED?))
 (12 6 (:TYPE-PRESCRIPTION APP))
 (9 9 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (8 8 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (8 2 (:REWRITE JVM::LOADER-INV-HELPER-CORRECT-LOADED?-IMPLIES-LOADER-INV-HELPER1))
 (8 2 (:REWRITE JVM::LOADER-INV-HELPER-AND-LOADED-IMPLIES-CORRECTLY-LOADED?-2))
 (7 7 (:TYPE-PRESCRIPTION JVM::CLASS-LOADED?))
 (7 7 (:REWRITE JVM::MEM-ALL-CORRECTLY-LOADED?-IMPLIES))
 (7 7 (:REWRITE JVM::LOADER-INV-HELPER1-IMPLIES-MEM))
 (6 6 (:TYPE-PRESCRIPTION JVM::LOADER-INV-HELPER1))
 (6 6 (:TYPE-PRESCRIPTION JVM::COLLECT-ALL-ASSIGNABLETONAME))
 (2 2 (:TYPE-PRESCRIPTION JVM::ISCLASSTERM))
 (2 2 (:REWRITE JVM::CORRECTLY-LOADED?-IMPLIES-CLASSNAME-CLASS-BY-NAME))
 (2 2 (:REWRITE JVM::CORRECTLY-LOADED?-CLASSNAME-CLASS-BY-NAME))
 (1 1 (:REWRITE CDR-CONS))
 (1 1 (:REWRITE CAR-CONS))
 )
(JVM::LOAD_CP_ENTRY_GUARD_PRESERVED_BY_LOAD_CLASS
 (947 22 (:DEFINITION JVM::LOAD_CLASS_X))
 (895 179 (:DEFINITION JVM::CLASS-BY-NAME))
 (888 16 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIED-BY))
 (832 8 (:DEFINITION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (618 606 (:REWRITE DEFAULT-CDR))
 (580 546 (:REWRITE DEFAULT-CAR))
 (358 358 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (330 165 (:REWRITE DEFAULT-+-2))
 (256 8 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (208 8 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (208 8 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (200 8 (:DEFINITION JVM::WFF-FIELD))
 (192 8 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (192 8 (:DEFINITION JVM::CLASS-EXISTS?))
 (165 165 (:REWRITE DEFAULT-+-1))
 (160 160 (:REWRITE DEL-SET-LEN))
 (150 22 (:DEFINITION JVM::FATALERROR))
 (136 34 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (128 22 (:DEFINITION JVM::M6-INTERNAL-ERROR))
 (120 6 (:REWRITE JVM::ONCE-LOADED-SUPERCHAIN-DOES-NOT-CHANGE))
 (118 118 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (118 38 (:DEFINITION NTH))
 (106 22 (:DEFINITION JVM::STATE-SET-ERROR-FLAG))
 (92 92 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (68 22 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (40 8 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE-B))
 (40 8 (:DEFINITION TRUE-LISTP))
 (32 32 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (32 32 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (32 32 (:REWRITE JVM::ALL-CORRECTLY-LOADED-IMPLIES-COLLECT-SUPERCLASS-LIST))
 (32 8 (:DEFINITION JVM::FIELDS))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (22 22 (:REWRITE MEM-SUBSET))
 (22 22 (:DEFINITION MEM))
 (16 16 (:TYPE-PRESCRIPTION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (12 6 (:REWRITE JVM::WFF-STATE-EQUIV-STATE-INSTANCE-CLASS-TABLE))
 (8 8 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (8 8 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 (6 6 (:TYPE-PRESCRIPTION JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE))
 )
(JVM::LOAD_CP_ENTRIES_GUARD_PRESERVED_BY_LOAD_CLASS
 (15 15 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (4 4 (:REWRITE DEFAULT-CDR))
 )
(JVM::LOAD_CP_ENTRY_GUARD_PRESERVED_BY_LOAD_CLASS_X_MODE_3
 (522 12 (:DEFINITION JVM::LOAD_CLASS_X))
 (475 95 (:DEFINITION JVM::CLASS-BY-NAME))
 (444 8 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIED-BY))
 (416 4 (:DEFINITION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (380 368 (:REWRITE DEFAULT-CDR))
 (370 346 (:REWRITE DEFAULT-CAR))
 (216 108 (:REWRITE DEFAULT-+-2))
 (190 190 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (156 6 (:DEFINITION JVM::COLLECT-SUPERCLASS-LIST1))
 (128 4 (:DEFINITION JVM::WFF-CLASS-FIELDS))
 (108 108 (:REWRITE DEFAULT-+-1))
 (105 105 (:REWRITE DEL-SET-LEN))
 (104 4 (:REWRITE JVM::WFF-CLASS-REP-IF-EXISTS-IN-WFF-INSTANCE-TABLE))
 (104 4 (:REWRITE JVM::LOADED-FROM-WFF-IMPLIES-WFF))
 (100 4 (:DEFINITION JVM::WFF-FIELD))
 (96 24 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (96 4 (:DEFINITION JVM::CLASS-IS-LOADED?))
 (96 4 (:DEFINITION JVM::CLASS-EXISTS?))
 (72 24 (:DEFINITION JVM::FATALERROR))
 (58 58 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (50 50 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (48 24 (:DEFINITION JVM::M6-INTERNAL-ERROR))
 (48 12 (:DEFINITION MEM))
 (42 4 (:REWRITE JVM::ONCE-LOADED-SUPERCHAIN-DOES-NOT-CHANGE))
 (28 14 (:DEFINITION NTH))
 (24 24 (:REWRITE MEM-SUBSET))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:DEFINITION JVM::STATE-SET-ERROR-FLAG))
 (24 12 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (24 6 (:DEFINITION JVM::CLASSSUPERCLASSNAME))
 (20 4 (:REWRITE JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-IMPLIES-ALTERNATIVE-B))
 (20 4 (:DEFINITION TRUE-LISTP))
 (18 6 (:DEFINITION JVM::SUPER))
 (16 16 (:TYPE-PRESCRIPTION JVM::WFF-CLASS-FIELDS))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (16 4 (:DEFINITION JVM::FIELDS))
 (12 12 (:TYPE-PRESCRIPTION MEM))
 (12 12 (:REWRITE JVM::ALL-CORRECTLY-LOADED-IMPLIES-COLLECT-SUPERCLASS-LIST))
 (10 6 (:REWRITE JVM::WFF-STATE-EQUIV-STATE-INSTANCE-CLASS-TABLE))
 (8 8 (:TYPE-PRESCRIPTION JVM::BUILD-IMMEDIATE-INSTANCE-DATA-GUARD-ALTERNATIVE))
 (4 4 (:TYPE-PRESCRIPTION JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE))
 (4 4 (:TYPE-PRESCRIPTION JVM::CLASS-IS-LOADED?))
 (4 4 (:TYPE-PRESCRIPTION JVM::CLASS-EXISTS?))
 )
(JVM::LOAD_CP_ENTRY_GUARD_PRESERVED_BY_LOAD_CLASS_X_MODE_2
 (430 412 (:REWRITE DEFAULT-CAR))
 (412 373 (:REWRITE DEFAULT-CDR))
 (405 15 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (372 78 (:DEFINITION MV-NTH))
 (348 87 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (345 15 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (315 15 (:REWRITE JVM::CLASS-LOADED-LOAD_CLASS_X_3))
 (300 30 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (210 42 (:DEFINITION JVM::CLASS-BY-NAME))
 (210 12 (:DEFINITION SUBSET))
 (183 183 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (132 66 (:REWRITE DEFAULT-+-2))
 (84 84 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (66 66 (:REWRITE DEFAULT-+-1))
 (65 65 (:REWRITE DEL-SET-LEN))
 (63 63 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (60 15 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (52 52 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (33 33 (:REWRITE SUBSET-TRANSITIVE))
 (18 9 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (15 15 (:REWRITE SET-EQUAL-CONS))
 (9 9 (:REWRITE JVM::ENV-DOES-NOT-CHANGE-LOAD_CLASS_X))
 (9 9 (:REWRITE CDR-CONS))
 (9 9 (:REWRITE CAR-CONS))
 (8 4 (:REWRITE JVM::WFF-STATE-EQUIV-STATE-INSTANCE-CLASS-TABLE))
 (4 4 (:TYPE-PRESCRIPTION JVM::EQUIV-STATE-INSTANCE-CLASS-TABLE))
 )
(JVM::MODE-0-LOADED-INDUCT
 (3 3 (:TYPE-PRESCRIPTION JVM::LOAD_CLASS_X))
 )
(JVM::LOAD_CP_ENTRY_GUARD_PRESERVED_BY_LOAD_CLASS_X_MODE_0
 (1655 331 (:DEFINITION JVM::CLASS-BY-NAME))
 (1201 1147 (:REWRITE DEFAULT-CAR))
 (966 966 (:REWRITE DEFAULT-CDR))
 (662 662 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (477 27 (:REWRITE JVM::CLASS-LOADED?-IS-PERSERVED-BY-LOAD_CLASS_X))
 (424 212 (:REWRITE DEFAULT-+-2))
 (400 400 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (236 236 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (216 216 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (216 54 (:DEFINITION MV-NTH))
 (216 54 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (212 212 (:REWRITE DEL-SET-LEN))
 (212 212 (:REWRITE DEFAULT-+-1))
 (54 54 (:DEFINITION JVM::EXTERNAL-CLASS-TABLE))
 (3 3 (:REWRITE SUBSET-TRANSITIVE))
 )
(JVM::LOAD_CP_ENTRY_GUARD_PRESERVED_BY_LOAD_CLASS_X_MODE_1
 (135 135 (:REWRITE DEFAULT-CAR))
 (135 5 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (124 114 (:REWRITE DEFAULT-CDR))
 (115 5 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (110 22 (:DEFINITION JVM::CLASS-BY-NAME))
 (100 10 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (80 20 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (78 3 (:REWRITE JVM::LOAD_CLASS_DOES_NOT_CHANGE_LOADED_CLASS))
 (78 3 (:REWRITE JVM::CLASS-LOADED-LOAD_CLASS_X_3))
 (70 20 (:DEFINITION MV-NTH))
 (70 4 (:DEFINITION SUBSET))
 (44 44 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (40 40 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (26 26 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (26 13 (:REWRITE DEFAULT-+-2))
 (20 5 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (18 18 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (13 13 (:REWRITE DEL-SET-LEN))
 (13 13 (:REWRITE DEFAULT-+-1))
 (11 11 (:REWRITE SUBSET-TRANSITIVE))
 (9 9 (:REWRITE JVM::LOAD_CLASS_X_ONLY_CHANGE_CLASS_TABLE_ERROR_FLAG_HEAP))
 (6 6 (:TYPE-PRESCRIPTION JVM::ISINTERFACE))
 (6 6 (:REWRITE JVM::ENV-DOES-NOT-CHANGE-LOAD_CLASS_X))
 (6 3 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (5 5 (:REWRITE SET-EQUAL-CONS))
 (3 3 (:REWRITE CDR-CONS))
 (3 3 (:REWRITE CAR-CONS))
 )
(JVM::LOAD_CP_ENTRY_GUARD_PRESERVED_BY_LOAD_CLASS_X
 (627 27 (:REWRITE JVM::CLASS-LOADED-LOAD_CLASS_X_3))
 (601 592 (:REWRITE DEFAULT-CAR))
 (589 571 (:REWRITE DEFAULT-CDR))
 (555 111 (:DEFINITION JVM::CLASS-BY-NAME))
 (486 18 (:DEFINITION JVM::ALL-CLASS-NAMES-S))
 (477 9 (:DEFINITION JVM::LOAD_CLASS_2-INV))
 (477 9 (:DEFINITION JVM::LOAD_CLASS_1-INV))
 (450 72 (:DEFINITION MEM))
 (414 18 (:REWRITE SET-EQUAL-MEM-CONS-2))
 (360 36 (:REWRITE JVM::FOUND-IMPLIES-MEM))
 (306 153 (:REWRITE DEFAULT-+-2))
 (252 63 (:DEFINITION JVM::CLASS-BY-NAME-S))
 (234 9 (:REWRITE JVM::LOAD_CLASS_DOES_NOT_CHANGE_LOADED_CLASS))
 (225 63 (:DEFINITION JVM::FATALERROR))
 (222 222 (:REWRITE JVM::NOT-FOUND-IN-ENV-CL-NOT-CLASS-TERM))
 (216 63 (:DEFINITION MV-NTH))
 (162 162 (:TYPE-PRESCRIPTION MEM))
 (162 63 (:DEFINITION JVM::M6-INTERNAL-ERROR))
 (153 153 (:REWRITE DEFAULT-+-1))
 (152 152 (:LINEAR SUBSET-NODUP-SET-SIZE))
 (148 148 (:REWRITE DEL-SET-LEN))
 (144 144 (:TYPE-PRESCRIPTION JVM::CLASS-BY-NAME-S))
 (144 144 (:REWRITE MEM-SUBSET))
 (108 108 (:TYPE-PRESCRIPTION JVM::ALL-CLASS-NAMES-S))
 (99 99 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (99 63 (:DEFINITION JVM::STATE-SET-ERROR-FLAG))
 (72 18 (:REWRITE JVM::NO-FATAL-ERROR?-LOAD_CLASS2-IMPLIES-FOUND))
 (40 40 (:REWRITE DEFAULT-<-2))
 (40 40 (:REWRITE DEFAULT-<-1))
 (36 18 (:DEFINITION JVM::TRIVIAL-INV-ENV-DO-NOT-CHANGE))
 (27 27 (:REWRITE JVM::LOAD_CLASS_X_ONLY_CHANGE_CLASS_TABLE_ERROR_FLAG_HEAP))
 (27 27 (:REWRITE JVM::ENV-DOES-NOT-CHANGE-LOAD_CLASS_X))
 (27 27 (:DEFINITION JVM::EXTERNAL-CLASS-TABLE))
 (18 18 (:TYPE-PRESCRIPTION JVM::ISINTERFACE))
 (18 18 (:REWRITE SET-EQUAL-CONS))
 (10 10 (:REWRITE JVM::WFF-STATE-EQUIV-STATE-INSTANCE-CLASS-TABLE))
 )
(JVM::LOAD_CP_ENTRIES_GUARD_PRESERVED_BY_LOAD_CLASS_X
 (15 15 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
 (4 4 (:REWRITE DEFAULT-CDR))
 )