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

(SETQ %THEORYDATA (QUOTE ((PARENTS |ltree| BASIC-HOL) (TYPES) (NAMETYPES) (OPERATORS (TRP |fun| (|fun| (%VARTYPE . *) (|fun| (|list| (|ltree| (%VARTYPE . *))) (|bool|))) (|fun| (|ltree| (%VARTYPE . *)) (|bool|)))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502544058)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 11 (|tl%10| |list| (%VARTYPE . **)) (|fn%9| |fun| (%VARTYPE . **) (%VARTYPE . ***)) (|f%8| |fun| (|list| (%VARTYPE . ***)) (|fun| (%VARTYPE . *) (|fun| (|list| (%VARTYPE . **)) (%VARTYPE . ***)))) (|a%7| %VARTYPE . **) (ABS%6 |fun| (|ltree| (%VARTYPE . *)) (%VARTYPE . **)) (REP%5 |fun| (%VARTYPE . **) (|ltree| (%VARTYPE . *))) (|Node%4| |ltree| (%VARTYPE . *)) (|tl%3| |list| (|ltree| (%VARTYPE . *))) (|v%2| %VARTYPE . *) (TRP%1 |fun| (|ltree| (%VARTYPE . *)) (|bool|)) (P%0 |fun| (%VARTYPE . *) (|fun| (|list| (|ltree| (%VARTYPE . *))) (|bool|)))) (AXIOM (TRP_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR P %T . P%0) COMB ((COMB ((CONST =) COMB ((CONST TRP) VAR P %T . P%0) %T . TRP%1)) COMB ((CONST @) ABS ((VAR |trp| %T . TRP%1) COMB ((CONST !) ABS ((VAR |v| %T . |v%2|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%3|) COMB ((COMB ((CONST =) COMB ((VAR |trp| %T . TRP%1) COMB ((COMB ((CONST |Node|) VAR |v| %T . |v%2|)) VAR |tl| %T . |tl%3|)))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((VAR P %T . P%0) VAR |v|)) VAR |tl|))) COMB ((COMB ((CONST ALL_EL) VAR |trp| %T . TRP%1)) VAR |tl| %T . |tl%3|))) |bool|)) |bool|)) |bool|)) %T . TRP%1) |bool|))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |v%2|) |bool|) (|exists_TRP| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%0) COMB ((COMB ((CONST ==>) COMB ((CONST ?) ABS ((VAR |v| %T . |v%2|) COMB ((COMB ((VAR P %T . P%0) VAR |v|)) CONST NIL))))) COMB ((CONST ?) ABS ((VAR |t| %T . |Node%4|) COMB ((COMB ((CONST TRP) VAR P %T . P%0)) VAR |t| %T . |Node%4|) |bool|))))) |bool|) (TY_DEF_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR REP %T . REP%5) COMB ((CONST !) ABS ((VAR ABS %T . ABS%6) COMB ((CONST !) ABS ((VAR P %T . P%0) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |a| %T . |a%7|) COMB ((COMB ((CONST =) COMB ((VAR ABS %T . ABS%6) COMB ((VAR REP %T . REP%5) VAR |a|)))) VAR |a| %T . |a%7|) |bool|)))) COMB ((CONST !) ABS ((VAR |r| %T . |Node%4|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST TRP) VAR P %T . P%0)) VAR |r| %T . |Node%4|) |bool|)) COMB ((COMB ((CONST =) COMB ((VAR REP %T . REP%5) COMB ((VAR ABS %T . ABS%6) VAR |r|)))) VAR |r| %T . |Node%4|) |bool|) |bool|))))) COMB ((CONST !) ABS ((VAR |f| %T . |f%8|) COMB ((CONST ?!) ABS ((VAR |fn| %T . |fn%9|) COMB ((CONST !) ABS ((VAR |v| %T . |v%2|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%10|) COMB ((COMB ((CONST ==>) COMB ((COMB ((VAR P %T . P%0) VAR |v|)) COMB ((COMB ((CONST MAP) VAR REP %T . REP%5)) VAR |tl| %T . |tl%10|)))) COMB ((COMB ((CONST =) COMB ((VAR |fn| %T . |fn%9|) COMB ((VAR ABS %T . ABS%6) COMB ((COMB ((CONST |Node|) VAR |v| %T . |v%2|)) COMB ((COMB ((CONST MAP) VAR REP %T . REP%5)) VAR |tl| %T . |tl%10|) %T . |tl%3|))))) COMB ((COMB ((COMB ((VAR |f| %T . |f%8|) COMB ((COMB ((CONST MAP) VAR |fn| %T . |fn%9|)) VAR |tl| %T . |tl%10|))) VAR |v|)) VAR |tl|))))) |bool|)) |bool|)) |bool|))))) |bool|)) |bool|)) |bool|) (TRP PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%0) COMB ((CONST !) ABS ((VAR |v| %T . |v%2|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%3|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST TRP) VAR P %T . P%0)) COMB ((COMB ((CONST |Node|) VAR |v| %T . |v%2|)) VAR |tl| %T . |tl%3|) %T . |Node%4|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((VAR P %T . P%0) VAR |v|)) VAR |tl|))) COMB ((COMB ((CONST ALL_EL) COMB ((CONST TRP) VAR P %T . P%0) %T . TRP%1)) VAR |tl| %T . |tl%3|))) |bool|)) |bool|)) |bool|)) |bool|)))))