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

(SETQ %THEORYDATA (QUOTE ((PARENTS BASIC-HOL) (TYPES) (NAMETYPES) (OPERATORS (I |fun| (%VARTYPE . *) (%VARTYPE . *)) (S |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . ***))) (|fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (%VARTYPE . ***)))) (K |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . *)))) (PAIRED-INFIXES) (CURRIED-INFIXES (|o| |fun| (|fun| (%VARTYPE . **) (%VARTYPE . ***)) (|fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (%VARTYPE . ***))))) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502444995)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 16 (I%15 |fun| (%VARTYPE . **) (%VARTYPE . **)) (|o%14| |fun| (%VARTYPE . **) (%VARTYPE . ****)) (|o%13| |fun| (%VARTYPE . *) (%VARTYPE . ****)) (|f%12| |fun| (%VARTYPE . ***) (%VARTYPE . ****)) (|o%11| %VARTYPE . ***) (K%10 |fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . *))) (K%9 |fun| (%VARTYPE . *) (|fun| (|fun| (%VARTYPE . *) (%VARTYPE . *)) (%VARTYPE . *))) (I%8 |fun| (%VARTYPE . *) (%VARTYPE . *)) (|f%7| |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . ***))) (S%6 |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . ***))) (|fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (%VARTYPE . ***)))) (|y%5| %VARTYPE . **) (K%4 |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . *))) (|x%3| %VARTYPE . *) (|o%2| |fun| (%VARTYPE . *) (%VARTYPE . ***)) (|g%1| |fun| (%VARTYPE . *) (%VARTYPE . **)) (|f%0| |fun| (%VARTYPE . **) (%VARTYPE . ***))) (AXIOM (I_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST I %T . I%8)) COMB ((COMB ((CONST S) CONST K %T . K%9)) CONST K %T . K%10) %T . I%8))) (S_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST S %T . S%6)) ABS ((VAR |f| %T . |f%7|) ABS ((VAR |g| %T . |g%1|) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((VAR |f| %T . |f%7|) VAR |x|)) COMB ((VAR |g| %T . |g%1|) VAR |x|)))))))) (K_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST K %T . K%4)) ABS ((VAR |x| %T . |x%3|) ABS ((VAR |y| %T . |y%5|) VAR |x| %T . |x%3|))))) (|o_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%0|) COMB ((CONST !) ABS ((VAR |g| %T . |g%1|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |o|) VAR |f| %T . |f%0|)) VAR |g| %T . |g%1|) %T . |o%2|)) ABS ((VAR |x| %T . |x%3|) COMB ((VAR |f| %T . |f%0|) COMB ((VAR |g| %T . |g%1|) VAR |x|)))) |bool|)) |bool|))))) (FACT (|I_o_ID| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |g%1|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |o|) CONST I %T . I%15)) VAR |f| %T . |g%1|) %T . |g%1|)) VAR |f| %T . |g%1|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |o|) VAR |f| %T . |g%1|)) CONST I %T . I%8) %T . |g%1|)) VAR |f| %T . |g%1|)))) |bool|) (I_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST =) COMB ((CONST I) VAR |x| %T . |x%3|) %T . |x%3|)) VAR |x| %T . |x%3|) |bool|)) |bool|) (S_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%7|) COMB ((CONST !) ABS ((VAR |g| %T . |g%1|) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((CONST S) VAR |f| %T . |f%7|)) VAR |g| %T . |g%1|)) VAR |x| %T . |x%3|) %T . |o%11|)) COMB ((COMB ((VAR |f| %T . |f%7|) VAR |x|)) COMB ((VAR |g| %T . |g%1|) VAR |x|))) |bool|)) |bool|)) |bool|)) |bool|) (K_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . |y%5|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST K) VAR |x| %T . |x%3|)) VAR |y| %T . |y%5|) %T . |x%3|)) VAR |x| %T . |x%3|) |bool|)) |bool|)) |bool|) (|o_ASSOC| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%12|) COMB ((CONST !) ABS ((VAR |g| %T . |f%0|) COMB ((CONST !) ABS ((VAR |h| %T . |g%1|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |o|) VAR |f| %T . |f%12|)) COMB ((COMB ((CONST |o|) VAR |g| %T . |f%0|)) VAR |h| %T . |g%1|) %T . |o%2|) %T . |o%13|)) COMB ((COMB ((CONST |o|) COMB ((COMB ((CONST |o|) VAR |f| %T . |f%12|)) VAR |g| %T . |f%0|) %T . |o%14|)) VAR |h| %T . |g%1|) %T . |o%13|) |bool|)) |bool|)) |bool|)) |bool|) (|o_THM| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%0|) COMB ((CONST !) ABS ((VAR |g| %T . |g%1|) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((CONST |o|) VAR |f| %T . |f%0|)) VAR |g| %T . |g%1|)) VAR |x| %T . |x%3|) %T . |o%11|)) COMB ((VAR |f| %T . |f%0|) COMB ((VAR |g| %T . |g%1|) VAR |x|))) |bool|)) |bool|)) |bool|)) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |x%3|) |bool|)))))