hol88-source 2.02.19940316-28 / usr / share / hol88-2.02.19940316 / theories / fun.th

(SETQ %THEORYDATA (QUOTE ((PARENTS BASIC-HOL) (TYPES) (NAMETYPES) (OPERATORS (MONOID |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (|fun| (%VARTYPE . *) (|bool|))) (LEFT_ID |fun| (|fun| (%VARTYPE . **) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (|fun| (%VARTYPE . **) (|bool|))) (RIGHT_ID |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . *))) (|fun| (%VARTYPE . **) (|bool|))) (FCOMM |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . *))) (|fun| (|fun| (%VARTYPE . ***) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (|bool|))) (COMM |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . **))) (|bool|)) (ASSOC |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (|bool|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502448625)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 8 (|f%7| |fun| (%VARTYPE . **) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (|z%6| %VARTYPE . **) (|x%5| %VARTYPE . ***) (|g%4| |fun| (%VARTYPE . ***) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (|f%3| |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . *))) (|f%2| |fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . **))) (|x%1| %VARTYPE . *) (|f%0| |fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . *)))) (AXIOM (MONOID_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%0|) COMB ((CONST !) ABS ((VAR |e| %T . |x%1|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MONOID) VAR |f| %T . |f%0|)) VAR |e| %T . |x%1|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((CONST ASSOC) VAR |f| %T . |f%0|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST RIGHT_ID) VAR |f| %T . |f%0|)) VAR |e| %T . |x%1|))) COMB ((COMB ((CONST LEFT_ID) VAR |f| %T . |f%0|)) VAR |e| %T . |x%1|)))) |bool|)) |bool|)))) (LEFT_ID_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%7|) COMB ((CONST !) ABS ((VAR |e| %T . |z%6|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST LEFT_ID) VAR |f| %T . |f%7|)) VAR |e| %T . |z%6|) |bool|)) COMB ((CONST !) ABS ((VAR |x| %T . |x%1|) COMB ((COMB ((CONST =) COMB ((COMB ((VAR |f| %T . |f%7|) VAR |e|)) VAR |x|))) VAR |x| %T . |x%1|) |bool|)) |bool|) |bool|)) |bool|)))) (RIGHT_ID_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%3|) COMB ((CONST !) ABS ((VAR |e| %T . |z%6|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST RIGHT_ID) VAR |f| %T . |f%3|)) VAR |e| %T . |z%6|) |bool|)) COMB ((CONST !) ABS ((VAR |x| %T . |x%1|) COMB ((COMB ((CONST =) COMB ((COMB ((VAR |f| %T . |f%3|) VAR |x|)) VAR |e|))) VAR |x| %T . |x%1|) |bool|)) |bool|) |bool|)) |bool|)))) (FCOMM_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%3|) COMB ((CONST !) ABS ((VAR |g| %T . |g%4|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST FCOMM) VAR |f| %T . |f%3|)) VAR |g| %T . |g%4|) |bool|)) COMB ((CONST !) ABS ((VAR |x| %T . |x%5|) COMB ((CONST !) ABS ((VAR |y| %T . |x%1|) COMB ((CONST !) ABS ((VAR |z| %T . |z%6|) COMB ((COMB ((CONST =) COMB ((COMB ((VAR |g| %T . |g%4|) VAR |x|)) COMB ((COMB ((VAR |f| %T . |f%3|) VAR |y|)) VAR |z|)))) COMB ((COMB ((VAR |f| %T . |f%3|) COMB ((COMB ((VAR |g| %T . |g%4|) VAR |x|)) VAR |y|))) VAR |z|)) |bool|)) |bool|)) |bool|)) |bool|) |bool|)) |bool|)))) (COMM_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%2|) COMB ((COMB ((CONST =) COMB ((CONST COMM) VAR |f| %T . |f%2|) |bool|)) COMB ((CONST !) ABS ((VAR |x| %T . |x%1|) COMB ((CONST !) ABS ((VAR |y| %T . |x%1|) COMB ((COMB ((CONST =) COMB ((COMB ((VAR |f| %T . |f%2|) VAR |x|)) VAR |y|))) COMB ((COMB ((VAR |f| %T . |f%2|) VAR |y|)) VAR |x|)) |bool|)) |bool|)) |bool|) |bool|)))) (ASSOC_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%0|) COMB ((COMB ((CONST =) COMB ((CONST ASSOC) VAR |f| %T . |f%0|) |bool|)) COMB ((CONST !) ABS ((VAR |x| %T . |x%1|) COMB ((CONST !) ABS ((VAR |y| %T . |x%1|) COMB ((CONST !) ABS ((VAR |z| %T . |x%1|) COMB ((COMB ((CONST =) COMB ((COMB ((VAR |f| %T . |f%0|) VAR |x|)) COMB ((COMB ((VAR |f| %T . |f%0|) VAR |y|)) VAR |z|)))) COMB ((COMB ((VAR |f| %T . |f%0|) COMB ((COMB ((VAR |f| %T . |f%0|) VAR |x|)) VAR |y|))) VAR |z|)) |bool|)) |bool|)) |bool|)) |bool|) |bool|))))) (FACT (MONOID_DISJ_F PRED HOL_ASSERT COMB ((COMB ((CONST MONOID) CONST |\\/|)) CONST F) |bool|) (MONOID_CONJ_T PRED HOL_ASSERT COMB ((COMB ((CONST MONOID) CONST |/\\|)) CONST T) |bool|) (FCOMM_ASSOC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%0|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST FCOMM) VAR |f| %T . |f%0|)) VAR |f| %T . |f%0|) |bool|)) COMB ((CONST ASSOC) VAR |f| %T . |f%0|) |bool|) |bool|)) |bool|) (ASSOC_DISJ PRED HOL_ASSERT COMB ((CONST ASSOC) CONST |\\/|) |bool|) (ASSOC_CONJ PRED HOL_ASSERT COMB ((CONST ASSOC) CONST |/\\|) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |x%1|) |bool|)))))