acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / meta / meta-plus-lessp.cert

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