acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / hints / consider-hint-tests.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (MAKE-EVENT (PPROGN (SHOW-CUSTOM-KEYWORD-HINT-EXPANSION T) (VALUE (QUOTE (VALUE-TRIPLE NIL))))) (VALUE-TRIPLE NIL)) (24 RECORD-EXPANSION (THM? (EQUAL (BUMPER1 (APPEND A B) I J) (APPEND (BUMPER1 A I J) (BUMPER1 B I J))) :HINTS (("Goal" :CONSIDER (MAP-H-APPEND :TARGET (BUMPER1 (APPEND A B) I J))))) (VALUE-TRIPLE (QUOTE T))) (25 RECORD-EXPANSION (THM? (EQUAL (BUMPER1 (APPEND A B) I J) (APPEND (BUMPER1 A I J) (BUMPER1 B I J))) :HINTS (("Goal" :CONSIDER MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (26 RECORD-EXPANSION (THM? (EQUAL (BUMPER2 (APPEND A B) I J) (APPEND (BUMPER2 A I J) (BUMPER2 B I J))) :HINTS (("Goal" :CONSIDER MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (27 RECORD-EXPANSION (THM? (EQUAL (BUMPER3 (APPEND A B) I J) (APPEND (BUMPER3 A I J) (BUMPER3 B I J))) :HINTS (("Goal" :CONSIDER MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (28 RECORD-EXPANSION (THM? (EQUAL (BUMPER1 (APPEND A B) I J) (APPEND (BUMPER1 A I J) (BUMPER1 B I J))) :HINTS (("Goal" :CONSIDER FILTER-MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (29 RECORD-EXPANSION (THM? (EQUAL (BUMPER2 (APPEND A B) I J) (APPEND (BUMPER2 A I J) (BUMPER2 B I J))) :HINTS (("Goal" :CONSIDER FILTER-MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (30 RECORD-EXPANSION (THM? (EQUAL (BUMPER3 (APPEND A B) I J) (APPEND (BUMPER3 A I J) (BUMPER3 B I J))) :HINTS (("Goal" :CONSIDER FILTER-MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (31 RECORD-EXPANSION (THM? (EQUAL (BUMPER4 (APPEND A B) I) (APPEND (BUMPER4 A I) (BUMPER4 B I))) :HINTS (("Goal" :CONSIDER FILTER-MAP-H-APPEND))) (VALUE-TRIPLE (QUOTE T))) (32 RECORD-EXPANSION (THM? (IMPLIES (AND (INTEGERP I) (<= 0 I) (INTEGERP J) (<= 0 J)) (EQUAL (M5-RUN S (+ I J)) (M5-RUN (M5-RUN S I) J))) :HINTS (("Goal" :CONSIDER GENERIC-RUN-SUM))) (VALUE-TRIPLE (QUOTE T))) (33 RECORD-EXPANSION (THM? (EQUAL (GET-INTEGERS (APPEND X Y) Z) (GET-INTEGERS Y (GET-INTEGERS X Z))) :HINTS (("Goal" :CONSIDER GENERIC-LIST-ITERATOR-APPEND))) (VALUE-TRIPLE (QUOTE T))) (34 RECORD-EXPANSION (THM? (EQUAL (GET-BIG-INTEGERS (APPEND X Y) U Z) (GET-BIG-INTEGERS Y U (GET-BIG-INTEGERS X U Z))) :HINTS (("Goal" :CONSIDER GENERIC-LIST-ITERATOR-APPEND))) (VALUE-TRIPLE (QUOTE T))) (36 RECORD-EXPANSION (THM? (EQUAL A B) :HINTS (("Goal" :CONSIDER G-THM))) (VALUE-TRIPLE (QUOTE T))) (37 RECORD-EXPANSION (NOT-THM? (EQUAL A B) :HINTS (("Goal" :CONSIDER (G-THM :INSTANCE ((X C)))))) (VALUE-TRIPLE (QUOTE T))) (38 RECORD-EXPANSION (THM? (EQUAL A B) :HINTS (("Goal" :CONSIDER (G-THM :FUNCTIONAL-INSTANCE ((G (LAMBDA (X Y) (EQUAL X B)))))))) (VALUE-TRIPLE (QUOTE T))) (40 RECORD-EXPANSION (THM? (EQUAL (APPEND XXX (APPEND A (APPEND A A))) (APPEND XXX (APPEND (APPEND A A) A))) :HINTS (("Goal" :CONSIDER ASSOC-APPEND))) (VALUE-TRIPLE (QUOTE T))) (48 RECORD-EXPANSION (THM? (EQUAL (APP (APP (REV (REV (REV A))) B) C) (APP (REV A) (APP B C))) :HINTS (("Goal" :DO-NOT (QUOTE (GENERALIZE)) :CONSIDER (ASSOC-OF-APP TRIPLE-REV)))) (VALUE-TRIPLE (QUOTE T))) (51 RECORD-EXPANSION (NOT-THM? (EQUAL (APPEND A B) (APPEND B A)) :HINTS (("Subgoal *1/1" :IN-THEORY (DISABLE CAR-CONS) :OR ((:DO-NOT (QUOTE (GENERALIZE)) :ORE ((:BY NIL) (:YOUSE (:INSTANCE CAR-CONS (X CASE) (Y 2))))) (:YOUSE (:INSTANCE CAR-CONS (X CASE) (Y 3))))))) (VALUE-TRIPLE (QUOTE T))) (53 RECORD-EXPANSION (THM? (<= A (+ A (NFIX B))) :HINTS (("Goal" :CONSIDER FFF-CONSTRAINT))) (VALUE-TRIPLE (QUOTE T))) (54 RECORD-EXPANSION (THM? (<= A (+ A (NFIX B))) :HINTS (("Goal" :CONSIDER (FFF-CONSTRAINT :INSTANCE ((V B)))))) (VALUE-TRIPLE (QUOTE T))) (73 RECORD-EXPANSION (NOT-THM? (AND (TRUE-LISTP (APP A B)) (PROPERTYP (APP (REV (REV (REV (REV B)))) (REV (REV (REV A)))))) :HINTS (("Subgoal 1" :CONSIDER DERIVED-FACT) ("Subgoal 1.D14'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D13'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D12'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D11'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D10'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D9'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D8'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D7'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D6'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D5'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D4'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D3'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D2'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D1'" :IN-THEORY (ENABLE PROPERTYP-FALSE))) :OTF-FLG T) (VALUE-TRIPLE (QUOTE T))) (74 RECORD-EXPANSION (NOT-THM? (AND (TRUE-LISTP (APP A B)) (PROPERTYP (APP (REV (REV (REV (REV B)))) (REV (REV (REV A)))))) :HINTS (("Subgoal 1" :CONSIDER DERIVED-FACT) ("Subgoal 1.D14'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D13'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D11'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D10'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D9'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D8'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D7'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D6'" :IN-THEORY (ENABLE PROPERTYP-FALSE)) ("Subgoal 1.D5'" :CONSIDER DERIVED-FACT)) :OTF-FLG T) (VALUE-TRIPLE (QUOTE T))))
NIL
(("/usr/share/acl2-6.3/books/hints/consider-hint-tests.lisp" "consider-hint-tests" "consider-hint-tests" ((:SKIPPED-PROOFSP . T) (:AXIOMSP) (:TTAGS)) . 698768688) ("/usr/share/acl2-6.3/books/hints/consider-hint.lisp" "consider-hint" "consider-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1007119152) ("/usr/share/acl2-6.3/books/hints/merge-hint.lisp" "merge-hint" "merge-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2129857917) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "misc/eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718) ("/usr/share/acl2-6.3/books/hints/huet-lang-algorithm.lisp" "huet-lang-algorithm" "huet-lang-algorithm" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 50416838))
1524047989