/usr/share/hol88-2.02.19940316/theories/num.th is in hol88-source 2.02.19940316-28.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 | (SETQ %THEORYDATA (QUOTE ((PARENTS BASIC-HOL) (TYPES (0 . |num|)) (NAMETYPES) (OPERATORS (SUC |fun| (|num|) (|num|)) (|0| |num|) (|ABS_num| |fun| (|ind|) (|num|)) (|REP_num| |fun| (|num|) (|ind|)) (IS_NUM_REP |fun| (|ind|) (|bool|)) (ZERO_REP |ind|) (SUC_REP |fun| (|ind|) (|ind|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502445619))))
(SETQ %THEOREMS (QUOTE ((SHARETYPES 5 (P%4 |fun| (|num|) (|bool|)) (|arb%3| %VARTYPE . *) (|rep%2| |fun| (|num|) (|ind|)) (P%1 |fun| (|ind|) (|bool|)) (|f%0| |fun| (|ind|) (|ind|))) (AXIOM (SUC_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |m|))) COMB ((CONST |ABS_num|) COMB ((CONST SUC_REP) COMB ((CONST |REP_num|) VAR |m|)))) |bool|)))) (ZERO_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |0|)) COMB ((CONST |ABS_num|) CONST ZERO_REP)))) (|num_ISO_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |a| |num|) COMB ((COMB ((CONST =) COMB ((CONST |ABS_num|) COMB ((CONST |REP_num|) VAR |a|)))) VAR |a| |num|) |bool|)))) COMB ((CONST !) ABS ((VAR |r| |ind|) COMB ((COMB ((CONST =) COMB ((CONST IS_NUM_REP) VAR |r|))) COMB ((COMB ((CONST =) COMB ((CONST |REP_num|) COMB ((CONST |ABS_num|) VAR |r|)))) VAR |r| |ind|) |bool|) |bool|))))) (|num_TY_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST ?) ABS ((VAR |rep| %T . |rep%2|) COMB ((COMB ((CONST TYPE_DEFINITION) CONST IS_NUM_REP)) VAR |rep| %T . |rep%2|) |bool|)))) (IS_NUM_REP PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |m| |ind|) COMB ((COMB ((CONST =) COMB ((CONST IS_NUM_REP) VAR |m|))) COMB ((CONST !) ABS ((VAR P %T . P%1) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . P%1) CONST ZERO_REP))) COMB ((CONST !) ABS ((VAR |n| |ind|) COMB ((COMB ((CONST ==>) COMB ((VAR P %T . P%1) VAR |n|))) COMB ((VAR P %T . P%1) COMB ((CONST SUC_REP) VAR |n|)))))))) COMB ((VAR P %T . P%1) VAR |m|)))) |bool|) |bool|)))) (ZERO_REP_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST ZERO_REP)) COMB ((CONST @) ABS ((VAR |x| |ind|) COMB ((CONST !) ABS ((VAR |y| |ind|) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |x| |ind|)) COMB ((CONST SUC_REP) VAR |y|))))) |bool|)) |ind|))) (SUC_REP_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST SUC_REP)) COMB ((CONST @) ABS ((VAR |f| %T . |f%0|) COMB ((COMB ((CONST |/\\|) COMB ((CONST ONE_ONE) VAR |f| %T . |f%0|))) COMB ((CONST ~) COMB ((CONST ONTO) VAR |f| %T . |f%0|))))) %T . |f%0|)))) (FACT (INDUCTION PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%4) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . P%4) CONST |0|))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((VAR P %T . P%4) VAR |n|))) COMB ((VAR P %T . P%4) COMB ((CONST SUC) VAR |n|)))))))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((VAR P %T . P%4) VAR |n|)))))) |bool|) (INV_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |m|))) COMB ((CONST SUC) VAR |n|)))) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|)))) |bool|)) |bool|) (NOT_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |n|))) CONST |0|)))) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%3|) |bool|)))))
|