round-trip/gold/axioms.lisp

168                (CONS (CODE-CHAR '0)
693                     (IF (CHARACTERP X) X (CODE-CHAR '0))))
726                     (IF (CHARACTERP X) X (CODE-CHAR '0))))
1194                                      CDDDDR CLRHASH COUNT CDDDR CODE-CHAR
1203                                      CHAR-CODE COMPILER-MACRO-FUNCTION
1205                                      CHAR-CODE-LIMIT COMPLEMENT DEFCLASS
2474 (DEFAXIOM CHAR-CODE-LINEAR (< (CHAR-CODE X) '256))
2476 (DEFAXIOM CODE-CHAR-TYPE (CHARACTERP (CODE-CHAR N)))
2478 (DEFAXIOM CODE-CHAR-CHAR-CODE-IS-IDENTITY
2480                    (EQUAL (CODE-CHAR (CHAR-CODE C)) C)))
2482 (DEFAXIOM CHAR-CODE-CODE-CHAR-IS-IDENTITY
2488                    (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))
2490 (DEFUN CHAR< (X Y) (< (CHAR-CODE X) (CHAR-CODE Y)))
2492 (DEFUN CHAR> (X Y) (< (CHAR-CODE Y) (CHAR-CODE X)))
2494 (DEFUN CHAR<= (X Y) (NOT (< (CHAR-CODE Y) (CHAR-CODE X))))
2496 (DEFUN CHAR>= (X Y) (NOT (< (CHAR-CODE X) (CHAR-CODE Y))))
2729 (DEFTHM EQUAL-CHAR-CODE
2731                  (IMPLIES (EQUAL (CHAR-CODE X) (CHAR-CODE Y))
3858             (LOGIC-FNS-WITH-RAW-CODE MOD-EXPT HEADER SEARCH-FN
3919             (MACROS-WITH-RAW-CODE MBE
4005             (PROGRAM-FNS-WITH-RAW-CODE
4060             (REDUNDANT-WITH-RAW-CODE-OKP)
4236             (LOGIC-FNS-WITH-RAW-CODE MOD-EXPT HEADER SEARCH-FN
4297             (MACROS-WITH-RAW-CODE MBE
4383             (PROGRAM-FNS-WITH-RAW-CODE
4438             (REDUNDANT-WITH-RAW-CODE-OKP)
4612             (LOGIC-FNS-WITH-RAW-CODE MOD-EXPT HEADER SEARCH-FN
4673             (MACROS-WITH-RAW-CODE MBE
4759             (PROGRAM-FNS-WITH-RAW-CODE
4814             (REDUNDANT-WITH-RAW-CODE-OKP)
4995      (LOGIC-FNS-WITH-RAW-CODE MOD-EXPT HEADER SEARCH-FN
5056      (MACROS-WITH-RAW-CODE MBE
5142      (PROGRAM-FNS-WITH-RAW-CODE RELIEVE-HYP-SYNP
5196      (REDUNDANT-WITH-RAW-CODE-OKP)
5297      (LOGIC-FNS-WITH-RAW-CODE MOD-EXPT HEADER SEARCH-FN
5358      (MACROS-WITH-RAW-CODE MBE
5444      (PROGRAM-FNS-WITH-RAW-CODE RELIEVE-HYP-SYNP
5498      (REDUNDANT-WITH-RAW-CODE-OKP)
7591 (DEFAXIOM COMPLETION-OF-CHAR-CODE
7592           (EQUAL (CHAR-CODE X)
7593                  (IF (CHARACTERP X) (CHAR-CODE X) '0)))
7595 (DEFTHM DEFAULT-CHAR-CODE
7597                  (EQUAL (CHAR-CODE X) '0)))
7599 (DEFAXIOM COMPLETION-OF-CODE-CHAR
7600           (EQUAL (CODE-CHAR X)
7604                      (CODE-CHAR X)
7605                      (CODE-CHAR '0))))
8002                          (NOT (< (CHAR-CODE Y) (CHAR-CODE X)))