round-trip/gold/axioms.lisp

1488                                      UPDATE-INSTANCE-FOR-DIFFERENT-CLASS
1490                                      UPDATE-INSTANCE-FOR-REDEFINED-CLASS
1865    UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX-1
1871                  (UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX-1 (CDR DEFS)))
1874                      (UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX-1 (CDR DEFS)))
1876                      (UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX-1 (CDR DEFS)))))))
1878 (DEFUN UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX
1883            (UPDATE-MUTUAL-RECURSION-FOR-DEFUN-NX-1 DEFS)
3374 (DEFUN UPDATE-NTH (KEY VAL L)
3378                  (UPDATE-NTH (BINARY-+ '-1 KEY)
3381 (DEFUN UPDATE-NTH-ARRAY (J KEY VAL L)
3382        (UPDATE-NTH J (UPDATE-NTH KEY VAL (NTH J L))
3431 (DEFUN UPDATE-OPEN-INPUT-CHANNELS (X ST) (UPDATE-NTH '0 X ST))
3435 (DEFUN UPDATE-OPEN-OUTPUT-CHANNELS (X ST) (UPDATE-NTH '1 X ST))
3439 (DEFUN UPDATE-GLOBAL-TABLE (X ST) (UPDATE-NTH '2 X ST))
3443 (DEFUN UPDATE-T-STACK (X ST) (UPDATE-NTH '3 X ST))
3447 (DEFUN UPDATE-32-BIT-INTEGER-STACK (X ST) (UPDATE-NTH '4 X ST))
3451 (DEFUN UPDATE-BIG-CLOCK-ENTRY (X ST) (UPDATE-NTH '5 X ST))
3455 (DEFUN UPDATE-IDATES (X ST) (UPDATE-NTH '6 X ST))
3459 (DEFUN UPDATE-ACL2-ORACLE (X ST) (UPDATE-NTH '7 X ST))
3463 (DEFUN UPDATE-FILE-CLOCK (X ST) (UPDATE-NTH '8 X ST))
3469 (DEFUN UPDATE-WRITTEN-FILES (X ST) (UPDATE-NTH '10 X ST))
3473 (DEFUN UPDATE-READ-FILES (X ST) (UPDATE-NTH '11 X ST))
3479 (DEFUN UPDATE-LIST-ALL-PACKAGE-NAMES-LST (X ST) (UPDATE-NTH '13 X ST))
3483 (DEFUN UPDATE-USER-STOBJ-ALIST1 (X ST) (UPDATE-NTH '14 X ST))
3876                                      READ-ACL2-ORACLE UPDATE-USER-STOBJ-ALIST
4008                  NTH-UPDATE-REWRITER
4254                                      READ-ACL2-ORACLE UPDATE-USER-STOBJ-ALIST
4386                  NTH-UPDATE-REWRITER
4630                                      READ-ACL2-ORACLE UPDATE-USER-STOBJ-ALIST
4762                  NTH-UPDATE-REWRITER
4910        (UPDATE-GLOBAL-TABLE (DELETE-PAIR X (GLOBAL-TABLE STATE-STATE))
4917        (UPDATE-GLOBAL-TABLE (ADD-PAIR KEY VALUE (GLOBAL-TABLE STATE-STATE))
5013                               READ-ACL2-ORACLE UPDATE-USER-STOBJ-ALIST
5144                                 NTH-UPDATE-REWRITER
5315                               READ-ACL2-ORACLE UPDATE-USER-STOBJ-ALIST
5446                                 NTH-UPDATE-REWRITER
6204    (UPDATE-OPEN-OUTPUT-CHANNELS
6229                 (UPDATE-OPEN-OUTPUT-CHANNELS
6240                 (UPDATE-OPEN-OUTPUT-CHANNELS
6277           (UPDATE-OPEN-INPUT-CHANNELS
6296   (UPDATE-FILE-CLOCK (BINARY-+ '1 (FILE-CLOCK STATE-STATE))
6300 (DEFTHM NTH-UPDATE-NTH
6301         (EQUAL (NTH M (UPDATE-NTH N VAL L))
6305 (DEFTHM TRUE-LISTP-UPDATE-NTH
6307                  (TRUE-LISTP (UPDATE-NTH KEY VAL L))))
6309 (DEFTHM NTH-UPDATE-NTH-ARRAY
6310         (EQUAL (NTH M (UPDATE-NTH-ARRAY N I VAL L))
6312                    (UPDATE-NTH I VAL (NTH M L))
6324                   (UPDATE-OPEN-INPUT-CHANNELS
6328          (UPDATE-READ-FILES
6339   (UPDATE-FILE-CLOCK (BINARY-+ '1 (FILE-CLOCK STATE-STATE))
6358         (UPDATE-OPEN-OUTPUT-CHANNELS
6372   (UPDATE-FILE-CLOCK (BINARY-+ '1 (FILE-CLOCK STATE-STATE))
6445                  (UPDATE-OPEN-OUTPUT-CHANNELS
6449         (UPDATE-WRITTEN-FILES
6464   (UPDATE-FILE-CLOCK (BINARY-+ '1 (FILE-CLOCK STATE-STATE))
6472                     (CONS (UPDATE-OPEN-INPUT-CHANNELS
6491                     (CONS (UPDATE-OPEN-INPUT-CHANNELS
6508                     (CONS (UPDATE-OPEN-INPUT-CHANNELS
6657        (UPDATE-T-STACK (BINARY-APPEND (T-STACK STATE-STATE)
6688     (UPDATE-T-STACK (FIRST-N-AC (MAX '0
6698        (UPDATE-T-STACK (UPDATE-NTH I VAL (T-STACK STATE-STATE))
6711        (UPDATE-32-BIT-INTEGER-STACK
6719   (UPDATE-32-BIT-INTEGER-STACK
6733        (UPDATE-32-BIT-INTEGER-STACK
6734             (UPDATE-NTH I
6742        (UPDATE-BIG-CLOCK-ENTRY (BINARY-+ '-1
6748              (CONS (UPDATE-LIST-ALL-PACKAGE-NAMES-LST
6755 (DEFUN UPDATE-USER-STOBJ-ALIST (X STATE-STATE)
6756        (UPDATE-USER-STOBJ-ALIST1 X STATE-STATE))
6768              (CONS (UPDATE-IDATES (CDR (IDATES STATE-STATE))
6778              (CONS (UPDATE-ACL2-ORACLE (CDR (ACL2-ORACLE STATE-STATE))
6785                    (CONS (UPDATE-ACL2-ORACLE (CDR (ACL2-ORACLE STATE-STATE))
6816 (DEFTHM LEN-UPDATE-NTH
6817         (EQUAL (LEN (UPDATE-NTH N VAL X))
6820 (DEFTHM UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1
6824                  (STATE-P1 (UPDATE-ACL2-ORACLE X STATE))))
6973 (DEFTHM STATE-P1-UPDATE-MAIN-TIMER
6975                  (STATE-P1 (UPDATE-NTH '2
7128     STATE-P1-UPDATE-NTH-2-WORLD
7142              (STATE-P1 (UPDATE-NTH '2