acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / misc / beta-reduce.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((1 RECORD-EXPANSION (DEFEVALUATOR BETA-EVAL BETA-EVAL-LIST NIL) (PROGN (RECORD-EXPANSION (WITH-OUTPUT :OFF ERROR :STACK :PUSH (MAKE-EVENT (ER-PROGN (WITH-OUTPUT :STACK :POP (DEFEVALUATOR-CHECK (QUOTE (DEFEVALUATOR BETA-EVAL BETA-EVAL-LIST NIL)) (QUOTE BETA-EVAL) (QUOTE BETA-EVAL-LIST) (QUOTE NIL) (QUOTE (DEFEVALUATOR . BETA-EVAL)) STATE)) (VALUE (QUOTE (VALUE-TRIPLE NIL)))))) (WITH-OUTPUT :OFF ERROR :STACK :PUSH (VALUE-TRIPLE NIL))) (ENCAPSULATE (((BETA-EVAL * *) => *) ((BETA-EVAL-LIST * *) => *)) (SET-INHIBIT-WARNINGS "theory") (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*)) (LOCAL (MUTUAL-RECURSION (DEFUN-NX BETA-EVAL (X A) (DECLARE (XARGS :VERIFY-GUARDS NIL :MEASURE (ACL2-COUNT X) :WELL-FOUNDED-RELATION O< :MODE :LOGIC)) (COND ((SYMBOLP X) (AND X (CDR (ASSOC-EQ X A)))) ((ATOM X) NIL) ((EQ (CAR X) (QUOTE QUOTE)) (CAR (CDR X))) ((CONSP (CAR X)) (BETA-EVAL (CAR (CDR (CDR (CAR X)))) (PAIRLIS$ (CAR (CDR (CAR X))) (BETA-EVAL-LIST (CDR X) A)))) (T NIL))) (DEFUN-NX BETA-EVAL-LIST (X-LST A) (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST) :WELL-FOUNDED-RELATION O<)) (COND ((ENDP X-LST) NIL) (T (CONS (BETA-EVAL (CAR X-LST) A) (BETA-EVAL-LIST (CDR X-LST) A))))))) (LOCAL (DEFTHM EVAL-LIST-KWOTE-LST (EQUAL (BETA-EVAL-LIST (KWOTE-LST ARGS) A) (FIX-TRUE-LIST ARGS)))) (DEFTHMD BETA-EVAL-CONSTRAINT-0 (IMPLIES (AND (CONSP X) (SYNTAXP (NOT (EQUAL A (QUOTE (QUOTE NIL))))) (NOT (EQUAL (CAR X) (QUOTE QUOTE)))) (EQUAL (BETA-EVAL X A) (BETA-EVAL (CONS (CAR X) (KWOTE-LST (BETA-EVAL-LIST (CDR X) A))) NIL))) :HINTS (("Goal" :EXPAND ((:FREE (X) (HIDE X)) (BETA-EVAL X A)) :IN-THEORY (DISABLE (:EXECUTABLE-COUNTERPART BETA-EVAL))))) (DEFTHM BETA-EVAL-CONSTRAINT-1 (IMPLIES (SYMBOLP X) (EQUAL (BETA-EVAL X A) (AND X (CDR (ASSOC-EQUAL X A)))))) (DEFTHM BETA-EVAL-CONSTRAINT-2 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE QUOTE))) (EQUAL (BETA-EVAL X A) (CADR X)))) (DEFTHM BETA-EVAL-CONSTRAINT-3 (IMPLIES (AND (CONSP X) (CONSP (CAR X))) (EQUAL (BETA-EVAL X A) (BETA-EVAL (CADDAR X) (PAIRLIS$ (CADAR X) (BETA-EVAL-LIST (CDR X) A)))))) (DEFTHM BETA-EVAL-CONSTRAINT-4 (IMPLIES (NOT (CONSP X-LST)) (EQUAL (BETA-EVAL-LIST X-LST A) NIL))) (DEFTHM BETA-EVAL-CONSTRAINT-5 (IMPLIES (CONSP X-LST) (EQUAL (BETA-EVAL-LIST X-LST A) (CONS (BETA-EVAL (CAR X-LST) A) (BETA-EVAL-LIST (CDR X-LST) A)))))))) (11 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (DEFEVALUATOR TEST TEST-LIST NIL) (BETA-REDUCTION-THEOREM TEST TEST-LIST))) (LOCAL (VALUE-TRIPLE :ELIDED))))
NIL
(("/usr/share/acl2-6.3/books/misc/beta-reduce.lisp" "beta-reduce" "beta-reduce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1796882416))
2059609387