File: BINOMIAL_integer.th

package info (click to toggle)
hol88 2.02.19940316dfsg-8
  • links: PTS
  • area: main
  • in suites: forky, sid
  • size: 65,960 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (2 lines) | stat: -rw-r--r-- 1,293 bytes parent folder | download | duplicates (11) 
1
2
 
(setq %theorydata '((parents integer more_gp BINOMIAL HOL) (types) (nametypes) (operators) (paired-infixes) (curried-infixes) (predicates) (version . "1.13 (pre-release)") (stamp . 680432812)))
(setq %theorems '((sharetypes 5 (arb%4 %VARTYPE . *) (BINTERM%3 fun (num) (integer)) (|,%2| prod (fun (integer) (fun (integer) (integer))) (prod (num) (num))) (|,%1| prod (num) (num)) (|,%0| prod (fun (integer) (fun (integer) (integer))) (fun (integer) (fun (integer) (integer))))) (axiom) (fact (LIST_OF_BINDERS pred HOL_ASSERT comb ((const BINDERS) var arb %t . arb%4) bool) (BINOMIAL_integer pred HOL_ASSERT comb ((const !) abs ((var a integer) comb ((const !) abs ((var b integer) comb ((const !) abs ((var n num) comb ((comb ((const =) comb ((comb ((comb ((const POWER) const times)) var n num)) comb ((comb ((const plus) var a)) var b)) integer)) comb ((comb ((const SIGMA) comb ((comb ((const |,|) const plus)) comb ((comb ((const |,|) const |0|)) comb ((const SUC) var n)) %t . |,%1|) %t . |,%2|)) comb ((comb ((comb ((comb ((comb ((const BINTERM) const plus)) const times)) var a integer)) var b integer)) var n num) %t . BINTERM%3) integer) bool)) bool)) bool)) bool) (RING_integer pred HOL_ASSERT comb ((const RING) comb ((comb ((const |,|) const plus)) const times) %t . |,%0|) bool))))