File: pred.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-- 6,303 bytes
parent folder | download | duplicates (9)

(SETQ %THEORYDATA (QUOTE ((PARENTS |exseq| |string| |more_arithmetic| HOL) (TYPES) (NAMETYPES) (OPERATORS (|subs| |fun| (|fun| (|fun| (|string|) (|num|)) (|num|)) (|fun| (|string|) (|fun| (|fun| (|fun| (|string|) (|num|)) (|bool|)) (|fun| (|fun| (|string|) (|num|)) (|bool|))))) (|forsome| |fun| (|string|) (|fun| (|fun| (|fun| (|string|) (|num|)) (|bool|)) (|fun| (|fun| (|string|) (|num|)) (|bool|)))) (|forevery| |fun| (|string|) (|fun| (|fun| (|fun| (|string|) (|num|)) (|bool|)) (|fun| (|fun| (|string|) (|num|)) (|bool|)))) (|bnd| |fun| (|num|) (|fun| (|string|) (|fun| (|fun| (|string|) (|num|)) (|fun| (|string|) (|num|))))) (SW |fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (EWR |fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (NOT |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (%VARTYPE . *) (|bool|))) (|true| |fun| (%VARTYPE . *) (|bool|)) (|false| |fun| (%VARTYPE . *) (|bool|))) (PAIRED-INFIXES) (CURRIED-INFIXES (IMPLIES |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (%VARTYPE . *) (|bool|)))) (AND |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (%VARTYPE . *) (|bool|)))) (OR |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (%VARTYPE . *) (|bool|))))) (PREDICATES) (VERSION . "2.01 (SUN4/AKCL: pre-release)") (STAMP . 2932130060)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 5 (|exp%4| |fun| (|fun| (|string|) (|num|)) (|num|)) (P%3 |fun| (|fun| (|string|) (|num|)) (|bool|)) (|s%2| |fun| (|string|) (|num|)) (|s%1| %VARTYPE . *) (|false%0| |fun| (%VARTYPE . *) (|bool|))) (AXIOM (|subs| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |exp| %T . |exp%4|) COMB ((CONST !) ABS ((VAR |x| |string|) COMB ((CONST !) ABS ((VAR P %T . P%3) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((CONST |subs|) VAR |exp|)) VAR |x|)) VAR P))) ABS ((VAR |s| %T . |s%2|) COMB ((VAR P %T . P%3) COMB ((COMB ((COMB ((CONST |bnd|) COMB ((VAR |exp| %T . |exp%4|) VAR |s|))) VAR |x|)) VAR |s|)))) |bool|)) |bool|)) |bool|)))) (|forsome| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%3) COMB ((CONST !) ABS ((VAR |x| |string|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |forsome|) VAR |x|)) VAR P))) ABS ((VAR |s| %T . |s%2|) COMB ((CONST ?) ABS ((VAR |val| |num|) COMB ((VAR P %T . P%3) COMB ((COMB ((COMB ((CONST |bnd|) VAR |val|)) VAR |x|)) VAR |s|)))) |bool|)) |bool|)) |bool|)))) (|forevery| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%3) COMB ((CONST !) ABS ((VAR |x| |string|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |forevery|) VAR |x|)) VAR P))) ABS ((VAR |s| %T . |s%2|) COMB ((CONST !) ABS ((VAR |val| |num|) COMB ((VAR P %T . P%3) COMB ((COMB ((COMB ((CONST |bnd|) VAR |val|)) VAR |x|)) VAR |s|)))) |bool|)) |bool|)) |bool|)))) (|bnd| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |x| |string|) COMB ((CONST !) ABS ((VAR |s| %T . |s%2|) COMB ((CONST !) ABS ((VAR |value| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((CONST |bnd|) VAR |value|)) VAR |x|)) VAR |s|))) ABS ((VAR |z| |string|) COMB ((COMB ((COMB ((CONST COND) COMB ((COMB ((CONST =) VAR |z| |string|)) VAR |x| |string|) |bool|)) VAR |value| |num|)) COMB ((VAR |s| %T . |s%2|) VAR |z|)) |num|)) |bool|)) |bool|)) |bool|)))) (SW PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |false%0|) COMB ((COMB ((CONST =) COMB ((CONST SW) VAR |p| %T . |false%0|) |bool|)) COMB ((CONST ?) ABS ((VAR |t| %T . |s%1|) COMB ((VAR |p| %T . |false%0|) VAR |t|))) |bool|) |bool|)))) (EWR PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |false%0|) COMB ((COMB ((CONST =) COMB ((CONST EWR) VAR |p| %T . |false%0|) |bool|)) COMB ((CONST !) ABS ((VAR |t| %T . |s%1|) COMB ((VAR |p| %T . |false%0|) VAR |t|))) |bool|) |bool|)))) (IMPLIES PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |b| %T . |false%0|) COMB ((CONST !) ABS ((VAR |b'| %T . |false%0|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST IMPLIES) VAR |b| %T . |false%0|)) VAR |b'| %T . |false%0|) %T . |false%0|)) ABS ((VAR |s| %T . |s%1|) COMB ((COMB ((CONST ==>) COMB ((VAR |b| %T . |false%0|) VAR |s|))) COMB ((VAR |b'| %T . |false%0|) VAR |s|)))) |bool|)) |bool|)))) (AND PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |b| %T . |false%0|) COMB ((CONST !) ABS ((VAR |b'| %T . |false%0|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST AND) VAR |b| %T . |false%0|)) VAR |b'| %T . |false%0|) %T . |false%0|)) ABS ((VAR |s| %T . |s%1|) COMB ((COMB ((CONST |/\\|) COMB ((VAR |b| %T . |false%0|) VAR |s|))) COMB ((VAR |b'| %T . |false%0|) VAR |s|)))) |bool|)) |bool|)))) (OR PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |b| %T . |false%0|) COMB ((CONST !) ABS ((VAR |b'| %T . |false%0|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST OR) VAR |b| %T . |false%0|)) VAR |b'| %T . |false%0|) %T . |false%0|)) ABS ((VAR |s| %T . |s%1|) COMB ((COMB ((CONST |\\/|) COMB ((VAR |b| %T . |false%0|) VAR |s|))) COMB ((VAR |b'| %T . |false%0|) VAR |s|)))) |bool|)) |bool|)))) (NOT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |b| %T . |false%0|) COMB ((COMB ((CONST =) COMB ((CONST NOT) VAR |b| %T . |false%0|) %T . |false%0|)) ABS ((VAR |s| %T . |s%1|) COMB ((CONST ~) COMB ((VAR |b| %T . |false%0|) VAR |s|)))) |bool|)))) (ALL PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |true| %T . |false%0|)) ABS ((VAR |s| %T . |s%1|) CONST T)))) (NONE PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |false| %T . |false%0|)) ABS ((VAR |s| %T . |s%1|) CONST F))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |s%1|) |bool|) (PRED_AND_OVER_FORALL PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . |false%0|) COMB ((CONST !) ABS ((VAR Q %T . |false%0|) COMB ((COMB ((CONST =) COMB ((CONST !) ABS ((VAR |s| %T . |s%1|) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . |false%0|) VAR |s|))) COMB ((VAR Q %T . |false%0|) VAR |s|)))) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |s| %T . |s%1|) COMB ((VAR P %T . |false%0|) VAR |s|))))) COMB ((CONST !) ABS ((VAR |s| %T . |s%1|) COMB ((VAR Q %T . |false%0|) VAR |s|))))) |bool|)) |bool|)) |bool|)))))