hol88-source 2.02.19940316-28 / usr / share / hol88-2.02.19940316 / theories / arithmetic.th

(SETQ %THEORYDATA (QUOTE ((PARENTS |fun| |prim_rec| BASIC-HOL) (TYPES) (NAMETYPES) (OPERATORS (ODD |fun| (|num|) (|bool|)) (EVEN |fun| (|num|) (|bool|)) (FACT |fun| (|num|) (|num|))) (PAIRED-INFIXES) (CURRIED-INFIXES (DIV |fun| (|num|) (|fun| (|num|) (|num|))) (MOD |fun| (|num|) (|fun| (|num|) (|num|))) (>= |fun| (|num|) (|fun| (|num|) (|bool|))) (<= |fun| (|num|) (|fun| (|num|) (|bool|))) (> |fun| (|num|) (|fun| (|num|) (|bool|))) (EXP |fun| (|num|) (|fun| (|num|) (|num|))) (* |fun| (|num|) (|fun| (|num|) (|num|))) (- |fun| (|num|) (|fun| (|num|) (|num|))) (+ |fun| (|num|) (|fun| (|num|) (|num|)))) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502449350)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 3 (P%2 |fun| (|num|) (|bool|)) (|f%1| |fun| (%VARTYPE . *) (|bool|)) (|arb%0| %VARTYPE . *)) (AXIOM (DIVISION PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) COMB ((COMB ((CONST DIV) VAR |k|)) VAR |n|))) VAR |n|))) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|))))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|))) VAR |n|))))))))) (ODD PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST ODD) CONST |0|))) CONST F))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ODD) COMB ((CONST SUC) VAR |n|)))) COMB ((CONST ~) COMB ((CONST ODD) VAR |n|))) |bool|))))) (EVEN PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST EVEN) CONST |0|))) CONST T))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST EVEN) COMB ((CONST SUC) VAR |n|)))) COMB ((CONST ~) COMB ((CONST EVEN) VAR |n|))) |bool|))))) (FACT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST FACT) CONST |0|))) CONST |1|))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST FACT) COMB ((CONST SUC) VAR |n|)))) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |n|))) COMB ((CONST FACT) VAR |n|))) |bool|))))) (GREATER_OR_EQ PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST >=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST >) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|))) |bool|)) |bool|)))) (LESS_OR_EQ PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|))) |bool|)) |bool|)))) (GREATER PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST >) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|)) |bool|)) |bool|)))) (EXP PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST EXP) VAR |m|)) CONST |0|))) CONST |1|) |bool|)))) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST EXP) VAR |m|)) COMB ((CONST SUC) VAR |n|)))) COMB ((COMB ((CONST *) VAR |m|)) COMB ((COMB ((CONST EXP) VAR |m|)) VAR |n|))) |bool|)) |bool|))))) (MULT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) CONST |0|)) VAR |n|))) CONST |0|) |bool|)))) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |m|))) VAR |n|))) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))) VAR |n|)) |bool|)) |bool|))))) (SUB PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) CONST |0|)) VAR |m|))) CONST |0|) |bool|)))) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) COMB ((CONST SUC) VAR |m|))) VAR |n|))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) CONST |0|)) COMB ((CONST SUC) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) |num|) |bool|)) |bool|))))) (ADD PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) CONST |0|)) VAR |n|))) VAR |n| |num|) |bool|)))) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) COMB ((CONST SUC) VAR |m|))) VAR |n|))) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) |bool|)) |bool|)))))) (FACT (MONOID_MULT_1 PRED HOL_ASSERT COMB ((COMB ((CONST MONOID) CONST *)) CONST |1|) |bool|) (LEFT_ID_MULT_1 PRED HOL_ASSERT COMB ((COMB ((CONST LEFT_ID) CONST *)) CONST |1|) |bool|) (RIGHT_ID_MULT_1 PRED HOL_ASSERT COMB ((COMB ((CONST RIGHT_ID) CONST *)) CONST |1|) |bool|) (ASSOC_MULT PRED HOL_ASSERT COMB ((CONST ASSOC) CONST *) |bool|) (MONOID_ADD_0 PRED HOL_ASSERT COMB ((COMB ((CONST MONOID) CONST +)) CONST |0|) |bool|) (LEFT_ID_ADD_0 PRED HOL_ASSERT COMB ((COMB ((CONST LEFT_ID) CONST +)) CONST |0|) |bool|) (RIGHT_ID_ADD_0 PRED HOL_ASSERT COMB ((COMB ((CONST RIGHT_ID) CONST +)) CONST |0|) |bool|) (ASSOC_ADD PRED HOL_ASSERT COMB ((CONST ASSOC) CONST +) |bool|) (SUB_RIGHT_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p| |num|) |bool|)) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |m| |num|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |p|)) CONST |0|)))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) VAR |m| |num|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)) |bool|)) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |m|)) CONST |0|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|)))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_RIGHT_GREATER PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST >) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST >) VAR |m|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_GREATER PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST >) VAR |m|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST >) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n|))) COMB ((COMB ((CONST >) VAR |m|)) CONST |0|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_RIGHT_GREATER_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST >=) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST >=) VAR |m|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST >=) CONST |0|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_GREATER_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST >=) VAR |m|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST >=) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n|)) |bool|)) |bool|)) |bool|)) |bool|) (SUB_RIGHT_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |m|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) CONST |0|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) VAR |m|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n|)) |bool|)) |bool|)) |bool|)) |bool|) (SUB_RIGHT_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST <=) VAR |m|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) VAR |m|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n|))) COMB ((COMB ((CONST <=) VAR |m|)) CONST |0|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST SUC) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|)))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((CONST SUC) CONST |0|))) COMB ((COMB ((CONST -) COMB ((CONST SUC) VAR |m|))) VAR |n|)) |num|) |bool|)) |bool|)) |bool|) (SUB_RIGHT_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST -) VAR |m|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |m|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|))) VAR |m| |num|)) COMB ((COMB ((CONST -) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n|)) |num|) |bool|)) |bool|)) |bool|)) |bool|) (SUB_RIGHT_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) VAR |p| |num|)) COMB ((COMB ((CONST -) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) VAR |n|)) |num|) |bool|)) |bool|)) |bool|)) |bool|) (SUB_LEFT_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) COMB ((COMB ((CONST -) VAR |n|)) VAR |p|)))) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|))) VAR |m| |num|)) COMB ((COMB ((CONST -) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) VAR |p|)) |num|) |bool|)) |bool|)) |bool|)) |bool|) (MULT_LESS_EQ_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |p|))) VAR |m|))) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |p|))) VAR |n|))) |bool|)) |bool|)) |bool|)) |bool|) (NOT_SUC_ADD_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST <=) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) VAR |m|)))) |bool|)) |bool|) (SUC_ADD_SYM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST +) COMB ((CONST SUC) VAR |n|))) VAR |m|)) |bool|)) |bool|)) |bool|) (SUC_ONE_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |n|))) COMB ((COMB ((CONST +) CONST |1|)) VAR |n|)) |bool|)) |bool|) (NOT_GREATER_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST >=) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |m|))) VAR |n|)) |bool|)) |bool|)) |bool|) (NOT_GREATER PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST >) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)) |bool|)) |bool|)) |bool|) (NOT_NUM_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|)))) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |m|))) VAR |n|))) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |n|))) VAR |m|))) |bool|)) |bool|)) |bool|) (NOT_LEQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |n|))) VAR |m|)) |bool|)) |bool|)) |bool|) (NOT_SUC_LESS_EQ_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |n|))) CONST |0|)))) |bool|) (ADD_MONO_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|)))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|)) |bool|)) |bool|)) |bool|)) |bool|) (EQ_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|))) |bool|)) |bool|)) |bool|) (ODD_EXISTS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ODD) VAR |n|))) COMB ((CONST ?) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((CONST SUC) COMB ((COMB ((CONST *) CONST |2|)) VAR |m|))) |bool|)) |bool|) |bool|)) |bool|) (EVEN_EXISTS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST EVEN) VAR |n|))) COMB ((CONST ?) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((COMB ((CONST *) CONST |2|)) VAR |m|)) |bool|)) |bool|) |bool|)) |bool|) (EVEN_ODD_EXISTS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST ==>) COMB ((CONST EVEN) VAR |n|))) COMB ((CONST ?) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((COMB ((CONST *) CONST |2|)) VAR |m|)) |bool|))))) COMB ((COMB ((CONST ==>) COMB ((CONST ODD) VAR |n|))) COMB ((CONST ?) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((CONST SUC) COMB ((COMB ((CONST *) CONST |2|)) VAR |m|))) |bool|)))))) |bool|) (ODD_DOUBLE PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ODD) COMB ((CONST SUC) COMB ((COMB ((CONST *) CONST |2|)) VAR |n|))))) |bool|) (EVEN_DOUBLE PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST EVEN) COMB ((COMB ((CONST *) CONST |2|)) VAR |n|)))) |bool|) (ODD_MULT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ODD) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST |/\\|) COMB ((CONST ODD) VAR |m|))) COMB ((CONST ODD) VAR |n|))) |bool|)) |bool|)) |bool|) (ODD_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ODD) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) COMB ((CONST ~) COMB ((COMB ((CONST =) COMB ((CONST ODD) VAR |m|))) COMB ((CONST ODD) VAR |n|)))) |bool|)) |bool|)) |bool|) (EVEN_MULT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST EVEN) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST |\\/|) COMB ((CONST EVEN) VAR |m|))) COMB ((CONST EVEN) VAR |n|))) |bool|)) |bool|)) |bool|) (EVEN_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST EVEN) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST =) COMB ((CONST EVEN) VAR |m|))) COMB ((CONST EVEN) VAR |n|)) |bool|) |bool|)) |bool|)) |bool|) (EVEN_AND_ODD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST |/\\|) COMB ((CONST EVEN) VAR |n|))) COMB ((CONST ODD) VAR |n|))))) |bool|) (EVEN_OR_ODD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |\\/|) COMB ((CONST EVEN) VAR |n|))) COMB ((CONST ODD) VAR |n|)))) |bool|) (ODD_EVEN PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ODD) VAR |n|))) COMB ((CONST ~) COMB ((CONST EVEN) VAR |n|))) |bool|)) |bool|) (EVEN_ODD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST EVEN) VAR |n|))) COMB ((CONST ~) COMB ((CONST ODD) VAR |n|))) |bool|)) |bool|) (FACT_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST <) CONST |0|)) COMB ((CONST FACT) VAR |n|)))) |bool|) (LESS_LESS_EQ_TRANS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |p|)))) |bool|)) |bool|)) |bool|) (LESS_EQ_LESS_TRANS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |p|)))) |bool|)) |bool|)) |bool|) (LESS_MULT2 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 <) CONST |0|)) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))))) |bool|)) |bool|) (MULT_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|))) CONST |0|) |bool|)) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |m| |num|)) CONST |0|))) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|))) |bool|)) |bool|)) |bool|) (LESS_EQ_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) VAR |n|)) CONST |0|))) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|) |bool|) |bool|)) |bool|) (NOT_LESS_EQUAL PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|)) |bool|)) |bool|)) |bool|) (LESS_EQ_EXISTS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((CONST ?) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|)) |bool|)) |bool|) |bool|)) |bool|)) |bool|) (LESS_EQUAL_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((CONST ?) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|)) |bool|))))) |bool|)) |bool|) (LESS_EQ_CASES PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|)))) |bool|)) |bool|) (GREATER_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|))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)) |bool|)) |bool|)) |bool|) (LESS_LESS_CASES PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|))) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|))))) |bool|)) |bool|) (LESS_EXP_SUC_MONO 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|) (TIMES2 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|) (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|) (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|) (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 |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |m| |num|) 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 ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |m|))) COMB ((CONST !) ABS ((VAR |n| |num|) 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|) (MOD_MOD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|))) VAR |n|))) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|)) |bool|))))) |bool|) (MOD_PLUS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |j| |num|) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) COMB ((COMB ((CONST +) COMB ((COMB ((CONST MOD) VAR |j|)) VAR |n|))) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|)))) VAR |n|))) COMB ((COMB ((CONST MOD) COMB ((COMB ((CONST +) VAR |j|)) VAR |k|))) VAR |n|)) |bool|)) |bool|))))) |bool|) (MOD_TIMES PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((CONST !) ABS ((VAR |r| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) VAR |r|))) VAR |n|))) COMB ((COMB ((CONST MOD) VAR |r|)) VAR |n|)) |bool|)) |bool|))))) |bool|) (MOD_MULT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |r| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |r|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) VAR |r|))) VAR |n|))) VAR |r| |num|) |bool|))))) |bool|)) |bool|) (ZERO_DIV PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST DIV) CONST |0|)) VAR |n|))) CONST |0|)))) |bool|) (ZERO_MOD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) CONST |0|)) VAR |n|))) CONST |0|)))) |bool|) (MOD_EQ_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) COMB ((COMB ((CONST *) VAR |k|)) VAR |n|))) VAR |n|))) CONST |0|) |bool|))))) |bool|) (LESS_MOD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |k|)) VAR |n|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|))) VAR |k| |num|)))) |bool|)) |bool|) (DIV_MULT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |r| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |r|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST DIV) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) VAR |r|))) VAR |n|))) VAR |q| |num|) |bool|))))) |bool|)) |bool|) (MOD_UNIQUE PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((CONST !) ABS ((VAR |r| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ?) ABS ((VAR |q| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) VAR |r|)))) COMB ((COMB ((CONST <) VAR |r|)) VAR |n|)))))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) VAR |k|)) VAR |n|))) VAR |r| |num|)))) |bool|)) |bool|)) |bool|) (DIV_UNIQUE PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ?) ABS ((VAR |r| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) VAR |r|)))) COMB ((COMB ((CONST <) VAR |r|)) VAR |n|)))))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST DIV) VAR |k|)) VAR |n|))) VAR |q| |num|)))) |bool|)) |bool|)) |bool|) (DIV_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST DIV) VAR |k|)) VAR |n|))) VAR |k|)))))) |bool|) (MOD_ONE PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MOD) VAR |k|)) COMB ((CONST SUC) CONST |0|)))) CONST |0|) |bool|)) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%0|) |bool|) (DA PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((CONST ?) ABS ((VAR |r| |num|) COMB ((CONST ?) ABS ((VAR |q| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) VAR |r|)))) COMB ((COMB ((CONST <) VAR |r|)) VAR |n|)))) |bool|))))) |bool|)) |bool|) (WOP PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((COMB ((CONST ==>) COMB ((CONST ?) ABS ((VAR |n| |num|) COMB ((VAR P %T . P%2) VAR |n|))))) COMB ((CONST ?) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . P%2) VAR |n|))) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((CONST ~) COMB ((VAR P %T . P%2) VAR |m|))))))))))) |bool|) (LESS_OR_EQ_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| |num|)) COMB ((COMB ((CONST +) VAR |p|)) VAR |m|)) |bool|))))) |bool|)) |bool|) (LESS_EQ_MONO 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|) (ZERO_LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST <=) CONST |0|)) VAR |n|))) |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|) (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|) (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|) (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|) (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_ADD_1 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 ((CONST ?) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) VAR |m| |num|)) COMB ((COMB ((CONST +) VAR |n|)) COMB ((COMB ((CONST +) VAR |p|)) CONST |1|))) |bool|))))) |bool|)) |bool|) (LEFT_SUB_DISTRIB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |p|)) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST -) COMB ((COMB ((CONST *) VAR |p|)) VAR |m|))) COMB ((COMB ((CONST *) VAR |p|)) VAR |n|))) |bool|)) |bool|)) |bool|)) |bool|) (RIGHT_SUB_DISTRIB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST -) COMB ((COMB ((CONST *) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST *) VAR |n|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (LESS_MONO_MULT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST *) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST *) VAR |n|)) VAR |p|))))) |bool|)) |bool|)) |bool|) (LESS_IMP_LESS_OR_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)))) |bool|)) |bool|) (LESS_EQ_REFL PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |m|))) |bool|) (LESS_EQ_LESS_EQ_MONO PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((CONST !) ABS ((VAR |q| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |q|)))) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST +) VAR |p|)) VAR |q|))))) |bool|)) |bool|)) |bool|)) |bool|) (LESS_EQ_TRANS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |p|)))) |bool|)) |bool|)) |bool|) (LESS_EQ_MONO_ADD_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)) |bool|)) |bool|)) |bool|)) |bool|) (EQ_MONO_ADD_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)) |bool|)) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|) |bool|) |bool|)) |bool|)) |bool|)) |bool|) (LESS_MONO_ADD_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|)) |bool|)) |bool|)) |bool|)) |bool|) (LESS_MONO_ADD_INV PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|)))) |bool|)) |bool|)) |bool|) (LESS_MONO_ADD PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST +) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|))))) |bool|)) |bool|)) |bool|) (ADD_EQ_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) VAR |n|)) VAR |p|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) VAR |p| |num|) |bool|)) COMB ((COMB ((CONST =) VAR |m| |num|)) COMB ((COMB ((CONST -) VAR |p|)) VAR |n|)) |bool|)))) |bool|)) |bool|)) |bool|) (LESS_SUC_NOT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((CONST ~) COMB ((COMB ((CONST <) VAR |n|)) COMB ((CONST SUC) VAR |m|)))))) |bool|)) |bool|) (INV_PRE_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|)) |bool|)) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|) |bool|)))) |bool|)) |bool|) (PRE_SUC_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) CONST |0|)) VAR |n|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) VAR |m| |num|)) COMB ((CONST PRE) VAR |n|)) |bool|)) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |m|))) VAR |n| |num|) |bool|)))) |bool|)) |bool|) (ADD_INV_0_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 +) VAR |m|)) VAR |n|))) VAR |m| |num|) |bool|)) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|) |bool|) |bool|)) |bool|)) |bool|) (ADD_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|))) CONST |0|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |m| |num|)) CONST |0|))) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|))) |bool|)) |bool|)) |bool|) (PRE_SUB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST PRE) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST -) COMB ((CONST PRE) VAR |m|))) VAR |n|)) |bool|)) |bool|)) |bool|) (SUB_ADD 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 =) COMB ((COMB ((CONST +) COMB ((COMB ((CONST -) VAR |m|)) VAR |n|))) VAR |n|))) VAR |m| |num|)))) |bool|)) |bool|) (MULT_ASSOC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) COMB ((COMB ((CONST *) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST *) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))) VAR |p|)) |bool|)) |bool|)) |bool|)) |bool|) (LEFT_ADD_DISTRIB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |p|)) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |p|)) VAR |m|))) COMB ((COMB ((CONST *) VAR |p|)) VAR |n|))) |bool|)) |bool|)) |bool|)) |bool|) (RIGHT_ADD_DISTRIB PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) VAR |p|))) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |m|)) VAR |p|))) COMB ((COMB ((CONST *) VAR |n|)) VAR |p|))) |bool|)) |bool|)) |bool|)) |bool|) (MULT_SYM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST *) VAR |n|)) VAR |m|)) |bool|)) |bool|)) |bool|) (MULT_CLAUSES 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|))) CONST |0|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) CONST |0|))) CONST |0|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) CONST |1|)) VAR |m|))) VAR |m| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) CONST |1|))) VAR |m| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) COMB ((CONST SUC) VAR |m|))) VAR |n|))) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))) VAR |n|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) COMB ((CONST SUC) VAR |n|)))) COMB ((COMB ((CONST +) VAR |m|)) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|)))))))))) |bool|)) |bool|) (MULT_RIGHT_1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) CONST |1|))) VAR |m| |num|) |bool|)) |bool|) (MULT_LEFT_1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) CONST |1|)) VAR |m|))) VAR |m| |num|) |bool|)) |bool|) (MULT_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) COMB ((CONST SUC) VAR |n|)))) COMB ((COMB ((CONST +) VAR |m|)) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))) |bool|)) |bool|)) |bool|) (MULT_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST *) VAR |m|)) CONST |0|))) CONST |0|) |bool|)) |bool|) (ADD_ASSOC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) COMB ((COMB ((CONST +) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST +) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) VAR |p|)) |bool|)) |bool|)) |bool|)) |bool|) (SUB_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|))) CONST |0|) |bool|)) COMB ((COMB ((CONST <=) VAR |m|)) VAR |n|)) |bool|)) |bool|)) |bool|) (NOT_LESS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST ~) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|)) |bool|)) |bool|)) |bool|) (LESS_EQ_ANTISYM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|))))) |bool|)) |bool|) (LESS_ADD_NONZERO PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) COMB ((COMB ((CONST <) VAR |m|)) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))))) |bool|)) |bool|) (LESS_EQ_SUC_REFL PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST <=) VAR |m|)) COMB ((CONST SUC) VAR |m|)))) |bool|) (LESS_EQ_ADD 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|)) VAR |n|)))) |bool|)) |bool|) (ADD_INV_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|))) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) |bool|)) |bool|) (LESS_CASES PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) VAR |n|)) VAR |m|)))) |bool|)) |bool|) (LESS_CASES_IMP PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((CONST ~) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|)))) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |m| |num|)) VAR |n| |num|))))) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|)))) |bool|)) |bool|) (LESS_0_CASES PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) CONST |0|)) VAR |m| |num|))) COMB ((COMB ((CONST <) CONST |0|)) VAR |m|)))) |bool|) (LESS_NOT_SUC 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|))) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) COMB ((CONST SUC) VAR |m|)))))) COMB ((COMB ((CONST <) COMB ((CONST SUC) VAR |m|))) VAR |n|)))) |bool|)) |bool|) (LESS_SUC_EQ_COR 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|))) COMB ((CONST ~) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |m|))) VAR |n| |num|))))) COMB ((COMB ((CONST <) COMB ((CONST SUC) VAR |m|))) VAR |n|)))) |bool|)) |bool|) (LESS_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |m|))) VAR |n|)) |bool|)) |bool|)) |bool|) (OR_LESS 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|))) VAR |n|))) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|)))) |bool|)) |bool|) (LESS_OR PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <=) COMB ((CONST SUC) VAR |m|))) VAR |n|)))) |bool|)) |bool|) (FUN_EQ_LEMMA PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%1|) COMB ((CONST !) ABS ((VAR |x1| %T . |arb%0|) COMB ((CONST !) ABS ((VAR |x2| %T . |arb%0|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((VAR |f| %T . |f%1|) VAR |x1|))) COMB ((CONST ~) COMB ((VAR |f| %T . |f%1|) VAR |x2|))))) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |x1| %T . |arb%0|)) VAR |x2| %T . |arb%0|))))) |bool|)) |bool|)) |bool|) (LESS_LESS_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |n|)) COMB ((CONST SUC) VAR |m|)))))) |bool|)) |bool|) (LESS_ANTISYM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |n|)) VAR |m|))))) |bool|)) |bool|) (ADD1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((CONST SUC) VAR |m|))) COMB ((COMB ((CONST +) VAR |m|)) CONST |1|)) |bool|)) |bool|) (LESS_TRANS PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |p| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |n|)) VAR |p|)))) COMB ((COMB ((CONST <) VAR |m|)) VAR |p|)))) |bool|)) |bool|)) |bool|) (SUB_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) CONST |0|)) VAR |m|))) CONST |0|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) VAR |m|)) CONST |0|))) VAR |m| |num|)))) |bool|) (LESS_ADD 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 ((CONST ?) ABS ((VAR |p| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |p|)) VAR |n|))) VAR |m| |num|) |bool|))))) |bool|)) |bool|) (PRE_SUB1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((CONST PRE) VAR |m|))) COMB ((COMB ((CONST -) VAR |m|)) CONST |1|)) |bool|)) |bool|) (SUC_SUB1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST -) COMB ((CONST SUC) VAR |m|))) CONST |1|))) VAR |m| |num|) |bool|)) |bool|) (LESS_MONO_EQ 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|)) VAR |n|)) |bool|)) |bool|)) |bool|) (LESS_MONO_REV 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|)) VAR |n|)))) |bool|)) |bool|) (|num_CASES| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |m| |num|)) CONST |0|))) COMB ((CONST ?) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) VAR |m| |num|)) COMB ((CONST SUC) VAR |n|)) |bool|))))) |bool|) (ADD_SYM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))) COMB ((COMB ((CONST +) VAR |n|)) VAR |m|)) |bool|)) |bool|)) |bool|) (ADD_CLAUSES PRED HOL_ASSERT COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) CONST |0|)) VAR |m|))) VAR |m| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) CONST |0|))) VAR |m| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) COMB ((CONST SUC) VAR |m|))) VAR |n|))) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) COMB ((CONST SUC) VAR |n|)))) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))))))) (ADD_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST +) VAR |m|)) COMB ((CONST SUC) VAR |n|))) |bool|)) |bool|)) |bool|) (ADD_0 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) CONST |0|))) VAR |m| |num|) |bool|)) |bool|) (SUC_NOT PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST ~) COMB ((COMB ((CONST =) CONST |0|)) COMB ((CONST SUC) VAR |n|))))) |bool|)))))