round-trip/gold/axioms.lisp

43 (DEFUN TRUE-LISTP (X) (IF (CONSP X) (TRUE-LISTP (CDR X)) (EQ X 'NIL)))
110                (IF (TRUE-LISTP (CAR CLAUSES))
187 (DEFTHM ALISTP-FORWARD-TO-TRUE-LISTP (IMPLIES (ALISTP X) (TRUE-LISTP X)))
226 (DEFTHM SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP
228                  (TRUE-LISTP X)))
352 (DEFUN PROPER-CONSP (X) (IF (CONSP X) (TRUE-LISTP X) 'NIL))
354 (DEFUN IMPROPER-CONSP (X) (IF (CONSP X) (NOT (TRUE-LISTP X)) 'NIL))
891 (DEFTHM ATOM-LISTP-FORWARD-TO-TRUE-LISTP
892         (IMPLIES (ATOM-LISTP X) (TRUE-LISTP X)))
1546 (DEFTHM TRUE-LISTP-APPEND
1547         (IMPLIES (TRUE-LISTP B)
1548                  (TRUE-LISTP (BINARY-APPEND A B))))
1551         (IMPLIES (TRUE-LISTP X)
1558         (IMPLIES (TRUE-LISTP X)
1565         (IMPLIES (TRUE-LISTP X)
1668         (IMPLIES (TRUE-LISTP X)
1719                (IF (TRUE-LISTP (CAR RST))
1720                    (IF (TRUE-LISTP (CAR (CDR (CDR (CAR RST)))))
1897      (IF (NOT (TRUE-LISTP X))
1903                  (IF (TRUE-LISTP (CAR X))
1922 (DEFTHM PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP
1924                  (TRUE-LISTP X)))
2148 (DEFUN TRUE-LIST-LISTP (X)
2151            (IF (TRUE-LISTP (CAR X))
2152                (TRUE-LIST-LISTP (CDR X))
2155 (DEFTHM TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP
2156         (IMPLIES (TRUE-LIST-LISTP X)
2157                  (TRUE-LISTP X)))
2796                (IF (TRUE-LISTP X)
2845 (DEFTHM KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP
2847                  (TRUE-LISTP X)))
2878           (TRUE-LISTP DIMENSIONS)
2915       (TRUE-LISTP (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3039          (TRUE-LISTP DIMENSIONS)
3086       (TRUE-LISTP (CAR (CDR (ASSOC-KEYWORD ':DIMENSIONS
3403 (DEFTHM RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP
3405                  (TRUE-LISTP X)))
3520            (IF (TRUE-LISTP (CAR X))
3528 (DEFTHM KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP
3530                  (IF (TRUE-LIST-LISTP X)
3545 (DEFTHM TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP
3547                  (IF (TRUE-LIST-LISTP X)
3566 (DEFTHM TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP
3568                  (TRUE-LISTP X)))
3573   (TRUE-LISTP L)
3577             (IF (TRUE-LISTP HEADER)
3597 (DEFTHM OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP
3599                  (IF (TRUE-LISTP X) (CONSP X) 'NIL)))
3616                      (TRUE-LIST-LISTP X)
3627     (TRUE-LISTP X)
3630                  (IF (TRUE-LISTP KEY)
3647 (DEFTHM READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP
3649                  (IF (TRUE-LISTP X) (CONSP X) 'NIL)))
3658 (DEFTHM READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP
3660                  (IF (TRUE-LIST-LISTP X)
3673   (TRUE-LISTP X)
3677              (IF (TRUE-LISTP KEY)
3696 (DEFTHM WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP
3698                  (IF (TRUE-LISTP X) (CONSP X) 'NIL)))
3707 (DEFTHM WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP
3709                  (IF (TRUE-LIST-LISTP X)
3720        (IF (TRUE-LISTP X)
3733 (DEFTHM READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP
3735                  (IF (TRUE-LISTP X) (CONSP X) 'NIL)))
3744 (DEFTHM READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP
3746                  (TRUE-LIST-LISTP X)))
3755        (IF (TRUE-LISTP X)
3766 (DEFTHM WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP
3768                  (IF (TRUE-LISTP X) (CONSP X) 'NIL)))
3777 (DEFTHM WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP
3779                  (TRUE-LIST-LISTP X)))
3790   (TRUE-LISTP X)
4121             (TRUE-LISTP (T-STACK X))
4129                 (TRUE-LISTP (ACL2-ORACLE X))
4139                          (IF (TRUE-LIST-LISTP (LIST-ALL-PACKAGE-NAMES-LST X))
4168    (TRUE-LISTP X)
4498              (TRUE-LISTP (NTH '3 X))
4504                     (IF (TRUE-LISTP (NTH '7 X))
4510                                             (IF (TRUE-LIST-LISTP (NTH '13 X))
6056 (DEFTHM TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ
6057         (IMPLIES (TRUE-LIST-LISTP L)
6058                  (TRUE-LISTP (ASSOC-EQ KEY L))))
6060 (DEFTHM TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P
6062                  (TRUE-LISTP (CAR (CDR (ASSOC-EQ KEY ALIST))))))
6305 (DEFTHM TRUE-LISTP-UPDATE-NTH
6306         (IMPLIES (TRUE-LISTP L)
6307                  (TRUE-LISTP (UPDATE-NTH KEY VAL L))))
6822                      (TRUE-LISTP X)
6945                      (TRUE-LISTP (MAIN-TIMER STATE))
7147 (DEFTHM TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL
7148         (IMPLIES (TRUE-LIST-LISTP L)
7149                  (TRUE-LISTP (ASSOC-EQUAL KEY L))))
7474 (DEFUN FIX-TRUE-LIST (X)
7476            (CONS (CAR X) (FIX-TRUE-LIST (CDR X)))
7479 (DEFTHM PAIRLIS$-FIX-TRUE-LIST
7480         (EQUAL (PAIRLIS$ X (FIX-TRUE-LIST Y))
7843    (TRUE-LISTP MFC)
7845     (TRUE-LISTP
7877        (IF (TRUE-LISTP MFC)
7902        (IF (IF (TRUE-LISTP MFC)
7916     (TRUE-LISTP MFC)
7917     (TRUE-LISTP ((LAMBDA (ANCESTORS)
8082 (DEFTHM TRUE-LISTP-MERGE-SORT-LEXORDER
8083         (IMPLIES (IF (TRUE-LISTP L1)
8084                      (TRUE-LISTP L2)
8086                  (TRUE-LISTP (MERGE-LEXORDER L1 L2 ACC))))
8234       (IF (TRUE-LISTP SEQ1)
8235           (TRUE-LISTP SEQ2)