acl2/ml/defaxioms.lisp.trans.ml

4897 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-NTH") (
4906 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (
4916 "UPDATE-NTH-ARRAY") (mkpair (mkpair (mksym "ACL2" "J") (mkpair (mksym "ACL2"
4918 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (
4919 mksym "ACL2" "J") (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (mksym
5009 "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (
5011 "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
5026 "UPDATE-OPEN-OUTPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (
5028 "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
5043 "UPDATE-GLOBAL-TABLE") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym
5045 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
5059 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-T-STACK") (
5061 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (
5076 "UPDATE-32-BIT-INTEGER-STACK") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (
5078 "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
5093 "UPDATE-BIG-CLOCK-ENTRY") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym
5095 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
5108 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-IDATES") (
5110 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (
5125 "UPDATE-RUN-TIMES") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
5127 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
5142 "UPDATE-FILE-CLOCK") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
5144 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
5167 "UPDATE-WRITTEN-FILES") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym
5169 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
5184 "UPDATE-READ-FILES") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
5186 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
5209 "UPDATE-LIST-ALL-PACKAGE-NAMES-LST") (mkpair (mkpair (mksym "ACL2" "X") (
5211 mksym "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
5226 "UPDATE-USER-STOBJ-ALIST1") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym
5228 "UPDATE-NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
6159 "UPDATE-GLOBAL-TABLE") (mkpair (mkpair (mksym "ACL2" "DELETE-PAIR") (mkpair (
6178 mksym "ACL2" "UPDATE-GLOBAL-TABLE") (mkpair (mkpair (mksym "ACL2" "ADD-PAIR") (
7004 "ACL2" "UPDATE-OPEN-OUTPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2"
7029 "ACL2" "UPDATE-OPEN-OUTPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2"
7061 "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "DELETE-PAIR") (
7067 "UPDATE-READ-FILES") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
7095 mkpair (mkpair (mksym "ACL2" "UPDATE-FILE-CLOCK") (mkpair (mkpair (mksym
7120 "UPDATE-OPEN-OUTPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "DELETE-PAIR") (
7126 "UPDATE-WRITTEN-FILES") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
7160 mksym "ACL2" "UPDATE-FILE-CLOCK") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (
7178 "ACL2" "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "ADD-PAIR") (
7221 "ACL2" "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "ADD-PAIR") (
7254 mkpair (mksym "ACL2" "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym
7392 "ACL2" "UPDATE-T-STACK") (mkpair (mkpair (mksym "ACL2" "BINARY-APPEND") (
7483 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UPDATE-T-STACK") (
7510 "ACL2" "UPDATE-T-STACK") (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (
7535 "NIL")))) (mkpair (mkpair (mksym "ACL2" "UPDATE-32-BIT-INTEGER-STACK") (
7549 mksym "ACL2" "UPDATE-32-BIT-INTEGER-STACK") (mkpair (mkpair (mksym "ACL2"
7577 "NIL")))) (mkpair (mkpair (mksym "ACL2" "UPDATE-32-BIT-INTEGER-STACK") (
7578 mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (mksym "ACL2" "I") (mkpair (
7596 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "UPDATE-BIG-CLOCK-ENTRY") (
7612 "UPDATE-LIST-ALL-PACKAGE-NAMES-LST") (mkpair (mkpair (mksym "COMMON-LISP"
7629 "UPDATE-USER-STOBJ-ALIST") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym
7631 "ACL2" "UPDATE-USER-STOBJ-ALIST1") (mkpair (mksym "ACL2" "X") (mkpair (mksym
7662 "UPDATE-IDATES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (
7682 "UPDATE-RUN-TIMES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
11038 "UPDATE-INSTANCE-FOR-DIFFERENT-CLASS") (mkpair (mksym "COMMON-LISP"
11040 "UPDATE-INSTANCE-FOR-REDEFINED-CLASS") (mkpair (mksym "COMMON-LISP"
12733 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "NTH-UPDATE-NTH") (
12736 "UPDATE-NTH") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VAL") (mkpair (
12748 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "TRUE-LISTP-UPDATE-NTH") (
12752 "UPDATE-NTH") (mkpair (mksym "ACL2" "KEY") (mkpair (mksym "ACL2" "VAL") (
12758 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "NTH-UPDATE-NTH-ARRAY") (
12761 "UPDATE-NTH-ARRAY") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "I") (
12768 mksym "ACL2" "UPDATE-NTH") (mkpair (mksym "ACL2" "I") (mkpair (mksym "ACL2"
12777 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "LEN-UPDATE-NTH") (
12779 "LEN") (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (mksym "ACL2" "N") (
12792 "UPDATE-RUN-TIMES-PRESERVES-STATE-P1") (mkpair (mkpair (mksym "ACL2"
12799 mkpair (mksym "ACL2" "UPDATE-RUN-TIMES") (mkpair (mksym "ACL2" "TIMES") (
12984 "STATE-P1-UPDATE-MAIN-TIMER") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
12987 mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (mkpair (mksym
13026 "STATE-P1-UPDATE-NTH-2-WORLD") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
13052 "ACL2" "STATE-P1") (mkpair (mkpair (mksym "ACL2" "UPDATE-NTH") (mkpair (