(SETQ %THEORYDATA (QUOTE ((PARENTS HOL) (TYPES) (NAMETYPES) (OPERATORS (STABLE |fun| (|prod| (|num|) (|num|)) (|fun| (|fun| (|num|) (%VARTYPE . *)) (|bool|))) (NEXT |fun| (|prod| (|num|) (|num|)) (|fun| (|fun| (|num|) (|bool|)) (|bool|)))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.01 (SUN4/AKCL)") (STAMP . 2940577250)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 8 (|b%7| %VARTYPE . **) (|a%6| %VARTYPE . *) (|s%5| |fun| (|num|) (%VARTYPE . **)) (|f%4| |fun| (%VARTYPE . **) (|bool|)) (FUN%3 |fun| (|prod| (%VARTYPE . *) (%VARTYPE . **)) (%VARTYPE . **)) (|,%2| |prod| (|num|) (|num|)) (|i%1| |fun| (|num|) (%VARTYPE . *)) (|done%0| |fun| (|num|) (|bool|))) (AXIOM (STABLE PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |i| %T . |i%1|) COMB ((CONST !) ABS ((VAR |x1| |num|) COMB ((CONST !) ABS ((VAR |x2| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST STABLE) COMB ((COMB ((CONST |,|) VAR |x1| |num|)) VAR |x2| |num|) %T . |,%2|)) VAR |i| %T . |i%1|) |bool|)) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <=) VAR |x1|)) VAR |x|))) COMB ((COMB ((CONST <) VAR |x|)) VAR |x2|)))) COMB ((COMB ((CONST =) COMB ((VAR |i| %T . |i%1|) VAR |x|))) COMB ((VAR |i| %T . |i%1|) VAR |x1|))))) |bool|) |bool|)) |bool|)) |bool|)))) (NEXT PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((CONST !) ABS ((VAR |done| %T . |done%0|) COMB ((CONST !) ABS ((VAR |x1| |num|) COMB ((CONST !) ABS ((VAR |x2| |num|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x1| |num|)) VAR |x2| |num|))) VAR |done|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |x1|)) VAR |x2|))) COMB ((COMB ((CONST |/\\|) COMB ((VAR |done| %T . |done%0|) VAR |x2|))) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST <) VAR |x1|)) VAR |x|))) COMB ((COMB ((CONST <) VAR |x|)) VAR |x2|)))) COMB ((CONST ~) COMB ((VAR |done| %T . |done%0|) VAR |x|)))))))) |bool|)) |bool|)) |bool|))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |a%6|) |bool|) (NEXT_THM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR FUN %T . FUN%3) COMB ((CONST !) ABS ((VAR |f| %T . |f%4|) COMB ((CONST !) ABS ((VAR |g| %T . FUN%3) COMB ((CONST !) ABS ((VAR |done| %T . |done%0|) COMB ((CONST !) ABS ((VAR |i| %T . |i%1|) COMB ((CONST !) ABS ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((VAR |done| %T . |done%0|) VAR |x|))) COMB ((VAR |f| %T . |f%4|) COMB ((VAR |s| %T . |s%5|) VAR |x|))))) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST +) VAR |x|)) CONST |1|)))) COMB ((VAR |g| %T . FUN%3) COMB ((COMB ((CONST |,|) COMB ((VAR |i| %T . |i%1|) VAR |x|))) COMB ((VAR |s| %T . |s%5|) VAR |x|))))))))) COMB ((CONST !) ABS ((VAR |a| %T . |a%6|) COMB ((CONST !) ABS ((VAR |b| %T . |b%7|) COMB ((COMB ((CONST =) COMB ((VAR FUN %T . FUN%3) COMB ((COMB ((CONST |,|) VAR |a| %T . |a%6|)) VAR |b| %T . |b%7|)))) COMB ((COMB ((COMB ((CONST COND) COMB ((VAR |f| %T . |f%4|) VAR |b|))) VAR |b| %T . |b%7|)) COMB ((VAR FUN %T . FUN%3) COMB ((COMB ((CONST |,|) VAR |a| %T . |a%6|)) COMB ((VAR |g| %T . FUN%3) COMB ((COMB ((CONST |,|) VAR |a| %T . |a%6|)) VAR |b| %T . |b%7|))))) %T . |b%7|) |bool|)) |bool|))))) COMB ((CONST !) ABS ((VAR |d| |num|) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x| |num|)) COMB ((COMB ((CONST +) VAR |x|)) VAR |d|)))) VAR |done|))) COMB ((COMB ((CONST STABLE) COMB ((COMB ((CONST |,|) VAR |x| |num|)) COMB ((COMB ((CONST +) VAR |x|)) VAR |d|)) %T . |,%2|)) VAR |i| %T . |i%1|)))) COMB ((COMB ((CONST =) COMB ((VAR |s| %T . |s%5|) COMB ((COMB ((CONST +) VAR |x|)) VAR |d|)))) COMB ((VAR FUN %T . FUN%3) COMB ((COMB ((CONST |,|) COMB ((VAR |i| %T . |i%1|) VAR |x|))) COMB ((VAR |g| %T . FUN%3) COMB ((COMB ((CONST |,|) COMB ((VAR |i| %T . |i%1|) VAR |x|))) COMB ((VAR |s| %T . |s%5|) VAR |x|))))))))) |bool|))))) |bool|)) |bool|)) |bool|)) |bool|)) |bool|)) |bool|) (NEXT_LEMMA2 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((CONST !) ABS ((VAR |d| |num|) COMB ((CONST !) ABS ((VAR |done| %T . |done%0|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x| |num|)) COMB ((COMB ((CONST +) COMB ((CONST SUC) VAR |x|))) VAR |d|)))) VAR |done|))) COMB ((CONST ~) COMB ((VAR |done| %T . |done%0|) COMB ((CONST SUC) VAR |x|)))))) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |d| |num|)) CONST |0|))))) |bool|)) |bool|)) |bool|) (NEXT_LEMMA1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |done| %T . |done%0|) COMB ((CONST !) ABS ((VAR |x1| |num|) COMB ((CONST !) ABS ((VAR |x2| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x1| |num|)) VAR |x2| |num|))) VAR |done|))) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x1| |num|)) VAR |x3| |num|))) VAR |done|)))) COMB ((COMB ((CONST =) VAR |x2| |num|)) VAR |x3| |num|)))) |bool|)) |bool|)) |bool|) (STABLE_LEMMA PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((CONST !) ABS ((VAR |d| |num|) COMB ((CONST !) ABS ((VAR |i| %T . |i%1|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST STABLE) COMB ((COMB ((CONST |,|) VAR |x| |num|)) COMB ((COMB ((CONST +) COMB ((CONST SUC) VAR |x|))) VAR |d|)) %T . |,%2|)) VAR |i| %T . |i%1|))) COMB ((CONST ~) COMB ((COMB ((CONST =) VAR |d| |num|)) CONST |0|))))) COMB ((COMB ((CONST =) COMB ((VAR |i| %T . |i%1|) VAR |x|))) COMB ((VAR |i| %T . |i%1|) COMB ((CONST SUC) VAR |x|)))))) |bool|)) |bool|)) |bool|) (SUC_LEMMA PRED HOL_ASSERT COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) CONST |0|)) VAR |m|))) VAR |m| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) CONST |0|))) VAR |m| |num|))) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST =) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|)))) COMB ((COMB ((CONST +) COMB ((CONST SUC) VAR |m|))) VAR |n|)))) COMB ((COMB ((CONST =) COMB ((COMB ((CONST +) VAR |m|)) COMB ((CONST SUC) VAR |n|)))) COMB ((CONST SUC) COMB ((COMB ((CONST +) VAR |m|)) VAR |n|))))))) (STABLE_SUC PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x1| |num|) COMB ((CONST !) ABS ((VAR |x2| |num|) COMB ((CONST !) ABS ((VAR |i| %T . |i%1|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST STABLE) COMB ((COMB ((CONST |,|) VAR |x1| |num|)) VAR |x2| |num|) %T . |,%2|)) VAR |i| %T . |i%1|))) COMB ((COMB ((CONST STABLE) COMB ((COMB ((CONST |,|) COMB ((CONST SUC) VAR |x1|))) VAR |x2| |num|) %T . |,%2|)) VAR |i| %T . |i%1|)))) |bool|)) |bool|)) |bool|) (NEXT_SUC2 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |done| %T . |done%0|) COMB ((CONST !) ABS ((VAR |x1| |num|) COMB ((CONST !) ABS ((VAR |x2| |num|) COMB ((COMB ((CONST ==>) COMB ((COMB ((CONST |/\\|) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x1| |num|)) VAR |x2| |num|))) VAR |done|))) COMB ((CONST ~) COMB ((VAR |done| %T . |done%0|) COMB ((CONST SUC) VAR |x1|)))))) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) COMB ((CONST SUC) VAR |x1|))) VAR |x2| |num|))) VAR |done|)))) |bool|)) |bool|)) |bool|) (NEXT_SUC1 PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |done| %T . |done%0|) COMB ((CONST !) ABS ((VAR |x| |num|) COMB ((COMB ((CONST ==>) COMB ((VAR |done| %T . |done%0|) COMB ((CONST SUC) VAR |x|)))) COMB ((COMB ((CONST NEXT) COMB ((COMB ((CONST |,|) VAR |x| |num|)) COMB ((CONST SUC) VAR |x|)))) VAR |done|)))) |bool|)) |bool|)))))