File: mod.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-- 6,023 bytes
parent folder | download | duplicates (11)

(SETQ %THEORYDATA '((PARENTS |da| HOL) (TYPES) (NAMETYPES) (OPERATORS) (PAIRED-INFIXES) (CURRIED-INFIXES (|Div| |fun| (|num|) (|fun| (|num|) (|num|))) (|Mod| |fun| (|num|) (|fun| (|num|) (|num|)))) (PREDICATES) (VERSION . "1.12 (Sun4/Allegro 4.0)") (STAMP . 2878303080))) 

(SETQ %THEOREMS '((SHARETYPES 1 (|arb%0| %VARTYPE . *)) (AXIOM (|Div| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Div|) VAR |k|)) VAR |n|))) COMB ((CONST @) ABS ((VAR |q| |num|) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q|)) VAR |n|))) COMB ((COMB ((CONST |Mod|) VAR |k|)) VAR |n|))) |bool|)) |num|) |bool|)) |bool|)))) (|Mod| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) VAR |k|)) 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|)) |num|) |bool|)) |bool|))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%0|) |bool|) (|Mod_Mod| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |k| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) COMB ((COMB ((CONST |Mod|) VAR |n|)) VAR |k|))) VAR |k|))) COMB ((COMB ((CONST |Mod|) VAR |n|)) VAR |k|)) |bool|))))) |bool|) (|Add_Mod| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |k| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) COMB ((COMB ((CONST +) COMB ((COMB ((CONST |Mod|) VAR |n|)) VAR |k|))) COMB ((COMB ((CONST |Mod|) VAR |m|)) VAR |k|)))) VAR |k|))) COMB ((COMB ((CONST |Mod|) COMB ((COMB ((CONST +) VAR |n|)) VAR |m|))) VAR |k|)) |bool|)) |bool|))))) |bool|) (|Mod_thm| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |k| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |r| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |n|)) VAR |k|))) VAR |r|))) VAR |k|))) COMB ((COMB ((CONST |Mod|) VAR |r|)) VAR |k|)) |bool|)) |bool|))))) |bool|) (|Mod_Rem_thm| 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 ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |m|)) VAR |n|))) VAR |k|))) VAR |n|))) VAR |k| |num|) |bool|))))) |bool|)) |bool|) (|Zero_Mod| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |k| |num|)) CONST |0|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) CONST |0|)) VAR |k|))) CONST |0|)))) |bool|) (|Mod_EQ_0| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |k| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) COMB ((COMB ((CONST *) VAR |n|)) VAR |k|))) VAR |k|))) 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|) (|Mod_One| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Mod|) VAR |k|)) CONST |1|))) CONST |0|) |bool|)) |bool|) (|Div_thm| 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_Less| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST <) COMB ((COMB ((CONST |Mod|) VAR |k|)) VAR |n|))) VAR |n|)))))) |bool|) (|Div_less_eq| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST <=) COMB ((COMB ((CONST |Div|) VAR |k|)) VAR |n|))) VAR |k|)))))) |bool|) (|Da_Div_thm| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |k| |num|) 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|))) |bool|))))) |bool|) (|Da_Mod_thm| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) COMB ((CONST !) ABS ((VAR |k| |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|))) COMB ((COMB ((CONST |Mod|) VAR |k|)) VAR |n|))))) COMB ((COMB ((CONST <) COMB ((COMB ((CONST |Mod|) VAR |k|)) VAR |n|))) VAR |n|)))) |bool|))))) |bool|))))