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

(SETQ %THEORYDATA (QUOTE ((PARENTS |combin| |tree| BASIC-HOL) (TYPES (1 . |ltree|)) (NAMETYPES) (OPERATORS (PART |fun| (|list| (|num|)) (|fun| (|list| (%VARTYPE . *)) (|list| (|list| (%VARTYPE . *))))) (SPLIT |fun| (|num|) (|fun| (|list| (%VARTYPE . *)) (|prod| (|list| (%VARTYPE . *)) (|list| (%VARTYPE . *))))) (AP |fun| (|list| (|fun| (%VARTYPE . *) (%VARTYPE . **))) (|fun| (|list| (%VARTYPE . *)) (|list| (%VARTYPE . **)))) (|Node| |fun| (%VARTYPE . *) (|fun| (|list| (|ltree| (%VARTYPE . *))) (|ltree| (%VARTYPE . *)))) (|ABS_ltree| |fun| (|prod| (|tree|) (|list| (%VARTYPE . *))) (|ltree| (%VARTYPE . *))) (|REP_ltree| |fun| (|ltree| (%VARTYPE . *)) (|prod| (|tree|) (|list| (%VARTYPE . *)))) (|Is_ltree| |fun| (|prod| (|tree|) (|list| (%VARTYPE . *))) (|bool|)) (|Size| |fun| (|tree|) (|num|))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.02 (GCL)") (STAMP . 36231502540180)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 22 (P%21 |fun| (|ltree| (%VARTYPE . *)) (|bool|)) (|fn%20| |fun| (|ltree| (%VARTYPE . *)) (%VARTYPE . **)) (|f%19| |fun| (|list| (%VARTYPE . **)) (|fun| (%VARTYPE . *) (|fun| (|list| (|ltree| (%VARTYPE . *))) (%VARTYPE . **)))) (NIL%18 |list| (|num|)) (SPLIT%17 |prod| (|list| (%VARTYPE . *)) (|list| (%VARTYPE . *))) (|h%16| |fun| (%VARTYPE . *) (%VARTYPE . **)) (AP%15 |list| (%VARTYPE . **)) (NIL%14 |list| (|fun| (%VARTYPE . *) (%VARTYPE . **))) (MAP%13 |list| (|list| (%VARTYPE . *))) (|o%12| |fun| (|ltree| (%VARTYPE . *)) (|list| (%VARTYPE . *))) (SND%11 |fun| (|prod| (|tree|) (|list| (%VARTYPE . *))) (|list| (%VARTYPE . *))) (|o%10| |fun| (|ltree| (%VARTYPE . *)) (|tree|)) (FST%9 |fun| (|prod| (|tree|) (|list| (%VARTYPE . *))) (|tree|)) (|tl%8| |list| (|ltree| (%VARTYPE . *))) (|v%7| %VARTYPE . *) (|a%6| |ltree| (%VARTYPE . *)) (|Is_ltree%5| |fun| (|prod| (|tree|) (|list| (%VARTYPE . *))) (|bool|)) (|rep%4| |fun| (|ltree| (%VARTYPE . *)) (|prod| (|tree|) (|list| (%VARTYPE . *)))) (|,%3| |prod| (|tree|) (|list| (%VARTYPE . *))) (|l%2| |list| (%VARTYPE . *)) (|tl%1| |list| (|tree|)) (|fn%0| |fun| (|tree|) (|num|))) (AXIOM (PART PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST PART) CONST NIL %T . NIL%18)) VAR |l| %T . |l%2|) %T . MAP%13)) CONST NIL %T . MAP%13) |bool|)))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |t| %T . NIL%18) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST PART) COMB ((COMB ((CONST CONS) VAR |n| |num|)) VAR |t| %T . NIL%18) %T . NIL%18)) VAR |l| %T . |l%2|) %T . MAP%13)) COMB ((COMB ((CONST CONS) COMB ((CONST FST) COMB ((COMB ((CONST SPLIT) VAR |n| |num|)) VAR |l| %T . |l%2|) %T . SPLIT%17) %T . |l%2|)) COMB ((COMB ((CONST PART) VAR |t| %T . NIL%18)) COMB ((CONST SND) COMB ((COMB ((CONST SPLIT) VAR |n| |num|)) VAR |l| %T . |l%2|) %T . SPLIT%17) %T . |l%2|) %T . MAP%13) %T . MAP%13) |bool|)) |bool|)) |bool|))))) (SPLIT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST SPLIT) CONST |0|)) VAR |l| %T . |l%2|) %T . SPLIT%17)) COMB ((COMB ((CONST |,|) CONST NIL %T . |l%2|)) VAR |l| %T . |l%2|) %T . SPLIT%17) |bool|)))) COMB ((CONST !) ABS ((VAR |n| |num|) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST SPLIT) COMB ((CONST SUC) VAR |n|))) VAR |l| %T . |l%2|) %T . SPLIT%17)) COMB ((COMB ((CONST |,|) COMB ((COMB ((CONST CONS) COMB ((CONST HD) VAR |l| %T . |l%2|) %T . |v%7|)) COMB ((CONST FST) COMB ((COMB ((CONST SPLIT) VAR |n| |num|)) COMB ((CONST TL) VAR |l| %T . |l%2|) %T . |l%2|) %T . SPLIT%17) %T . |l%2|) %T . |l%2|)) COMB ((CONST SND) COMB ((COMB ((CONST SPLIT) VAR |n| |num|)) COMB ((CONST TL) VAR |l| %T . |l%2|) %T . |l%2|) %T . SPLIT%17) %T . |l%2|) %T . SPLIT%17) |bool|)) |bool|))))) (AP PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST AP) CONST NIL %T . NIL%14)) VAR |l| %T . |l%2|) %T . AP%15)) CONST NIL %T . AP%15) |bool|)))) COMB ((CONST !) ABS ((VAR |h| %T . |h%16|) COMB ((CONST !) ABS ((VAR |t| %T . NIL%14) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST AP) COMB ((COMB ((CONST CONS) VAR |h| %T . |h%16|)) VAR |t| %T . NIL%14) %T . NIL%14)) VAR |l| %T . |l%2|) %T . AP%15)) COMB ((COMB ((CONST CONS) COMB ((VAR |h| %T . |h%16|) COMB ((CONST HD) VAR |l| %T . |l%2|)))) COMB ((COMB ((CONST AP) VAR |t| %T . NIL%14)) COMB ((CONST TL) VAR |l| %T . |l%2|) %T . |l%2|) %T . AP%15) %T . AP%15) |bool|)) |bool|)) |bool|))))) (|Node| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |v| %T . |v%7|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%8|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Node|) VAR |v| %T . |v%7|)) VAR |tl| %T . |tl%8|) %T . |a%6|)) COMB ((CONST |ABS_ltree|) COMB ((COMB ((CONST |,|) COMB ((CONST |node|) COMB ((COMB ((CONST MAP) COMB ((COMB ((CONST |o|) CONST FST %T . FST%9)) CONST |REP_ltree| %T . |rep%4|) %T . |o%10|)) VAR |tl| %T . |tl%8|)))) COMB ((COMB ((CONST CONS) VAR |v| %T . |v%7|)) COMB ((CONST FLAT) COMB ((COMB ((CONST MAP) COMB ((COMB ((CONST |o|) CONST SND %T . SND%11)) CONST |REP_ltree| %T . |rep%4|) %T . |o%12|)) VAR |tl| %T . |tl%8|) %T . MAP%13) %T . |l%2|) %T . |l%2|) %T . |,%3|) %T . |a%6|) |bool|)) |bool|)))) (|ltree_ISO_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |a| %T . |a%6|) COMB ((COMB ((CONST =) COMB ((CONST |ABS_ltree|) COMB ((CONST |REP_ltree|) VAR |a| %T . |a%6|) %T . |,%3|) %T . |a%6|)) VAR |a| %T . |a%6|) |bool|)))) COMB ((CONST !) ABS ((VAR |r| %T . |,%3|) COMB ((COMB ((CONST =) COMB ((CONST |Is_ltree|) VAR |r| %T . |,%3|) |bool|)) COMB ((COMB ((CONST =) COMB ((CONST |REP_ltree|) COMB ((CONST |ABS_ltree|) VAR |r| %T . |,%3|) %T . |a%6|) %T . |,%3|)) VAR |r| %T . |,%3|) |bool|) |bool|))))) (|ltree_TY_DEF| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST ?) ABS ((VAR |rep| %T . |rep%4|) COMB ((COMB ((CONST TYPE_DEFINITION) CONST |Is_ltree| %T . |Is_ltree%5|)) VAR |rep| %T . |rep%4|) |bool|)))) (|Is_ltree| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |t| |tree|) COMB ((CONST !) ABS ((VAR |l| %T . |l%2|) COMB ((COMB ((CONST =) COMB ((CONST |Is_ltree|) COMB ((COMB ((CONST |,|) VAR |t| |tree|)) VAR |l| %T . |l%2|) %T . |,%3|) |bool|)) COMB ((COMB ((CONST =) COMB ((CONST |Size|) VAR |t|))) COMB ((CONST LENGTH) VAR |l| %T . |l%2|) |num|) |bool|) |bool|)) |bool|)))) (|Size| PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST =) CONST |Size|)) COMB ((CONST @) ABS ((VAR |fn| %T . |fn%0|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%1|) COMB ((COMB ((CONST =) COMB ((VAR |fn| %T . |fn%0|) COMB ((CONST |node|) VAR |tl|)))) COMB ((CONST SUC) COMB ((CONST SUM) COMB ((COMB ((CONST MAP) VAR |fn| %T . |fn%0|)) VAR |tl| %T . |tl%1|)))) |bool|)) |bool|)) %T . |fn%0|)))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |v%7|) |bool|) (|Node_onto| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |l| %T . |a%6|) COMB ((CONST ?) ABS ((VAR |v| %T . |v%7|) COMB ((CONST ?) ABS ((VAR |trl| %T . |tl%8|) COMB ((COMB ((CONST =) VAR |l| %T . |a%6|)) COMB ((COMB ((CONST |Node|) VAR |v| %T . |v%7|)) VAR |trl| %T . |tl%8|) %T . |a%6|) |bool|)) |bool|)) |bool|)) |bool|) (|Node_11| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |v1| %T . |v%7|) COMB ((CONST !) ABS ((VAR |v2| %T . |v%7|) COMB ((CONST !) ABS ((VAR |trl1| %T . |tl%8|) COMB ((CONST !) ABS ((VAR |trl2| %T . |tl%8|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST =) COMB ((COMB ((CONST |Node|) VAR |v1| %T . |v%7|)) VAR |trl1| %T . |tl%8|) %T . |a%6|)) COMB ((COMB ((CONST |Node|) VAR |v2| %T . |v%7|)) VAR |trl2| %T . |tl%8|) %T . |a%6|) |bool|)) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) VAR |v1| %T . |v%7|)) VAR |v2| %T . |v%7|))) COMB ((COMB ((CONST =) VAR |trl1| %T . |tl%8|)) VAR |trl2| %T . |tl%8|))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (|ltree_Induct| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR P %T . P%21) COMB ((COMB ((CONST ==>) COMB ((CONST !) ABS ((VAR |t| %T . |tl%8|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST ALL_EL) VAR P %T . P%21)) VAR |t| %T . |tl%8|))) COMB ((CONST !) ABS ((VAR |h| %T . |v%7|) COMB ((VAR P %T . P%21) COMB ((COMB ((CONST |Node|) VAR |h| %T . |v%7|)) VAR |t| %T . |tl%8|))))))))) COMB ((CONST !) ABS ((VAR |l| %T . |a%6|) COMB ((VAR P %T . P%21) VAR |l|)))))) |bool|) (|ltree_Axiom| PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |f| %T . |f%19|) COMB ((CONST ?!) ABS ((VAR |fn| %T . |fn%20|) COMB ((CONST !) ABS ((VAR |v| %T . |v%7|) COMB ((CONST !) ABS ((VAR |tl| %T . |tl%8|) COMB ((COMB ((CONST =) COMB ((VAR |fn| %T . |fn%20|) COMB ((COMB ((CONST |Node|) VAR |v| %T . |v%7|)) VAR |tl| %T . |tl%8|)))) COMB ((COMB ((COMB ((VAR |f| %T . |f%19|) COMB ((COMB ((CONST MAP) VAR |fn| %T . |fn%20|)) VAR |tl| %T . |tl%8|))) VAR |v|)) VAR |tl|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)))))