tt('type/integer/int', ty, $t).
tt('const/integer/ABS', ty, ('type/integer/int' > 'type/integer/int')).
tt('const/integer/LEAST_INT', ty, (('type/integer/int' > $o) > 'type/integer/int')).
tt('const/integer/Num', ty, ('type/integer/int' > 'type/num/num')).
tt('const/integer/int_0', ty, 'type/integer/int').
tt('const/integer/int_1', ty, 'type/integer/int').
tt('const/integer/int_ABS', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/integer/int')).
tt('const/integer/int_ABS_CLASS', ty, ((('type/pair/prod' 'type/num/num' 'type/num/num') > $o) > 'type/integer/int')).
tt('const/integer/int_REP', ty, ('type/integer/int' > ('type/pair/prod' 'type/num/num' 'type/num/num'))).
tt('const/integer/int_REP_CLASS', ty, ('type/integer/int' > (('type/pair/prod' 'type/num/num' 'type/num/num') > $o))).
tt('const/integer/int_add', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_div', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_divides', ty, ('type/integer/int' > ('type/integer/int' > $o))).
tt('const/integer/int_exp', ty, ('type/integer/int' > ('type/num/num' > 'type/integer/int'))).
tt('const/integer/int_ge', ty, ('type/integer/int' > ('type/integer/int' > $o))).
tt('const/integer/int_gt', ty, ('type/integer/int' > ('type/integer/int' > $o))).
tt('const/integer/int_le', ty, ('type/integer/int' > ('type/integer/int' > $o))).
tt('const/integer/int_lt', ty, ('type/integer/int' > ('type/integer/int' > $o))).
tt('const/integer/int_max', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_min', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_mod', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_mul', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_neg', ty, ('type/integer/int' > 'type/integer/int')).
tt('const/integer/int_of_num', ty, ('type/num/num' > 'type/integer/int')).
tt('const/integer/int_quot', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_rem', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/int_sub', ty, ('type/integer/int' > ('type/integer/int' > 'type/integer/int'))).
tt('const/integer/tint_0', ty, ('type/pair/prod' 'type/num/num' 'type/num/num')).
tt('const/integer/tint_1', ty, ('type/pair/prod' 'type/num/num' 'type/num/num')).
tt('const/integer/tint_add', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/integer/tint_eq', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' 'type/num/num') > $o))).
tt('const/integer/tint_lt', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' 'type/num/num') > $o))).
tt('const/integer/tint_mul', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/integer/tint_neg', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' 'type/num/num'))).
tt('const/integer/tint_of_num', ty, ('type/num/num' > ('type/pair/prod' 'type/num/num' 'type/num/num'))).
tt('thm/integer/EQ_LADD_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: ((('const/arithmetic/+' x y) = ('const/arithmetic/+' x z)) = (y = z)))).
tt('thm/integer/EQ_ADDL_', ax, (![x : 'type/num/num', y : 'type/num/num']: ((x = ('const/arithmetic/+' x y)) = (y = 'const/num/0')))).
tt('thm/integer/LT_LADD_', ax, (![x : 'type/num/num', y : 'type/num/num', z : 'type/num/num']: (('const/prim_rec/<' ('const/arithmetic/+' x y) ('const/arithmetic/+' x z)) = ('const/prim_rec/<' y z)))).
tt('thm/integer/LT_ADDL_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/prim_rec/<' x ('const/arithmetic/+' x y)) = ('const/prim_rec/<' 'const/num/0' y)))).
tt('thm/integer/LT_ADDR_', ax, (![x : 'type/num/num', y : 'type/num/num']: (~ ('const/prim_rec/<' ('const/arithmetic/+' x y) x)))).
tt('thm/integer/LT_ADD2_', ax, (![x1 : 'type/num/num', x2 : 'type/num/num', y1 : 'type/num/num', y2 : 'type/num/num']: ((('const/prim_rec/<' x1 y1) & ('const/prim_rec/<' x2 y2)) => ('const/prim_rec/<' ('const/arithmetic/+' x1 x2) ('const/arithmetic/+' y1 y2))))).
tt('thm/integer/tint_0_', def, ('const/integer/tint_0' = (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/integer/tint_1_', def, ('const/integer/tint_1' = (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/integer/tint_neg_', def, (![x : 'type/num/num', y : 'type/num/num']: (('const/integer/tint_neg' (('const/pair/,' 'type/num/num' 'type/num/num') x y)) = (('const/pair/,' 'type/num/num' 'type/num/num') y x)))).
tt('thm/integer/tint_add_', def, (![x1 : 'type/num/num', y1 : 'type/num/num', x2 : 'type/num/num', y2 : 'type/num/num']: (('const/integer/tint_add' (('const/pair/,' 'type/num/num' 'type/num/num') x1 y1) (('const/pair/,' 'type/num/num' 'type/num/num') x2 y2)) = (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/+' x1 x2) ('const/arithmetic/+' y1 y2))))).
tt('thm/integer/tint_mul_', def, (![x1 : 'type/num/num', y1 : 'type/num/num', x2 : 'type/num/num', y2 : 'type/num/num']: (('const/integer/tint_mul' (('const/pair/,' 'type/num/num' 'type/num/num') x1 y1) (('const/pair/,' 'type/num/num' 'type/num/num') x2 y2)) = (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/+' ('const/arithmetic/*' x1 x2) ('const/arithmetic/*' y1 y2)) ('const/arithmetic/+' ('const/arithmetic/*' x1 y2) ('const/arithmetic/*' y1 x2)))))).
tt('thm/integer/tint_lt_', def, (![x1 : 'type/num/num', y1 : 'type/num/num', x2 : 'type/num/num', y2 : 'type/num/num']: (('const/integer/tint_lt' (('const/pair/,' 'type/num/num' 'type/num/num') x1 y1) (('const/pair/,' 'type/num/num' 'type/num/num') x2 y2)) = ('const/prim_rec/<' ('const/arithmetic/+' x1 y2) ('const/arithmetic/+' x2 y1))))).
tt('thm/integer/tint_eq_', def, (![x1 : 'type/num/num', y1 : 'type/num/num', x2 : 'type/num/num', y2 : 'type/num/num']: (('const/integer/tint_eq' (('const/pair/,' 'type/num/num' 'type/num/num') x1 y1) (('const/pair/,' 'type/num/num' 'type/num/num') x2 y2)) = (('const/arithmetic/+' x1 y2) = ('const/arithmetic/+' x2 y1))))).
tt('thm/integer/TINT_EQ_REFL_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/integer/tint_eq' x x))).
tt('thm/integer/TINT_EQ_SYM_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' x y) = ('const/integer/tint_eq' y x)))).
tt('thm/integer/TINT_EQ_TRANS_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num'), z : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/integer/tint_eq' x y) & ('const/integer/tint_eq' y z)) => ('const/integer/tint_eq' x z)))).
tt('thm/integer/TINT_EQ_EQUIV_', ax, (![p : ('type/pair/prod' 'type/num/num' 'type/num/num'), q : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' p q) = (('const/integer/tint_eq' p) = ('const/integer/tint_eq' q))))).
tt('thm/integer/TINT_EQ_AP_', ax, (![p : ('type/pair/prod' 'type/num/num' 'type/num/num'), q : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((p = q) => ('const/integer/tint_eq' p q)))).
tt('thm/integer/TINT_10_', ax, (~ ('const/integer/tint_eq' 'const/integer/tint_1' 'const/integer/tint_0'))).
tt('thm/integer/TINT_ADD_SYM_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_add' x y) = ('const/integer/tint_add' y x)))).
tt('thm/integer/TINT_MUL_SYM_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_mul' x y) = ('const/integer/tint_mul' y x)))).
tt('thm/integer/TINT_ADD_ASSOC_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num'), z : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_add' x ('const/integer/tint_add' y z)) = ('const/integer/tint_add' ('const/integer/tint_add' x y) z)))).
tt('thm/integer/TINT_MUL_ASSOC_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num'), z : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_mul' x ('const/integer/tint_mul' y z)) = ('const/integer/tint_mul' ('const/integer/tint_mul' x y) z)))).
tt('thm/integer/TINT_LDISTRIB_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num'), z : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_mul' x ('const/integer/tint_add' y z)) = ('const/integer/tint_add' ('const/integer/tint_mul' x y) ('const/integer/tint_mul' x z))))).
tt('thm/integer/TINT_ADD_LID_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/integer/tint_eq' ('const/integer/tint_add' 'const/integer/tint_0' x) x))).
tt('thm/integer/TINT_MUL_LID_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/integer/tint_eq' ('const/integer/tint_mul' 'const/integer/tint_1' x) x))).
tt('thm/integer/TINT_ADD_LINV_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/integer/tint_eq' ('const/integer/tint_add' ('const/integer/tint_neg' x) x) 'const/integer/tint_0'))).
tt('thm/integer/TINT_LT_TOTAL_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' x y) | (('const/integer/tint_lt' x y) | ('const/integer/tint_lt' y x))))).
tt('thm/integer/TINT_LT_REFL_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (~ ('const/integer/tint_lt' x x)))).
tt('thm/integer/TINT_LT_TRANS_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num'), z : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/integer/tint_lt' x y) & ('const/integer/tint_lt' y z)) => ('const/integer/tint_lt' x z)))).
tt('thm/integer/TINT_LT_ADD_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num'), z : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_lt' y z) => ('const/integer/tint_lt' ('const/integer/tint_add' x y) ('const/integer/tint_add' x z))))).
tt('thm/integer/TINT_LT_MUL_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/integer/tint_lt' 'const/integer/tint_0' x) & ('const/integer/tint_lt' 'const/integer/tint_0' y)) => ('const/integer/tint_lt' 'const/integer/tint_0' ('const/integer/tint_mul' x y))))).
tt('thm/integer/TINT_NEG_WELLDEF_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' x1 x2) => ('const/integer/tint_eq' ('const/integer/tint_neg' x1) ('const/integer/tint_neg' x2))))).
tt('thm/integer/TINT_ADD_WELLDEFR_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' x1 x2) => ('const/integer/tint_eq' ('const/integer/tint_add' x1 y) ('const/integer/tint_add' x2 y))))).
tt('thm/integer/TINT_ADD_WELLDEF_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y2 : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/integer/tint_eq' x1 x2) & ('const/integer/tint_eq' y1 y2)) => ('const/integer/tint_eq' ('const/integer/tint_add' x1 y1) ('const/integer/tint_add' x2 y2))))).
tt('thm/integer/TINT_MUL_WELLDEFR_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' x1 x2) => ('const/integer/tint_eq' ('const/integer/tint_mul' x1 y) ('const/integer/tint_mul' x2 y))))).
tt('thm/integer/TINT_MUL_WELLDEF_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y2 : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/integer/tint_eq' x1 x2) & ('const/integer/tint_eq' y1 y2)) => ('const/integer/tint_eq' ('const/integer/tint_mul' x1 y1) ('const/integer/tint_mul' x2 y2))))).
tt('thm/integer/TINT_LT_WELLDEFR_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' x1 x2) => (('const/integer/tint_lt' x1 y) = ('const/integer/tint_lt' x2 y))))).
tt('thm/integer/TINT_LT_WELLDEFL_', ax, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), y1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y2 : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' y1 y2) => (('const/integer/tint_lt' x y1) = ('const/integer/tint_lt' x y2))))).
tt('thm/integer/TINT_LT_WELLDEF_', ax, (![x1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), x2 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y1 : ('type/pair/prod' 'type/num/num' 'type/num/num'), y2 : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/integer/tint_eq' x1 x2) & ('const/integer/tint_eq' y1 y2)) => (('const/integer/tint_lt' x1 y1) = ('const/integer/tint_lt' x2 y2))))).
tt('thm/integer/tint_of_num_0', def, (('const/integer/tint_of_num' 'const/num/0') = 'const/integer/tint_0')).
tt('thm/integer/tint_of_num_e1', def, (![n : 'type/num/num']: (('const/integer/tint_of_num' ('const/num/SUC' n)) = ('const/integer/tint_add' ('const/integer/tint_of_num' n) 'const/integer/tint_1')))).
tt('thm/integer/tint_of_num_eq_', ax, (![n : 'type/num/num']: ((('const/pair/FST' 'type/num/num' 'type/num/num') ('const/integer/tint_of_num' n)) = ('const/arithmetic/+' (('const/pair/SND' 'type/num/num' 'type/num/num') ('const/integer/tint_of_num' n)) n)))).
tt('thm/integer/TINT_INJ_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/tint_eq' ('const/integer/tint_of_num' m) ('const/integer/tint_of_num' n)) = (m = n)))).
tt('thm/integer/NUM_POSTINT_EX_', ax, (![t : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((~ ('const/integer/tint_lt' t 'const/integer/tint_0')) => (?[n : 'type/num/num']: ('const/integer/tint_eq' t ('const/integer/tint_of_num' n)))))).
tt('thm/integer/int_TY_DEF_', def, (?[rep : ('type/integer/int' > (('type/pair/prod' 'type/num/num' 'type/num/num') > $o))]: (('const/bool/TYPE_DEFINITION' (('type/pair/prod' 'type/num/num' 'type/num/num') > $o) 'type/integer/int') (^[c : (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)]: (?[r : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' r r) & (c = ('const/integer/tint_eq' r))))) rep))).
tt('thm/integer/int_bijections_0', def, (![a : 'type/integer/int']: (('const/integer/int_ABS_CLASS' ('const/integer/int_REP_CLASS' a)) = a))).
tt('thm/integer/int_bijections_e1', def, (![r : (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)]: (((^[c : (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)]: (?[r0 : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' r0 r0) & (c = ('const/integer/tint_eq' r0))))) r) = (('const/integer/int_REP_CLASS' ('const/integer/int_ABS_CLASS' r)) = r)))).
tt('thm/integer/int_ABS_REP_CLASS_0', ax, (![a : 'type/integer/int']: (('const/integer/int_ABS_CLASS' ('const/integer/int_REP_CLASS' a)) = a))).
tt('thm/integer/int_ABS_REP_CLASS_e1', ax, (![c : (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)]: ((?[r : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/tint_eq' r r) & (c = ('const/integer/tint_eq' r)))) = (('const/integer/int_REP_CLASS' ('const/integer/int_ABS_CLASS' c)) = c)))).
tt('thm/integer/int_REP_def_', def, (![a : 'type/integer/int']: (('const/integer/int_REP' a) = (('const/min/@' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/integer/int_REP_CLASS' a))))).
tt('thm/integer/int_ABS_def_', def, (![r : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/integer/int_ABS' r) = ('const/integer/int_ABS_CLASS' ('const/integer/tint_eq' r))))).
tt('thm/integer/int_QUOTIENT_', ax, (('const/quotient/QUOTIENT' ('type/pair/prod' 'type/num/num' 'type/num/num') 'type/integer/int') 'const/integer/tint_eq' 'const/integer/int_ABS' 'const/integer/int_REP')).
tt('thm/integer/int_0_', def, ('const/integer/int_0' = ('const/integer/int_ABS' 'const/integer/tint_0'))).
tt('thm/integer/int_1_', def, ('const/integer/int_1' = ('const/integer/int_ABS' 'const/integer/tint_1'))).
tt('thm/integer/int_neg_', def, (![T1 : 'type/integer/int']: (('const/integer/int_neg' T1) = ('const/integer/int_ABS' ('const/integer/tint_neg' ('const/integer/int_REP' T1)))))).
tt('thm/integer/int_add_', def, (![T1 : 'type/integer/int', T2 : 'type/integer/int']: (('const/integer/int_add' T1 T2) = ('const/integer/int_ABS' ('const/integer/tint_add' ('const/integer/int_REP' T1) ('const/integer/int_REP' T2)))))).
tt('thm/integer/int_mul_', def, (![T1 : 'type/integer/int', T2 : 'type/integer/int']: (('const/integer/int_mul' T1 T2) = ('const/integer/int_ABS' ('const/integer/tint_mul' ('const/integer/int_REP' T1) ('const/integer/int_REP' T2)))))).
tt('thm/integer/int_lt_', def, (![T1 : 'type/integer/int', T2 : 'type/integer/int']: (('const/integer/int_lt' T1 T2) = ('const/integer/tint_lt' ('const/integer/int_REP' T1) ('const/integer/int_REP' T2))))).
tt('thm/integer/INT_10_', ax, (~ ('const/integer/int_1' = 'const/integer/int_0'))).
tt('thm/integer/INT_ADD_SYM_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' x y) = ('const/integer/int_add' y x)))).
tt('thm/integer/INT_ADD_COMM_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' x y) = ('const/integer/int_add' y x)))).
tt('thm/integer/INT_MUL_SYM_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_mul' x y) = ('const/integer/int_mul' y x)))).
tt('thm/integer/INT_MUL_COMM_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_mul' x y) = ('const/integer/int_mul' y x)))).
tt('thm/integer/INT_ADD_ASSOC_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_add' y z)) = ('const/integer/int_add' ('const/integer/int_add' x y) z)))).
tt('thm/integer/INT_MUL_ASSOC_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_mul' x ('const/integer/int_mul' y z)) = ('const/integer/int_mul' ('const/integer/int_mul' x y) z)))).
tt('thm/integer/INT_LDISTRIB_', ax, (![z : 'type/integer/int', y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_mul' x ('const/integer/int_add' y z)) = ('const/integer/int_add' ('const/integer/int_mul' x y) ('const/integer/int_mul' x z))))).
tt('thm/integer/INT_LT_TOTAL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((x = y) | (('const/integer/int_lt' x y) | ('const/integer/int_lt' y x))))).
tt('thm/integer/INT_LT_REFL_', ax, (![x : 'type/integer/int']: (~ ('const/integer/int_lt' x x)))).
tt('thm/integer/INT_LT_TRANS_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_lt' x y) & ('const/integer/int_lt' y z)) => ('const/integer/int_lt' x z)))).
tt('thm/integer/INT_LT_LADD_IMP_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' y z) => ('const/integer/int_lt' ('const/integer/int_add' x y) ('const/integer/int_add' x z))))).
tt('thm/integer/INT_LT_MUL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_lt' 'const/integer/int_0' x) & ('const/integer/int_lt' 'const/integer/int_0' y)) => ('const/integer/int_lt' 'const/integer/int_0' ('const/integer/int_mul' x y))))).
tt('thm/integer/int_of_num_0', ax, (('const/integer/int_of_num' 'const/num/0') = 'const/integer/int_0')).
tt('thm/integer/int_of_num_e1', ax, (![n : 'type/num/num']: (('const/integer/int_of_num' ('const/num/SUC' n)) = ('const/integer/int_add' ('const/integer/int_of_num' n) 'const/integer/int_1')))).
tt('thm/integer/NUM_POSINT_EX_', ax, (![t : 'type/integer/int']: ((~ ('const/integer/int_lt' t 'const/integer/int_0')) => (?[n : 'type/num/num']: (t = ('const/integer/int_of_num' n)))))).
tt('thm/integer/int_sub_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' x y) = ('const/integer/int_add' x ('const/integer/int_neg' y))))).
tt('thm/integer/int_le_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x y) = (~ ('const/integer/int_lt' y x))))).
tt('thm/integer/int_gt_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_gt' x y) = ('const/integer/int_lt' y x)))).
tt('thm/integer/int_ge_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_ge' x y) = ('const/integer/int_le' y x)))).
tt('thm/integer/INT_0_', ax, ('const/integer/int_0' = ('const/integer/int_of_num' 'const/num/0'))).
tt('thm/integer/INT_1_', ax, ('const/integer/int_1' = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/integer/INT_ADD_LID_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_of_num' 'const/num/0') x) = x))).
tt('thm/integer/INT_ADD_RID_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_of_num' 'const/num/0')) = x))).
tt('thm/integer/INT_ADD_LINV_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_neg' x) x) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_ADD_RINV_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' x ('const/integer/int_neg' x)) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_MUL_LID_', ax, (![x : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) = x))).
tt('thm/integer/INT_MUL_RID_', ax, (![x : 'type/integer/int']: (('const/integer/int_mul' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = x))).
tt('thm/integer/INT_RDISTRIB_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_add' x y) z) = ('const/integer/int_add' ('const/integer/int_mul' x z) ('const/integer/int_mul' y z))))).
tt('thm/integer/INT_EQ_LADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_add' x y) = ('const/integer/int_add' x z)) = (y = z)))).
tt('thm/integer/INT_EQ_RADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_add' x z) = ('const/integer/int_add' y z)) = (x = y)))).
tt('thm/integer/INT_ADD_LID_UNIQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_add' x y) = y) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_ADD_RID_UNIQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_add' x y) = x) = (y = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_LNEG_UNIQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_add' x y) = ('const/integer/int_of_num' 'const/num/0')) = (x = ('const/integer/int_neg' y))))).
tt('thm/integer/INT_RNEG_UNIQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_add' x y) = ('const/integer/int_of_num' 'const/num/0')) = (y = ('const/integer/int_neg' x))))).
tt('thm/integer/INT_NEG_ADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_add' x y)) = ('const/integer/int_add' ('const/integer/int_neg' x) ('const/integer/int_neg' y))))).
tt('thm/integer/INT_MUL_LZERO_', ax, (![x : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_of_num' 'const/num/0') x) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_MUL_RZERO_', ax, (![x : 'type/integer/int']: (('const/integer/int_mul' x ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_NEG_LMUL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_mul' x y)) = ('const/integer/int_mul' ('const/integer/int_neg' x) y)))).
tt('thm/integer/INT_NEG_RMUL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_mul' x y)) = ('const/integer/int_mul' x ('const/integer/int_neg' y))))).
tt('thm/integer/INT_NEGNEG_', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' x)) = x))).
tt('thm/integer/INT_NEG_MUL2_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_neg' x) ('const/integer/int_neg' y)) = ('const/integer/int_mul' x y)))).
tt('thm/integer/INT_LT_LADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_add' x y) ('const/integer/int_add' x z)) = ('const/integer/int_lt' y z)))).
tt('thm/integer/INT_LT_RADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_add' x z) ('const/integer/int_add' y z)) = ('const/integer/int_lt' x y)))).
tt('thm/integer/INT_NOT_LT_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((~ ('const/integer/int_lt' x y)) = ('const/integer/int_le' y x)))).
tt('thm/integer/INT_LT_ANTISYM_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (~ (('const/integer/int_lt' x y) & ('const/integer/int_lt' y x))))).
tt('thm/integer/INT_LT_GT_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' x y) => (~ ('const/integer/int_lt' y x))))).
tt('thm/integer/INT_NOT_LE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((~ ('const/integer/int_le' x y)) = ('const/integer/int_lt' y x)))).
tt('thm/integer/INT_LE_TOTAL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x y) | ('const/integer/int_le' y x)))).
tt('thm/integer/INT_LET_TOTAL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x y) | ('const/integer/int_lt' y x)))).
tt('thm/integer/INT_LTE_TOTAL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' x y) | ('const/integer/int_le' y x)))).
tt('thm/integer/INT_LE_REFL_', ax, (![x : 'type/integer/int']: ('const/integer/int_le' x x))).
tt('thm/integer/INT_LE_LT_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x y) = (('const/integer/int_lt' x y) | (x = y))))).
tt('thm/integer/INT_LT_LE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' x y) = (('const/integer/int_le' x y) & (~ (x = y)))))).
tt('thm/integer/INT_LT_IMP_LE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' x y) => ('const/integer/int_le' x y)))).
tt('thm/integer/INT_LTE_TRANS_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_lt' x y) & ('const/integer/int_le' y z)) => ('const/integer/int_lt' x z)))).
tt('thm/integer/INT_LET_TRANS_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_le' x y) & ('const/integer/int_lt' y z)) => ('const/integer/int_lt' x z)))).
tt('thm/integer/INT_LE_TRANS_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_le' x y) & ('const/integer/int_le' y z)) => ('const/integer/int_le' x z)))).
tt('thm/integer/INT_LE_ANTISYM_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_le' x y) & ('const/integer/int_le' y x)) = (x = y)))).
tt('thm/integer/INT_LET_ANTISYM_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (~ (('const/integer/int_lt' x y) & ('const/integer/int_le' y x))))).
tt('thm/integer/INT_LTE_ANTSYM_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (~ (('const/integer/int_le' x y) & ('const/integer/int_lt' y x))))).
tt('thm/integer/INT_NEG_LT0_', ax, (![x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_neg' x) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x)))).
tt('thm/integer/INT_NEG_GT0_', ax, (![x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' x)) = ('const/integer/int_lt' x ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_NEG_LE0_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_neg' x) ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x)))).
tt('thm/integer/INT_NEG_GE0_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' x)) = ('const/integer/int_le' x ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_LT_NEGTOTAL_', ax, (![x : 'type/integer/int']: ((x = ('const/integer/int_of_num' 'const/num/0')) | (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x) | ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' x)))))).
tt('thm/integer/INT_LE_NEGTOTAL_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x) | ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' x))))).
tt('thm/integer/INT_LE_MUL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x) & ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') y)) => ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_mul' x y))))).
tt('thm/integer/INT_LE_SQUARE_', ax, (![x : 'type/integer/int']: ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_mul' x x)))).
tt('thm/integer/INT_LE_01_', ax, ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/integer/INT_LT_01_', ax, ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/integer/INT_LE_LADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_add' x y) ('const/integer/int_add' x z)) = ('const/integer/int_le' y z)))).
tt('thm/integer/INT_LE_RADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_add' x z) ('const/integer/int_add' y z)) = ('const/integer/int_le' x y)))).
tt('thm/integer/INT_LT_ADD2_', ax, (![w : 'type/integer/int', x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_lt' w x) & ('const/integer/int_lt' y z)) => ('const/integer/int_lt' ('const/integer/int_add' w y) ('const/integer/int_add' x z))))).
tt('thm/integer/INT_LE_ADD2_', ax, (![w : 'type/integer/int', x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_le' w x) & ('const/integer/int_le' y z)) => ('const/integer/int_le' ('const/integer/int_add' w y) ('const/integer/int_add' x z))))).
tt('thm/integer/INT_LE_ADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x) & ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') y)) => ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' x y))))).
tt('thm/integer/INT_LT_ADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x) & ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') y)) => ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' x y))))).
tt('thm/integer/INT_LT_ADDNEG_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' y ('const/integer/int_add' x ('const/integer/int_neg' z))) = ('const/integer/int_lt' ('const/integer/int_add' y z) x)))).
tt('thm/integer/INT_LT_ADDNEG2_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_add' x ('const/integer/int_neg' y)) z) = ('const/integer/int_lt' x ('const/integer/int_add' z y))))).
tt('thm/integer/INT_LT_ADD1_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x y) => ('const/integer/int_lt' x ('const/integer/int_add' y ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/integer/INT_SUB_ADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_sub' x y) y) = x))).
tt('thm/integer/INT_SUB_ADD2_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_add' y ('const/integer/int_sub' x y)) = x))).
tt('thm/integer/INT_SUB_REFL_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' x x) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_SUB_0_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_sub' x y) = ('const/integer/int_of_num' 'const/num/0')) = (x = y)))).
tt('thm/integer/INT_LE_DOUBLE_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' x x)) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x)))).
tt('thm/integer/INT_LE_NEGL_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_neg' x) x) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x)))).
tt('thm/integer/INT_LE_NEGR_', ax, (![x : 'type/integer/int']: (('const/integer/int_le' x ('const/integer/int_neg' x)) = ('const/integer/int_le' x ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_NEG_EQ0_', ax, (![x : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_of_num' 'const/num/0')) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_NEG_0_', ax, (('const/integer/int_neg' ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_of_num' 'const/num/0'))).
tt('thm/integer/INT_NEG_SUB_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_sub' x y)) = ('const/integer/int_sub' y x)))).
tt('thm/integer/INT_SUB_LT_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_sub' x y)) = ('const/integer/int_lt' y x)))).
tt('thm/integer/INT_SUB_LE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_sub' x y)) = ('const/integer/int_le' y x)))).
tt('thm/integer/INT_ADD_SUB_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_add' x y) x) = y))).
tt('thm/integer/INT_SUB_LDISTRIB_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_mul' x ('const/integer/int_sub' y z)) = ('const/integer/int_sub' ('const/integer/int_mul' x y) ('const/integer/int_mul' x z))))).
tt('thm/integer/INT_SUB_RDISTRIB_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_sub' x y) z) = ('const/integer/int_sub' ('const/integer/int_mul' x z) ('const/integer/int_mul' y z))))).
tt('thm/integer/INT_NEG_EQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_neg' x) = y) = (x = ('const/integer/int_neg' y))))).
tt('thm/integer/INT_NEG_MINUS1_', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' x) = ('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))).
tt('thm/integer/INT_LT_IMP_NE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' x y) => (~ (x = y))))).
tt('thm/integer/INT_LE_ADDR_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x ('const/integer/int_add' x y)) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') y)))).
tt('thm/integer/INT_LE_ADDL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' y ('const/integer/int_add' x y)) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x)))).
tt('thm/integer/INT_LT_ADDR_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_add' x y)) = ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') y)))).
tt('thm/integer/INT_LT_ADDL_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' y ('const/integer/int_add' x y)) = ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x)))).
tt('thm/integer/INT_ENTIRE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_mul' x y) = ('const/integer/int_of_num' 'const/num/0')) = ((x = ('const/integer/int_of_num' 'const/num/0')) | (y = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_EQ_LMUL_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_mul' x y) = ('const/integer/int_mul' x z)) = ((x = ('const/integer/int_of_num' 'const/num/0')) | (y = z))))).
tt('thm/integer/INT_EQ_RMUL_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_mul' x z) = ('const/integer/int_mul' y z)) = ((z = ('const/integer/int_of_num' 'const/num/0')) | (x = y))))).
tt('thm/integer/INT_', ax, (![n : 'type/num/num']: (('const/integer/int_of_num' ('const/num/SUC' n)) = ('const/integer/int_add' ('const/integer/int_of_num' n) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/integer/INT_POS_', ax, (![n : 'type/num/num']: ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' n)))).
tt('thm/integer/INT_LE_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/arithmetic/<=' m n)))).
tt('thm/integer/INT_LT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/prim_rec/<' m n)))).
tt('thm/integer/INT_INJ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/integer/int_of_num' m) = ('const/integer/int_of_num' n)) = (m = n)))).
tt('thm/integer/INT_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' ('const/arithmetic/+' m n))))).
tt('thm/integer/INT_MUL_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_mul' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' ('const/arithmetic/*' m n))))).
tt('thm/integer/INT_LT_NZ_', ax, (![n : 'type/num/num']: ((~ (('const/integer/int_of_num' n) = ('const/integer/int_of_num' 'const/num/0'))) = ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' n))))).
tt('thm/integer/INT_NZ_IMP_LT_', ax, (![n : 'type/num/num']: ((~ (n = 'const/num/0')) => ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' n))))).
tt('thm/integer/INT_DOUBLE_', ax, (![x : 'type/integer/int']: (('const/integer/int_add' x x) = ('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)))).
tt('thm/integer/INT_SUB_SUB_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_sub' x y) x) = ('const/integer/int_neg' y)))).
tt('thm/integer/INT_LT_ADD_SUB_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_add' x y) z) = ('const/integer/int_lt' x ('const/integer/int_sub' z y))))).
tt('thm/integer/INT_LT_SUB_RADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_sub' x y) z) = ('const/integer/int_lt' x ('const/integer/int_add' z y))))).
tt('thm/integer/INT_LT_SUB_LADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_sub' y z)) = ('const/integer/int_lt' ('const/integer/int_add' x z) y)))).
tt('thm/integer/INT_LE_SUB_LADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_le' x ('const/integer/int_sub' y z)) = ('const/integer/int_le' ('const/integer/int_add' x z) y)))).
tt('thm/integer/INT_LE_SUB_RADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_sub' x y) z) = ('const/integer/int_le' x ('const/integer/int_add' z y))))).
tt('thm/integer/INT_LT_NEG_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_neg' x) ('const/integer/int_neg' y)) = ('const/integer/int_lt' y x)))).
tt('thm/integer/INT_LE_NEG_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_neg' x) ('const/integer/int_neg' y)) = ('const/integer/int_le' y x)))).
tt('thm/integer/INT_ADD2_SUB2_', ax, (![a : 'type/integer/int', b : 'type/integer/int', c : 'type/integer/int', d : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_add' a b) ('const/integer/int_add' c d)) = ('const/integer/int_add' ('const/integer/int_sub' a c) ('const/integer/int_sub' b d))))).
tt('thm/integer/INT_SUB_LZERO_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_of_num' 'const/num/0') x) = ('const/integer/int_neg' x)))).
tt('thm/integer/INT_SUB_RZERO_', ax, (![x : 'type/integer/int']: (('const/integer/int_sub' x ('const/integer/int_of_num' 'const/num/0')) = x))).
tt('thm/integer/INT_LET_ADD2_', ax, (![w : 'type/integer/int', x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_le' w x) & ('const/integer/int_lt' y z)) => ('const/integer/int_lt' ('const/integer/int_add' w y) ('const/integer/int_add' x z))))).
tt('thm/integer/INT_LTE_ADD2_', ax, (![w : 'type/integer/int', x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_lt' w x) & ('const/integer/int_le' y z)) => ('const/integer/int_lt' ('const/integer/int_add' w y) ('const/integer/int_add' x z))))).
tt('thm/integer/INT_LET_ADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x) & ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') y)) => ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' x y))))).
tt('thm/integer/INT_LTE_ADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x) & ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') y)) => ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_add' x y))))).
tt('thm/integer/INT_LT_MUL2_', ax, (![x1 : 'type/integer/int', x2 : 'type/integer/int', y1 : 'type/integer/int', y2 : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') x1) & (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') y1) & (('const/integer/int_lt' x1 x2) & ('const/integer/int_lt' y1 y2)))) => ('const/integer/int_lt' ('const/integer/int_mul' x1 y1) ('const/integer/int_mul' x2 y2))))).
tt('thm/integer/INT_SUB_LNEG_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_neg' x) y) = ('const/integer/int_neg' ('const/integer/int_add' x y))))).
tt('thm/integer/INT_SUB_RNEG_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' x ('const/integer/int_neg' y)) = ('const/integer/int_add' x y)))).
tt('thm/integer/INT_SUB_NEG2_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_neg' x) ('const/integer/int_neg' y)) = ('const/integer/int_sub' y x)))).
tt('thm/integer/INT_SUB_TRIANGLE_', ax, (![a : 'type/integer/int', b : 'type/integer/int', c : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_sub' a b) ('const/integer/int_sub' b c)) = ('const/integer/int_sub' a c)))).
tt('thm/integer/INT_EQ_SUB_LADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((x = ('const/integer/int_sub' y z)) = (('const/integer/int_add' x z) = y)))).
tt('thm/integer/INT_EQ_SUB_RADD_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_sub' x y) = z) = (x = ('const/integer/int_add' z y))))).
tt('thm/integer/INT_SUB_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/<=' m n) => (('const/integer/int_sub' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/integer/int_of_num' ('const/arithmetic/-' n m)))))).
tt('thm/integer/INT_SUB_SUB2_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' x ('const/integer/int_sub' x y)) = y))).
tt('thm/integer/INT_ADD_SUB2_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' x ('const/integer/int_add' x y)) = ('const/integer/int_neg' y)))).
tt('thm/integer/INT_EQ_LMUL2_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((~ (x = ('const/integer/int_of_num' 'const/num/0'))) => ((y = z) = (('const/integer/int_mul' x y) = ('const/integer/int_mul' x z)))))).
tt('thm/integer/INT_EQ_IMP_LE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((x = y) => ('const/integer/int_le' x y)))).
tt('thm/integer/INT_POS_NZ_', ax, (![x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x) => (~ (x = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_EQ_RMUL_IMP_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (((~ (z = ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_mul' x z) = ('const/integer/int_mul' y z))) => (x = y)))).
tt('thm/integer/INT_EQ_LMUL_IMP_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (((~ (x = ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_mul' x y) = ('const/integer/int_mul' x z))) => (y = z)))).
tt('thm/integer/INT_DIFFSQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_add' x y) ('const/integer/int_sub' x y)) = ('const/integer/int_sub' ('const/integer/int_mul' x x) ('const/integer/int_mul' y y))))).
tt('thm/integer/INT_POASQ_', ax, (![x : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_mul' x x)) = (~ (x = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_SUMSQ_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_add' ('const/integer/int_mul' x x) ('const/integer/int_mul' y y)) = ('const/integer/int_of_num' 'const/num/0')) = ((x = ('const/integer/int_of_num' 'const/num/0')) & (y = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_EQ_NEG_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_neg' y)) = (x = y)))).
tt('thm/integer/INT_LT_CALCULATE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/prim_rec/<' n m)))).
tt('thm/integer/INT_LT_CALCULATE_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' n)) ('const/integer/int_neg' ('const/integer/int_of_num' m))) = ('const/prim_rec/<' m n)))).
tt('thm/integer/INT_LT_CALCULATE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' n)) ('const/integer/int_of_num' m)) = ((~ (n = 'const/num/0')) | (~ (m = 'const/num/0')))))).
tt('thm/integer/INT_LT_CALCULATE_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' n) ('const/integer/int_neg' ('const/integer/int_of_num' m))) = $false))).
tt('thm/integer/NUM_POSINT_', ax, (![i : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) => (('const/bool/?!' 'type/num/num') (^[n : 'type/num/num']: (i = ('const/integer/int_of_num' n))))))).
tt('thm/integer/NUM_POSINT_EXISTS_', ax, (![i : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) => (?[n : 'type/num/num']: (i = ('const/integer/int_of_num' n)))))).
tt('thm/integer/NUM_NEGINT_EXISTS_', ax, (![i : 'type/integer/int']: (('const/integer/int_le' i ('const/integer/int_of_num' 'const/num/0')) => (?[n : 'type/num/num']: (i = ('const/integer/int_neg' ('const/integer/int_of_num' n))))))).
tt('thm/integer/INT_NUM_CASES_', ax, (![p : 'type/integer/int']: ((?[n : 'type/num/num']: ((p = ('const/integer/int_of_num' n)) & (~ (n = 'const/num/0')))) | ((?[n : 'type/num/num']: ((p = ('const/integer/int_neg' ('const/integer/int_of_num' n))) & (~ (n = 'const/num/0')))) | (p = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_DISCRETE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (~ (('const/integer/int_lt' x y) & ('const/integer/int_lt' y ('const/integer/int_add' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/integer/INT_LE_LT1_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_le' x y) = ('const/integer/int_lt' x ('const/integer/int_add' y ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/integer/INT_LT_LE1_', ax, (![y : 'type/integer/int', x : 'type/integer/int']: (('const/integer/int_lt' x y) = ('const/integer/int_le' ('const/integer/int_add' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y)))).
tt('thm/integer/INT_MUL_EQ_1_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_mul' x y) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (((x = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) & (y = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) | ((x = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (y = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))).
tt('thm/integer/Num_', def, (![i : 'type/integer/int']: (('const/integer/Num' i) = (('const/min/@' 'type/num/num') (^[n : 'type/num/num']: (i = ('const/integer/int_of_num' n))))))).
tt('thm/integer/NUM_OF_INT_', ax, (![n : 'type/num/num']: (('const/integer/Num' ('const/integer/int_of_num' n)) = n))).
tt('thm/integer/INT_OF_NUM_', ax, (![i : 'type/integer/int']: ((('const/integer/int_of_num' ('const/integer/Num' i)) = i) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i)))).
tt('thm/integer/LE_NUM_OF_INT_', ax, (![n : 'type/num/num', i : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_of_num' n) i) => ('const/arithmetic/<=' n ('const/integer/Num' i))))).
tt('thm/integer/int_div_', def, (![i : 'type/integer/int', j : 'type/integer/int']: ((~ (j = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' i j) = (('const/bool/COND' 'type/integer/int') ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') j) (('const/bool/COND' 'type/integer/int') ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' i) ('const/integer/Num' j))) ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' ('const/integer/int_neg' i)) ('const/integer/Num' j)))) (('const/bool/COND' 'type/integer/int') (('const/arithmetic/MOD' ('const/integer/Num' ('const/integer/int_neg' i)) ('const/integer/Num' j)) = 'const/num/0') ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) (('const/bool/COND' 'type/integer/int') ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' i) ('const/integer/Num' ('const/integer/int_neg' j))))) (('const/bool/COND' 'type/integer/int') (('const/arithmetic/MOD' ('const/integer/Num' i) ('const/integer/Num' ('const/integer/int_neg' j))) = 'const/num/0') ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' ('const/integer/int_neg' i)) ('const/integer/Num' ('const/integer/int_neg' j)))))))))).
tt('thm/integer/INT_DIV_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((~ (m = 'const/num/0')) => (('const/integer/int_div' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/integer/int_of_num' ('const/arithmetic/DIV' n m)))))).
tt('thm/integer/INT_DIV_NEG_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' p ('const/integer/int_neg' q)) = ('const/integer/int_div' ('const/integer/int_neg' p) q))))).
tt('thm/integer/INT_DIV_1_', ax, (![p : 'type/integer/int']: (('const/integer/int_div' p ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = p))).
tt('thm/integer/INT_DIV_0_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' ('const/integer/int_of_num' 'const/num/0') q) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_DIV_ID_', ax, (![p : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' p p) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/integer/int_mod_', def, (![i : 'type/integer/int', j : 'type/integer/int']: ((~ (j = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' i j) = ('const/integer/int_sub' i ('const/integer/int_mul' ('const/integer/int_div' i j) j)))))).
tt('thm/integer/INT_MOD_BOUNDS_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/bool/COND' $o) ('const/integer/int_lt' q ('const/integer/int_of_num' 'const/num/0')) (('const/integer/int_lt' q ('const/integer/int_mod' p q)) & ('const/integer/int_le' ('const/integer/int_mod' p q) ('const/integer/int_of_num' 'const/num/0'))) (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_mod' p q)) & ('const/integer/int_lt' ('const/integer/int_mod' p q) q)))))).
tt('thm/integer/INT_DIVISION_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (![p : 'type/integer/int']: ((p = ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_div' p q) q) ('const/integer/int_mod' p q))) & (('const/bool/COND' $o) ('const/integer/int_lt' q ('const/integer/int_of_num' 'const/num/0')) (('const/integer/int_lt' q ('const/integer/int_mod' p q)) & ('const/integer/int_le' ('const/integer/int_mod' p q) ('const/integer/int_of_num' 'const/num/0'))) (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_mod' p q)) & ('const/integer/int_lt' ('const/integer/int_mod' p q) q)))))))).
tt('thm/integer/INT_MOD_', ax, (![n : 'type/num/num', m : 'type/num/num']: ((~ (m = 'const/num/0')) => (('const/integer/int_mod' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/integer/int_of_num' ('const/arithmetic/MOD' n m)))))).
tt('thm/integer/INT_MOD_NEG_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' p ('const/integer/int_neg' q)) = ('const/integer/int_neg' ('const/integer/int_mod' ('const/integer/int_neg' p) q)))))).
tt('thm/integer/INT_MOD0_', ax, (![p : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' ('const/integer/int_of_num' 'const/num/0') p) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_DIV_MUL_ID_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: (((~ (q = ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_mod' p q) = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mul' ('const/integer/int_div' p q) q) = p)))).
tt('thm/integer/INT_DIV_UNIQUE_', ax, (![i : 'type/integer/int', j : 'type/integer/int', q : 'type/integer/int']: ((?[r : 'type/integer/int']: ((i = ('const/integer/int_add' ('const/integer/int_mul' q j) r)) & (('const/bool/COND' $o) ('const/integer/int_lt' j ('const/integer/int_of_num' 'const/num/0')) (('const/integer/int_lt' j r) & ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0'))) (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) & ('const/integer/int_lt' r j))))) => (('const/integer/int_div' i j) = q)))).
tt('thm/integer/INT_MOD_UNIQUE_', ax, (![i : 'type/integer/int', j : 'type/integer/int', m : 'type/integer/int']: ((?[q : 'type/integer/int']: ((i = ('const/integer/int_add' ('const/integer/int_mul' q j) m)) & (('const/bool/COND' $o) ('const/integer/int_lt' j ('const/integer/int_of_num' 'const/num/0')) (('const/integer/int_lt' j m) & ('const/integer/int_le' m ('const/integer/int_of_num' 'const/num/0'))) (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') m) & ('const/integer/int_lt' m j))))) => (('const/integer/int_mod' i j) = m)))).
tt('thm/integer/INT_MOD_ID_', ax, (![i : 'type/integer/int']: ((~ (i = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' i i) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_MOD_COMMON_FACTOR_', ax, (![p : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (![q : 'type/integer/int']: (('const/integer/int_mod' ('const/integer/int_mul' q p) p) = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_DIV_LMUL_', ax, (![i : 'type/integer/int', j : 'type/integer/int']: ((~ (i = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' ('const/integer/int_mul' i j) i) = j)))).
tt('thm/integer/INT_DIV_RMUL_', ax, (![i : 'type/integer/int', j : 'type/integer/int']: ((~ (i = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' ('const/integer/int_mul' j i) i) = j)))).
tt('thm/integer/INT_MOD_EQ0_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (![p : 'type/integer/int']: ((('const/integer/int_mod' p q) = ('const/integer/int_of_num' 'const/num/0')) = (?[k : 'type/integer/int']: (p = ('const/integer/int_mul' k q)))))))).
tt('thm/integer/INT_MUL_DIV_', ax, (![p : 'type/integer/int', q : 'type/integer/int', k : 'type/integer/int']: (((~ (q = ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_mod' p q) = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' ('const/integer/int_mul' k p) q) = ('const/integer/int_mul' k ('const/integer/int_div' p q)))))).
tt('thm/integer/INT_ADD_DIV_', ax, (![i : 'type/integer/int', j : 'type/integer/int', k : 'type/integer/int']: (((~ (k = ('const/integer/int_of_num' 'const/num/0'))) & ((('const/integer/int_mod' i k) = ('const/integer/int_of_num' 'const/num/0')) | (('const/integer/int_mod' j k) = ('const/integer/int_of_num' 'const/num/0')))) => (('const/integer/int_div' ('const/integer/int_add' i j) k) = ('const/integer/int_add' ('const/integer/int_div' i k) ('const/integer/int_div' j k)))))).
tt('thm/integer/INT_MOD_ADD_MULTIPLES_', ax, (![r : 'type/integer/int', q : 'type/integer/int', k : 'type/integer/int']: ((~ (k = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' ('const/integer/int_add' ('const/integer/int_mul' q k) r) k) = ('const/integer/int_mod' r k))))).
tt('thm/integer/INT_MOD_NEG_NUMERATOR_', ax, (![x : 'type/integer/int', k : 'type/integer/int']: ((~ (k = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' ('const/integer/int_neg' x) k) = ('const/integer/int_mod' ('const/integer/int_sub' k x) k))))).
tt('thm/integer/INT_MOD_PLUS_', ax, (![k : 'type/integer/int', j : 'type/integer/int', i : 'type/integer/int']: ((~ (k = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' ('const/integer/int_add' ('const/integer/int_mod' i k) ('const/integer/int_mod' j k)) k) = ('const/integer/int_mod' ('const/integer/int_add' i j) k))))).
tt('thm/integer/INT_MOD_SUB_', ax, (![k : 'type/integer/int', j : 'type/integer/int', i : 'type/integer/int']: ((~ (k = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' ('const/integer/int_sub' ('const/integer/int_mod' i k) ('const/integer/int_mod' j k)) k) = ('const/integer/int_mod' ('const/integer/int_sub' i j) k))))).
tt('thm/integer/INT_MOD_MOD_', ax, (![k : 'type/integer/int', j : 'type/integer/int']: ((~ (k = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' ('const/integer/int_mod' j k) k) = ('const/integer/int_mod' j k))))).
tt('thm/integer/INT_DIV_P_', ax, (![P : ('type/integer/int' > $o), x : 'type/integer/int', c : 'type/integer/int']: ((~ (c = ('const/integer/int_of_num' 'const/num/0'))) => ((P ('const/integer/int_div' x c)) = (?[k : 'type/integer/int', r : 'type/integer/int']: ((x = ('const/integer/int_add' ('const/integer/int_mul' k c) r)) & (((('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0')) & (('const/integer/int_lt' c r) & ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0')))) | ((~ ('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) & ('const/integer/int_lt' r c)))) & (P k)))))))).
tt('thm/integer/INT_MOD_P_', ax, (![P : ('type/integer/int' > $o), x : 'type/integer/int', c : 'type/integer/int']: ((~ (c = ('const/integer/int_of_num' 'const/num/0'))) => ((P ('const/integer/int_mod' x c)) = (?[k : 'type/integer/int', r : 'type/integer/int']: ((x = ('const/integer/int_add' ('const/integer/int_mul' k c) r)) & (((('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0')) & (('const/integer/int_lt' c r) & ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0')))) | ((~ ('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) & ('const/integer/int_lt' r c)))) & (P r)))))))).
tt('thm/integer/INT_DIV_FORALL_P_', ax, (![P : ('type/integer/int' > $o), x : 'type/integer/int', c : 'type/integer/int']: ((~ (c = ('const/integer/int_of_num' 'const/num/0'))) => ((P ('const/integer/int_div' x c)) = (![k : 'type/integer/int', r : 'type/integer/int']: (((x = ('const/integer/int_add' ('const/integer/int_mul' k c) r)) & ((('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0')) & (('const/integer/int_lt' c r) & ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0')))) | ((~ ('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) & ('const/integer/int_lt' r c))))) => (P k))))))).
tt('thm/integer/INT_MOD_FORALL_P_', ax, (![P : ('type/integer/int' > $o), x : 'type/integer/int', c : 'type/integer/int']: ((~ (c = ('const/integer/int_of_num' 'const/num/0'))) => ((P ('const/integer/int_mod' x c)) = (![q : 'type/integer/int', r : 'type/integer/int']: (((x = ('const/integer/int_add' ('const/integer/int_mul' q c) r)) & ((('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0')) & (('const/integer/int_lt' c r) & ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0')))) | ((~ ('const/integer/int_lt' c ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) & ('const/integer/int_lt' r c))))) => (P r))))))).
tt('thm/integer/INT_MOD_1_', ax, (![i : 'type/integer/int']: (('const/integer/int_mod' i ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_LESS_MOD_', ax, (![i : 'type/integer/int', j : 'type/integer/int']: ((('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) & ('const/integer/int_lt' i j)) => (('const/integer/int_mod' i j) = i)))).
tt('thm/integer/INT_MOD_MINUS1_', ax, (![n : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') n) => (('const/integer/int_mod' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) n) = ('const/integer/int_sub' n ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/integer/INT_ABS_', def, (![n : 'type/integer/int']: (('const/integer/ABS' n) = (('const/bool/COND' 'type/integer/int') ('const/integer/int_lt' n ('const/integer/int_of_num' 'const/num/0')) ('const/integer/int_neg' n) n)))).
tt('thm/integer/INT_ABS_POS_', ax, (![p : 'type/integer/int']: ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/ABS' p)))).
tt('thm/integer/INT_ABS_NUM_', ax, (![n : 'type/num/num']: (('const/integer/ABS' ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' n)))).
tt('thm/integer/INT_NEG_SAME_EQ_', ax, (![p : 'type/integer/int']: ((p = ('const/integer/int_neg' p)) = (p = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_ABS_NEG_', ax, (![p : 'type/integer/int']: (('const/integer/ABS' ('const/integer/int_neg' p)) = ('const/integer/ABS' p)))).
tt('thm/integer/INT_ABS_ABS_', ax, (![p : 'type/integer/int']: (('const/integer/ABS' ('const/integer/ABS' p)) = ('const/integer/ABS' p)))).
tt('thm/integer/INT_ABS_EQ_ID_', ax, (![p : 'type/integer/int']: ((('const/integer/ABS' p) = p) = ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') p)))).
tt('thm/integer/INT_ABS_MUL_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/ABS' p) ('const/integer/ABS' q)) = ('const/integer/ABS' ('const/integer/int_mul' p q))))).
tt('thm/integer/INT_ABS_EQ0_', ax, (![p : 'type/integer/int']: ((('const/integer/ABS' p) = ('const/integer/int_of_num' 'const/num/0')) = (p = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_ABS_LT0_', ax, (![p : 'type/integer/int']: (~ ('const/integer/int_lt' ('const/integer/ABS' p) ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_ABS_LE0_', ax, (![p : 'type/integer/int']: (('const/integer/int_le' ('const/integer/ABS' p) ('const/integer/int_of_num' 'const/num/0')) = (p = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_ABS_LT_0', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/ABS' p) q) = (('const/integer/int_lt' p q) & ('const/integer/int_lt' ('const/integer/int_neg' q) p))))).
tt('thm/integer/INT_ABS_LT_1', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_lt' q ('const/integer/ABS' p)) = (('const/integer/int_lt' q p) | ('const/integer/int_lt' p ('const/integer/int_neg' q)))))).
tt('thm/integer/INT_ABS_LT_2', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/ABS' p)) q) = (('const/integer/int_lt' ('const/integer/int_neg' q) p) | ('const/integer/int_lt' p q))))).
tt('thm/integer/INT_ABS_LT_e3', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_lt' q ('const/integer/int_neg' ('const/integer/ABS' p))) = (('const/integer/int_lt' p ('const/integer/int_neg' q)) & ('const/integer/int_lt' q p))))).
tt('thm/integer/INT_ABS_LE_0', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_le' ('const/integer/ABS' p) q) = (('const/integer/int_le' p q) & ('const/integer/int_le' ('const/integer/int_neg' q) p))))).
tt('thm/integer/INT_ABS_LE_1', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_le' q ('const/integer/ABS' p)) = (('const/integer/int_le' q p) | ('const/integer/int_le' p ('const/integer/int_neg' q)))))).
tt('thm/integer/INT_ABS_LE_2', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_le' ('const/integer/int_neg' ('const/integer/ABS' p)) q) = (('const/integer/int_le' ('const/integer/int_neg' q) p) | ('const/integer/int_le' p q))))).
tt('thm/integer/INT_ABS_LE_e3', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_le' q ('const/integer/int_neg' ('const/integer/ABS' p))) = (('const/integer/int_le' p ('const/integer/int_neg' q)) & ('const/integer/int_le' q p))))).
tt('thm/integer/INT_ABS_EQ_0', ax, (![q : 'type/integer/int', p : 'type/integer/int']: ((('const/integer/ABS' p) = q) = (((p = q) & ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') q)) | ((p = ('const/integer/int_neg' q)) & ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') q)))))).
tt('thm/integer/INT_ABS_EQ_e1', ax, (![q : 'type/integer/int', p : 'type/integer/int']: ((q = ('const/integer/ABS' p)) = (((p = q) & ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') q)) | ((p = ('const/integer/int_neg' q)) & ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') q)))))).
tt('thm/integer/int_quot_', def, (![i : 'type/integer/int', j : 'type/integer/int']: ((~ (j = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_quot' i j) = (('const/bool/COND' 'type/integer/int') ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') j) (('const/bool/COND' 'type/integer/int') ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' i) ('const/integer/Num' j))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' ('const/integer/int_neg' i)) ('const/integer/Num' j))))) (('const/bool/COND' 'type/integer/int') ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') i) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' i) ('const/integer/Num' ('const/integer/int_neg' j))))) ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/integer/Num' ('const/integer/int_neg' i)) ('const/integer/Num' ('const/integer/int_neg' j)))))))))).
tt('thm/integer/INT_QUOT_', ax, (![p : 'type/num/num', q : 'type/num/num']: ((~ (q = 'const/num/0')) => (('const/integer/int_quot' ('const/integer/int_of_num' p) ('const/integer/int_of_num' q)) = ('const/integer/int_of_num' ('const/arithmetic/DIV' p q)))))).
tt('thm/integer/INT_QUOT_0_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_quot' ('const/integer/int_of_num' 'const/num/0') q) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_QUOT_1_', ax, (![p : 'type/integer/int']: (('const/integer/int_quot' p ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = p))).
tt('thm/integer/INT_QUOT_NEG_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => ((('const/integer/int_quot' ('const/integer/int_neg' p) q) = ('const/integer/int_neg' ('const/integer/int_quot' p q))) & (('const/integer/int_quot' p ('const/integer/int_neg' q)) = ('const/integer/int_neg' ('const/integer/int_quot' p q))))))).
tt('thm/integer/INT_ABS_QUOT_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => ('const/integer/int_le' ('const/integer/ABS' ('const/integer/int_mul' ('const/integer/int_quot' p q) q)) ('const/integer/ABS' p))))).
tt('thm/integer/INT_QUOT_UNIQUE_', ax, (![p : 'type/integer/int', q : 'type/integer/int', k : 'type/integer/int']: ((?[r : 'type/integer/int']: ((p = ('const/integer/int_add' ('const/integer/int_mul' k q) r)) & ((('const/bool/COND' $o) ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') p) ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0'))) & ('const/integer/int_lt' ('const/integer/ABS' r) ('const/integer/ABS' q))))) => (('const/integer/int_quot' p q) = k)))).
tt('thm/integer/INT_QUOT_ID_', ax, (![p : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_quot' p p) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/integer/int_rem_', def, (![i : 'type/integer/int', j : 'type/integer/int']: ((~ (j = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_rem' i j) = ('const/integer/int_sub' i ('const/integer/int_mul' ('const/integer/int_quot' i j) j)))))).
tt('thm/integer/INT_REM_', ax, (![p : 'type/num/num', q : 'type/num/num']: ((~ (q = 'const/num/0')) => (('const/integer/int_rem' ('const/integer/int_of_num' p) ('const/integer/int_of_num' q)) = ('const/integer/int_of_num' ('const/arithmetic/MOD' p q)))))).
tt('thm/integer/INT_REMQUOT_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (![p : 'type/integer/int']: ((p = ('const/integer/int_add' ('const/integer/int_mul' ('const/integer/int_quot' p q) q) ('const/integer/int_rem' p q))) & ((('const/bool/COND' $o) ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') p) ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_rem' p q)) ('const/integer/int_le' ('const/integer/int_rem' p q) ('const/integer/int_of_num' 'const/num/0'))) & ('const/integer/int_lt' ('const/integer/ABS' ('const/integer/int_rem' p q)) ('const/integer/ABS' q)))))))).
tt('thm/integer/INT_REM_UNIQUE_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: ((('const/integer/int_lt' ('const/integer/ABS' r) ('const/integer/ABS' q)) & ((('const/bool/COND' $o) ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') p) ('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') r) ('const/integer/int_le' r ('const/integer/int_of_num' 'const/num/0'))) & (?[k : 'type/integer/int']: (p = ('const/integer/int_add' ('const/integer/int_mul' k q) r))))) => (('const/integer/int_rem' p q) = r)))).
tt('thm/integer/INT_REM_NEG_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => ((('const/integer/int_rem' ('const/integer/int_neg' p) q) = ('const/integer/int_neg' ('const/integer/int_rem' p q))) & (('const/integer/int_rem' p ('const/integer/int_neg' q)) = ('const/integer/int_rem' p q)))))).
tt('thm/integer/INT_REM_ID_', ax, (![p : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_rem' p p) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_REM0_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_rem' ('const/integer/int_of_num' 'const/num/0') q) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_REM_COMMON_FACTOR_', ax, (![p : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (![q : 'type/integer/int']: (('const/integer/int_rem' ('const/integer/int_mul' q p) p) = ('const/integer/int_of_num' 'const/num/0')))))).
tt('thm/integer/INT_REM_EQ0_', ax, (![q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (![p : 'type/integer/int']: ((('const/integer/int_rem' p q) = ('const/integer/int_of_num' 'const/num/0')) = (?[k : 'type/integer/int']: (p = ('const/integer/int_mul' k q)))))))).
tt('thm/integer/INT_MUL_QUOT_', ax, (![p : 'type/integer/int', q : 'type/integer/int', k : 'type/integer/int']: (((~ (q = ('const/integer/int_of_num' 'const/num/0'))) & (('const/integer/int_rem' p q) = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_quot' ('const/integer/int_mul' k p) q) = ('const/integer/int_mul' k ('const/integer/int_quot' p q)))))).
tt('thm/integer/INT_REM_EQ_MOD_', ax, (![i : 'type/integer/int', n : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') n) => (('const/integer/int_rem' i n) = (('const/bool/COND' 'type/integer/int') ('const/integer/int_lt' i ('const/integer/int_of_num' 'const/num/0')) ('const/integer/int_add' ('const/integer/int_sub' ('const/integer/int_mod' ('const/integer/int_sub' i ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) n) n) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/integer/int_mod' i n)))))).
tt('thm/integer/INT_DIVIDES_', def, (![p : 'type/integer/int', q : 'type/integer/int']: (('const/integer/int_divides' p q) = (?[m : 'type/integer/int']: (('const/integer/int_mul' m p) = q))))).
tt('thm/integer/INT_DIVIDES_MOD0_', ax, (![p : 'type/integer/int', q : 'type/integer/int']: (('const/integer/int_divides' p q) = (((('const/integer/int_mod' q p) = ('const/integer/int_of_num' 'const/num/0')) & (~ (p = ('const/integer/int_of_num' 'const/num/0')))) | ((p = ('const/integer/int_of_num' 'const/num/0')) & (q = ('const/integer/int_of_num' 'const/num/0'))))))).
tt('thm/integer/INT_DIVIDES_0_0', ax, (![x : 'type/integer/int']: ('const/integer/int_divides' x ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_0_e1', ax, (![x : 'type/integer/int']: (('const/integer/int_divides' ('const/integer/int_of_num' 'const/num/0') x) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_DIVIDES_1_0', ax, (![x : 'type/integer/int']: ('const/integer/int_divides' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x))).
tt('thm/integer/INT_DIVIDES_1_e1', ax, (![x : 'type/integer/int']: (('const/integer/int_divides' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((x = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) | (x = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/integer/INT_DIVIDES_REFL_', ax, (![x : 'type/integer/int']: ('const/integer/int_divides' x x))).
tt('thm/integer/INT_DIVIDES_TRANS_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: ((('const/integer/int_divides' x y) & ('const/integer/int_divides' y z)) => ('const/integer/int_divides' x z)))).
tt('thm/integer/INT_DIVIDES_MUL_0', ax, (![q : 'type/integer/int', p : 'type/integer/int']: ('const/integer/int_divides' p ('const/integer/int_mul' p q)))).
tt('thm/integer/INT_DIVIDES_MUL_e1', ax, (![q : 'type/integer/int', p : 'type/integer/int']: ('const/integer/int_divides' p ('const/integer/int_mul' q p)))).
tt('thm/integer/INT_DIVIDES_LMUL_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: (('const/integer/int_divides' p q) => ('const/integer/int_divides' p ('const/integer/int_mul' q r))))).
tt('thm/integer/INT_DIVIDES_RMUL_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: (('const/integer/int_divides' p q) => ('const/integer/int_divides' p ('const/integer/int_mul' r q))))).
tt('thm/integer/INT_DIVIDES_MUL_BOTH_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: ((~ (p = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_divides' ('const/integer/int_mul' p q) ('const/integer/int_mul' p r)) = ('const/integer/int_divides' q r))))).
tt('thm/integer/INT_DIVIDES_LADD_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: (('const/integer/int_divides' p q) => (('const/integer/int_divides' p ('const/integer/int_add' q r)) = ('const/integer/int_divides' p r))))).
tt('thm/integer/INT_DIVIDES_RADD_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: (('const/integer/int_divides' p q) => (('const/integer/int_divides' p ('const/integer/int_add' r q)) = ('const/integer/int_divides' p r))))).
tt('thm/integer/INT_DIVIDES_NEG_0', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_divides' p ('const/integer/int_neg' q)) = ('const/integer/int_divides' p q)))).
tt('thm/integer/INT_DIVIDES_NEG_e1', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_divides' ('const/integer/int_neg' p) q) = ('const/integer/int_divides' p q)))).
tt('thm/integer/INT_DIVIDES_LSUB_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: (('const/integer/int_divides' p q) => (('const/integer/int_divides' p ('const/integer/int_sub' q r)) = ('const/integer/int_divides' p r))))).
tt('thm/integer/INT_DIVIDES_RSUB_', ax, (![p : 'type/integer/int', q : 'type/integer/int', r : 'type/integer/int']: (('const/integer/int_divides' p q) => (('const/integer/int_divides' p ('const/integer/int_sub' r q)) = ('const/integer/int_divides' p r))))).
tt('thm/integer/int_exp_0', def, (![p : 'type/integer/int']: (('const/integer/int_exp' p 'const/num/0') = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/integer/int_exp_e1', def, (![p : 'type/integer/int', n : 'type/num/num']: (('const/integer/int_exp' p ('const/num/SUC' n)) = ('const/integer/int_mul' p ('const/integer/int_exp' p n))))).
tt('thm/integer/INT_EXP_', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_of_num' n) m) = ('const/integer/int_of_num' ('const/arithmetic/EXP' n m))))).
tt('thm/integer/INT_EXP_EQ0_', ax, (![p : 'type/integer/int', n : 'type/num/num']: ((('const/integer/int_exp' p n) = ('const/integer/int_of_num' 'const/num/0')) = ((p = ('const/integer/int_of_num' 'const/num/0')) & (~ (n = 'const/num/0')))))).
tt('thm/integer/INT_MUL_SIGN_CASES_0', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_mul' p q)) = ((('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') p) & ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') q)) | (('const/integer/int_lt' p ('const/integer/int_of_num' 'const/num/0')) & ('const/integer/int_lt' q ('const/integer/int_of_num' 'const/num/0'))))))).
tt('thm/integer/INT_MUL_SIGN_CASES_e1', ax, (![q : 'type/integer/int', p : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_mul' p q) ('const/integer/int_of_num' 'const/num/0')) = ((('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') p) & ('const/integer/int_lt' q ('const/integer/int_of_num' 'const/num/0'))) | (('const/integer/int_lt' p ('const/integer/int_of_num' 'const/num/0')) & ('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') q)))))).
tt('thm/integer/INT_EXP_NEG_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/EVEN' n) => (('const/integer/int_exp' ('const/integer/int_neg' ('const/integer/int_of_num' m)) n) = ('const/integer/int_of_num' ('const/arithmetic/EXP' m n)))))).
tt('thm/integer/INT_EXP_NEG_e1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/arithmetic/ODD' n) => (('const/integer/int_exp' ('const/integer/int_neg' ('const/integer/int_of_num' m)) n) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/EXP' m n))))))).
tt('thm/integer/INT_EXP_ADD_EXPONENTS_', ax, (![n : 'type/num/num', m : 'type/num/num', p : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_exp' p n) ('const/integer/int_exp' p m)) = ('const/integer/int_exp' p ('const/arithmetic/+' n m))))).
tt('thm/integer/INT_EXP_MULTIPLY_EXPONENTS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/integer/int']: (('const/integer/int_exp' ('const/integer/int_exp' p n) m) = ('const/integer/int_exp' p ('const/arithmetic/*' n m))))).
tt('thm/integer/INT_EXP_MOD_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/integer/int']: ((('const/arithmetic/<=' n m) & (~ (p = ('const/integer/int_of_num' 'const/num/0')))) => (('const/integer/int_mod' ('const/integer/int_exp' p m) ('const/integer/int_exp' p n)) = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_EXP_SUBTRACT_EXPONENTS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/integer/int']: ((('const/arithmetic/<=' n m) & (~ (p = ('const/integer/int_of_num' 'const/num/0')))) => (('const/integer/int_div' ('const/integer/int_exp' p m) ('const/integer/int_exp' p n)) = ('const/integer/int_exp' p ('const/arithmetic/-' m n)))))).
tt('thm/integer/INT_MIN_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_min' x y) = (('const/bool/COND' 'type/integer/int') ('const/integer/int_lt' x y) x y)))).
tt('thm/integer/INT_MAX_', def, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_max' x y) = (('const/bool/COND' 'type/integer/int') ('const/integer/int_lt' x y) y x)))).
tt('thm/integer/INT_MIN_LT_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' x ('const/integer/int_min' y z)) => (('const/integer/int_lt' x y) & ('const/integer/int_lt' x z))))).
tt('thm/integer/INT_MAX_LT_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_max' x y) z) => (('const/integer/int_lt' x z) & ('const/integer/int_lt' y z))))).
tt('thm/integer/INT_MIN_NUM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_min' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' ('const/arithmetic/MIN' m n))))).
tt('thm/integer/INT_MAX_NUM_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_max' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' ('const/arithmetic/MAX' m n))))).
tt('thm/integer/INT_LT_MONO_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x) => (('const/integer/int_lt' ('const/integer/int_mul' x y) ('const/integer/int_mul' x z)) = ('const/integer/int_lt' y z))))).
tt('thm/integer/INT_LE_MONO_', ax, (![x : 'type/integer/int', y : 'type/integer/int', z : 'type/integer/int']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') x) => (('const/integer/int_le' ('const/integer/int_mul' x y) ('const/integer/int_mul' x z)) = ('const/integer/int_le' y z))))).
tt('thm/integer/INFINITE_INT_UNIV_', ax, (~ (('const/pred_set/FINITE' 'type/integer/int') ('const/pred_set/UNIV' 'type/integer/int')))).
tt('thm/integer/INT_ADD_CALCULATE_0', ax, (![p : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_of_num' 'const/num/0') p) = p))).
tt('thm/integer/INT_ADD_CALCULATE_1', ax, (![p : 'type/integer/int']: (('const/integer/int_add' p ('const/integer/int_of_num' 'const/num/0')) = p))).
tt('thm/integer/INT_ADD_CALCULATE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/integer/int_of_num' ('const/arithmetic/+' n m))))).
tt('thm/integer/INT_ADD_CALCULATE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_of_num' n) ('const/integer/int_neg' ('const/integer/int_of_num' m))) = (('const/bool/COND' 'type/integer/int') ('const/arithmetic/<=' m n) ('const/integer/int_of_num' ('const/arithmetic/-' n m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/-' m n))))))).
tt('thm/integer/INT_ADD_CALCULATE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' n)) ('const/integer/int_of_num' m)) = (('const/bool/COND' 'type/integer/int') ('const/arithmetic/<=' n m) ('const/integer/int_of_num' ('const/arithmetic/-' m n)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/-' n m))))))).
tt('thm/integer/INT_ADD_CALCULATE_e5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' n)) ('const/integer/int_neg' ('const/integer/int_of_num' m))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/+' n m)))))).
tt('thm/integer/INT_ADD_REDUCE_0', ax, (![p : 'type/integer/int']: (('const/integer/int_add' ('const/integer/int_of_num' 'const/num/0') p) = p))).
tt('thm/integer/INT_ADD_REDUCE_1', ax, (![p : 'type/integer/int']: (('const/integer/int_add' p ('const/integer/int_of_num' 'const/num/0')) = p))).
tt('thm/integer/INT_ADD_REDUCE_2', ax, (('const/integer/int_neg' ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_of_num' 'const/num/0'))).
tt('thm/integer/INT_ADD_REDUCE_3', ax, (![p : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' p)) = p))).
tt('thm/integer/INT_ADD_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/numeral/iZ' ('const/arithmetic/+' n m))))))).
tt('thm/integer/INT_ADD_REDUCE_5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = (('const/bool/COND' 'type/integer/int') ('const/arithmetic/<=' m n) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/-' n m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/-' m n)))))))).
tt('thm/integer/INT_ADD_REDUCE_6', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = (('const/bool/COND' 'type/integer/int') ('const/arithmetic/<=' n m) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/-' m n))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/-' n m)))))))).
tt('thm/integer/INT_ADD_REDUCE_e7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/numeral/iZ' ('const/arithmetic/+' n m)))))))).
tt('thm/integer/INT_SUB_CALCULATE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_sub' x y) = ('const/integer/int_add' x ('const/integer/int_neg' y))))).
tt('thm/integer/INT_SUB_REDUCE_0', ax, (![p : 'type/integer/int']: (('const/integer/int_sub' p ('const/integer/int_of_num' 'const/num/0')) = p))).
tt('thm/integer/INT_SUB_REDUCE_1', ax, (![p : 'type/integer/int']: (('const/integer/int_sub' ('const/integer/int_of_num' 'const/num/0') p) = ('const/integer/int_neg' p)))).
tt('thm/integer/INT_SUB_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_sub' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/integer/int_add' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))))))).
tt('thm/integer/INT_SUB_REDUCE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_sub' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))))))).
tt('thm/integer/INT_SUB_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_sub' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = ('const/integer/int_add' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))))).
tt('thm/integer/INT_SUB_REDUCE_e5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_sub' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))))).
tt('thm/integer/INT_MUL_CALCULATE_0', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/integer/int_mul' ('const/integer/int_of_num' m) ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' ('const/arithmetic/*' m n))))).
tt('thm/integer/INT_MUL_CALCULATE_1', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_neg' x) y) = ('const/integer/int_neg' ('const/integer/int_mul' x y))))).
tt('thm/integer/INT_MUL_CALCULATE_2', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_mul' x ('const/integer/int_neg' y)) = ('const/integer/int_neg' ('const/integer/int_mul' x y))))).
tt('thm/integer/INT_MUL_CALCULATE_e3', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' x)) = x))).
tt('thm/integer/INT_MUL_REDUCE_0', ax, (![p : 'type/integer/int']: (('const/integer/int_mul' p ('const/integer/int_of_num' 'const/num/0')) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_MUL_REDUCE_1', ax, (![p : 'type/integer/int']: (('const/integer/int_mul' ('const/integer/int_of_num' 'const/num/0') p) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_MUL_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/*' m n)))))).
tt('thm/integer/INT_MUL_REDUCE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/*' m n))))))).
tt('thm/integer/INT_MUL_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_mul' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/*' m n))))))).
tt('thm/integer/INT_MUL_REDUCE_e5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_mul' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/*' m n)))))).
tt('thm/integer/INT_DIV_CALCULATE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: ((~ (m = 'const/num/0')) => (('const/integer/int_div' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/integer/int_of_num' ('const/arithmetic/DIV' n m)))))).
tt('thm/integer/INT_DIV_CALCULATE_1', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_div' p ('const/integer/int_neg' q)) = ('const/integer/int_div' ('const/integer/int_neg' p) q))))).
tt('thm/integer/INT_DIV_CALCULATE_2', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/integer/int_of_num' m) = ('const/integer/int_of_num' n)) = (m = n)))).
tt('thm/integer/INT_DIV_CALCULATE_3', ax, (![x : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_of_num' 'const/num/0')) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_DIV_CALCULATE_e4', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' x)) = x))).
tt('thm/integer/INT_DIV_REDUCE_0', ax, (![n : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_DIV_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_DIV_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_DIV_REDUCE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_DIV_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) (('const/bool/COND' 'type/integer/int') (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = 'const/num/0') ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/integer/INT_DIV_REDUCE_5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) (('const/bool/COND' 'type/integer/int') (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = 'const/num/0') ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/integer/INT_DIV_REDUCE_6', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) (('const/bool/COND' 'type/integer/int') (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = 'const/num/0') ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/integer/INT_DIV_REDUCE_7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = ('const/integer/int_add' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) (('const/bool/COND' 'type/integer/int') (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = 'const/num/0') ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/integer/INT_DIV_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_DIV_REDUCE_e9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_div' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_QUOT_CALCULATE_0', ax, (![p : 'type/num/num', q : 'type/num/num']: ((~ (q = 'const/num/0')) => (('const/integer/int_quot' ('const/integer/int_of_num' p) ('const/integer/int_of_num' q)) = ('const/integer/int_of_num' ('const/arithmetic/DIV' p q)))))).
tt('thm/integer/INT_QUOT_CALCULATE_1', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => ((('const/integer/int_quot' ('const/integer/int_neg' p) q) = ('const/integer/int_neg' ('const/integer/int_quot' p q))) & (('const/integer/int_quot' p ('const/integer/int_neg' q)) = ('const/integer/int_neg' ('const/integer/int_quot' p q))))))).
tt('thm/integer/INT_QUOT_CALCULATE_2', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/integer/int_of_num' m) = ('const/integer/int_of_num' n)) = (m = n)))).
tt('thm/integer/INT_QUOT_CALCULATE_3', ax, (![x : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_of_num' 'const/num/0')) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_QUOT_CALCULATE_e4', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' x)) = x))).
tt('thm/integer/INT_QUOT_REDUCE_0', ax, (![n : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_QUOT_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_QUOT_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_QUOT_REDUCE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_QUOT_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))))).
tt('thm/integer/INT_QUOT_REDUCE_5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))))))).
tt('thm/integer/INT_QUOT_REDUCE_6', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))))).
tt('thm/integer/INT_QUOT_REDUCE_7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))))))).
tt('thm/integer/INT_QUOT_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_QUOT_REDUCE_e9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_quot' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = ('const/integer/int_of_num' ('const/arithmetic/DIV' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_MOD_CALCULATE_0', ax, (![n : 'type/num/num', m : 'type/num/num']: ((~ (m = 'const/num/0')) => (('const/integer/int_mod' ('const/integer/int_of_num' n) ('const/integer/int_of_num' m)) = ('const/integer/int_of_num' ('const/arithmetic/MOD' n m)))))).
tt('thm/integer/INT_MOD_CALCULATE_1', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => (('const/integer/int_mod' p ('const/integer/int_neg' q)) = ('const/integer/int_neg' ('const/integer/int_mod' ('const/integer/int_neg' p) q)))))).
tt('thm/integer/INT_MOD_CALCULATE_2', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' x)) = x))).
tt('thm/integer/INT_MOD_CALCULATE_3', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/integer/int_of_num' m) = ('const/integer/int_of_num' n)) = (m = n)))).
tt('thm/integer/INT_MOD_CALCULATE_e4', ax, (![x : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_of_num' 'const/num/0')) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_MOD_REDUCE_0', ax, (![n : 'type/num/num']: (('const/integer/int_mod' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_MOD_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_mod' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_MOD_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_mod' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_MOD_REDUCE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_mod' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_MOD_REDUCE_4', ax, (![x : 'type/integer/int', n : 'type/num/num']: (('const/integer/int_mod' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_sub' x ('const/integer/int_mul' ('const/integer/int_div' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))))).
tt('thm/integer/INT_MOD_REDUCE_e5', ax, (![x : 'type/integer/int', n : 'type/num/num']: (('const/integer/int_mod' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_sub' x ('const/integer/int_mul' ('const/integer/int_div' x ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))))))).
tt('thm/integer/INT_REM_CALCULATE_0', ax, (![p : 'type/num/num', q : 'type/num/num']: ((~ (q = 'const/num/0')) => (('const/integer/int_rem' ('const/integer/int_of_num' p) ('const/integer/int_of_num' q)) = ('const/integer/int_of_num' ('const/arithmetic/MOD' p q)))))).
tt('thm/integer/INT_REM_CALCULATE_1', ax, (![p : 'type/integer/int', q : 'type/integer/int']: ((~ (q = ('const/integer/int_of_num' 'const/num/0'))) => ((('const/integer/int_rem' ('const/integer/int_neg' p) q) = ('const/integer/int_neg' ('const/integer/int_rem' p q))) & (('const/integer/int_rem' p ('const/integer/int_neg' q)) = ('const/integer/int_rem' p q)))))).
tt('thm/integer/INT_REM_CALCULATE_2', ax, (![x : 'type/integer/int']: (('const/integer/int_neg' ('const/integer/int_neg' x)) = x))).
tt('thm/integer/INT_REM_CALCULATE_3', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/integer/int_of_num' m) = ('const/integer/int_of_num' n)) = (m = n)))).
tt('thm/integer/INT_REM_CALCULATE_e4', ax, (![x : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_of_num' 'const/num/0')) = (x = ('const/integer/int_of_num' 'const/num/0'))))).
tt('thm/integer/INT_REM_REDUCE_0', ax, (![n : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_REM_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' 'const/num/0')))).
tt('thm/integer/INT_REM_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_REM_REDUCE_3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_REM_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))))).
tt('thm/integer/INT_REM_REDUCE_5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))))))).
tt('thm/integer/INT_REM_REDUCE_6', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))))).
tt('thm/integer/INT_REM_REDUCE_7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))))).
tt('thm/integer/INT_REM_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))))))).
tt('thm/integer/INT_REM_REDUCE_e9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_rem' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))))))).
tt('thm/integer/INT_EXP_CALCULATE_0', ax, (![p : 'type/integer/int']: (('const/integer/int_exp' p 'const/num/0') = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/integer/INT_EXP_CALCULATE_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_of_num' n) m) = ('const/integer/int_of_num' ('const/arithmetic/EXP' n m))))).
tt('thm/integer/INT_EXP_CALCULATE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_neg' ('const/integer/int_of_num' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/EXP' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m))))))))).
tt('thm/integer/INT_EXP_CALCULATE_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_neg' ('const/integer/int_of_num' n)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/EXP' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)))))))).
tt('thm/integer/INT_EXP_REDUCE_0', ax, (![p : 'type/integer/int']: (('const/integer/int_exp' p 'const/num/0') = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/integer/INT_EXP_REDUCE_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/arithmetic/NUMERAL' m)) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/EXP' n m)))))).
tt('thm/integer/INT_EXP_REDUCE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/EXP' n ('const/arithmetic/BIT1' m)))))))).
tt('thm/integer/INT_EXP_REDUCE_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_exp' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/EXP' n ('const/arithmetic/BIT2' m))))))).
tt('thm/integer/INT_LT_REDUCE_0', ax, (![n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = $true))).
tt('thm/integer/INT_LT_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = $true))).
tt('thm/integer/INT_LT_REDUCE_2', ax, (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' 'const/num/0')) = $false)).
tt('thm/integer/INT_LT_REDUCE_3', ax, (![n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = $false))).
tt('thm/integer/INT_LT_REDUCE_4', ax, (![n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_LT_REDUCE_5', ax, (![n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_LT_REDUCE_6', ax, (![n : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_LT_REDUCE_7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = ('const/prim_rec/<' n m)))).
tt('thm/integer/INT_LT_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = $true))).
tt('thm/integer/INT_LT_REDUCE_9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = $true))).
tt('thm/integer/INT_LT_REDUCE_10', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = $false))).
tt('thm/integer/INT_LT_REDUCE_e11', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_lt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = ('const/prim_rec/<' m n)))).
tt('thm/integer/INT_LE_CALCULATE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_le' x y) = (('const/integer/int_lt' x y) | (x = y))))).
tt('thm/integer/INT_LE_REDUCE_0', ax, (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' 'const/num/0')) = $true)).
tt('thm/integer/INT_LE_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = $true))).
tt('thm/integer/INT_LE_REDUCE_2', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = $false))).
tt('thm/integer/INT_LE_REDUCE_3', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = $false))).
tt('thm/integer/INT_LE_REDUCE_4', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_LE_REDUCE_5', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_LE_REDUCE_6', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_LE_REDUCE_7', ax, (![n : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_LE_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = ('const/arithmetic/<=' n m)))).
tt('thm/integer/INT_LE_REDUCE_9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m))))) = $false))).
tt('thm/integer/INT_LE_REDUCE_10', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m))))) = $false))).
tt('thm/integer/INT_LE_REDUCE_11', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = $true))).
tt('thm/integer/INT_LE_REDUCE_e12', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_le' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = ('const/arithmetic/<=' m n)))).
tt('thm/integer/INT_GT_CALCULATE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_gt' x y) = ('const/integer/int_lt' y x)))).
tt('thm/integer/INT_GT_REDUCE_0', ax, (![n : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_GT_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_GT_REDUCE_2', ax, (('const/integer/int_gt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' 'const/num/0')) = $false)).
tt('thm/integer/INT_GT_REDUCE_3', ax, (![n : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_GT_REDUCE_4', ax, (![n : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = $false))).
tt('thm/integer/INT_GT_REDUCE_5', ax, (![n : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = $true))).
tt('thm/integer/INT_GT_REDUCE_6', ax, (![n : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = $true))).
tt('thm/integer/INT_GT_REDUCE_7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/prim_rec/<' n m)))).
tt('thm/integer/INT_GT_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = $true))).
tt('thm/integer/INT_GT_REDUCE_9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = $true))).
tt('thm/integer/INT_GT_REDUCE_10', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = $false))).
tt('thm/integer/INT_GT_REDUCE_e11', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_gt' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = ('const/prim_rec/<' m n)))).
tt('thm/integer/INT_GE_CALCULATE_', ax, (![x : 'type/integer/int', y : 'type/integer/int']: (('const/integer/int_ge' x y) = ('const/integer/int_le' y x)))).
tt('thm/integer/INT_GE_REDUCE_0', ax, (('const/integer/int_ge' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' 'const/num/0')) = $true)).
tt('thm/integer/INT_GE_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_GE_REDUCE_2', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_GE_REDUCE_3', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_GE_REDUCE_4', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = $false))).
tt('thm/integer/INT_GE_REDUCE_5', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = $false))).
tt('thm/integer/INT_GE_REDUCE_6', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = $true))).
tt('thm/integer/INT_GE_REDUCE_7', ax, (![n : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = $true))).
tt('thm/integer/INT_GE_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/arithmetic/<=' n m)))).
tt('thm/integer/INT_GE_REDUCE_9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = $false))).
tt('thm/integer/INT_GE_REDUCE_10', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = $false))).
tt('thm/integer/INT_GE_REDUCE_11', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = $true))).
tt('thm/integer/INT_GE_REDUCE_e12', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_ge' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)))) = ('const/arithmetic/<=' m n)))).
tt('thm/integer/INT_EQ_CALCULATE_0', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/integer/int_of_num' m) = ('const/integer/int_of_num' n)) = (m = n)))).
tt('thm/integer/INT_EQ_CALCULATE_1', ax, (![x : 'type/integer/int', y : 'type/integer/int']: ((('const/integer/int_neg' x) = ('const/integer/int_neg' y)) = (x = y)))).
tt('thm/integer/INT_EQ_CALCULATE_2', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_of_num' n) = ('const/integer/int_neg' ('const/integer/int_of_num' m))) = ((n = 'const/num/0') & (m = 'const/num/0'))))).
tt('thm/integer/INT_EQ_CALCULATE_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_neg' ('const/integer/int_of_num' n)) = ('const/integer/int_of_num' m)) = ((n = 'const/num/0') & (m = 'const/num/0'))))).
tt('thm/integer/INT_EQ_REDUCE_0', ax, ((('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_of_num' 'const/num/0')) = $true)).
tt('thm/integer/INT_EQ_REDUCE_1', ax, (![n : 'type/num/num']: ((('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_2', ax, (![n : 'type/num/num']: ((('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_3', ax, (![n : 'type/num/num']: ((('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_4', ax, (![n : 'type/num/num']: ((('const/integer/int_of_num' 'const/num/0') = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_5', ax, (![n : 'type/num/num']: ((('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_EQ_REDUCE_6', ax, (![n : 'type/num/num']: ((('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_EQ_REDUCE_7', ax, (![n : 'type/num/num']: ((('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_EQ_REDUCE_8', ax, (![n : 'type/num/num']: ((('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' 'const/num/0')) = $false))).
tt('thm/integer/INT_EQ_REDUCE_9', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n)) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = (n = m)))).
tt('thm/integer/INT_EQ_REDUCE_10', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_11', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_12', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_13', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = $false))).
tt('thm/integer/INT_EQ_REDUCE_e14', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' n))) = ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = (n = m)))).
tt('thm/integer/INT_DIVIDES_REDUCE_0', ax, (('const/integer/int_divides' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' 'const/num/0')) = $true)).
tt('thm/integer/INT_DIVIDES_REDUCE_1', ax, (![n : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) = $false))).
tt('thm/integer/INT_DIVIDES_REDUCE_2', ax, (![n : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_of_num' 'const/num/0') ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) = $false))).
tt('thm/integer/INT_DIVIDES_REDUCE_3', ax, (![p : 'type/integer/int']: (('const/integer/int_divides' p ('const/integer/int_of_num' 'const/num/0')) = $true))).
tt('thm/integer/INT_DIVIDES_REDUCE_4', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_5', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_6', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_7', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_8', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_9', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_10', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n)))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = 'const/num/0')))).
tt('thm/integer/INT_DIVIDES_REDUCE_e11', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/integer/int_divides' ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n)))) ('const/integer/int_neg' ('const/integer/int_of_num' ('const/arithmetic/NUMERAL' m)))) = (('const/arithmetic/MOD' ('const/arithmetic/NUMERAL' m) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = 'const/num/0')))).
tt('thm/integer/LEAST_INT_DEF_', def, (![P : ('type/integer/int' > $o)]: (('const/integer/LEAST_INT' P) = (('const/min/@' 'type/integer/int') (^[i : 'type/integer/int']: ((P i) & (![j : 'type/integer/int']: (('const/integer/int_lt' j i) => (~ (P j)))))))))).
