File: prims.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-- 5,666 bytes
parent folder | download | duplicates (9)

(SETQ %THEORYDATA (QUOTE ((PARENTS HOL) (TYPES) (NAMETYPES) (OPERATORS (ZERO |fun| (|fun| (|num|) (|num|)) (|bool|)) (OR_GATE |fun| (|prod| (|fun| (|num|) (|bool|)) (|prod| (|fun| (|num|) (|bool|)) (|fun| (|num|) (|bool|)))) (|bool|)) (ZERO_TEST |fun| (|prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|bool|))) (|bool|)) (ADDER |fun| (|prod| (|fun| (|num|) (|num|)) (|prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|num|)))) (|bool|)) (DEC |fun| (|prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|num|))) (|bool|)) (FLIPFLOP |fun| (|prod| (|fun| (|num|) (|bool|)) (|fun| (|num|) (|bool|))) (|bool|)) (REG |fun| (|prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|num|))) (|bool|)) (MUX |fun| (|prod| (|fun| (|num|) (|bool|)) (|prod| (|fun| (|num|) (|num|)) (|prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|num|))))) (|bool|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.01 (SUN4/AKCL)") (STAMP . 2940578553)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 6 (|arb%5| %VARTYPE . *) (|,%4| |prod| (|fun| (|num|) (|bool|)) (|fun| (|num|) (|bool|))) (|,%3| |prod| (|fun| (|num|) (|num|)) (|prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|num|)))) (|,%2| |prod| (|fun| (|num|) (|num|)) (|fun| (|num|) (|num|))) (|i1%1| |fun| (|num|) (|num|)) (|switch%0| |fun| (|num|) (|bool|))) (AXIOM (ZERO PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |out| %T . |i1%1|) COMB ((COMB ((CONST =) COMB ((CONST ZERO) VAR |out|))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |i1%1|) VAR |x|))) CONST |0|) |bool|)) |bool|) |bool|)))) (OR_GATE PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i1| %T . |switch%0|) COMB ((CONST !) ABS ((VAR |i2| %T . |switch%0|) COMB ((CONST !) ABS ((VAR |out| %T . |switch%0|) COMB ((COMB ((CONST =) COMB ((CONST OR_GATE) COMB ((COMB ((CONST |,|) VAR |i1| %T . |switch%0|)) COMB ((COMB ((CONST |,|) VAR |i2| %T . |switch%0|)) VAR |out| %T . |switch%0|) %T . |,%4|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |switch%0|) VAR |x|))) COMB ((COMB ((CONST |\\/|) COMB ((VAR |i1| %T . |switch%0|) VAR |x|))) COMB ((VAR |i2| %T . |switch%0|) VAR |x|))) |bool|)) |bool|) |bool|)) |bool|)) |bool|)))) (ZERO_TEST PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |out| %T . |switch%0|) COMB ((COMB ((CONST =) COMB ((CONST ZERO_TEST) COMB ((COMB ((CONST |,|) VAR |i| %T . |i1%1|)) VAR |out| %T . |switch%0|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |switch%0|) VAR |x|))) COMB ((COMB ((CONST =) COMB ((VAR |i| %T . |i1%1|) VAR |x|))) CONST |0|) |bool|) |bool|)) |bool|) |bool|)) |bool|)))) (ADDER PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i1| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |i2| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |out| %T . |i1%1|) COMB ((COMB ((CONST =) COMB ((CONST ADDER) COMB ((COMB ((CONST |,|) VAR |i1| %T . |i1%1|)) COMB ((COMB ((CONST |,|) VAR |i2| %T . |i1%1|)) VAR |out| %T . |i1%1|) %T . |,%2|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |i1%1|) VAR |x|))) COMB ((COMB ((CONST +) COMB ((VAR |i1| %T . |i1%1|) VAR |x|))) COMB ((VAR |i2| %T . |i1%1|) VAR |x|))) |bool|)) |bool|) |bool|)) |bool|)) |bool|)))) (DEC PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |out| %T . |i1%1|) COMB ((COMB ((CONST =) COMB ((CONST DEC) COMB ((COMB ((CONST |,|) VAR |i| %T . |i1%1|)) VAR |out| %T . |i1%1|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |i1%1|) VAR |x|))) COMB ((COMB ((CONST -) COMB ((VAR |i| %T . |i1%1|) VAR |x|))) CONST |1|)) |bool|)) |bool|) |bool|)) |bool|)))) (FLIPFLOP PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i| %T . |switch%0|) COMB ((CONST !) ABS ((VAR |out| %T . |switch%0|) COMB ((COMB ((CONST =) COMB ((CONST FLIPFLOP) COMB ((COMB ((CONST |,|) VAR |i| %T . |switch%0|)) VAR |out| %T . |switch%0|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |switch%0|) COMB ((COMB ((CONST +) VAR |x|)) CONST |1|)))) COMB ((VAR |i| %T . |switch%0|) VAR |x|)) |bool|)) |bool|) |bool|)) |bool|)))) (REG PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |out| %T . |i1%1|) COMB ((COMB ((CONST =) COMB ((CONST REG) COMB ((COMB ((CONST |,|) VAR |i| %T . |i1%1|)) VAR |out| %T . |i1%1|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |i1%1|) COMB ((COMB ((CONST +) VAR |x|)) CONST |1|)))) COMB ((VAR |i| %T . |i1%1|) VAR |x|)) |bool|)) |bool|) |bool|)) |bool|)))) (MUX PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |switch| %T . |switch%0|) COMB ((CONST !) ABS ((VAR |i1| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |i2| %T . |i1%1|) COMB ((CONST !) ABS ((VAR |out| %T . |i1%1|) COMB ((COMB ((CONST =) COMB ((CONST MUX) COMB ((COMB ((CONST |,|) VAR |switch| %T . |switch%0|)) COMB ((COMB ((CONST |,|) VAR |i1| %T . |i1%1|)) COMB ((COMB ((CONST |,|) VAR |i2| %T . |i1%1|)) VAR |out| %T . |i1%1|) %T . |,%2|) %T . |,%3|)))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST =) COMB ((VAR |out| %T . |i1%1|) VAR |x|))) COMB ((COMB ((COMB ((CONST COND) COMB ((VAR |switch| %T . |switch%0|) VAR |x|))) COMB ((VAR |i1| %T . |i1%1|) VAR |x|))) COMB ((VAR |i2| %T . |i1%1|) VAR |x|)) |num|) |bool|)) |bool|) |bool|)) |bool|)) |bool|)) |bool|))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%5|) |bool|)))))