acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / tools / mv-nth.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((1 RECORD-EXPANSION (DEFEVALUATOR EVAL-FOR-MV-NTH EVAL-FOR-MV-NTH-LIST ((MV-NTH N X) (CONS A B))) (PROGN (RECORD-EXPANSION (WITH-OUTPUT :OFF ERROR :STACK :PUSH (MAKE-EVENT (ER-PROGN (WITH-OUTPUT :STACK :POP (DEFEVALUATOR-CHECK (QUOTE (DEFEVALUATOR EVAL-FOR-MV-NTH EVAL-FOR-MV-NTH-LIST ((MV-NTH N X) (CONS A B)))) (QUOTE EVAL-FOR-MV-NTH) (QUOTE EVAL-FOR-MV-NTH-LIST) (QUOTE ((MV-NTH N X) (CONS A B))) (QUOTE (DEFEVALUATOR . EVAL-FOR-MV-NTH)) STATE)) (VALUE (QUOTE (VALUE-TRIPLE NIL)))))) (WITH-OUTPUT :OFF ERROR :STACK :PUSH (VALUE-TRIPLE NIL))) (ENCAPSULATE (((EVAL-FOR-MV-NTH * *) => *) ((EVAL-FOR-MV-NTH-LIST * *) => *)) (SET-INHIBIT-WARNINGS "theory") (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*)) (LOCAL (MUTUAL-RECURSION (DEFUN-NX EVAL-FOR-MV-NTH (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)) (EVAL-FOR-MV-NTH (CAR (CDR (CDR (CAR X)))) (PAIRLIS$ (CAR (CDR (CAR X))) (EVAL-FOR-MV-NTH-LIST (CDR X) A)))) ((EQUAL (CAR X) (QUOTE MV-NTH)) (MV-NTH (EVAL-FOR-MV-NTH (CAR (CDR X)) A) (EVAL-FOR-MV-NTH (CAR (CDR (CDR X))) A))) ((EQUAL (CAR X) (QUOTE CONS)) (CONS (EVAL-FOR-MV-NTH (CAR (CDR X)) A) (EVAL-FOR-MV-NTH (CAR (CDR (CDR X))) A))) (T NIL))) (DEFUN-NX EVAL-FOR-MV-NTH-LIST (X-LST A) (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST) :WELL-FOUNDED-RELATION O<)) (COND ((ENDP X-LST) NIL) (T (CONS (EVAL-FOR-MV-NTH (CAR X-LST) A) (EVAL-FOR-MV-NTH-LIST (CDR X-LST) A))))))) (LOCAL (DEFTHM EVAL-LIST-KWOTE-LST (EQUAL (EVAL-FOR-MV-NTH-LIST (KWOTE-LST ARGS) A) (FIX-TRUE-LIST ARGS)))) (DEFTHMD EVAL-FOR-MV-NTH-CONSTRAINT-0 (IMPLIES (AND (CONSP X) (SYNTAXP (NOT (EQUAL A (QUOTE (QUOTE NIL))))) (NOT (EQUAL (CAR X) (QUOTE QUOTE)))) (EQUAL (EVAL-FOR-MV-NTH X A) (EVAL-FOR-MV-NTH (CONS (CAR X) (KWOTE-LST (EVAL-FOR-MV-NTH-LIST (CDR X) A))) NIL))) :HINTS (("Goal" :EXPAND ((:FREE (X) (HIDE X)) (EVAL-FOR-MV-NTH X A)) :IN-THEORY (DISABLE (:EXECUTABLE-COUNTERPART EVAL-FOR-MV-NTH))))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-1 (IMPLIES (SYMBOLP X) (EQUAL (EVAL-FOR-MV-NTH X A) (AND X (CDR (ASSOC-EQUAL X A)))))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-2 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE QUOTE))) (EQUAL (EVAL-FOR-MV-NTH X A) (CADR X)))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-3 (IMPLIES (AND (CONSP X) (CONSP (CAR X))) (EQUAL (EVAL-FOR-MV-NTH X A) (EVAL-FOR-MV-NTH (CADDAR X) (PAIRLIS$ (CADAR X) (EVAL-FOR-MV-NTH-LIST (CDR X) A)))))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-4 (IMPLIES (NOT (CONSP X-LST)) (EQUAL (EVAL-FOR-MV-NTH-LIST X-LST A) NIL))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-5 (IMPLIES (CONSP X-LST) (EQUAL (EVAL-FOR-MV-NTH-LIST X-LST A) (CONS (EVAL-FOR-MV-NTH (CAR X-LST) A) (EVAL-FOR-MV-NTH-LIST (CDR X-LST) A))))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-6 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE MV-NTH))) (EQUAL (EVAL-FOR-MV-NTH X A) (MV-NTH (EVAL-FOR-MV-NTH (CADR X) A) (EVAL-FOR-MV-NTH (CADDR X) A))))) (DEFTHM EVAL-FOR-MV-NTH-CONSTRAINT-7 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE CONS))) (EQUAL (EVAL-FOR-MV-NTH X A) (CONS (EVAL-FOR-MV-NTH (CADR X) A) (EVAL-FOR-MV-NTH (CADDR X) A)))))))))
NIL
(("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140))
1504201595