/usr/share/acl2-6.3/books/hints/basic-tests.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)))) (VALUE-TRIPLE (QUOTE T))) (6 RECORD-EXPANSION (MUST-SUCCEED (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/3'5'" :EXPAND ((NTH U V)))))) (VALUE-TRIPLE (QUOTE T))) (8 RECORD-EXPANSION (MUST-SUCCEED (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/3'5'" :EXPAND ((NTH U V)))))) (VALUE-TRIPLE (QUOTE T))) (10 RECORD-EXPANSION (MUST-SUCCEED (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/3'5'" :EXPAND ((NTH U V)))))) (VALUE-TRIPLE (QUOTE T))) (11 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)))) (VALUE-TRIPLE (QUOTE T))) (13 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)))) (VALUE-TRIPLE (QUOTE T))) (16 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/2" :IN-THEORY (DISABLE REV)) ("Subgoal *1/1" :IN-THEORY (DISABLE REV)) ("Subgoal *1/1'" :IN-THEORY (DISABLE TRUE-LISTP REV (REV)))))) (VALUE-TRIPLE (QUOTE T))) (18 RECORD-EXPANSION (MUST-SUCCEED (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/2" :IN-THEORY (DISABLE REV)) ("Subgoal *1/1" :IN-THEORY (DISABLE REV)) ("Subgoal *1/1'" :IN-THEORY (DISABLE TRUE-LISTP REV (REV)))))) (VALUE-TRIPLE (QUOTE T))) (19 RECORD-EXPANSION (MUST-SUCCEED (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Goal" :IN-THEORY (DISABLE REV))))) (VALUE-TRIPLE (QUOTE T))) (20 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Goal" :IN-THEORY (DISABLE REV)) (QUOTE (:HANDS-OFF REV))))) (VALUE-TRIPLE (QUOTE T))) (22 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Goal" :IN-THEORY (DISABLE REV)) (AND (EQUAL ID *INITIAL-CLAUSE-ID*) (QUOTE (:HANDS-OFF REV)))))) (VALUE-TRIPLE (QUOTE T))) (23 RECORD-EXPANSION (MUST-SUCCEED (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/3'" :IN-THEORY (DISABLE REV)) (AND (EQUAL ID (PARSE-CLAUSE-ID "Subgoal *1/3'")) (QUOTE (:HANDS-OFF REV)))))) (VALUE-TRIPLE (QUOTE T))) (26 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/3'" :IN-THEORY (DISABLE REV))))) (VALUE-TRIPLE (QUOTE T))) (27 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS ((AND (EQUAL ID (PARSE-CLAUSE-ID "Subgoal *1/3'")) (QUOTE (:HANDS-OFF REV)))))) (VALUE-TRIPLE (QUOTE T))) (29 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)))) (VALUE-TRIPLE (QUOTE T))) (31 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)))) (VALUE-TRIPLE (QUOTE T))) (32 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)) :HINTS (("Subgoal *1.1/2" :IN-THEORY (ENABLE CAR-CONS))))) (VALUE-TRIPLE (QUOTE T))) (33 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST))) :AT-END NIL) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X))))) (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST))) :AT-END NIL) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)))) (VALUE-TRIPLE (QUOTE T))))) (34 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST)))) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X))))) (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST)))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)))) (VALUE-TRIPLE (QUOTE T))))) (36 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST))) :AT-END T) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X))))) (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST))) :AT-END T) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)))) (VALUE-TRIPLE (QUOTE T))))) (37 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS! (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST))) :AT-END T) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X))))) (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS! (QUOTE ((IF (EQUAL (PARSE-CLAUSE-ID "Subgoal *1.1/2") ID) (LIST* :IN-THEORY (QUOTE (ENABLE CAR-CONS)) KEYWORD-ALIST) KEYWORD-ALIST))) :AT-END T) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X X) X) (APPEND X X X)))) (VALUE-TRIPLE (QUOTE T))))) (41 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((REMOVE-KEYWORD :EXPAND KEYWORD-ALIST)))) (MUST-SUCCEED (THM (EQUAL X X) :HINTS ((QUOTE (:COMPUTED-HINT-REPLACEMENT T :EXPAND ((NTH U V)))))))) (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((REMOVE-KEYWORD :EXPAND KEYWORD-ALIST)))) (RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL X X) :HINTS ((QUOTE (:COMPUTED-HINT-REPLACEMENT T :EXPAND ((NTH U V))))))) (VALUE-TRIPLE (QUOTE T))))) (45 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (REV0 (APP A B)) (APP (REV0 B) (REV0 A))))) (VALUE-TRIPLE (QUOTE T))) (49 RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL (REV0 (APP A B)) (APP (REV0 B) (REV0 A))))) (VALUE-TRIPLE (QUOTE T))) (51 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (REV0 (APP A B)) (APP (REV0 B) (REV0 A))))) (VALUE-TRIPLE (QUOTE T))) (54 RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL (REV0 (APP A B)) (APP (REV0 B) (REV0 A))) :HINTS (("Subgoal *1/2'" :IN-THEORY (ENABLE NTH))))) (VALUE-TRIPLE (QUOTE T))) (57 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (REV0 (APP A B)) (APP (REV0 B) (REV0 A))) :HINTS (("Subgoal *1/2'" :EXPAND ((NTH Y Z)))))) (VALUE-TRIPLE (QUOTE T))) (61 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)))) (VALUE-TRIPLE (QUOTE T))) (62 RECORD-EXPANSION (MUST-FAIL (THM (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X)) :HINTS (("Subgoal *1/3'5'" :EXPAND ((NTH U V)))))) (VALUE-TRIPLE (QUOTE T))) (63 RECORD-EXPANSION (ENCAPSULATE NIL (SET-DEFAULT-HINTS (QUOTE ((AND (EQ PROCESSOR (QUOTE GENERALIZE-CLAUSE)) (QUOTE (:IN-THEORY (DISABLE APPEND))))))) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))))) (ENCAPSULATE NIL (SET-DEFAULT-HINTS (QUOTE ((AND (EQ PROCESSOR (QUOTE GENERALIZE-CLAUSE)) (QUOTE (:IN-THEORY (DISABLE APPEND))))))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)))) (VALUE-TRIPLE (QUOTE T))))) (64 RECORD-EXPANSION (ENCAPSULATE NIL (SET-DEFAULT-HINTS (QUOTE ((AND (EQ PROCESSOR (QUOTE GENERALIZE-CLAUSE)) (NULL CLAUSE-LIST) KEYWORD-ALIST (QUOTE (:IN-THEORY (DISABLE APPEND))))))) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))))) (ENCAPSULATE NIL (SET-DEFAULT-HINTS (QUOTE ((AND (EQ PROCESSOR (QUOTE GENERALIZE-CLAUSE)) (NULL CLAUSE-LIST) KEYWORD-ALIST (QUOTE (:IN-THEORY (DISABLE APPEND))))))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)))) (VALUE-TRIPLE (QUOTE T))))) (65 RECORD-EXPANSION (ENCAPSULATE NIL (SET-DEFAULT-HINTS (QUOTE ((AND (EQ PROCESSOR (QUOTE GENERALIZE-CLAUSE)) (NULL CLAUSE-LIST) KEYWORD-ALIST FOO (QUOTE (:IN-THEORY (DISABLE APPEND))))))) (MUST-FAIL (THM (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))))) (ENCAPSULATE NIL (SET-DEFAULT-HINTS (QUOTE ((AND (EQ PROCESSOR (QUOTE GENERALIZE-CLAUSE)) (NULL CLAUSE-LIST) KEYWORD-ALIST FOO (QUOTE (:IN-THEORY (DISABLE APPEND))))))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)))) (VALUE-TRIPLE (QUOTE T))))) (69 RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y)))) (VALUE-TRIPLE (QUOTE T))) (70 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-DEFAULT-HINTS (QUOTE ((QUOTE (:NO-THANKS T))))) (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y))))) (ENCAPSULATE NIL (ADD-DEFAULT-HINTS (QUOTE ((QUOTE (:NO-THANKS T))))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y)))) (VALUE-TRIPLE (QUOTE T))))) (71 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-DEFAULT-HINTS (QUOTE ((QUOTE (:COMPUTED-HINT-REPLACEMENT T :NO-THANKS T))))) (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y))))) (ENCAPSULATE NIL (ADD-DEFAULT-HINTS (QUOTE ((QUOTE (:COMPUTED-HINT-REPLACEMENT T :NO-THANKS T))))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y)))) (VALUE-TRIPLE (QUOTE T))))) (72 RECORD-EXPANSION (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((COND ((OR (NULL KEYWORD-ALIST) (ASSOC-KEYWORD :NO-THANKS KEYWORD-ALIST)) KEYWORD-ALIST) (T (APPEND (QUOTE (:NO-THANKS T)) KEYWORD-ALIST)))))) (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y))))) (ENCAPSULATE NIL (ADD-OVERRIDE-HINTS (QUOTE ((COND ((OR (NULL KEYWORD-ALIST) (ASSOC-KEYWORD :NO-THANKS KEYWORD-ALIST)) KEYWORD-ALIST) (T (APPEND (QUOTE (:NO-THANKS T)) KEYWORD-ALIST)))))) (RECORD-EXPANSION (MUST-FAIL (THM (EQUAL (APPEND X Y X) (APPEND Y X Y)))) (VALUE-TRIPLE (QUOTE T))))) (75 RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:EXPAND ((NTH U V)))))))) (VALUE-TRIPLE (QUOTE T))) (76 RECORD-EXPANSION (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE APPEND))) (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:IN-THEORY (ENABLE APPEND)))))))) (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE APPEND))) (RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:IN-THEORY (ENABLE APPEND))))))) (VALUE-TRIPLE (QUOTE T))))) (77 RECORD-EXPANSION (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE APPEND))) (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:COMPUTED-HINT-REPLACEMENT T :IN-THEORY (ENABLE APPEND)))))))) (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE APPEND))) (RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:COMPUTED-HINT-REPLACEMENT T :IN-THEORY (ENABLE APPEND))))))) (VALUE-TRIPLE (QUOTE T))))) (78 RECORD-EXPANSION (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE APPEND))) (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:COMPUTED-HINT-REPLACEMENT ((QUOTE (:IN-THEORY (ENABLE APPEND)))) :NO-OP T))))))) (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE APPEND))) (RECORD-EXPANSION (MUST-SUCCEED (THM (EQUAL (CAR (APPEND X Y)) (IF (CONSP X) (CAR X) (CAR Y))) :HINTS (("Goal" :BACKTRACK (QUOTE (:COMPUTED-HINT-REPLACEMENT ((QUOTE (:IN-THEORY (ENABLE APPEND)))) :NO-OP T)))))) (VALUE-TRIPLE (QUOTE T))))) (88 RECORD-EXPANSION (NOT-THM? (PROPERTY (GGG AAA)) :HINTS (("Goal" :USE (:INSTANCE (:FUNCTIONAL-INSTANCE PROPERTY-FFF (FFF GGG)) (X BBB)) :CASES ((PPP 1) (PPP 2) (PPP 3)))) :OTF-FLG T) (VALUE-TRIPLE (QUOTE T))) (89 RECORD-EXPANSION (THM? (PROPERTY (GGG AAA)) :HINTS (("Goal" :USE ((:INSTANCE (:FUNCTIONAL-INSTANCE PROPERTY-FFF (FFF GGG)) (X AAA)) (:INSTANCE CONSTRP-GGG (X X))) :CASES ((PPP 1) (PPP 2) (PPP 3))) ("Goal'" :USE ((:INSTANCE CONSTRP-GGG (X X)))))) (VALUE-TRIPLE (QUOTE T))) (96 RECORD-EXPANSION (NOT-THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:USE (:INSTANCE BAR (X DISJ-CASE-1)) :DO-NOT (QUOTE (GENERALIZE))) (:USE (:INSTANCE BAR (X DISJ-CASE-2)) :DO-NOT (QUOTE (FERTILIZE)))))) :OTF-FLG T) (VALUE-TRIPLE (QUOTE T))) (97 RECORD-EXPANSION (NOT-THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:USE (:INSTANCE BAR (X DISJ-CASE-1)) :DO-NOT (QUOTE (GENERALIZE))) (:USE (:INSTANCE BAR (X DISJ-CASE-2)) :DO-NOT (QUOTE (FERTILIZE)))))) :OTF-FLG NIL) (VALUE-TRIPLE (QUOTE T))) (98 RECORD-EXPANSION (THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:IN-THEORY (ENABLE AAA) :USE (:INSTANCE BAR (X CCC))) (:IN-THEORY (ENABLE BBB) :USE (:INSTANCE MUM (X DDD))))))) (VALUE-TRIPLE (QUOTE T))) (99 RECORD-EXPANSION (THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:IN-THEORY (ENABLE AAA) :USE (:INSTANCE BAR (X DDD))) (:IN-THEORY (ENABLE BBB) :USE (:INSTANCE MUM (X CCC))))))) (VALUE-TRIPLE (QUOTE T))) (100 RECORD-EXPANSION (NOT-THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:IN-THEORY (ENABLE AAA) :USE (:INSTANCE BAR (X DDD))) (:IN-THEORY (ENABLE BBB) :USE (:INSTANCE MUM (X DDD))))))) (VALUE-TRIPLE (QUOTE T))) (101 RECORD-EXPANSION (THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:USE (:INSTANCE BAR (X CCC))) (:IN-THEORY (ENABLE BBB) :USE (:INSTANCE MUM (X DDD))))))) (VALUE-TRIPLE (QUOTE T))) (102 RECORD-EXPANSION (NOT-THM? (PROPERTY CCC) :HINTS (("Goal" :OR ((:INDUCT (APPEND CCC X)) (:IN-THEORY (ENABLE BBB) :USE (:INSTANCE MUM (X DDD))))))) (VALUE-TRIPLE (QUOTE T))) (104 RECORD-EXPANSION (NOT-THM? (EQUAL X Y) :HINTS (("Goal" :IN-THEORY (DISABLE CAR-CONS) :SYN-USE CAR-CONS :DO-NOT (QUOTE (GENERALIZE))) ("Goal'" :IN-THEORY (ENABLE CAR-CONS)))) (VALUE-TRIPLE (QUOTE T))) (105 RECORD-EXPANSION (NOT-THM? (EQUAL X Y) :HINTS (("Goal" :IN-THEORY (DISABLE CAR-CONS) :SYN-USE CAR-CONS :DO-NOT (QUOTE (GENERALIZED))) ("Goal'" :IN-THEORY (ENABLE CAR-CONS)))) (VALUE-TRIPLE (QUOTE T))) (108 RECORD-EXPANSION (NOT-THM? (EQUAL X Y) :HINTS (("Goal" :IN-THEORY (DISABLE CAR-CONS) :SYN-USE CAR-CONS :DO-NOT (QUOTE (GENERALIZE))) ("Goal'" :IN-THEORY (ENABLE CAR-CONS)))) (VALUE-TRIPLE (QUOTE T))) (109 RECORD-EXPANSION (NOT-THM? (EQUAL X Y) :HINTS (("Goal" :IN-THEORY (DISABLE CAR-CONS) :SYN-USE CDR-CONS :DO-NOT (QUOTE (GENERALIZED))) ("Goal'" :IN-THEORY (ENABLE CAR-CONS)))) (VALUE-TRIPLE (QUOTE T))) (111 RECORD-EXPANSION (NOT-THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :EROR (A B C)))) (VALUE-TRIPLE (QUOTE T))) (114 RECORD-EXPANSION (NOT-THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :EROR (A B C)))) (VALUE-TRIPLE (QUOTE T))) (117 RECORD-EXPANSION (THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :IN-THEORY (DISABLE CAR-CONS) :SYN-USE CAR-CONS :DO-NOT (QUOTE (GENERALIZE))))) (VALUE-TRIPLE (QUOTE T))) (119 RECORD-EXPANSION (THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :COUNT-DOWN 7))) (VALUE-TRIPLE (QUOTE T))) (120 RECORD-EXPANSION (THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :COUNT-DOWN 2))) (VALUE-TRIPLE (QUOTE T))) (122 RECORD-EXPANSION (NOT-THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :COUNT-DOWN 2))) (VALUE-TRIPLE (QUOTE T))) (124 RECORD-EXPANSION (NOT-THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :COUNT-DOWN T))) (VALUE-TRIPLE (QUOTE T))) (125 RECORD-EXPANSION (THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :COUNT-DOWN 7))) (VALUE-TRIPLE (QUOTE T))) (126 RECORD-EXPANSION (THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/1'" :COUNT-DOWN 2))) (VALUE-TRIPLE (QUOTE T))) (128 RECORD-EXPANSION (THM? (EQUAL (APPEND (APPEND A B) C) (APPEND A (APPEND B C))) :HINTS (("Subgoal *1/2" :IN-THEORY (DISABLE CDR-CONS CONS-CAR-CDR CAR-CDR-ELIM)) ("Subgoal *1/2'" :NO-OP T :RECURSE T) ("Subgoal *1/2''" :IN-THEORY (DISABLE CDR-CONS CONS-CAR-CDR)) ("Subgoal *1/2'4'" :IN-THEORY (ENABLE CDR-CONS)))) (VALUE-TRIPLE (QUOTE T))) (132 RECORD-EXPANSION (ENCAPSULATE NIL (LOCAL (DEFUN NONLINEARP-DEFAULT-HINT (STABLE-UNDER-SIMPLIFICATIONP HIST PSPV) (DECLARE (XARGS :GUARD (AND (CONSP PSPV) (CONSP (CAR PSPV)) (CONSP (CAR (CAR PSPV))) (CONSP (CDR (CAR (CAR PSPV)))) (CONSP (CDR (CDR (CAR (CAR PSPV))))) (CONSP (CDR (CDR (CDR (CAR (CAR PSPV)))))) (CONSP (CDR (CDR (CDR (CDR (CAR (CAR PSPV))))))) (CONSP (CDR (CDR (CDR (CDR (CDR (CAR (CAR PSPV)))))))) (CONSP (CDR (CDR (CDR (CDR (CDR (CDR (CAR (CAR PSPV))))))))) (CONSP (CAR (CDR (CDR (CDR (CDR (CDR (CDR (CAR (CAR PSPV))))))))))))) (COND (STABLE-UNDER-SIMPLIFICATIONP (IF (NOT (ACCESS REWRITE-CONSTANT (ACCESS PROVE-SPEC-VAR PSPV :REWRITE-CONSTANT) :NONLINEARP)) (PROG2$ (CW "~%~%[Note: We now enable non-linear arithmetic.]~%~%") (QUOTE (:COMPUTED-HINT-REPLACEMENT T :NONLINEARP T))) NIL)) ((ACCESS REWRITE-CONSTANT (ACCESS PROVE-SPEC-VAR PSPV :REWRITE-CONSTANT) :NONLINEARP) (IF (AND (CONSP HIST) (CONSP (CAR HIST))) (PROG2$ (CW "~%~%[Note: We now disable non-linear arithmetic.]~%~%") (QUOTE (:COMPUTED-HINT-REPLACEMENT T :NONLINEARP NIL))) NIL)) (T NIL)))) (LOCAL (ADD-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))))) (MUST-FAIL (WITH-PROVER-TIME-LIMIT 1/5 (DEFTHM TEST1 (EQUAL (LEN (APPEND X NIL)) (LEN X)) :RULE-CLASSES NIL)))) (ENCAPSULATE NIL (LOCAL (DEFUN NONLINEARP-DEFAULT-HINT (STABLE-UNDER-SIMPLIFICATIONP HIST PSPV) (DECLARE (XARGS :GUARD (AND (CONSP PSPV) (CONSP (CAR PSPV)) (CONSP (CAR (CAR PSPV))) (CONSP (CDR (CAR (CAR PSPV)))) (CONSP (CDR (CDR (CAR (CAR PSPV))))) (CONSP (CDR (CDR (CDR (CAR (CAR PSPV)))))) (CONSP (CDR (CDR (CDR (CDR (CAR (CAR PSPV))))))) (CONSP (CDR (CDR (CDR (CDR (CDR (CAR (CAR PSPV)))))))) (CONSP (CDR (CDR (CDR (CDR (CDR (CDR (CAR (CAR PSPV))))))))) (CONSP (CAR (CDR (CDR (CDR (CDR (CDR (CDR (CAR (CAR PSPV))))))))))))) (COND (STABLE-UNDER-SIMPLIFICATIONP (IF (NOT (ACCESS REWRITE-CONSTANT (ACCESS PROVE-SPEC-VAR PSPV :REWRITE-CONSTANT) :NONLINEARP)) (PROG2$ (CW "~%~%[Note: We now enable non-linear arithmetic.]~%~%") (QUOTE (:COMPUTED-HINT-REPLACEMENT T :NONLINEARP T))) NIL)) ((ACCESS REWRITE-CONSTANT (ACCESS PROVE-SPEC-VAR PSPV :REWRITE-CONSTANT) :NONLINEARP) (IF (AND (CONSP HIST) (CONSP (CAR HIST))) (PROG2$ (CW "~%~%[Note: We now disable non-linear arithmetic.]~%~%") (QUOTE (:COMPUTED-HINT-REPLACEMENT T :NONLINEARP NIL))) NIL)) (T NIL)))) (LOCAL (ADD-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))))) (RECORD-EXPANSION (MUST-FAIL (WITH-PROVER-TIME-LIMIT 1/5 (DEFTHM TEST1 (EQUAL (LEN (APPEND X NIL)) (LEN X)) :RULE-CLASSES NIL))) (VALUE-TRIPLE (QUOTE T))))))
NIL
(("/usr/share/acl2-6.3/books/hints/basic-tests.lisp" "basic-tests" "basic-tests" ((:SKIPPED-PROOFSP . T) (:AXIOMSP . T) (:TTAGS)) . 1987254049) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "misc/eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718))
1989832752
|