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

(SETQ %THEORYDATA (QUOTE ((PARENTS |combin| BASIC-HOL) (TYPES (2 . |sum|)) (NAMETYPES) (OPERATORS (OUTR |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . **)) (OUTL |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . *)) (ISR |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (|bool|)) (ISL |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (|bool|)) (INR |fun| (%VARTYPE . **) (|sum| (%VARTYPE . *) (%VARTYPE . **))) (INL |fun| (%VARTYPE . *) (|sum| (%VARTYPE . *) (%VARTYPE . **))) (|ABS_sum| |fun| (|fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|)))) (|sum| (%VARTYPE . *) (%VARTYPE . **))) (|REP_sum| |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))))) (IS_SUM_REP |fun| (|fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|)))) (|bool|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502546415)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 11 (INR%10 |fun| (%VARTYPE . **) (|sum| (%VARTYPE . *) (%VARTYPE . **))) (INL%9 |fun| (%VARTYPE . *) (|sum| (%VARTYPE . *) (%VARTYPE . **))) (|h%8| |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . ***)) (|g%7| |fun| (%VARTYPE . **) (%VARTYPE . ***)) (|f%6| |fun| (%VARTYPE . *) (%VARTYPE . ***)) (|a%5| |sum| (%VARTYPE . *) (%VARTYPE . **)) (IS_SUM_REP%4 |fun| (|fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|)))) (|bool|)) (|rep%3| |fun| (|sum| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))))) (|v2%2| %VARTYPE . **) (|v1%1| %VARTYPE . *) (|f%0| |fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))))) (AXIOM (OUTR PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |x| %T . |v2%2|) COMB ((COMB ((CONST =) COMB ((CONST OUTR) COMB ((CONST INR) VAR |x| %T . |v2%2|) %T . |a%5|) %T . |v2%2|)) VAR |x| %T . |v2%2|) |bool|)))) (OUTL PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |x| %T . |v1%1|) COMB ((COMB ((CONST =) COMB ((CONST OUTL) COMB ((CONST INL) VAR |x| %T . |v1%1|) %T . |a%5|) %T . |v1%1|)) VAR |x| %T . |v1%1|) |bool|)))) (ISR PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |x| %T . |v2%2|) COMB ((CONST ISR) COMB ((CONST INR) VAR |x| %T . |v2%2|) %T . |a%5|) |bool|)))) COMB ((CONST !) ABS ((VAR |y| %T . |v1%1|) COMB ((CONST ~) COMB ((CONST ISR) COMB ((CONST INL) VAR |y| %T . |v1%1|) %T . |a%5|))))))) (ISL PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |x| %T . |v1%1|) COMB ((CONST ISL) COMB ((CONST INL) VAR |x| %T . |v1%1|) %T . |a%5|) |bool|)))) COMB ((CONST !) ABS ((VAR |y| %T . |v2%2|) COMB ((CONST ~) COMB ((CONST ISL) COMB ((CONST INR) VAR |y| %T . |v2%2|) %T . |a%5|))))))) (INR_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |e| %T . |v2%2|) COMB ((COMB ((CONST =) COMB ((CONST INR) VAR |e| %T . |v2%2|) %T . |a%5|)) COMB ((CONST |ABS_sum|) ABS ((VAR |b| |bool|) ABS ((VAR |x| %T . |v1%1|) ABS ((VAR |y| %T . |v2%2|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |y| %T . |v2%2|)) VAR |e| %T . |v2%2|))) COMB ((CONST ~) VAR |b|)))))) %T . |a%5|) |bool|)))) (INL_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |e| %T . |v1%1|) COMB ((COMB ((CONST =) COMB ((CONST INL) VAR |e| %T . |v1%1|) %T . |a%5|)) COMB ((CONST |ABS_sum|) ABS ((VAR |b| |bool|) ABS ((VAR |x| %T . |v1%1|) ABS ((VAR |y| %T . |v2%2|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |x| %T . |v1%1|)) VAR |e| %T . |v1%1|))) VAR |b|))))) %T . |a%5|) |bool|)))) (|sum_ISO_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |a| %T . |a%5|) COMB ((COMB ((CONST =) COMB ((CONST |ABS_sum|) COMB ((CONST |REP_sum|) VAR |a| %T . |a%5|) %T . |f%0|) %T . |a%5|)) VAR |a| %T . |a%5|) |bool|)))) COMB ((CONST !) ABS ((VAR |r| %T . |f%0|) COMB ((COMB ((CONST =) COMB ((CONST IS_SUM_REP) VAR |r| %T . |f%0|) |bool|)) COMB ((COMB ((CONST =) COMB ((CONST |REP_sum|) COMB ((CONST |ABS_sum|) VAR |r| %T . |f%0|) %T . |a%5|) %T . |f%0|)) VAR |r| %T . |f%0|) |bool|) |bool|))))) (|sum_TY_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST ?) ABS ((VAR |rep| %T . |rep%3|) COMB ((COMB ((CONST TYPE_DEFINITION) CONST IS_SUM_REP %T . IS_SUM_REP%4)) VAR |rep| %T . |rep%3|) |bool|)))) (IS_SUM_REP PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%0|) COMB ((COMB ((CONST =) COMB ((CONST IS_SUM_REP) VAR |f| %T . |f%0|) |bool|)) COMB ((CONST ?) ABS ((VAR |v1| %T . |v1%1|) COMB ((CONST ?) ABS ((VAR |v2| %T . |v2%2|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |f| %T . |f%0|)) ABS ((VAR |b| |bool|) ABS ((VAR |x| %T . |v1%1|) ABS ((VAR |y| %T . |v2%2|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |x| %T . |v1%1|)) VAR |v1| %T . |v1%1|))) VAR |b|))))))) COMB ((COMB ((CONST =) VAR |f| %T . |f%0|)) ABS ((VAR |b| |bool|) ABS ((VAR |x| %T . |v1%1|) ABS ((VAR |y| %T . |v2%2|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |y| %T . |v2%2|)) VAR |v2| %T . |v2%2|))) COMB ((CONST ~) VAR |b|))))))))) |bool|)) |bool|) |bool|))))) (FACT (INR PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |a%5|) COMB ((COMB ((CONST ==>) COMB ((CONST ISR) VAR |x| %T . |a%5|))) COMB ((COMB ((CONST =) COMB ((CONST INR) COMB ((CONST OUTR) VAR |x| %T . |a%5|) %T . |v2%2|) %T . |a%5|)) VAR |x| %T . |a%5|)))) |bool|) (INL PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |a%5|) COMB ((COMB ((CONST ==>) COMB ((CONST ISL) VAR |x| %T . |a%5|))) COMB ((COMB ((CONST =) COMB ((CONST INL) COMB ((CONST OUTL) VAR |x| %T . |a%5|) %T . |v1%1|) %T . |a%5|)) VAR |x| %T . |a%5|)))) |bool|) (ISL_OR_ISR PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |a%5|) COMB ((COMB ((CONST |\\/|) COMB ((CONST ISL) VAR |x| %T . |a%5|))) COMB ((CONST ISR) VAR |x| %T . |a%5|)))) |bool|) (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |v1%1|) |bool|) (|sum_Axiom| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%6|) COMB ((CONST !) ABS ((VAR |g| %T . |g%7|) COMB ((CONST ?!) ABS ((VAR |h| %T . |h%8|) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |x| %T . |v1%1|) COMB ((COMB ((CONST =) COMB ((VAR |h| %T . |h%8|) COMB ((CONST INL) VAR |x| %T . |v1%1|)))) COMB ((VAR |f| %T . |f%6|) VAR |x|)) |bool|)))) COMB ((CONST !) ABS ((VAR |x| %T . |v2%2|) COMB ((COMB ((CONST =) COMB ((VAR |h| %T . |h%8|) COMB ((CONST INR) VAR |x| %T . |v2%2|)))) COMB ((VAR |g| %T . |g%7|) VAR |x|)) |bool|))))) |bool|)) |bool|)) |bool|) (|sum_axiom| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%6|) COMB ((CONST !) ABS ((VAR |g| %T . |g%7|) COMB ((CONST ?!) ABS ((VAR |h| %T . |h%8|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |o|) VAR |h| %T . |h%8|)) CONST INL %T . INL%9) %T . |f%6|)) VAR |f| %T . |f%6|))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |o|) VAR |h| %T . |h%8|)) CONST INR %T . INR%10) %T . |g%7|)) VAR |g| %T . |g%7|)))) |bool|)) |bool|)) |bool|)))))