File: arith.th

package info (click to toggle)
hol88 2.02.19940316-8
links: PTS
area: main
in suites: lenny
size: 63,120 kB
ctags: 19,367
sloc: ml: 199,939; ansic: 9,300; sh: 7,118; makefile: 6,074; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (4 lines) | stat: -rw-r--r-- 11,641 bytes
parent folder | download | duplicates (11)

(SETQ %THEORYDATA '((PARENTS HOL) (TYPES) (NAMETYPES) (OPERATORS) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "1.12 (Sun4/Allegro 4.0)") (STAMP . 2878299101))) 

(SETQ %THEOREMS '((SHARETYPES 1 (|arb%0| %VARTYPE . *)) (AXIOM) (FACT (|less_EXP_lemma| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST <) COMB ((COMB ((CONST EXP) COMB ((CONST SUC) COMB ((CONST SUC) VAR |m|)))) VAR |n|))) COMB ((COMB ((CONST EXP) COMB ((CONST SUC) COMB ((CONST SUC) VAR |m|)))) COMB ((CONST SUC) VAR |n|))))) |bool|)) |bool|) (|Odd_Or_Even| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ?) ABS ((VAR |m| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((COMB ((CONST *) COMB ((CONST SUC) COMB ((CONST SUC) CONST |0|)))) VAR |m|)))) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) COMB ((CONST SUC) COMB ((CONST SUC) CONST |0|)))) VAR |m|))) CONST |1|))))) |bool|)) |bool|) (|Zero_LESS_EXP| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST <) CONST |0|)) COMB ((COMB ((CONST EXP) COMB ((CONST SUC) VAR |n|))) VAR |m|)))) |bool|)) |bool|) (|Not_EXP_0| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST =) COMB ((COMB ((CONST EXP) COMB ((CONST SUC) VAR |n|))) VAR |m|))) CONST |0|)))) |bool|)) |bool|) (CANCEL_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |p|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |p|)) VAR |m|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|))) COMB ((COMB ((CONST -) VAR |m|)) VAR |p|)) |bool|)) COMB ((COMB ((CONST =) VAR |n| |num|)) VAR |m| |num|) |bool|)))) |bool|)) |bool|)) |bool|) (SUB_CANCEL PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |p|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |p|)) VAR |n|))) COMB ((COMB ((CONST -) VAR |p|)) VAR |m|)) |bool|)) COMB ((COMB ((CONST =) VAR |n| |num|)) VAR |m| |num|) |bool|)))) |bool|)) |bool|)) |bool|) (SUB_LESS_EQ_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |m|)) VAR |p|))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST -) VAR |p|)) VAR |m|))) VAR |n|))) COMB ((COMB ((CONST <=) VAR |p|)) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) |bool|))))) |bool|)) |bool|) (LESS_EQ_IMP_LESS_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|))) COMB ((COMB ((CONST <) VAR |n|)) COMB ((CONST SUC) VAR |m|))))) |bool|)) |bool|) (LESS_IMP_LESS_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|))) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST <) VAR |n|)) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))))))) |bool|)) |bool|) (SUB_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |b| |num|) COMB ((CONST !) ABS ((VAR |c| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |c|)) VAR |b|))) COMB ((CONST !) ABS ((VAR |a| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |a|)) COMB ((COMB ((CONST -) VAR |b|)) VAR |c|)))) COMB ((COMB ((CONST -) COMB ((COMB ((CONST +) VAR |a|)) VAR |c|))) VAR |b|)) |bool|))))) |bool|)) |bool|) (NOT_SUC_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |n|))) VAR |m|)))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)) |bool|)) |bool|)) |bool|) (LESS_EQ_SUB_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |a| |num|) COMB ((CONST !) ABS ((VAR |b| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |b|)) VAR |a|))) COMB ((CONST !) ABS ((VAR |c| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) COMB ((COMB ((CONST -) VAR |a|)) VAR |b|))) VAR |c|))) COMB ((COMB ((CONST <) VAR |a|)) COMB ((COMB ((CONST +) VAR |b|)) VAR |c|))) |bool|))))) |bool|)) |bool|) (SUB_EQUAL_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |c| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |c|)) VAR |c|))) CONST |0|) |bool|)) |bool|) (LESS_EQ_ADD_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |c| |num|) COMB ((CONST !) ABS ((VAR |b| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |c|)) VAR |b|))) COMB ((CONST !) ABS ((VAR |a| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) COMB ((COMB ((CONST +) VAR |a|)) VAR |b|))) VAR |c|))) COMB ((COMB ((CONST +) VAR |a|)) COMB ((COMB ((CONST -) VAR |b|)) VAR |c|))) |bool|))))) |bool|)) |bool|) (ADD_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |a| |num|) COMB ((CONST !) ABS ((VAR |c| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) COMB ((COMB ((CONST +) VAR |a|)) VAR |c|))) VAR |c|))) VAR |a| |num|) |bool|)) |bool|)) |bool|) (MULT_MONO_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |i| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |n|))) VAR |m|))) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |n|))) VAR |i|)) |bool|)) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |i| |num|) |bool|) |bool|)) |bool|)) |bool|)) |bool|) (LESS_MULT_MONO PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |i| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |n|))) VAR |m|))) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |n|))) VAR |i|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |i|)) |bool|)) |bool|)) |bool|)) |bool|) (TIMES_2 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) CONST |2|)) VAR |n|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |n|)) |bool|)) |bool|) (NOT_ODD_EQ_EVEN PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST ~) COMB ((COMB ((CONST =) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |n|)) VAR |n|)))) COMB ((COMB ((CONST +) VAR |m|)) VAR |m|))))) |bool|)) |bool|) (MULT_EXP_MONO PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |n|)) COMB ((COMB ((CONST EXP) COMB ((CONST SUC) VAR |q|))) VAR |p|)))) COMB ((COMB ((CONST *) VAR |m|)) COMB ((COMB ((CONST EXP) COMB ((CONST SUC) VAR |q|))) VAR |p|))) |bool|)) COMB ((COMB ((CONST =) VAR |n| |num|)) VAR |m| |num|) |bool|) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (MULT_SUC_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |n|)) COMB ((CONST SUC) VAR |p|)))) COMB ((COMB ((CONST *) VAR |m|)) COMB ((CONST SUC) VAR |p|))) |bool|)) COMB ((COMB ((CONST =) VAR |n| |num|)) VAR |m| |num|) |bool|) |bool|)) |bool|)) |bool|)) |bool|) (EXP_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST EXP) VAR |n|)) COMB ((COMB ((CONST +) VAR |p|)) VAR |q|)))) COMB ((COMB ((CONST *) COMB ((COMB ((CONST EXP) VAR |n|)) VAR |p|))) COMB ((COMB ((CONST EXP) VAR |n|)) VAR |q|))) |bool|)) |bool|)) |bool|)) |bool|) (LESS_SUB_ADD_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |i| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |i|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |m|)))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) VAR |i|)) VAR |m|))) VAR |n|)))) |bool|)) |bool|)) |bool|) (LESS_ADD_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST <) VAR |m|)) COMB ((COMB ((CONST +) VAR |m|)) COMB ((CONST SUC) VAR |n|))))) |bool|)) |bool|) (SUB_LESS_OR PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|))) COMB ((COMB ((CONST <=) VAR |n|)) COMB ((COMB ((CONST -) VAR |m|)) CONST |1|))))) |bool|)) |bool|) (SUB_LESS_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) CONST |0|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |m|))) |bool|)) |bool|)) |bool|) (SUB_EQ_EQ_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |m| |num|) |bool|)) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |m| |num|)) CONST |0|))) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|))) |bool|)) |bool|)) |bool|) (LESS_EQUAL_ANTISYM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST =) VAR |n| |num|)) VAR |m| |num|)))) |bool|)) |bool|) (SUB_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST -) VAR |n|)) VAR |m|))) VAR |n|))) |bool|)) |bool|) (INV_PRE_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) CONST |0|)) VAR |m|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) COMB ((CONST PRE) VAR |m|))) COMB ((CONST PRE) VAR |n|)))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))))) |bool|)) |bool|) (INV_PRE_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) CONST |0|)) VAR |m|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) COMB ((CONST PRE) VAR |m|))) COMB ((CONST PRE) VAR |n|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))))) |bool|)) |bool|) (SUB_PLUS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |a| |num|) COMB ((CONST !) ABS ((VAR |b| |num|) COMB ((CONST !) ABS ((VAR |c| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |a|)) COMB ((COMB ((CONST +) VAR |b|)) VAR |c|)))) COMB ((COMB ((CONST -) COMB ((COMB ((CONST -) VAR |a|)) VAR |b|))) VAR |c|)) |bool|)) |bool|)) |bool|)) |bool|) (SUB_MONO_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) COMB ((CONST SUC) VAR |n|))) COMB ((CONST SUC) VAR |m|)))) COMB ((COMB ((CONST -) VAR |n|)) VAR |m|)) |bool|)) |bool|)) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%0|) |bool|))))