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

(SETQ %THEORYDATA (QUOTE ((PARENTS |list| BASIC-HOL) (TYPES (0 . |tree|)) (NAMETYPES) (OPERATORS (|trf| |fun| (|num|) (|fun| (|fun| (|list| (%VARTYPE . **)) (%VARTYPE . **)) (|fun| (|tree|) (%VARTYPE . **)))) (HT |fun| (|tree|) (|num|)) (|bht| |fun| (|num|) (|fun| (|tree|) (|bool|))) (|dest_node| |fun| (|tree|) (|list| (|tree|))) (|node| |fun| (|list| (|tree|)) (|tree|)) (|ABS_tree| |fun| (|num|) (|tree|)) (|REP_tree| |fun| (|tree|) (|num|)) (|Is_tree_REP| |fun| (|num|) (|bool|)) (|node_REP| |fun| (|list| (|num|)) (|num|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502535367)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 10 (|arb%9| %VARTYPE . *) (|f%8| |fun| (|list| (%VARTYPE . **)) (|fun| (|list| (|tree|)) (%VARTYPE . **))) (|trf%7| |fun| (|tree|) (%VARTYPE . **)) (|f%6| |fun| (|list| (%VARTYPE . **)) (%VARTYPE . **)) (PRIM_REC%5 |fun| (|num|) (|fun| (|tree|) (|bool|))) (P%4 |fun| (|tree|) (|bool|)) (|tl%3| |list| (|tree|)) (|rep%2| |fun| (|tree|) (|num|)) (P%1 |fun| (|num|) (|bool|)) (|t%0| |list| (|num|))) (AXIOM (|trf| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |f| %T . |f%6|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |trf|) VAR |n| |num|)) VAR |f| %T . |f%6|) %T . |trf%7|)) COMB ((CONST @) ABS ((VAR |fn| %T . |trf%7|) COMB ((CONST !) ABS ((VAR |trl| %T . |tl%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <=) COMB ((CONST HT) COMB ((CONST |node|) VAR |trl|)))) VAR |n|))) COMB ((COMB ((CONST =) COMB ((VAR |fn| %T . |trf%7|) COMB ((CONST |node|) VAR |trl|)))) COMB ((VAR |f| %T . |f%6|) COMB ((COMB ((CONST MAP) VAR |fn| %T . |trf%7|)) VAR |trl| %T . |tl%3|)))))) |bool|)) %T . |trf%7|) |bool|)) |bool|)))) (HT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |t| |tree|) COMB ((COMB ((CONST =) COMB ((CONST HT) VAR |t|))) COMB ((CONST @) ABS ((VAR |n| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST |bht|) VAR |n|)) VAR |t|))) COMB ((CONST !) ABS ((VAR |m| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST <) VAR |m|)) VAR |n|))) COMB ((CONST ~) COMB ((COMB ((CONST |bht|) VAR |m|)) VAR |t|)))))))) |num|) |bool|)))) (|bht| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |bht|)) COMB ((COMB ((CONST PRIM_REC) ABS ((VAR |tr| |tree|) COMB ((COMB ((CONST =) VAR |tr| |tree|)) COMB ((CONST |node|) CONST NIL)) |bool|))) ABS ((VAR |res| %T . P%4) ABS ((VAR |n| |num|) ABS ((VAR |tr| |tree|) COMB ((CONST ?) ABS ((VAR |trl| %T . |tl%3|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |tr| |tree|)) COMB ((CONST |node|) VAR |trl|)))) COMB ((COMB ((CONST ALL_EL) VAR |res| %T . P%4)) VAR |trl| %T . |tl%3|)))) |bool|)))) %T . PRIM_REC%5))) (|dest_node| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |t| |tree|) COMB ((COMB ((CONST =) COMB ((CONST |dest_node|) VAR |t|))) COMB ((CONST @) ABS ((VAR |p| %T . |tl%3|) COMB ((COMB ((CONST =) VAR |t| |tree|)) COMB ((CONST |node|) VAR |p|)) |bool|)) %T . |tl%3|) |bool|)))) (|node| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%3|) COMB ((COMB ((CONST =) COMB ((CONST |node|) VAR |tl|))) COMB ((CONST |ABS_tree|) COMB ((CONST |node_REP|) COMB ((COMB ((CONST MAP) CONST |REP_tree|)) VAR |tl| %T . |tl%3|)))) |bool|)))) (|tree_ISO_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |a| |tree|) COMB ((COMB ((CONST =) COMB ((CONST |ABS_tree|) COMB ((CONST |REP_tree|) VAR |a|)))) VAR |a| |tree|) |bool|)))) COMB ((CONST !) ABS ((VAR |r| |num|) COMB ((COMB ((CONST =) COMB ((CONST |Is_tree_REP|) VAR |r|))) COMB ((COMB ((CONST =) COMB ((CONST |REP_tree|) COMB ((CONST |ABS_tree|) VAR |r|)))) VAR |r| |num|) |bool|) |bool|))))) (|tree_TY_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST ?) ABS ((VAR |rep| %T . |rep%2|) COMB ((COMB ((CONST TYPE_DEFINITION) CONST |Is_tree_REP|)) VAR |rep| %T . |rep%2|) |bool|)))) (|Is_tree_REP| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |Is_tree_REP|)) ABS ((VAR |t| |num|) COMB ((CONST !) ABS ((VAR P %T . P%1) COMB ((COMB ((CONST ==>) COMB ((CONST !) ABS ((VAR |tl| %T . |t%0|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ALL_EL) VAR P %T . P%1)) VAR |tl| %T . |t%0|))) COMB ((VAR P %T . P%1) COMB ((CONST |node_REP|) VAR |tl|))))))) COMB ((VAR P %T . P%1) VAR |t|)))) |bool|)))) (|node_REP| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST |node_REP|) CONST NIL))) CONST |0|))) COMB ((CONST !) ABS ((VAR |h| |num|) COMB ((CONST !) ABS ((VAR |t| %T . |t%0|) COMB ((COMB ((CONST =) COMB ((CONST |node_REP|) COMB ((COMB ((CONST CONS) VAR |h| |num|)) VAR |t| %T . |t%0|)))) COMB ((COMB ((CONST *) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |h|)) VAR |h|)))) COMB ((COMB ((CONST EXP) CONST |2|)) COMB ((CONST |node_REP|) VAR |t|)))) |bool|)) |bool|)))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |arb%9|) |bool|) (|tree_Axiom| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%8|) COMB ((CONST ?!) ABS ((VAR |fn| %T . |trf%7|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%3|) COMB ((COMB ((CONST =) COMB ((VAR |fn| %T . |trf%7|) COMB ((CONST |node|) VAR |tl|)))) COMB ((COMB ((VAR |f| %T . |f%8|) COMB ((COMB ((CONST MAP) VAR |fn| %T . |trf%7|)) VAR |tl| %T . |tl%3|))) VAR |tl|)) |bool|)) |bool|)) |bool|)) |bool|) (|tree_Induct| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%4) COMB ((COMB ((CONST ==>) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%3|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ALL_EL) VAR P %T . P%4)) VAR |tl| %T . |tl%3|))) COMB ((VAR P %T . P%4) COMB ((CONST |node|) VAR |tl|))))))) COMB ((CONST !) ABS ((VAR |t| |tree|) COMB ((VAR P %T . P%4) VAR |t|)))))) |bool|) (|node_11| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |tl1| %T . |tl%3|) COMB ((CONST !) ABS ((VAR |tl2| %T . |tl%3|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((CONST |node|) VAR |tl1|))) COMB ((CONST |node|) VAR |tl2|)) |bool|)) COMB ((COMB ((CONST =) VAR |tl1| %T . |tl%3|)) VAR |tl2| %T . |tl%3|) |bool|) |bool|)) |bool|)) |bool|)))))