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

(SETQ %THEORYDATA (QUOTE ((PARENTS PPLAMB) (TYPES (2 . |prod|) (0 . |bool|)) (NAMETYPES) (OPERATORS (CURRY |fun| (|fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . ***)) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . ***)))) (UNCURRY |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . ***))) (|fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . ***))) (SND |fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . **)) (FST |fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . *)) (|REP_prod| |fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|)))) (IS_PAIR |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))) (|bool|)) (MK_PAIR |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))))) (TYPE_DEFINITION |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . **) (%VARTYPE . *)) (|bool|))) (ONTO |fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|bool|)) (ONE_ONE |fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|bool|)) (RES_ABSTRACT |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (%VARTYPE . **)))) (ARB %VARTYPE . *) (RES_SELECT |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *))) (RES_EXISTS |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|))) (RES_FORALL |fun| (|fun| (%VARTYPE . *) (|bool|)) (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|))) (COND |fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . *)))) (LET |fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (%VARTYPE . **))) (?! |fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (~ |fun| (|bool|) (|bool|)) (F |bool|) (! |fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (T |bool|) (? |fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (@ |fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *)) (HOL_DEFINITION |fun| (|bool|) (|bool|)) (BINDERS |fun| (%VARTYPE . *) (|bool|))) (PAIRED-INFIXES) (CURRIED-INFIXES (|,| |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|prod| (%VARTYPE . *) (%VARTYPE . **)))) (IS_ASSUMPTION_OF |fun| (|bool|) (|fun| (|bool|) (|bool|))) (|\\/| |fun| (|bool|) (|fun| (|bool|) (|bool|))) (|/\\| |fun| (|bool|) (|fun| (|bool|) (|bool|))) (==> |fun| (|bool|) (|fun| (|bool|) (|bool|))) (= |fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (|bool|)))) (PREDICATES (HOL_ASSERT |bool|)) (VERSION . "2.02 (GCL)") (STAMP . 36231502017593)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 21 (|,%20| |prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (|prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (|prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (|prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *)) (%VARTYPE . *))))) (|,%19| |prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (|prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (|prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *)) (%VARTYPE . *)))) (|,%18| |prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (|prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *)) (%VARTYPE . *))) (|,%17| |prod| (|fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *)) (%VARTYPE . *)) (@%16 |fun| (|fun| (%VARTYPE . *) (|bool|)) (%VARTYPE . *)) (|f%15| |fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . ***)) (UNCURRY%14 %VARTYPE . ***) (|f%13| |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (%VARTYPE . ***))) (|p'%12| |prod| (%VARTYPE . *) (%VARTYPE . **)) (IS_PAIR%11 |fun| (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))) (|bool|)) (|rep%10| |fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|)))) (MK_PAIR%9 |fun| (%VARTYPE . *) (|fun| (%VARTYPE . **) (|bool|))) (|rep%8| |fun| (%VARTYPE . **) (%VARTYPE . *)) (ARB%7 %VARTYPE . **) (COND%6 |fun| (|bool|) (|fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (%VARTYPE . *)))) (|f%5| |fun| (%VARTYPE . *) (%VARTYPE . **)) (LET%4 |fun| (|fun| (%VARTYPE . *) (%VARTYPE . **)) (|fun| (%VARTYPE . *) (%VARTYPE . **))) (|x%3| %VARTYPE . *) (P%2 |fun| (%VARTYPE . *) (|bool|)) (!%1 |fun| (|fun| (%VARTYPE . *) (|bool|)) (|bool|)) (=%0 |fun| (%VARTYPE . *) (|fun| (%VARTYPE . *) (|bool|)))) (AXIOM (CURRY_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%15|) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((COMB ((COMB ((CONST CURRY) VAR |f| %T . |f%15|)) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . UNCURRY%14)) COMB ((VAR |f| %T . |f%15|) COMB ((COMB ((CONST |,|) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7))) |bool|)) |bool|)) |bool|)))) (UNCURRY_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%13|) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((COMB ((CONST UNCURRY) VAR |f| %T . |f%13|)) COMB ((COMB ((CONST |,|) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . |p'%12|) %T . UNCURRY%14)) COMB ((COMB ((VAR |f| %T . |f%13|) VAR |x|)) VAR |y|)) |bool|)) |bool|)) |bool|)))) (SND_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |p'%12|) COMB ((COMB ((CONST =) COMB ((CONST SND) VAR |p| %T . |p'%12|) %T . ARB%7)) COMB ((CONST @) ABS ((VAR |y| %T . ARB%7) COMB ((CONST ?) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MK_PAIR) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . MK_PAIR%9)) COMB ((CONST |REP_prod|) VAR |p| %T . |p'%12|) %T . MK_PAIR%9) |bool|)) |bool|)) %T . ARB%7) |bool|)))) (FST_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . |p'%12|) COMB ((COMB ((CONST =) COMB ((CONST FST) VAR |p| %T . |p'%12|) %T . |x%3|)) COMB ((CONST @) ABS ((VAR |x| %T . |x%3|) COMB ((CONST ?) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MK_PAIR) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . MK_PAIR%9)) COMB ((CONST |REP_prod|) VAR |p| %T . |p'%12|) %T . MK_PAIR%9) |bool|)) |bool|)) %T . |x%3|) |bool|)))) (COMMA_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |,|) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . |p'%12|)) COMB ((CONST @) ABS ((VAR |p| %T . |p'%12|) COMB ((COMB ((CONST =) COMB ((CONST |REP_prod|) VAR |p| %T . |p'%12|) %T . MK_PAIR%9)) COMB ((COMB ((CONST MK_PAIR) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . MK_PAIR%9) |bool|)) %T . |p'%12|) |bool|)) |bool|)))) (|REP_prod| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |REP_prod| %T . |rep%10|)) COMB ((CONST @) ABS ((VAR |rep| %T . |rep%10|) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |p'| %T . |p'%12|) COMB ((CONST !) ABS ((VAR |p''| %T . |p'%12|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST =) COMB ((VAR |rep| %T . |rep%10|) VAR |p'|))) COMB ((VAR |rep| %T . |rep%10|) VAR |p''|)))) COMB ((COMB ((CONST =) VAR |p'| %T . |p'%12|)) VAR |p''| %T . |p'%12|)))) |bool|)))) COMB ((CONST !) ABS ((VAR |p| %T . MK_PAIR%9) COMB ((COMB ((CONST =) COMB ((CONST IS_PAIR) VAR |p| %T . MK_PAIR%9) |bool|)) COMB ((CONST ?) ABS ((VAR |p'| %T . |p'%12|) COMB ((COMB ((CONST =) VAR |p| %T . MK_PAIR%9)) COMB ((VAR |rep| %T . |rep%10|) VAR |p'|)) |bool|)) |bool|) |bool|))))) %T . |rep%10|))) (|prod_TY_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST ?) ABS ((VAR |rep| %T . |rep%10|) COMB ((COMB ((CONST TYPE_DEFINITION) CONST IS_PAIR %T . IS_PAIR%11)) VAR |rep| %T . |rep%10|) |bool|)))) (IS_PAIR_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |p| %T . MK_PAIR%9) COMB ((COMB ((CONST =) COMB ((CONST IS_PAIR) VAR |p| %T . MK_PAIR%9) |bool|)) COMB ((CONST ?) ABS ((VAR |x| %T . |x%3|) COMB ((CONST ?) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) VAR |p| %T . MK_PAIR%9)) COMB ((COMB ((CONST MK_PAIR) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . MK_PAIR%9) |bool|)) |bool|)) |bool|) |bool|)))) (MK_PAIR_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((COMB ((CONST MK_PAIR) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . MK_PAIR%9)) ABS ((VAR |a| %T . |x%3|) ABS ((VAR |b| %T . ARB%7) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |a| %T . |x%3|)) VAR |x| %T . |x%3|))) COMB ((COMB ((CONST =) VAR |b| %T . ARB%7)) VAR |y| %T . ARB%7))))) |bool|)) |bool|)))) (TYPE_DEFINITION PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((CONST !) ABS ((VAR |rep| %T . |rep%8|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST TYPE_DEFINITION) VAR P %T . P%2)) VAR |rep| %T . |rep%8|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |x'| %T . ARB%7) COMB ((CONST !) ABS ((VAR |x''| %T . ARB%7) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST =) COMB ((VAR |rep| %T . |rep%8|) VAR |x'|))) COMB ((VAR |rep| %T . |rep%8|) VAR |x''|)))) COMB ((COMB ((CONST =) VAR |x'| %T . ARB%7)) VAR |x''| %T . ARB%7)))) |bool|)))) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST =) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((CONST ?) ABS ((VAR |x'| %T . ARB%7) COMB ((COMB ((CONST =) VAR |x| %T . |x%3|)) COMB ((VAR |rep| %T . |rep%8|) VAR |x'|)) |bool|)) |bool|) |bool|)))) |bool|)) |bool|)))) (IS_ASSUMPTION_OF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |t1| |bool|) COMB ((CONST !) ABS ((VAR |t2| |bool|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST IS_ASSUMPTION_OF) VAR |t1|)) VAR |t2|))) COMB ((COMB ((CONST ==>) VAR |t1|)) VAR |t2|)) |bool|)) |bool|)))) (SELECT_AX PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST ==>) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((VAR P %T . P%2) COMB ((CONST @) VAR P %T . P%2))))) |bool|)) |bool|) (ETA_AX PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |t| %T . |f%5|) COMB ((COMB ((CONST =) ABS ((VAR |x| %T . |x%3|) COMB ((VAR |t| %T . |f%5|) VAR |x|)))) VAR |t| %T . |f%5|) |bool|)) |bool|) (IMP_ANTISYM_AX PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |t1| |bool|) COMB ((CONST !) ABS ((VAR |t2| |bool|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ==>) VAR |t1|)) VAR |t2|))) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ==>) VAR |t2|)) VAR |t1|))) COMB ((COMB ((CONST =) VAR |t1| |bool|)) VAR |t2| |bool|))))) |bool|)) |bool|) (BOOL_CASES_AX PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |t| |bool|) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |t| |bool|)) CONST T))) COMB ((COMB ((CONST =) VAR |t| |bool|)) CONST F)))) |bool|) (ONTO_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%5|) COMB ((COMB ((CONST =) COMB ((CONST ONTO) VAR |f| %T . |f%5|) |bool|)) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((CONST ?) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST =) VAR |y| %T . ARB%7)) COMB ((VAR |f| %T . |f%5|) VAR |x|)) |bool|)) |bool|)) |bool|) |bool|)))) (ONE_ONE_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |f| %T . |f%5|) COMB ((COMB ((CONST =) COMB ((CONST ONE_ONE) VAR |f| %T . |f%5|) |bool|)) COMB ((CONST !) ABS ((VAR |x1| %T . |x%3|) COMB ((CONST !) ABS ((VAR |x2| %T . |x%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST =) COMB ((VAR |f| %T . |f%5|) VAR |x1|))) COMB ((VAR |f| %T . |f%5|) VAR |x2|)))) COMB ((COMB ((CONST =) VAR |x1| %T . |x%3|)) VAR |x2| %T . |x%3|)))) |bool|)) |bool|) |bool|)))) (RES_ABSTRACT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((CONST !) ABS ((VAR B %T . |f%5|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST RES_ABSTRACT) VAR P %T . P%2)) VAR B %T . |f%5|) %T . |f%5|)) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((COMB ((CONST COND) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((VAR B %T . |f%5|) VAR |x|))) CONST ARB %T . ARB%7) %T . ARB%7)) |bool|)) |bool|)))) (ARB PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST ARB %T . |x%3|)) COMB ((CONST @) ABS ((VAR |x| %T . |x%3|) CONST T)) %T . |x%3|))) (RES_SELECT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((CONST !) ABS ((VAR B %T . P%2) COMB ((COMB ((CONST =) COMB ((COMB ((CONST RES_SELECT) VAR P %T . P%2)) VAR B %T . P%2) %T . |x%3|)) COMB ((CONST @) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((VAR B %T . P%2) VAR |x|)))) %T . |x%3|) |bool|)) |bool|)))) (RES_EXISTS PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((CONST !) ABS ((VAR B %T . P%2) COMB ((COMB ((CONST =) COMB ((COMB ((CONST RES_EXISTS) VAR P %T . P%2)) VAR B %T . P%2) |bool|)) COMB ((CONST ?) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((VAR B %T . P%2) VAR |x|)))) |bool|) |bool|)) |bool|)))) (RES_FORALL PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%2) COMB ((CONST !) ABS ((VAR B %T . P%2) COMB ((COMB ((CONST =) COMB ((COMB ((CONST RES_FORALL) VAR P %T . P%2)) VAR B %T . P%2) |bool|)) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST ==>) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((VAR B %T . P%2) VAR |x|)))) |bool|) |bool|)) |bool|)))) (COND_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST COND %T . COND%6)) ABS ((VAR |t| |bool|) ABS ((VAR |t1| %T . |x%3|) ABS ((VAR |t2| %T . |x%3|) COMB ((CONST @) ABS ((VAR |x| %T . |x%3|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST =) VAR |t| |bool|)) CONST T))) COMB ((COMB ((CONST =) VAR |x| %T . |x%3|)) VAR |t1| %T . |x%3|)))) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST =) VAR |t| |bool|)) CONST F))) COMB ((COMB ((CONST =) VAR |x| %T . |x%3|)) VAR |t2| %T . |x%3|))))) %T . |x%3|)))))) (LET_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST LET %T . LET%4)) ABS ((VAR |f| %T . |f%5|) ABS ((VAR |x| %T . |x%3|) COMB ((VAR |f| %T . |f%5|) VAR |x|)))))) (EXISTS_UNIQUE_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST ?! %T . !%1)) ABS ((VAR P %T . P%2) COMB ((COMB ((CONST |/\\|) COMB ((CONST ?) VAR P %T . P%2))) COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . |x%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((VAR P %T . P%2) VAR |x|))) COMB ((VAR P %T . P%2) VAR |y|)))) COMB ((COMB ((CONST =) VAR |x| %T . |x%3|)) VAR |y| %T . |x%3|)))) |bool|))))))) (NOT_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST ~)) ABS ((VAR |t| |bool|) COMB ((COMB ((CONST ==>) VAR |t|)) CONST F))))) (F_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST F)) COMB ((CONST !) ABS ((VAR |t| |bool|) VAR |t| |bool|)) |bool|))) (OR_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |\\/|)) ABS ((VAR |t1| |bool|) ABS ((VAR |t2| |bool|) COMB ((CONST !) ABS ((VAR |t| |bool|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ==>) VAR |t1|)) VAR |t|))) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ==>) VAR |t2|)) VAR |t|))) VAR |t|)))) |bool|))))) (AND_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |/\\|)) ABS ((VAR |t1| |bool|) ABS ((VAR |t2| |bool|) COMB ((CONST !) ABS ((VAR |t| |bool|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ==>) VAR |t1|)) COMB ((COMB ((CONST ==>) VAR |t2|)) VAR |t|)))) VAR |t|))) |bool|))))) (EXISTS_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST ? %T . !%1)) ABS ((VAR P %T . P%2) COMB ((VAR P %T . P%2) COMB ((CONST @) VAR P %T . P%2)))))) (FORALL_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST ! %T . !%1)) ABS ((VAR P %T . P%2) COMB ((COMB ((CONST =) VAR P %T . P%2)) ABS ((VAR |x| %T . |x%3|) CONST T)) |bool|)))) (T_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST T)) COMB ((COMB ((CONST =) ABS ((VAR |x| |bool|) VAR |x| |bool|))) ABS ((VAR |x| |bool|) VAR |x| |bool|)) |bool|))) (ARB_THM PRED HOL_ASSERT COMB ((COMB ((CONST =) CONST = %T . =%0)) CONST = %T . =%0) |bool|)) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) COMB ((COMB ((CONST |,|) CONST ?! %T . !%1)) COMB ((COMB ((CONST |,|) CONST ! %T . !%1)) COMB ((COMB ((CONST |,|) CONST ? %T . !%1)) COMB ((COMB ((CONST |,|) CONST @ %T . @%16)) VAR |arb| %T . |x%3|) %T . |,%17|) %T . |,%18|) %T . |,%19|) %T . |,%20|) |bool|) (PAIR_EQ PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((CONST !) ABS ((VAR |a| %T . |x%3|) COMB ((CONST !) ABS ((VAR |b| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |,|) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . |p'%12|)) COMB ((COMB ((CONST |,|) VAR |a| %T . |x%3|)) VAR |b| %T . ARB%7) %T . |p'%12|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |x| %T . |x%3|)) VAR |a| %T . |x%3|))) COMB ((COMB ((CONST =) VAR |y| %T . ARB%7)) VAR |b| %T . ARB%7))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (SND PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((CONST SND) COMB ((COMB ((CONST |,|) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . |p'%12|) %T . ARB%7)) VAR |y| %T . ARB%7) |bool|)) |bool|)) |bool|) (FST PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |x%3|) COMB ((CONST !) ABS ((VAR |y| %T . ARB%7) COMB ((COMB ((CONST =) COMB ((CONST FST) COMB ((COMB ((CONST |,|) VAR |x| %T . |x%3|)) VAR |y| %T . ARB%7) %T . |p'%12|) %T . |x%3|)) VAR |x| %T . |x%3|) |bool|)) |bool|)) |bool|) (PAIR PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |p'%12|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |,|) COMB ((CONST FST) VAR |x| %T . |p'%12|) %T . |x%3|)) COMB ((CONST SND) VAR |x| %T . |p'%12|) %T . ARB%7) %T . |p'%12|)) VAR |x| %T . |p'%12|) |bool|)) |bool|) (PAIR_EXISTS PRED HOL_ASSERT COMB ((CONST ?) ABS ((VAR |p| %T . MK_PAIR%9) COMB ((CONST IS_PAIR) VAR |p| %T . MK_PAIR%9) |bool|)) |bool|)))))