File: da.th

package info (click to toggle)
hol88 2.02.19940316-35.1
  • links: PTS
  • area: main
  • in suites: bullseye
  • size: 66,004 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (4 lines) | stat: -rw-r--r-- 2,306 bytes parent folder | download | duplicates (9) 
1
2
3
4
 

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

(SETQ %THEOREMS '((SHARETYPES 1 (|arb%0| %VARTYPE . *)) (AXIOM) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%0|) |bool|) (|Remainder_Unique| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |r1| |num|) COMB ((CONST !) ABS ((VAR |r2| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |r1|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |r2|)) VAR |n|)))) COMB ((COMB ((CONST ==>) COMB ((CONST ?) ABS ((VAR |q1| |num|) COMB ((CONST ?) ABS ((VAR |q2| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q1|)) VAR |n|))) VAR |r1|))) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q2|)) VAR |n|))) VAR |r2|)) |bool|)) |bool|)))) COMB ((COMB ((CONST =) VAR |r1| |num|)) VAR |r2| |num|))))) |bool|)) |bool|)) |bool|) (|Quotient_Unique| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |r1| |num|) COMB ((CONST !) ABS ((VAR |r2| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |r1|)) VAR |n|))) COMB ((COMB ((CONST <) VAR |r2|)) VAR |n|)))) COMB ((CONST !) ABS ((VAR |q1| |num|) COMB ((CONST !) ABS ((VAR |q2| |num|) COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q1|)) VAR |n|))) VAR |r1|)))) COMB ((COMB ((CONST =) VAR |k| |num|)) COMB ((COMB ((CONST +) COMB ((COMB ((CONST *) VAR |q2|)) VAR |n|))) VAR |r2|))))) COMB ((COMB ((CONST =) VAR |q1| |num|)) VAR |q2| |num|)))) |bool|)) |bool|))))) |bool|)) |bool|)) |bool|) (|Da| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |k| |num|) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((COMB ((CONST ==>) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |n| |num|)) CONST |0|)))) 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|))))