tt('const/real/#slash#', ty, ('type/realax/real' > ('type/realax/real' > 'type/realax/real'))).
tt('const/real/NUM_CEILING', ty, ('type/realax/real' > 'type/num/num')).
tt('const/real/NUM_FLOOR', ty, ('type/realax/real' > 'type/num/num')).
tt('const/real/abs', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/real/inf', ty, (('type/realax/real' > $o) > 'type/realax/real')).
tt('const/real/max', ty, ('type/realax/real' > ('type/realax/real' > 'type/realax/real'))).
tt('const/real/min', ty, ('type/realax/real' > ('type/realax/real' > 'type/realax/real'))).
tt('const/real/pos', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/real/pow', ty, ('type/realax/real' > ('type/num/num' > 'type/realax/real'))).
tt('const/real/real_ge', ty, ('type/realax/real' > ('type/realax/real' > $o))).
tt('const/real/real_gt', ty, ('type/realax/real' > ('type/realax/real' > $o))).
tt('const/real/real_lte', ty, ('type/realax/real' > ('type/realax/real' > $o))).
tt('const/real/real_of_num', ty, ('type/num/num' > 'type/realax/real')).
tt('const/real/real_sub', ty, ('type/realax/real' > ('type/realax/real' > 'type/realax/real'))).
tt('const/real/sum', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/num/num' > 'type/realax/real') > 'type/realax/real'))).
tt('const/real/sum_tupled', ty, (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) > 'type/realax/real')).
tt('const/real/sup', ty, (('type/realax/real' > $o) > 'type/realax/real')).
tt('thm/real/real_of_num_0', def, (('const/real/real_of_num' 'const/num/0') = 'const/realax/real_0')).
tt('thm/real/real_of_num_e1', def, (![n : 'type/num/num']: (('const/real/real_of_num' ('const/num/SUC' n)) = ('const/realax/real_add' ('const/real/real_of_num' n) 'const/realax/real_1')))).
tt('thm/real/REAL_0_', ax, ('const/realax/real_0' = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/real/REAL_1_', ax, ('const/realax/real_1' = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_10_', ax, (~ (('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_ADD_SYM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' x y) = ('const/realax/real_add' y x)))).
tt('thm/real/REAL_ADD_COMM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' x y) = ('const/realax/real_add' y x)))).
tt('thm/real/REAL_ADD_ASSOC_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_add' x ('const/realax/real_add' y z)) = ('const/realax/real_add' ('const/realax/real_add' x y) z)))).
tt('thm/real/REAL_ADD_LID_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' ('const/real/real_of_num' 'const/num/0') x) = x))).
tt('thm/real/REAL_ADD_LINV_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' ('const/realax/real_neg' x) x) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_LDISTRIB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' x ('const/realax/real_add' y z)) = ('const/realax/real_add' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z))))).
tt('thm/real/REAL_LT_TOTAL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((x = y) | (('const/realax/real_lt' x y) | ('const/realax/real_lt' y x))))).
tt('thm/real/REAL_LT_REFL_', ax, (![x : 'type/realax/real']: (~ ('const/realax/real_lt' x x)))).
tt('thm/real/REAL_LT_TRANS_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' x y) & ('const/realax/real_lt' y z)) => ('const/realax/real_lt' x z)))).
tt('thm/real/REAL_LT_IADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' y z) => ('const/realax/real_lt' ('const/realax/real_add' x y) ('const/realax/real_add' x z))))).
tt('thm/real/REAL_SUP_ALLPOS_', ax, (![P : ('type/realax/real' > $o)]: (((![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x))) & ((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z)))))) => (?[s : 'type/realax/real']: (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y s))))))).
tt('thm/real/REAL_MUL_SYM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' x y) = ('const/realax/real_mul' y x)))).
tt('thm/real/REAL_MUL_COMM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' x y) = ('const/realax/real_mul' y x)))).
tt('thm/real/REAL_MUL_ASSOC_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' x ('const/realax/real_mul' y z)) = ('const/realax/real_mul' ('const/realax/real_mul' x y) z)))).
tt('thm/real/REAL_MUL_LID_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) = x))).
tt('thm/real/REAL_MUL_LINV_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_mul' ('const/realax/inv' x) x) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_LT_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x y))))).
tt('thm/real/REAL_INV_0_', ax, (('const/realax/inv' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/real/real_sub_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' x y) = ('const/realax/real_add' x ('const/realax/real_neg' y))))).
tt('thm/real/real_lte_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x y) = (~ ('const/realax/real_lt' y x))))).
tt('thm/real/real_gt_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_gt' x y) = ('const/realax/real_lt' y x)))).
tt('thm/real/real_ge_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_ge' x y) = ('const/real/real_lte' y x)))).
tt('thm/real/real_div_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/#slash#' x y) = ('const/realax/real_mul' x ('const/realax/inv' y))))).
tt('thm/real/REAL_ADD_RID_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' x ('const/real/real_of_num' 'const/num/0')) = x))).
tt('thm/real/REAL_ADD_RINV_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' x ('const/realax/real_neg' x)) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_MUL_RID_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = x))).
tt('thm/real/REAL_MUL_RINV_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_mul' x ('const/realax/inv' x)) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_RDISTRIB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/realax/real_add' x y) z) = ('const/realax/real_add' ('const/realax/real_mul' x z) ('const/realax/real_mul' y z))))).
tt('thm/real/REAL_EQ_LADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_add' x y) = ('const/realax/real_add' x z)) = (y = z)))).
tt('thm/real/REAL_EQ_RADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_add' x z) = ('const/realax/real_add' y z)) = (x = y)))).
tt('thm/real/REAL_ADD_LID_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_add' x y) = y) = (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_ADD_RID_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_add' x y) = x) = (y = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_LNEG_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_add' x y) = ('const/real/real_of_num' 'const/num/0')) = (x = ('const/realax/real_neg' y))))).
tt('thm/real/REAL_RNEG_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_add' x y) = ('const/real/real_of_num' 'const/num/0')) = (y = ('const/realax/real_neg' x))))).
tt('thm/real/REAL_NEG_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_neg' ('const/realax/real_add' x y)) = ('const/realax/real_add' ('const/realax/real_neg' x) ('const/realax/real_neg' y))))).
tt('thm/real/REAL_MUL_LZERO_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' ('const/real/real_of_num' 'const/num/0') x) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_MUL_RZERO_', ax, (![x : 'type/realax/real']: (('const/realax/real_mul' x ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_NEG_LMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_neg' ('const/realax/real_mul' x y)) = ('const/realax/real_mul' ('const/realax/real_neg' x) y)))).
tt('thm/real/REAL_NEG_RMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_neg' ('const/realax/real_mul' x y)) = ('const/realax/real_mul' x ('const/realax/real_neg' y))))).
tt('thm/real/REAL_NEGNEG_', ax, (![x : 'type/realax/real']: (('const/realax/real_neg' ('const/realax/real_neg' x)) = x))).
tt('thm/real/REAL_NEG_MUL2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' ('const/realax/real_neg' x) ('const/realax/real_neg' y)) = ('const/realax/real_mul' x y)))).
tt('thm/real/REAL_ENTIRE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_mul' x y) = ('const/real/real_of_num' 'const/num/0')) = ((x = ('const/real/real_of_num' 'const/num/0')) | (y = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/REAL_LT_LADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' x y) ('const/realax/real_add' x z)) = ('const/realax/real_lt' y z)))).
tt('thm/real/REAL_LT_RADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' x z) ('const/realax/real_add' y z)) = ('const/realax/real_lt' x y)))).
tt('thm/real/REAL_NOT_LT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((~ ('const/realax/real_lt' x y)) = ('const/real/real_lte' y x)))).
tt('thm/real/REAL_LT_ANTISYM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (~ (('const/realax/real_lt' x y) & ('const/realax/real_lt' y x))))).
tt('thm/real/REAL_LT_GT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) => (~ ('const/realax/real_lt' y x))))).
tt('thm/real/REAL_NOT_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((~ ('const/real/real_lte' x y)) = ('const/realax/real_lt' y x)))).
tt('thm/real/REAL_LE_TOTAL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x y) | ('const/real/real_lte' y x)))).
tt('thm/real/REAL_LET_TOTAL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x y) | ('const/realax/real_lt' y x)))).
tt('thm/real/REAL_LTE_TOTAL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) | ('const/real/real_lte' y x)))).
tt('thm/real/REAL_LE_REFL_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' x x))).
tt('thm/real/REAL_LE_LT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x y) = (('const/realax/real_lt' x y) | (x = y))))).
tt('thm/real/REAL_LT_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) = (('const/real/real_lte' x y) & (~ (x = y)))))).
tt('thm/real/REAL_LT_IMP_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) => ('const/real/real_lte' x y)))).
tt('thm/real/REAL_LTE_TRANS_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' x y) & ('const/real/real_lte' y z)) => ('const/realax/real_lt' x z)))).
tt('thm/real/REAL_LET_TRANS_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_lte' x y) & ('const/realax/real_lt' y z)) => ('const/realax/real_lt' x z)))).
tt('thm/real/REAL_LE_TRANS_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_lte' x y) & ('const/real/real_lte' y z)) => ('const/real/real_lte' x z)))).
tt('thm/real/REAL_LE_ANTISYM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' x y) & ('const/real/real_lte' y x)) = (x = y)))).
tt('thm/real/REAL_LET_ANTISYM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (~ (('const/realax/real_lt' x y) & ('const/real/real_lte' y x))))).
tt('thm/real/REAL_LTE_ANTSYM_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (~ (('const/real/real_lte' x y) & ('const/realax/real_lt' y x))))).
tt('thm/real/REAL_NEG_LT0_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_neg' x) ('const/real/real_of_num' 'const/num/0')) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_NEG_GT0_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_neg' x)) = ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_NEG_LE0_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' x) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_NEG_GE0_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_neg' x)) = ('const/real/real_lte' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_LT_NEGTOTAL_', ax, (![x : 'type/realax/real']: ((x = ('const/real/real_of_num' 'const/num/0')) | (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) | ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_neg' x)))))).
tt('thm/real/REAL_LE_NEGTOTAL_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) | ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_neg' x))))).
tt('thm/real/REAL_LE_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x y))))).
tt('thm/real/REAL_LE_SQUARE_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x x)))).
tt('thm/real/REAL_LE_01_', ax, ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_LT_01_', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_LE_LADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' x y) ('const/realax/real_add' x z)) = ('const/real/real_lte' y z)))).
tt('thm/real/REAL_LE_RADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_add' x z) ('const/realax/real_add' y z)) = ('const/real/real_lte' x y)))).
tt('thm/real/REAL_LT_ADD2_', ax, (![w : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' w x) & ('const/realax/real_lt' y z)) => ('const/realax/real_lt' ('const/realax/real_add' w y) ('const/realax/real_add' x z))))).
tt('thm/real/REAL_LE_ADD2_', ax, (![w : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_lte' w x) & ('const/real/real_lte' y z)) => ('const/real/real_lte' ('const/realax/real_add' w y) ('const/realax/real_add' x z))))).
tt('thm/real/REAL_LE_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_add' x y))))).
tt('thm/real/REAL_LT_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_add' x y))))).
tt('thm/real/REAL_LT_ADDNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' y ('const/realax/real_add' x ('const/realax/real_neg' z))) = ('const/realax/real_lt' ('const/realax/real_add' y z) x)))).
tt('thm/real/REAL_LT_ADDNEG2_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' x ('const/realax/real_neg' y)) z) = ('const/realax/real_lt' x ('const/realax/real_add' z y))))).
tt('thm/real/REAL_LT_ADD1_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x y) => ('const/realax/real_lt' x ('const/realax/real_add' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/real/REAL_SUB_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' ('const/real/real_sub' x y) y) = x))).
tt('thm/real/REAL_SUB_ADD2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' y ('const/real/real_sub' x y)) = x))).
tt('thm/real/REAL_SUB_REFL_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' x x) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_SUB_0_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_sub' x y) = ('const/real/real_of_num' 'const/num/0')) = (x = y)))).
tt('thm/real/REAL_LE_DOUBLE_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_add' x x)) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_LE_NEGL_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' x) x) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_LE_NEGR_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' x ('const/realax/real_neg' x)) = ('const/real/real_lte' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_NEG_EQ0_', ax, (![x : 'type/realax/real']: ((('const/realax/real_neg' x) = ('const/real/real_of_num' 'const/num/0')) = (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_NEG_0_', ax, (('const/realax/real_neg' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/real/REAL_NEG_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_neg' ('const/real/real_sub' x y)) = ('const/real/real_sub' y x)))).
tt('thm/real/REAL_SUB_LT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/real_sub' x y)) = ('const/realax/real_lt' y x)))).
tt('thm/real/REAL_SUB_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/real_sub' x y)) = ('const/real/real_lte' y x)))).
tt('thm/real/REAL_ADD_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) x) = y))).
tt('thm/real/REAL_EQ_LMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_mul' x y) = ('const/realax/real_mul' x z)) = ((x = ('const/real/real_of_num' 'const/num/0')) | (y = z))))).
tt('thm/real/REAL_EQ_RMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_mul' x z) = ('const/realax/real_mul' y z)) = ((z = ('const/real/real_of_num' 'const/num/0')) | (x = y))))).
tt('thm/real/REAL_SUB_LDISTRIB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' x ('const/real/real_sub' y z)) = ('const/real/real_sub' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z))))).
tt('thm/real/REAL_SUB_RDISTRIB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/real/real_sub' x y) z) = ('const/real/real_sub' ('const/realax/real_mul' x z) ('const/realax/real_mul' y z))))).
tt('thm/real/REAL_NEG_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_neg' x) = y) = (x = ('const/realax/real_neg' y))))).
tt('thm/real/REAL_NEG_MINUS1_', ax, (![x : 'type/realax/real']: (('const/realax/real_neg' x) = ('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))).
tt('thm/real/REAL_INV_NZ_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (~ (('const/realax/inv' x) = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/REAL_INVINV_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/inv' ('const/realax/inv' x)) = x)))).
tt('thm/real/REAL_LT_IMP_NE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) => (~ (x = y))))).
tt('thm/real/REAL_INV_POS_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/inv' x))))).
tt('thm/real/REAL_LT_LMUL_0_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x y)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y))))).
tt('thm/real/REAL_LT_RMUL_0_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) => (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x y)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x))))).
tt('thm/real/REAL_LT_LMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/realax/real_lt' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z)) = ('const/realax/real_lt' y z))))).
tt('thm/real/REAL_LT_RMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/realax/real_lt' ('const/realax/real_mul' x z) ('const/realax/real_mul' y z)) = ('const/realax/real_lt' x y))))).
tt('thm/real/REAL_LT_RMUL_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' x y) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z)) => ('const/realax/real_lt' ('const/realax/real_mul' x z) ('const/realax/real_mul' y z))))).
tt('thm/real/REAL_LT_LMUL_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' y z) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)) => ('const/realax/real_lt' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z))))).
tt('thm/real/REAL_LINV_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_mul' x y) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (x = ('const/realax/inv' y))))).
tt('thm/real/REAL_RINV_UNIQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_mul' x y) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (y = ('const/realax/inv' x))))).
tt('thm/real/REAL_INV_INV_', ax, (![x : 'type/realax/real']: (('const/realax/inv' ('const/realax/inv' x)) = x))).
tt('thm/real/REAL_INV_EQ_0_', ax, (![x : 'type/realax/real']: ((('const/realax/inv' x) = ('const/real/real_of_num' 'const/num/0')) = (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_NEG_INV_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_neg' ('const/realax/inv' x)) = ('const/realax/inv' ('const/realax/real_neg' x)))))).
tt('thm/real/REAL_INV_1OVER_', ax, (![x : 'type/realax/real']: (('const/realax/inv' x) = ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x)))).
tt('thm/real/REAL_LT_INV_EQ_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/inv' x)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_LE_INV_EQ_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/inv' x)) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_LE_INV_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/inv' x))))).
tt('thm/real/REAL_LE_ADDR_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x ('const/realax/real_add' x y)) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)))).
tt('thm/real/REAL_LE_ADDL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' y ('const/realax/real_add' x y)) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_LT_ADDR_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x ('const/realax/real_add' x y)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)))).
tt('thm/real/REAL_LT_ADDL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' y ('const/realax/real_add' x y)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/REAL_', ax, (![n : 'type/num/num']: (('const/real/real_of_num' ('const/num/SUC' n)) = ('const/realax/real_add' ('const/real/real_of_num' n) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_POS_', ax, (![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' n)))).
tt('thm/real/REAL_LE_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/real/real_lte' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/arithmetic/<=' m n)))).
tt('thm/real/REAL_LT_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/prim_rec/<' m n)))).
tt('thm/real/REAL_INJ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/real/real_of_num' m) = ('const/real/real_of_num' n)) = (m = n)))).
tt('thm/real/REAL_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/realax/real_add' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/real/real_of_num' ('const/arithmetic/+' m n))))).
tt('thm/real/REAL_MUL_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/realax/real_mul' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/real/real_of_num' ('const/arithmetic/*' m n))))).
tt('thm/real/REAL_INV1_', ax, (('const/realax/inv' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_OVER1_', ax, (![x : 'type/realax/real']: (('const/real/#slash#' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = x))).
tt('thm/real/REAL_DIV_REFL_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/real/#slash#' x x) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_DIV_LZERO_', ax, (![x : 'type/realax/real']: (('const/real/#slash#' ('const/real/real_of_num' 'const/num/0') x) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/REAL_LT_NZ_', ax, (![n : 'type/num/num']: ((~ (('const/real/real_of_num' n) = ('const/real/real_of_num' 'const/num/0'))) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' n))))).
tt('thm/real/REAL_NZ_IMP_LT_', ax, (![n : 'type/num/num']: ((~ (n = 'const/num/0')) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' n))))).
tt('thm/real/REAL_LT_RDIV_0_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' y z)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y))))).
tt('thm/real/REAL_LT_RDIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/realax/real_lt' ('const/real/#slash#' x z) ('const/real/#slash#' y z)) = ('const/realax/real_lt' x y))))).
tt('thm/real/REAL_LT_FRACTION_0_', ax, (![n : 'type/num/num', d : 'type/realax/real']: ((~ (n = 'const/num/0')) => (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' d ('const/real/real_of_num' n))) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') d))))).
tt('thm/real/REAL_LT_MULTIPLE_', ax, (![n : 'type/num/num', d : 'type/realax/real']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) => (('const/realax/real_lt' d ('const/realax/real_mul' ('const/real/real_of_num' n) d)) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') d))))).
tt('thm/real/REAL_LT_FRACTION_', ax, (![n : 'type/num/num', d : 'type/realax/real']: (('const/prim_rec/<' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) n) => (('const/realax/real_lt' ('const/real/#slash#' d ('const/real/real_of_num' n)) d) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') d))))).
tt('thm/real/REAL_LT_HALF1_', ax, (![d : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' d ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') d)))).
tt('thm/real/REAL_LT_HALF2_', ax, (![d : 'type/realax/real']: (('const/realax/real_lt' ('const/real/#slash#' d ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) d) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') d)))).
tt('thm/real/REAL_DOUBLE_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' x x) = ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x)))).
tt('thm/real/REAL_DIV_LMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((~ (y = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_mul' y ('const/real/#slash#' x y)) = x)))).
tt('thm/real/REAL_DIV_RMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((~ (y = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_mul' ('const/real/#slash#' x y) y) = x)))).
tt('thm/real/REAL_HALF_DOUBLE_', ax, (![x : 'type/realax/real']: (('const/realax/real_add' ('const/real/#slash#' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/#slash#' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = x))).
tt('thm/real/REAL_DOWN_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (?[y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) & ('const/realax/real_lt' y x)))))).
tt('thm/real/REAL_DOWN2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => (?[z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) & (('const/realax/real_lt' z x) & ('const/realax/real_lt' z y))))))).
tt('thm/real/REAL_SUB_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' ('const/real/real_sub' x y) x) = ('const/realax/real_neg' y)))).
tt('thm/real/REAL_LT_ADD_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_add' x y) z) = ('const/realax/real_lt' x ('const/real/real_sub' z y))))).
tt('thm/real/REAL_LT_SUB_RADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_sub' x y) z) = ('const/realax/real_lt' x ('const/realax/real_add' z y))))).
tt('thm/real/REAL_LT_SUB_LADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' x ('const/real/real_sub' y z)) = ('const/realax/real_lt' ('const/realax/real_add' x z) y)))).
tt('thm/real/REAL_LE_SUB_LADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/real/real_lte' x ('const/real/real_sub' y z)) = ('const/real/real_lte' ('const/realax/real_add' x z) y)))).
tt('thm/real/REAL_LE_SUB_RADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_sub' x y) z) = ('const/real/real_lte' x ('const/realax/real_add' z y))))).
tt('thm/real/REAL_LT_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/realax/real_neg' x) ('const/realax/real_neg' y)) = ('const/realax/real_lt' y x)))).
tt('thm/real/REAL_LE_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' x) ('const/realax/real_neg' y)) = ('const/real/real_lte' y x)))).
tt('thm/real/REAL_ADD2_SUB2_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real', d : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' a b) ('const/realax/real_add' c d)) = ('const/realax/real_add' ('const/real/real_sub' a c) ('const/real/real_sub' b d))))).
tt('thm/real/REAL_SUB_LZERO_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' ('const/real/real_of_num' 'const/num/0') x) = ('const/realax/real_neg' x)))).
tt('thm/real/REAL_SUB_RZERO_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' x ('const/real/real_of_num' 'const/num/0')) = x))).
tt('thm/real/REAL_LET_ADD2_', ax, (![w : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_lte' w x) & ('const/realax/real_lt' y z)) => ('const/realax/real_lt' ('const/realax/real_add' w y) ('const/realax/real_add' x z))))).
tt('thm/real/REAL_LTE_ADD2_', ax, (![w : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' w x) & ('const/real/real_lte' y z)) => ('const/realax/real_lt' ('const/realax/real_add' w y) ('const/realax/real_add' x z))))).
tt('thm/real/REAL_LET_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_add' x y))))).
tt('thm/real/REAL_LTE_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_add' x y))))).
tt('thm/real/REAL_LT_MUL2_', ax, (![x1 : 'type/realax/real', x2 : 'type/realax/real', y1 : 'type/realax/real', y2 : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x1) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y1) & (('const/realax/real_lt' x1 x2) & ('const/realax/real_lt' y1 y2)))) => ('const/realax/real_lt' ('const/realax/real_mul' x1 y1) ('const/realax/real_mul' x2 y2))))).
tt('thm/real/REAL_LT_INV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x y)) => ('const/realax/real_lt' ('const/realax/inv' y) ('const/realax/inv' x))))).
tt('thm/real/REAL_SUB_LNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_neg' x) y) = ('const/realax/real_neg' ('const/realax/real_add' x y))))).
tt('thm/real/REAL_SUB_RNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' x ('const/realax/real_neg' y)) = ('const/realax/real_add' x y)))).
tt('thm/real/REAL_SUB_NEG2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_neg' x) ('const/realax/real_neg' y)) = ('const/real/real_sub' y x)))).
tt('thm/real/REAL_SUB_TRIANGLE_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real']: (('const/realax/real_add' ('const/real/real_sub' a b) ('const/real/real_sub' b c)) = ('const/real/real_sub' a c)))).
tt('thm/real/REAL_EQ_SUB_LADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((x = ('const/real/real_sub' y z)) = (('const/realax/real_add' x z) = y)))).
tt('thm/real/REAL_EQ_SUB_RADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_sub' x y) = z) = (x = ('const/realax/real_add' z y))))).
tt('thm/real/REAL_INV_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (((~ (x = ('const/real/real_of_num' 'const/num/0'))) & (~ (y = ('const/real/real_of_num' 'const/num/0')))) => (('const/realax/inv' ('const/realax/real_mul' x y)) = ('const/realax/real_mul' ('const/realax/inv' x) ('const/realax/inv' y)))))).
tt('thm/real/REAL_LE_LMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/real_lte' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z)) = ('const/real/real_lte' y z))))).
tt('thm/real/REAL_LE_RMUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/real/real_lte' ('const/realax/real_mul' x z) ('const/realax/real_mul' y z)) = ('const/real/real_lte' x y))))).
tt('thm/real/REAL_SUB_INV2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (((~ (x = ('const/real/real_of_num' 'const/num/0'))) & (~ (y = ('const/real/real_of_num' 'const/num/0')))) => (('const/real/real_sub' ('const/realax/inv' x) ('const/realax/inv' y)) = ('const/real/#slash#' ('const/real/real_sub' y x) ('const/realax/real_mul' x y)))))).
tt('thm/real/REAL_SUB_SUB2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' x ('const/real/real_sub' x y)) = y))).
tt('thm/real/REAL_ADD_SUB2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' x ('const/realax/real_add' x y)) = ('const/realax/real_neg' y)))).
tt('thm/real/REAL_MEAN_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' x y) => (?[z : 'type/realax/real']: (('const/realax/real_lt' x z) & ('const/realax/real_lt' z y)))))).
tt('thm/real/REAL_EQ_LMUL2_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => ((y = z) = (('const/realax/real_mul' x y) = ('const/realax/real_mul' x z)))))).
tt('thm/real/REAL_LE_MUL2_', ax, (![x1 : 'type/realax/real', x2 : 'type/realax/real', y1 : 'type/realax/real', y2 : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x1) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y1) & (('const/real/real_lte' x1 x2) & ('const/real/real_lte' y1 y2)))) => ('const/real/real_lte' ('const/realax/real_mul' x1 y1) ('const/realax/real_mul' x2 y2))))).
tt('thm/real/REAL_LE_LDIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' y ('const/realax/real_mul' z x))) => ('const/real/real_lte' ('const/real/#slash#' y x) z)))).
tt('thm/real/REAL_LE_RDIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/realax/real_mul' y x) z)) => ('const/real/real_lte' y ('const/real/#slash#' z x))))).
tt('thm/real/REAL_LT_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' x y))))).
tt('thm/real/REAL_LE_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y)) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' x y))))).
tt('thm/real/REAL_LT_1_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x y)) => ('const/realax/real_lt' ('const/real/#slash#' x y) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_LE_LMUL_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' y z)) => ('const/real/real_lte' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z))))).
tt('thm/real/REAL_LE_RMUL_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' y z)) => ('const/real/real_lte' ('const/realax/real_mul' y x) ('const/realax/real_mul' z x))))).
tt('thm/real/REAL_EQ_IMP_LE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((x = y) => ('const/real/real_lte' x y)))).
tt('thm/real/REAL_INV_LT1_', ax, (![x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/realax/inv' x))))).
tt('thm/real/REAL_POS_NZ_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (~ (x = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/REAL_EQ_RMUL_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (((~ (z = ('const/real/real_of_num' 'const/num/0'))) & (('const/realax/real_mul' x z) = ('const/realax/real_mul' y z))) => (x = y)))).
tt('thm/real/REAL_EQ_LMUL_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (((~ (x = ('const/real/real_of_num' 'const/num/0'))) & (('const/realax/real_mul' x y) = ('const/realax/real_mul' x z))) => (y = z)))).
tt('thm/real/REAL_FACT_NZ_', ax, (![n : 'type/num/num']: (~ (('const/real/real_of_num' ('const/arithmetic/FACT' n)) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_DIFFSQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' ('const/realax/real_add' x y) ('const/real/real_sub' x y)) = ('const/real/real_sub' ('const/realax/real_mul' x x) ('const/realax/real_mul' y y))))).
tt('thm/real/REAL_POASQ_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_mul' x x)) = (~ (x = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/REAL_SUMSQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_add' ('const/realax/real_mul' x x) ('const/realax/real_mul' y y)) = ('const/real/real_of_num' 'const/num/0')) = ((x = ('const/real/real_of_num' 'const/num/0')) & (y = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/REAL_EQ_NEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_neg' x) = ('const/realax/real_neg' y)) = (x = y)))).
tt('thm/real/REAL_DIV_MUL2_', ax, (![x : 'type/realax/real', z : 'type/realax/real']: (((~ (x = ('const/real/real_of_num' 'const/num/0'))) & (~ (z = ('const/real/real_of_num' 'const/num/0')))) => (![y : 'type/realax/real']: (('const/real/#slash#' y z) = ('const/real/#slash#' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z))))))).
tt('thm/real/REAL_MIDDLE1_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/real/real_lte' a b) => ('const/real/real_lte' a ('const/real/#slash#' ('const/realax/real_add' a b) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))).
tt('thm/real/REAL_MIDDLE2_', ax, (![a : 'type/realax/real', b : 'type/realax/real']: (('const/real/real_lte' a b) => ('const/real/real_lte' ('const/real/#slash#' ('const/realax/real_add' a b) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) b)))).
tt('thm/real/abs_', def, (![x : 'type/realax/real']: (('const/real/abs' x) = (('const/bool/COND' 'type/realax/real') ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) x ('const/realax/real_neg' x))))).
tt('thm/real/ABS_ZERO_', ax, (![x : 'type/realax/real']: ((('const/real/abs' x) = ('const/real/real_of_num' 'const/num/0')) = (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/ABS_0_', ax, (('const/real/abs' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/real/ABS_1_', ax, (('const/real/abs' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/ABS_NEG_', ax, (![x : 'type/realax/real']: (('const/real/abs' ('const/realax/real_neg' x)) = ('const/real/abs' x)))).
tt('thm/real/ABS_TRIANGLE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/abs' ('const/realax/real_add' x y)) ('const/realax/real_add' ('const/real/abs' x) ('const/real/abs' y))))).
tt('thm/real/ABS_POS_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/abs' x)))).
tt('thm/real/ABS_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/abs' ('const/realax/real_mul' x y)) = ('const/realax/real_mul' ('const/real/abs' x) ('const/real/abs' y))))).
tt('thm/real/ABS_LT_MUL2_', ax, (![w : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/abs' w) y) & ('const/realax/real_lt' ('const/real/abs' x) z)) => ('const/realax/real_lt' ('const/real/abs' ('const/realax/real_mul' w x)) ('const/realax/real_mul' y z))))).
tt('thm/real/ABS_SUB_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/abs' ('const/real/real_sub' x y)) = ('const/real/abs' ('const/real/real_sub' y x))))).
tt('thm/real/ABS_NZ_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) = ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/abs' x))))).
tt('thm/real/ABS_INV_', ax, (![x : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/real/abs' ('const/realax/inv' x)) = ('const/realax/inv' ('const/real/abs' x)))))).
tt('thm/real/ABS_ABS_', ax, (![x : 'type/realax/real']: (('const/real/abs' ('const/real/abs' x)) = ('const/real/abs' x)))).
tt('thm/real/ABS_LE_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' x ('const/real/abs' x)))).
tt('thm/real/ABS_REFL_', ax, (![x : 'type/realax/real']: ((('const/real/abs' x) = x) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/ABS_N_', ax, (![n : 'type/num/num']: (('const/real/abs' ('const/real/real_of_num' n)) = ('const/real/real_of_num' n)))).
tt('thm/real/ABS_BETWEEN_', ax, (![x : 'type/realax/real', y : 'type/realax/real', d : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') d) & (('const/realax/real_lt' ('const/real/real_sub' x d) y) & ('const/realax/real_lt' y ('const/realax/real_add' x d)))) = ('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' y x)) d)))).
tt('thm/real/ABS_BOUND_', ax, (![x : 'type/realax/real', y : 'type/realax/real', d : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x y)) d) => ('const/realax/real_lt' y ('const/realax/real_add' x d))))).
tt('thm/real/ABS_STILLNZ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x y)) ('const/real/abs' y)) => (~ (x = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/ABS_CASES_', ax, (![x : 'type/realax/real']: ((x = ('const/real/real_of_num' 'const/num/0')) | ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/abs' x))))).
tt('thm/real/ABS_BETWEEN1_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_lt' x z) & ('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' y x)) ('const/real/real_sub' z x))) => ('const/realax/real_lt' y z)))).
tt('thm/real/ABS_SIGN_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x y)) y) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))).
tt('thm/real/ABS_SIGN2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x y)) ('const/realax/real_neg' y)) => ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/ABS_DIV_', ax, (![y : 'type/realax/real']: ((~ (y = ('const/real/real_of_num' 'const/num/0'))) => (![x : 'type/realax/real']: (('const/real/abs' ('const/real/#slash#' x y)) = ('const/real/#slash#' ('const/real/abs' x) ('const/real/abs' y))))))).
tt('thm/real/ABS_CIRCLE_', ax, (![x : 'type/realax/real', y : 'type/realax/real', h : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' h) ('const/real/real_sub' ('const/real/abs' y) ('const/real/abs' x))) => ('const/realax/real_lt' ('const/real/abs' ('const/realax/real_add' x h)) ('const/real/abs' y))))).
tt('thm/real/REAL_SUB_ABS_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_sub' ('const/real/abs' x) ('const/real/abs' y)) ('const/real/abs' ('const/real/real_sub' x y))))).
tt('thm/real/ABS_SUB_ABS_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/real/abs' x) ('const/real/abs' y))) ('const/real/abs' ('const/real/real_sub' x y))))).
tt('thm/real/ABS_BETWEEN2_', ax, (![x0 : 'type/realax/real', x : 'type/realax/real', y0 : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' x0 y0) & (('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' x x0)) ('const/real/#slash#' ('const/real/real_sub' y0 x0) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & ('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' y y0)) ('const/real/#slash#' ('const/real/real_sub' y0 x0) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) => ('const/realax/real_lt' x y)))).
tt('thm/real/ABS_BOUNDS_', ax, (![x : 'type/realax/real', k : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' x) k) = (('const/real/real_lte' ('const/realax/real_neg' k) x) & ('const/real/real_lte' x k))))).
tt('thm/real/pow_0', def, (![x : 'type/realax/real']: (('const/real/pow' x 'const/num/0') = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/real/pow_e1', def, (![x : 'type/realax/real', n : 'type/num/num']: (('const/real/pow' x ('const/num/SUC' n)) = ('const/realax/real_mul' x ('const/real/pow' x n))))).
tt('thm/real/POW_0_', ax, (![n : 'type/num/num']: (('const/real/pow' ('const/real/real_of_num' 'const/num/0') ('const/num/SUC' n)) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/POW_NZ_', ax, (![c : 'type/realax/real', n : 'type/num/num']: ((~ (c = ('const/real/real_of_num' 'const/num/0'))) => (~ (('const/real/pow' c n) = ('const/real/real_of_num' 'const/num/0')))))).
tt('thm/real/POW_INV_', ax, (![c : 'type/realax/real']: ((~ (c = ('const/real/real_of_num' 'const/num/0'))) => (![n : 'type/num/num']: (('const/realax/inv' ('const/real/pow' c n)) = ('const/real/pow' ('const/realax/inv' c) n)))))).
tt('thm/real/POW_ABS_', ax, (![c : 'type/realax/real', n : 'type/num/num']: (('const/real/pow' ('const/real/abs' c) n) = ('const/real/abs' ('const/real/pow' c n))))).
tt('thm/real/POW_PLUS1_', ax, (![e : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e) => (![n : 'type/num/num']: ('const/real/real_lte' ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/realax/real_mul' ('const/real/real_of_num' n) e)) ('const/real/pow' ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e) n)))))).
tt('thm/real/POW_ADD_', ax, (![c : 'type/realax/real', m : 'type/num/num', n : 'type/num/num']: (('const/real/pow' c ('const/arithmetic/+' m n)) = ('const/realax/real_mul' ('const/real/pow' c m) ('const/real/pow' c n))))).
tt('thm/real/POW_1_', ax, (![x : 'type/realax/real']: (('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = x))).
tt('thm/real/POW_2_', ax, (![x : 'type/realax/real']: (('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/realax/real_mul' x x)))).
tt('thm/real/POW_ONE_', ax, (![n : 'type/num/num']: (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) n) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/real/POW_POS_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' x n)))))).
tt('thm/real/POW_LE_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/real/real_lte' x y)) => ('const/real/real_lte' ('const/real/pow' x n) ('const/real/pow' y n))))).
tt('thm/real/POW_M1_', ax, (![n : 'type/num/num']: (('const/real/abs' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) n)) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/real/POW_MUL_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/pow' ('const/realax/real_mul' x y) n) = ('const/realax/real_mul' ('const/real/pow' x n) ('const/real/pow' y n))))).
tt('thm/real/REAL_LE_POW2_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/real/ABS_POW2_', ax, (![x : 'type/realax/real']: (('const/real/abs' ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/real/REAL_POW2_ABS_', ax, (![x : 'type/realax/real']: (('const/real/pow' ('const/real/abs' x) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/real/REAL_LE1_POW2_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) => ('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_LT1_POW2_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) => ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' x ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/real/POW_POS_LT_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' x ('const/num/SUC' n)))))).
tt('thm/real/POW_2_LE1_', ax, (![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))).
tt('thm/real/POW_2_LT_', ax, (![n : 'type/num/num']: ('const/realax/real_lt' ('const/real/real_of_num' n) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))).
tt('thm/real/POW_MINUS1_', ax, (![n : 'type/num/num']: (('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/*' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/real/POW_LT_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x y)) => ('const/realax/real_lt' ('const/real/pow' x ('const/num/SUC' n)) ('const/real/pow' y ('const/num/SUC' n)))))).
tt('thm/real/REAL_POW_LT_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' x n))))).
tt('thm/real/POW_EQ_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y) & (('const/real/pow' x ('const/num/SUC' n)) = ('const/real/pow' y ('const/num/SUC' n))))) => (x = y)))).
tt('thm/real/POW_ZERO_', ax, (![n : 'type/num/num', x : 'type/realax/real']: ((('const/real/pow' x n) = ('const/real/real_of_num' 'const/num/0')) => (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/POW_ZERO_EQ_', ax, (![n : 'type/num/num', x : 'type/realax/real']: ((('const/real/pow' x ('const/num/SUC' n)) = ('const/real/real_of_num' 'const/num/0')) = (x = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_POW_LT2_', ax, (![n : 'type/num/num', x : 'type/realax/real', y : 'type/realax/real']: (((~ (n = 'const/num/0')) & (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x y))) => ('const/realax/real_lt' ('const/real/pow' x n) ('const/real/pow' y n))))).
tt('thm/real/REAL_POW_MONO_LT_', ax, (![m : 'type/num/num', n : 'type/num/num', x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) & ('const/prim_rec/<' m n)) => ('const/realax/real_lt' ('const/real/pow' x m) ('const/real/pow' x n))))).
tt('thm/real/REAL_POW_POW_', ax, (![x : 'type/realax/real', m : 'type/num/num', n : 'type/num/num']: (('const/real/pow' ('const/real/pow' x m) n) = ('const/real/pow' x ('const/arithmetic/*' m n))))).
tt('thm/real/REAL_SUP_SOMEPOS_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x))) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z))))) => (?[s : 'type/realax/real']: (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y s))))))).
tt('thm/real/SUP_LEMMA1_', ax, (![P : ('type/realax/real' > $o), s : 'type/realax/real', d : 'type/realax/real']: ((![y : 'type/realax/real']: ((?[x : 'type/realax/real']: (((^[x0 : 'type/realax/real']: (P ('const/realax/real_add' x0 d))) x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y s))) => (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y ('const/realax/real_add' s d))))))).
tt('thm/real/SUP_LEMMA2_', ax, (![P : ('type/realax/real' > $o)]: ((?[x : 'type/realax/real']: (P x)) => (?[d : 'type/realax/real', x : 'type/realax/real']: (((^[x0 : 'type/realax/real']: (P ('const/realax/real_add' x0 d))) x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)))))).
tt('thm/real/SUP_LEMMA3_', ax, (![P : ('type/realax/real' > $o), d : 'type/realax/real']: ((?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z)))) => (?[z : 'type/realax/real']: (![x : 'type/realax/real']: (((^[x0 : 'type/realax/real']: (P ('const/realax/real_add' x0 d))) x) => ('const/realax/real_lt' x z))))))).
tt('thm/real/REAL_SUP_EXISTS_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z))))) => (?[s : 'type/realax/real']: (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y s))))))).
tt('thm/real/sup_', def, (![P : ('type/realax/real' > $o)]: (('const/real/sup' P) = (('const/min/@' 'type/realax/real') (^[s : 'type/realax/real']: (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y s)))))))).
tt('thm/real/REAL_SUP_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z))))) => (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y ('const/real/sup' P))))))).
tt('thm/real/REAL_SUP_UBOUND_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z))))) => (![y : 'type/realax/real']: ((P y) => ('const/real/real_lte' y ('const/real/sup' P))))))).
tt('thm/real/SETOK_LE_LT_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/real/real_lte' x z))))) = ((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/realax/real_lt' x z)))))))).
tt('thm/real/REAL_SUP_LE_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/real/real_lte' x z))))) => (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((P x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y ('const/real/sup' P))))))).
tt('thm/real/REAL_SUP_UBOUND_LE_', ax, (![P : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (P x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((P x) => ('const/real/real_lte' x z))))) => (![y : 'type/realax/real']: ((P y) => ('const/real/real_lte' y ('const/real/sup' P))))))).
tt('thm/real/REAL_ARCH_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) => (![y : 'type/realax/real']: (?[n : 'type/num/num']: ('const/realax/real_lt' y ('const/realax/real_mul' ('const/real/real_of_num' n) x))))))).
tt('thm/real/REAL_ARCH_LEAST_', ax, (![y : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y) => (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (?[n : 'type/num/num']: (('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' n) y) x) & ('const/realax/real_lt' x ('const/realax/real_mul' ('const/real/real_of_num' ('const/num/SUC' n)) y))))))))).
tt('thm/real/sum_tupled_primitive_', def, ('const/real/sum_tupled' = (('const/relation/WFREC' ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) 'type/realax/real') (('const/min/@' (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) > (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) > $o))) (^[R : (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) > (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) > $o))]: ((('const/relation/WF' ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real'))) R) & (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (R (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) (('const/pair/,' 'type/num/num' 'type/num/num') n m) f) (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/num/SUC' m)) f)))))) (^[sum_tupled : (('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) > 'type/realax/real'), a : ('type/pair/prod' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real'))]: (('const/pair/pair_CASE' 'type/realax/real' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) a (^[v : ('type/pair/prod' 'type/num/num' 'type/num/num'), f : ('type/num/num' > 'type/realax/real')]: (('const/pair/pair_CASE' 'type/realax/real' 'type/num/num' 'type/num/num') v (^[n : 'type/num/num', v3 : 'type/num/num']: (('const/arithmetic/num_CASE' 'type/realax/real') v3 (('const/combin/I' 'type/realax/real') ('const/real/real_of_num' 'const/num/0')) (^[m : 'type/num/num']: (('const/combin/I' 'type/realax/real') ('const/realax/real_add' (sum_tupled (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) (('const/pair/,' 'type/num/num' 'type/num/num') n m) f)) (f ('const/arithmetic/+' n m)))))))))))))).
tt('thm/real/sum_curried_', def, (![x : ('type/pair/prod' 'type/num/num' 'type/num/num'), x1 : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' x x1) = ('const/real/sum_tupled' (('const/pair/,' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/num/num' > 'type/realax/real')) x x1))))).
tt('thm/real/sum_ind_', ax, (![P : (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/num/num' > 'type/realax/real') > $o))]: (((![n : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (P (('const/pair/,' 'type/num/num' 'type/num/num') n 'const/num/0') f)) & (![n : 'type/num/num', m : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: ((P (('const/pair/,' 'type/num/num' 'type/num/num') n m) f) => (P (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/num/SUC' m)) f)))) => (![v : 'type/num/num', v1 : 'type/num/num', v2 : ('type/num/num' > 'type/realax/real')]: (P (('const/pair/,' 'type/num/num' 'type/num/num') v v1) v2))))).
tt('thm/real/sum_0', ax, (![n : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n 'const/num/0') f) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/sum_e1', ax, (![n : 'type/num/num', m : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/num/SUC' m)) f) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n m) f) (f ('const/arithmetic/+' n m)))))).
tt('thm/real/sum_compute_0', ax, (![n : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n 'const/num/0') f) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/sum_compute_1', ax, (![n : 'type/num/num', m : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m))) f) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) f) (f ('const/arithmetic/+' n ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/real/sum_compute_e2', ax, (![n : 'type/num/num', m : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' m))) f) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m))) f) (f ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' m)))))))).
tt('thm/real/SUM_TWO_', ax, (![f : ('type/num/num' > 'type/realax/real'), n : 'type/num/num', p : 'type/num/num']: (('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) f) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n p) f)) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' ('const/arithmetic/+' n p)) f)))).
tt('thm/real/SUM_DIFF_', ax, (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) = ('const/real/real_sub' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' ('const/arithmetic/+' m n)) f) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' m) f))))).
tt('thm/real/ABS_SUM_', ax, (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: ('const/real/real_lte' ('const/real/abs' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f)) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[n0 : 'type/num/num']: ('const/real/abs' (f n0))))))).
tt('thm/real/SUM_LE_', ax, (![f : ('type/num/num' > 'type/realax/real'), g : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: ((![r : 'type/num/num']: ((('const/arithmetic/<=' m r) & ('const/prim_rec/<' r ('const/arithmetic/+' n m))) => ('const/real/real_lte' (f r) (g r)))) => ('const/real/real_lte' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) g))))).
tt('thm/real/SUM_EQ_', ax, (![f : ('type/num/num' > 'type/realax/real'), g : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: ((![r : 'type/num/num']: ((('const/arithmetic/<=' m r) & ('const/prim_rec/<' r ('const/arithmetic/+' n m))) => ((f r) = (g r)))) => (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) g))))).
tt('thm/real/SUM_POS_', ax, (![f : ('type/num/num' > 'type/realax/real')]: ((![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (f n))) => (![m : 'type/num/num', n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f)))))).
tt('thm/real/SUM_POS_GEN_', ax, (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num']: ((![n : 'type/num/num']: (('const/arithmetic/<=' m n) => ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') (f n)))) => (![n : 'type/num/num']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f)))))).
tt('thm/real/SUM_ABS_', ax, (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (('const/real/abs' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[m0 : 'type/num/num']: ('const/real/abs' (f m0))))) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[m0 : 'type/num/num']: ('const/real/abs' (f m0))))))).
tt('thm/real/SUM_ABS_LE_', ax, (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: ('const/real/real_lte' ('const/real/abs' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f)) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[n0 : 'type/num/num']: ('const/real/abs' (f n0))))))).
tt('thm/real/SUM_ZERO_', ax, (![f : ('type/num/num' > 'type/realax/real'), N : 'type/num/num']: ((![n : 'type/num/num']: (('const/arithmetic/>=' n N) => ((f n) = ('const/real/real_of_num' 'const/num/0')))) => (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/>=' m N) => (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) = ('const/real/real_of_num' 'const/num/0'))))))).
tt('thm/real/SUM_ADD_', ax, (![f : ('type/num/num' > 'type/realax/real'), g : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[n0 : 'type/num/num']: ('const/realax/real_add' (f n0) (g n0)))) = ('const/realax/real_add' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) g))))).
tt('thm/real/SUM_CMUL_', ax, (![f : ('type/num/num' > 'type/realax/real'), c : 'type/realax/real', m : 'type/num/num', n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[n0 : 'type/num/num']: ('const/realax/real_mul' c (f n0)))) = ('const/realax/real_mul' c ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f))))).
tt('thm/real/SUM_NEG_', ax, (![f : ('type/num/num' > 'type/realax/real'), n : 'type/num/num', d : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n d) (^[n0 : 'type/num/num']: ('const/realax/real_neg' (f n0)))) = ('const/realax/real_neg' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n d) f))))).
tt('thm/real/SUM_SUB_', ax, (![f : ('type/num/num' > 'type/realax/real'), g : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[n0 : 'type/num/num']: ('const/real/real_sub' (f n0) (g n0)))) = ('const/real/real_sub' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) g))))).
tt('thm/real/SUM_SUBST_', ax, (![f : ('type/num/num' > 'type/realax/real'), g : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', n : 'type/num/num']: ((![p : 'type/num/num']: ((('const/arithmetic/<=' m p) & ('const/prim_rec/<' p ('const/arithmetic/+' m n))) => ((f p) = (g p)))) => (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) g))))).
tt('thm/real/SUM_NSUB_', ax, (![n : 'type/num/num', f : ('type/num/num' > 'type/realax/real'), c : 'type/realax/real']: (('const/real/real_sub' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) f) ('const/realax/real_mul' ('const/real/real_of_num' n) c)) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[p : 'type/num/num']: ('const/real/real_sub' (f p) c)))))).
tt('thm/real/SUM_BOUND_', ax, (![f : ('type/num/num' > 'type/realax/real'), k : 'type/realax/real', m : 'type/num/num', n : 'type/num/num']: ((![p : 'type/num/num']: ((('const/arithmetic/<=' m p) & ('const/prim_rec/<' p ('const/arithmetic/+' m n))) => ('const/real/real_lte' (f p) k))) => ('const/real/real_lte' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) f) ('const/realax/real_mul' ('const/real/real_of_num' n) k))))).
tt('thm/real/SUM_GROUP_', ax, (![n : 'type/num/num', k : 'type/num/num', f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/*' m k) k) f))) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' ('const/arithmetic/*' n k)) f)))).
tt('thm/real/SUM_1_', ax, (![f : ('type/num/num' > 'type/realax/real'), n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) f) = (f n)))).
tt('thm/real/SUM_2_', ax, (![f : ('type/num/num' > 'type/realax/real'), n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) f) = ('const/realax/real_add' (f n) (f ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/real/SUM_OFFSET_', ax, (![f : ('type/num/num' > 'type/realax/real'), n : 'type/num/num', k : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[m : 'type/num/num']: (f ('const/arithmetic/+' m k)))) = ('const/real/real_sub' ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' ('const/arithmetic/+' n k)) f) ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' k) f))))).
tt('thm/real/SUM_REINDEX_', ax, (![f : ('type/num/num' > 'type/realax/real'), m : 'type/num/num', k : 'type/num/num', n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/+' m k) n) f) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[r : 'type/num/num']: (f ('const/arithmetic/+' r k))))))).
tt('thm/real/SUM_0_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') m n) (^[r : 'type/num/num']: ('const/real/real_of_num' 'const/num/0'))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/SUM_PERMUTE_0_', ax, (![n : 'type/num/num', p : ('type/num/num' > 'type/num/num')]: ((![y : 'type/num/num']: (('const/prim_rec/<' y n) => (('const/bool/?!' 'type/num/num') (^[x : 'type/num/num']: (('const/prim_rec/<' x n) & ((p x) = y)))))) => (![f : ('type/num/num' > 'type/realax/real')]: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) (^[n0 : 'type/num/num']: (f (p n0)))) = ('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' n) f)))))).
tt('thm/real/SUM_CANCEL_', ax, (![f : ('type/num/num' > 'type/realax/real'), n : 'type/num/num', d : 'type/num/num']: (('const/real/sum' (('const/pair/,' 'type/num/num' 'type/num/num') n d) (^[n0 : 'type/num/num']: ('const/real/real_sub' (f ('const/num/SUC' n0)) (f n0)))) = ('const/real/real_sub' (f ('const/arithmetic/+' n d)) (f n))))).
tt('thm/real/REAL_MUL_RNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' x ('const/realax/real_neg' y)) = ('const/realax/real_neg' ('const/realax/real_mul' x y))))).
tt('thm/real/REAL_MUL_LNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_mul' ('const/realax/real_neg' x) y) = ('const/realax/real_neg' ('const/realax/real_mul' x y))))).
tt('thm/real/real_lt_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_lt' x y) = (~ ('const/real/real_lte' y x))))).
tt('thm/real/REAL_LE_LADD_IMP_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/real/real_lte' y z) => ('const/real/real_lte' ('const/realax/real_add' x y) ('const/realax/real_add' x z))))).
tt('thm/real/REAL_LE_LNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' x) y) = ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_add' x y))))).
tt('thm/real/REAL_LE_NEG2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/realax/real_neg' x) ('const/realax/real_neg' y)) = ('const/real/real_lte' y x)))).
tt('thm/real/REAL_NEG_NEG_', ax, (![x : 'type/realax/real']: (('const/realax/real_neg' ('const/realax/real_neg' x)) = x))).
tt('thm/real/REAL_LE_RNEG_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x ('const/realax/real_neg' y)) = ('const/real/real_lte' ('const/realax/real_add' x y) ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_POW_INV_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/real/pow' ('const/realax/inv' x) n) = ('const/realax/inv' ('const/real/pow' x n))))).
tt('thm/real/REAL_POW_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real', n : 'type/num/num']: (('const/real/pow' ('const/real/#slash#' x y) n) = ('const/real/#slash#' ('const/real/pow' x n) ('const/real/pow' y n))))).
tt('thm/real/REAL_POW_ADD_', ax, (![x : 'type/realax/real', m : 'type/num/num', n : 'type/num/num']: (('const/real/pow' x ('const/arithmetic/+' m n)) = ('const/realax/real_mul' ('const/real/pow' x m) ('const/real/pow' x n))))).
tt('thm/real/REAL_LE_RDIV_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/real/real_lte' x ('const/real/#slash#' y z)) = ('const/real/real_lte' ('const/realax/real_mul' x z) y))))).
tt('thm/real/REAL_LE_LDIV_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/real/real_lte' ('const/real/#slash#' x z) y) = ('const/real/real_lte' x ('const/realax/real_mul' y z)))))).
tt('thm/real/REAL_LT_RDIV_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/realax/real_lt' x ('const/real/#slash#' y z)) = ('const/realax/real_lt' ('const/realax/real_mul' x z) y))))).
tt('thm/real/REAL_LT_LDIV_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => (('const/realax/real_lt' ('const/real/#slash#' x z) y) = ('const/realax/real_lt' x ('const/realax/real_mul' y z)))))).
tt('thm/real/REAL_EQ_RDIV_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => ((x = ('const/real/#slash#' y z)) = (('const/realax/real_mul' x z) = y))))).
tt('thm/real/REAL_EQ_LDIV_EQ_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') z) => ((('const/real/#slash#' x z) = y) = (x = ('const/realax/real_mul' y z)))))).
tt('thm/real/REAL_OF_NUM_POW_', ax, (![x : 'type/num/num', n : 'type/num/num']: (('const/real/pow' ('const/real/real_of_num' x) n) = ('const/real/real_of_num' ('const/arithmetic/EXP' x n))))).
tt('thm/real/REAL_ADD_LDISTRIB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' x ('const/realax/real_add' y z)) = ('const/realax/real_add' ('const/realax/real_mul' x y) ('const/realax/real_mul' x z))))).
tt('thm/real/REAL_ADD_RDISTRIB_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/realax/real_add' x y) z) = ('const/realax/real_add' ('const/realax/real_mul' x z) ('const/realax/real_mul' y z))))).
tt('thm/real/REAL_OF_NUM_ADD_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/realax/real_add' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/real/real_of_num' ('const/arithmetic/+' m n))))).
tt('thm/real/REAL_OF_NUM_LE_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/real/real_lte' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/arithmetic/<=' m n)))).
tt('thm/real/REAL_OF_NUM_MUL_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/realax/real_mul' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = ('const/real/real_of_num' ('const/arithmetic/*' m n))))).
tt('thm/real/REAL_OF_NUM_SUC_', ax, (![n : 'type/num/num']: (('const/realax/real_add' ('const/real/real_of_num' n) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/num/SUC' n))))).
tt('thm/real/REAL_OF_NUM_EQ_', ax, (![m : 'type/num/num', n : 'type/num/num']: ((('const/real/real_of_num' m) = ('const/real/real_of_num' n)) = (m = n)))).
tt('thm/real/REAL_EQ_MUL_LCANCEL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((('const/realax/real_mul' x y) = ('const/realax/real_mul' x z)) = ((x = ('const/real/real_of_num' 'const/num/0')) | (y = z))))).
tt('thm/real/REAL_ABS_0_', ax, (('const/real/abs' ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_of_num' 'const/num/0'))).
tt('thm/real/REAL_ABS_TRIANGLE_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/abs' ('const/realax/real_add' x y)) ('const/realax/real_add' ('const/real/abs' x) ('const/real/abs' y))))).
tt('thm/real/REAL_ABS_MUL_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/abs' ('const/realax/real_mul' x y)) = ('const/realax/real_mul' ('const/real/abs' x) ('const/real/abs' y))))).
tt('thm/real/REAL_ABS_POS_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/abs' x)))).
tt('thm/real/REAL_LE_EPSILON_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((![e : 'type/realax/real']: (('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e) => ('const/real/real_lte' x ('const/realax/real_add' y e)))) => ('const/real/real_lte' x y)))).
tt('thm/real/REAL_BIGNUM_', ax, (![r : 'type/realax/real']: (?[n : 'type/num/num']: ('const/realax/real_lt' r ('const/real/real_of_num' n))))).
tt('thm/real/REAL_INV_LT_ANTIMONO_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => (('const/realax/real_lt' ('const/realax/inv' x) ('const/realax/inv' y)) = ('const/realax/real_lt' y x))))).
tt('thm/real/REAL_INV_INJ_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ((('const/realax/inv' x) = ('const/realax/inv' y)) = (x = y)))).
tt('thm/real/REAL_DIV_RMUL_CANCEL_', ax, (![c : 'type/realax/real', a : 'type/realax/real', b : 'type/realax/real']: ((~ (c = ('const/real/real_of_num' 'const/num/0'))) => (('const/real/#slash#' ('const/realax/real_mul' a c) ('const/realax/real_mul' b c)) = ('const/real/#slash#' a b))))).
tt('thm/real/REAL_DIV_LMUL_CANCEL_', ax, (![c : 'type/realax/real', a : 'type/realax/real', b : 'type/realax/real']: ((~ (c = ('const/real/real_of_num' 'const/num/0'))) => (('const/real/#slash#' ('const/realax/real_mul' c a) ('const/realax/real_mul' c b)) = ('const/real/#slash#' a b))))).
tt('thm/real/REAL_DIV_ADD_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_add' ('const/real/#slash#' y x) ('const/real/#slash#' z x)) = ('const/real/#slash#' ('const/realax/real_add' y z) x)))).
tt('thm/real/REAL_ADD_RAT_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real', d : 'type/realax/real']: (((~ (b = ('const/real/real_of_num' 'const/num/0'))) & (~ (d = ('const/real/real_of_num' 'const/num/0')))) => (('const/realax/real_add' ('const/real/#slash#' a b) ('const/real/#slash#' c d)) = ('const/real/#slash#' ('const/realax/real_add' ('const/realax/real_mul' a d) ('const/realax/real_mul' b c)) ('const/realax/real_mul' b d)))))).
tt('thm/real/REAL_SUB_RAT_', ax, (![a : 'type/realax/real', b : 'type/realax/real', c : 'type/realax/real', d : 'type/realax/real']: (((~ (b = ('const/real/real_of_num' 'const/num/0'))) & (~ (d = ('const/real/real_of_num' 'const/num/0')))) => (('const/real/real_sub' ('const/real/#slash#' a b) ('const/real/#slash#' c d)) = ('const/real/#slash#' ('const/real/real_sub' ('const/realax/real_mul' a d) ('const/realax/real_mul' b c)) ('const/realax/real_mul' b d)))))).
tt('thm/real/REAL_SUB_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/real/real_sub' ('const/real/real_of_num' m) ('const/real/real_of_num' n)) = (('const/bool/COND' 'type/realax/real') (('const/arithmetic/-' m n) = 'const/num/0') ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/-' n m))) ('const/real/real_of_num' ('const/arithmetic/-' m n)))))).
tt('thm/real/pos_def_', def, (![x : 'type/realax/real']: (('const/real/pos' x) = (('const/bool/COND' 'type/realax/real') ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_POS_POS_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/pos' x)))).
tt('thm/real/REAL_POS_ID_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => (('const/real/pos' x) = x)))).
tt('thm/real/REAL_POS_INFLATE_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' x ('const/real/pos' x)))).
tt('thm/real/REAL_POS_MONO_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' x y) => ('const/real/real_lte' ('const/real/pos' x) ('const/real/pos' y))))).
tt('thm/real/REAL_POS_EQ_ZERO_', ax, (![x : 'type/realax/real']: ((('const/real/pos' x) = ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_lte' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/REAL_POS_LE_ZERO_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/pos' x) ('const/real/real_of_num' 'const/num/0')) = ('const/real/real_lte' x ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/real/min_def_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/min' x y) = (('const/bool/COND' 'type/realax/real') ('const/real/real_lte' x y) x y)))).
tt('thm/real/REAL_MIN_REFL_', ax, (![x : 'type/realax/real']: (('const/real/min' x x) = x))).
tt('thm/real/REAL_LE_MIN_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' z ('const/real/min' x y)) = (('const/real/real_lte' z x) & ('const/real/real_lte' z y))))).
tt('thm/real/REAL_MIN_LE_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/real/min' x y) z) = (('const/real/real_lte' x z) | ('const/real/real_lte' y z))))).
tt('thm/real/REAL_MIN_LE1_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/min' x y) x))).
tt('thm/real/REAL_MIN_LE2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' ('const/real/min' x y) y))).
tt('thm/real/REAL_MIN_ALT_0', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_lte' x y) => (('const/real/min' x y) = x)))).
tt('thm/real/REAL_MIN_ALT_e1', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_lte' y x) => (('const/real/min' x y) = y)))).
tt('thm/real/REAL_MIN_LE_LIN_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z) & ('const/real/real_lte' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/real/real_lte' ('const/real/min' x y) ('const/realax/real_add' ('const/realax/real_mul' z x) ('const/realax/real_mul' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z) y)))))).
tt('thm/real/REAL_MIN_ADD_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/min' ('const/realax/real_add' x z) ('const/realax/real_add' y z)) = ('const/realax/real_add' ('const/real/min' x y) z)))).
tt('thm/real/REAL_MIN_SUB_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/min' ('const/real/real_sub' x z) ('const/real/real_sub' y z)) = ('const/real/real_sub' ('const/real/min' x y) z)))).
tt('thm/real/REAL_IMP_MIN_LE2_', ax, (![x1 : 'type/realax/real', x2 : 'type/realax/real', y1 : 'type/realax/real', y2 : 'type/realax/real']: ((('const/real/real_lte' x1 y1) & ('const/real/real_lte' x2 y2)) => ('const/real/real_lte' ('const/real/min' x1 x2) ('const/real/min' y1 y2))))).
tt('thm/real/max_def_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/max' x y) = (('const/bool/COND' 'type/realax/real') ('const/real/real_lte' x y) y x)))).
tt('thm/real/REAL_MAX_REFL_', ax, (![x : 'type/realax/real']: (('const/real/max' x x) = x))).
tt('thm/real/REAL_LE_MAX_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' z ('const/real/max' x y)) = (('const/real/real_lte' z x) | ('const/real/real_lte' z y))))).
tt('thm/real/REAL_LE_MAX1_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' x ('const/real/max' x y)))).
tt('thm/real/REAL_LE_MAX2_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: ('const/real/real_lte' y ('const/real/max' x y)))).
tt('thm/real/REAL_MAX_LE_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_lte' ('const/real/max' x y) z) = (('const/real/real_lte' x z) & ('const/real/real_lte' y z))))).
tt('thm/real/REAL_MAX_ALT_0', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_lte' x y) => (('const/real/max' x y) = y)))).
tt('thm/real/REAL_MAX_ALT_e1', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/real_lte' y x) => (('const/real/max' x y) = x)))).
tt('thm/real/REAL_MAX_MIN_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/max' x y) = ('const/realax/real_neg' ('const/real/min' ('const/realax/real_neg' x) ('const/realax/real_neg' y)))))).
tt('thm/real/REAL_MIN_MAX_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/min' x y) = ('const/realax/real_neg' ('const/real/max' ('const/realax/real_neg' x) ('const/realax/real_neg' y)))))).
tt('thm/real/REAL_LIN_LE_MAX_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') z) & ('const/real/real_lte' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) => ('const/real/real_lte' ('const/realax/real_add' ('const/realax/real_mul' z x) ('const/realax/real_mul' ('const/real/real_sub' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) z) y)) ('const/real/max' x y))))).
tt('thm/real/REAL_MAX_ADD_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/max' ('const/realax/real_add' x z) ('const/realax/real_add' y z)) = ('const/realax/real_add' ('const/real/max' x y) z)))).
tt('thm/real/REAL_MAX_SUB_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/real/max' ('const/real/real_sub' x z) ('const/real/real_sub' y z)) = ('const/real/real_sub' ('const/real/max' x y) z)))).
tt('thm/real/REAL_IMP_MAX_LE2_', ax, (![x1 : 'type/realax/real', x2 : 'type/realax/real', y1 : 'type/realax/real', y2 : 'type/realax/real']: ((('const/real/real_lte' x1 y1) & ('const/real/real_lte' x2 y2)) => ('const/real/real_lte' ('const/real/max' x1 x2) ('const/real/max' y1 y2))))).
tt('thm/real/inf_def_', def, (![p : ('type/realax/real' > $o)]: (('const/real/inf' p) = ('const/realax/real_neg' ('const/real/sup' (^[r : 'type/realax/real']: (p ('const/realax/real_neg' r)))))))).
tt('thm/real/REAL_SUP_EXISTS_UNIQUE_', ax, (![p : ('type/realax/real' > $o)]: (((?[x : 'type/realax/real']: (p x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((p x) => ('const/real/real_lte' x z))))) => (('const/bool/?!' 'type/realax/real') (^[s : 'type/realax/real']: (![y : 'type/realax/real']: ((?[x : 'type/realax/real']: ((p x) & ('const/realax/real_lt' y x))) = ('const/realax/real_lt' y s)))))))).
tt('thm/real/REAL_SUP_MAX_', ax, (![p : ('type/realax/real' > $o), z : 'type/realax/real']: (((p z) & (![x : 'type/realax/real']: ((p x) => ('const/real/real_lte' x z)))) => (('const/real/sup' p) = z)))).
tt('thm/real/REAL_IMP_SUP_LE_', ax, (![p : ('type/realax/real' > $o), x : 'type/realax/real']: (((?[r : 'type/realax/real']: (p r)) & (![r : 'type/realax/real']: ((p r) => ('const/real/real_lte' r x)))) => ('const/real/real_lte' ('const/real/sup' p) x)))).
tt('thm/real/REAL_IMP_LE_SUP_', ax, (![p : ('type/realax/real' > $o), x : 'type/realax/real']: (((?[r : 'type/realax/real']: (p r)) & ((?[z : 'type/realax/real']: (![r : 'type/realax/real']: ((p r) => ('const/real/real_lte' r z)))) & (?[r : 'type/realax/real']: ((p r) & ('const/real/real_lte' x r))))) => ('const/real/real_lte' x ('const/real/sup' p))))).
tt('thm/real/REAL_INF_MIN_', ax, (![p : ('type/realax/real' > $o), z : 'type/realax/real']: (((p z) & (![x : 'type/realax/real']: ((p x) => ('const/real/real_lte' z x)))) => (('const/real/inf' p) = z)))).
tt('thm/real/REAL_IMP_LE_INF_', ax, (![p : ('type/realax/real' > $o), r : 'type/realax/real']: (((?[x : 'type/realax/real']: (p x)) & (![x : 'type/realax/real']: ((p x) => ('const/real/real_lte' r x)))) => ('const/real/real_lte' r ('const/real/inf' p))))).
tt('thm/real/REAL_IMP_INF_LE_', ax, (![p : ('type/realax/real' > $o), r : 'type/realax/real']: (((?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((p x) => ('const/real/real_lte' z x)))) & (?[x : 'type/realax/real']: ((p x) & ('const/real/real_lte' x r)))) => ('const/real/real_lte' ('const/real/inf' p) r)))).
tt('thm/real/REAL_INF_LT_', ax, (![p : ('type/realax/real' > $o), z : 'type/realax/real']: (((?[x : 'type/realax/real']: (p x)) & ('const/realax/real_lt' ('const/real/inf' p) z)) => (?[x : 'type/realax/real']: ((p x) & ('const/realax/real_lt' x z)))))).
tt('thm/real/REAL_INF_CLOSE_', ax, (![p : ('type/realax/real' > $o), e : 'type/realax/real']: (((?[x : 'type/realax/real']: (p x)) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e)) => (?[x : 'type/realax/real']: ((p x) & ('const/realax/real_lt' x ('const/realax/real_add' ('const/real/inf' p) e))))))).
tt('thm/real/SUP_EPSILON_', ax, (![p : ('type/realax/real' > $o), e : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') e) & ((?[x : 'type/realax/real']: (p x)) & (?[z : 'type/realax/real']: (![x : 'type/realax/real']: ((p x) => ('const/real/real_lte' x z)))))) => (?[x : 'type/realax/real']: ((p x) & ('const/real/real_lte' ('const/real/sup' p) ('const/realax/real_add' x e))))))).
tt('thm/real/REAL_LE_SUP_', ax, (![p : ('type/realax/real' > $o), x : 'type/realax/real']: (((?[y : 'type/realax/real']: (p y)) & (?[y : 'type/realax/real']: (![z : 'type/realax/real']: ((p z) => ('const/real/real_lte' z y))))) => (('const/real/real_lte' x ('const/real/sup' p)) = (![y : 'type/realax/real']: ((![z : 'type/realax/real']: ((p z) => ('const/real/real_lte' z y))) => ('const/real/real_lte' x y))))))).
tt('thm/real/REAL_INF_LE_', ax, (![p : ('type/realax/real' > $o), x : 'type/realax/real']: (((?[y : 'type/realax/real']: (p y)) & (?[y : 'type/realax/real']: (![z : 'type/realax/real']: ((p z) => ('const/real/real_lte' y z))))) => (('const/real/real_lte' ('const/real/inf' p) x) = (![y : 'type/realax/real']: ((![z : 'type/realax/real']: ((p z) => ('const/real/real_lte' y z))) => ('const/real/real_lte' y x))))))).
tt('thm/real/REAL_SUP_CONST_', ax, (![x : 'type/realax/real']: (('const/real/sup' (^[r : 'type/realax/real']: (r = x))) = x))).
tt('thm/real/REAL_MUL_SUB2_CANCEL_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' ('const/realax/real_mul' x y) ('const/realax/real_mul' ('const/real/real_sub' z x) y)) = ('const/realax/real_mul' z y)))).
tt('thm/real/REAL_MUL_SUB1_CANCEL_', ax, (![z : 'type/realax/real', x : 'type/realax/real', y : 'type/realax/real']: (('const/realax/real_add' ('const/realax/real_mul' y x) ('const/realax/real_mul' y ('const/real/real_sub' z x))) = ('const/realax/real_mul' y z)))).
tt('thm/real/REAL_NEG_HALF_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' x ('const/real/#slash#' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/real/#slash#' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_NEG_THIRD_', ax, (![x : 'type/realax/real']: (('const/real/real_sub' x ('const/real/#slash#' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) = ('const/real/#slash#' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) x) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/real/REAL_DIV_DENOM_CANCEL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/real/#slash#' ('const/real/#slash#' y x) ('const/real/#slash#' z x)) = ('const/real/#slash#' y z))))).
tt('thm/real/REAL_DIV_DENOM_CANCEL2_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/real/#slash#' ('const/real/#slash#' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/#slash#' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/real/#slash#' y z)))).
tt('thm/real/REAL_DIV_DENOM_CANCEL3_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/real/#slash#' ('const/real/#slash#' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/#slash#' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) = ('const/real/#slash#' y z)))).
tt('thm/real/REAL_DIV_INNER_CANCEL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_mul' ('const/real/#slash#' y x) ('const/real/#slash#' x z)) = ('const/real/#slash#' y z))))).
tt('thm/real/REAL_DIV_INNER_CANCEL2_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/real/#slash#' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) z)) = ('const/real/#slash#' y z)))).
tt('thm/real/REAL_DIV_INNER_CANCEL3_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/real/#slash#' y ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) z)) = ('const/real/#slash#' y z)))).
tt('thm/real/REAL_DIV_OUTER_CANCEL_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: ((~ (x = ('const/real/real_of_num' 'const/num/0'))) => (('const/realax/real_mul' ('const/real/#slash#' x y) ('const/real/#slash#' z x)) = ('const/real/#slash#' z y))))).
tt('thm/real/REAL_DIV_OUTER_CANCEL2_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) y) ('const/real/#slash#' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/real/#slash#' z y)))).
tt('thm/real/REAL_DIV_OUTER_CANCEL3_', ax, (![y : 'type/realax/real', z : 'type/realax/real']: (('const/realax/real_mul' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y) ('const/real/#slash#' z ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) = ('const/real/#slash#' z y)))).
tt('thm/real/REAL_DIV_REFL2_', ax, (('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_DIV_REFL3_', ax, (('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_HALF_BETWEEN_tLL', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/real/REAL_HALF_BETWEEN_tRL', ax, ('const/realax/real_lt' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_HALF_BETWEEN_1', ax, ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))).
tt('thm/real/REAL_HALF_BETWEEN_e2', ax, ('const/real/real_lte' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_THIRDS_BETWEEN_tLL', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_THIRDS_BETWEEN_tLRL', ax, ('const/realax/real_lt' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_THIRDS_BETWEEN_tLRRL', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_THIRDS_BETWEEN_tRRRL', ax, ('const/realax/real_lt' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_THIRDS_BETWEEN_1', ax, ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_THIRDS_BETWEEN_2', ax, ('const/real/real_lte' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_THIRDS_BETWEEN_3', ax, ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/real/REAL_THIRDS_BETWEEN_e4', ax, ('const/real/real_lte' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/real/REAL_LE_SUB_CANCEL2_', ax, (![x : 'type/realax/real', y : 'type/realax/real', z : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_sub' x z) ('const/real/real_sub' y z)) = ('const/real/real_lte' x y)))).
tt('thm/real/REAL_ADD_SUB_ALT_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/real_sub' ('const/realax/real_add' x y) y) = x))).
tt('thm/real/INFINITE_REAL_UNIV_', ax, (~ (('const/pred_set/FINITE' 'type/realax/real') ('const/pred_set/UNIV' 'type/realax/real')))).
tt('thm/real/add_rat_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/realax/real_add' ('const/real/#slash#' x y) ('const/real/#slash#' u v)) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_add' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) ('const/real/#slash#' u v)) (('const/bool/COND' 'type/realax/real') (v = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_add' ('const/real/#slash#' x y) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u v))) (('const/bool/COND' 'type/realax/real') (y = v) ('const/real/#slash#' ('const/realax/real_add' x u) v) ('const/real/#slash#' ('const/realax/real_add' ('const/realax/real_mul' x v) ('const/realax/real_mul' u y)) ('const/realax/real_mul' y v)))))))).
tt('thm/real/add_ratl_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' ('const/real/#slash#' x y) z) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_add' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) z) ('const/real/#slash#' ('const/realax/real_add' x ('const/realax/real_mul' z y)) y))))).
tt('thm/real/add_ratr_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_add' x ('const/real/#slash#' y z)) = (('const/bool/COND' 'type/realax/real') (z = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_add' x (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' y z))) ('const/real/#slash#' ('const/realax/real_add' ('const/realax/real_mul' x z) y) z))))).
tt('thm/real/add_ints_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_add' ('const/real/real_of_num' n) ('const/real/real_of_num' m)) = ('const/real/real_of_num' ('const/arithmetic/+' n m))))).
tt('thm/real/add_ints_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_add' ('const/realax/real_neg' ('const/real/real_of_num' n)) ('const/real/real_of_num' m)) = (('const/bool/COND' 'type/realax/real') ('const/arithmetic/<=' n m) ('const/real/real_of_num' ('const/arithmetic/-' m n)) ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/-' n m))))))).
tt('thm/real/add_ints_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_add' ('const/real/real_of_num' n) ('const/realax/real_neg' ('const/real/real_of_num' m))) = (('const/bool/COND' 'type/realax/real') ('const/prim_rec/<' n m) ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/-' m n))) ('const/real/real_of_num' ('const/arithmetic/-' n m)))))).
tt('thm/real/add_ints_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_add' ('const/realax/real_neg' ('const/real/real_of_num' n)) ('const/realax/real_neg' ('const/real/real_of_num' m))) = ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/+' n m)))))).
tt('thm/real/mult_rat_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/realax/real_mul' ('const/real/#slash#' x y) ('const/real/#slash#' u v)) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_mul' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) ('const/real/#slash#' u v)) (('const/bool/COND' 'type/realax/real') (v = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_mul' ('const/real/#slash#' x y) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u v))) ('const/real/#slash#' ('const/realax/real_mul' x u) ('const/realax/real_mul' y v))))))).
tt('thm/real/mult_ratl_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_mul' ('const/real/#slash#' x y) z) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_mul' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) z) ('const/real/#slash#' ('const/realax/real_mul' x z) y))))).
tt('thm/real/mult_ratr_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_mul' x ('const/real/#slash#' y z)) = (('const/bool/COND' 'type/realax/real') (z = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_mul' x (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' y z))) ('const/real/#slash#' ('const/realax/real_mul' x y) z))))).
tt('thm/real/mult_ints_0', ax, (![b : 'type/num/num', a : 'type/num/num']: (('const/realax/real_mul' ('const/real/real_of_num' a) ('const/real/real_of_num' b)) = ('const/real/real_of_num' ('const/arithmetic/*' a b))))).
tt('thm/real/mult_ints_1', ax, (![b : 'type/num/num', a : 'type/num/num']: (('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' a)) ('const/real/real_of_num' b)) = ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/*' a b)))))).
tt('thm/real/mult_ints_2', ax, (![b : 'type/num/num', a : 'type/num/num']: (('const/realax/real_mul' ('const/real/real_of_num' a) ('const/realax/real_neg' ('const/real/real_of_num' b))) = ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/*' a b)))))).
tt('thm/real/mult_ints_e3', ax, (![b : 'type/num/num', a : 'type/num/num']: (('const/realax/real_mul' ('const/realax/real_neg' ('const/real/real_of_num' a)) ('const/realax/real_neg' ('const/real/real_of_num' b))) = ('const/real/real_of_num' ('const/arithmetic/*' a b))))).
tt('thm/real/pow_rat_0', ax, (![x : 'type/realax/real']: (('const/real/pow' x 'const/num/0') = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/real/pow_rat_1', ax, (![n : 'type/num/num']: (('const/real/pow' ('const/real/real_of_num' 'const/num/0') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' n))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/pow_rat_2', ax, (![n : 'type/num/num']: (('const/real/pow' ('const/real/real_of_num' 'const/num/0') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' n))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/real/pow_rat_3', ax, (![n : 'type/num/num', a : 'type/num/num']: (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' a)) ('const/arithmetic/NUMERAL' n)) = ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' a) ('const/arithmetic/NUMERAL' n)))))).
tt('thm/real/pow_rat_4', ax, (![n : 'type/num/num', a : 'type/num/num']: (('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' a))) ('const/arithmetic/NUMERAL' n)) = (('const/bool/COND' ('type/realax/real' > 'type/realax/real')) ('const/arithmetic/ODD' ('const/arithmetic/NUMERAL' n)) 'const/realax/real_neg' (^[x : 'type/realax/real']: x) ('const/real/real_of_num' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' a) ('const/arithmetic/NUMERAL' n))))))).
tt('thm/real/pow_rat_e5', ax, (![y : 'type/realax/real', x : 'type/realax/real', n : 'type/num/num']: (('const/real/pow' ('const/real/#slash#' x y) n) = ('const/real/#slash#' ('const/real/pow' x n) ('const/real/pow' y n))))).
tt('thm/real/neg_rat_0', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/realax/real_neg' ('const/real/#slash#' x y)) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/realax/real_neg' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y))) ('const/real/#slash#' ('const/realax/real_neg' x) y))))).
tt('thm/real/neg_rat_e1', ax, (![y : 'type/realax/real', x : 'type/realax/real']: (('const/real/#slash#' x ('const/realax/real_neg' y)) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) ('const/real/#slash#' ('const/realax/real_neg' x) y))))).
tt('thm/real/eq_rat_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: ((('const/real/#slash#' x y) = ('const/real/#slash#' u v)) = (('const/bool/COND' $o) (y = ('const/real/real_of_num' 'const/num/0')) ((('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) = ('const/real/#slash#' u v)) (('const/bool/COND' $o) (v = ('const/real/real_of_num' 'const/num/0')) (('const/real/#slash#' x y) = (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u v))) (('const/bool/COND' $o) (y = v) (x = u) (('const/realax/real_mul' x v) = ('const/realax/real_mul' y u)))))))).
tt('thm/real/eq_ratl_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: ((('const/real/#slash#' x y) = z) = (('const/bool/COND' $o) (y = ('const/real/real_of_num' 'const/num/0')) ((('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) = z) (x = ('const/realax/real_mul' y z)))))).
tt('thm/real/eq_ratr_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: ((z = ('const/real/#slash#' x y)) = (('const/bool/COND' $o) (y = ('const/real/real_of_num' 'const/num/0')) (z = (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y))) (('const/realax/real_mul' y z) = x))))).
tt('thm/real/eq_ints_0', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/real/real_of_num' n) = ('const/real/real_of_num' m)) = (n = m)))).
tt('thm/real/eq_ints_1', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/realax/real_neg' ('const/real/real_of_num' n)) = ('const/real/real_of_num' m)) = ((n = 'const/num/0') & (m = 'const/num/0'))))).
tt('thm/real/eq_ints_2', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/real/real_of_num' n) = ('const/realax/real_neg' ('const/real/real_of_num' m))) = ((n = 'const/num/0') & (m = 'const/num/0'))))).
tt('thm/real/eq_ints_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: ((('const/realax/real_neg' ('const/real/real_of_num' n)) = ('const/realax/real_neg' ('const/real/real_of_num' m))) = (n = m)))).
tt('thm/real/div_ratr_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/real/#slash#' x ('const/real/#slash#' y z)) = (('const/bool/COND' 'type/realax/real') ((y = ('const/real/real_of_num' 'const/num/0')) | (z = ('const/real/real_of_num' 'const/num/0'))) ('const/real/#slash#' x (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' y z))) ('const/real/#slash#' ('const/realax/real_mul' x z) y))))).
tt('thm/real/div_ratl_', ax, (![z : 'type/realax/real', y : 'type/realax/real', x : 'type/realax/real']: (('const/real/#slash#' ('const/real/#slash#' x y) z) = (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/real/#slash#' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) z) (('const/bool/COND' 'type/realax/real') (z = ('const/real/real_of_num' 'const/num/0')) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' ('const/real/#slash#' x y) z)) ('const/real/#slash#' x ('const/realax/real_mul' y z))))))).
tt('thm/real/div_rat_', ax, (![y : 'type/realax/real', x : 'type/realax/real', v : 'type/realax/real', u : 'type/realax/real']: (('const/real/#slash#' ('const/real/#slash#' x y) ('const/real/#slash#' u v)) = (('const/bool/COND' 'type/realax/real') ((u = ('const/real/real_of_num' 'const/num/0')) | (v = ('const/real/real_of_num' 'const/num/0'))) ('const/real/#slash#' ('const/real/#slash#' x y) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u v))) (('const/bool/COND' 'type/realax/real') (y = ('const/real/real_of_num' 'const/num/0')) ('const/real/#slash#' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x y)) ('const/real/#slash#' u v)) ('const/real/#slash#' ('const/realax/real_mul' x v) ('const/realax/real_mul' y u))))))).
tt('thm/real/le_rat_', ax, (![x : 'type/realax/real', u : 'type/realax/real', n : 'type/num/num', m : 'type/num/num']: (('const/real/real_lte' ('const/real/#slash#' x ('const/real/real_of_num' n)) ('const/real/#slash#' u ('const/real/real_of_num' m))) = (('const/bool/COND' $o) (n = 'const/num/0') ('const/real/real_lte' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x ('const/real/real_of_num' 'const/num/0'))) ('const/real/#slash#' u ('const/real/real_of_num' m))) (('const/bool/COND' $o) (m = 'const/num/0') ('const/real/real_lte' ('const/real/#slash#' x ('const/real/real_of_num' n)) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u ('const/real/real_of_num' 'const/num/0')))) ('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' m) x) ('const/realax/real_mul' ('const/real/real_of_num' n) u))))))).
tt('thm/real/le_ratl_', ax, (![x : 'type/realax/real', u : 'type/realax/real', n : 'type/num/num']: (('const/real/real_lte' ('const/real/#slash#' x ('const/real/real_of_num' n)) u) = (('const/bool/COND' $o) (n = 'const/num/0') ('const/real/real_lte' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x ('const/real/real_of_num' 'const/num/0'))) u) ('const/real/real_lte' x ('const/realax/real_mul' ('const/real/real_of_num' n) u)))))).
tt('thm/real/le_ratr_', ax, (![x : 'type/realax/real', u : 'type/realax/real', m : 'type/num/num']: (('const/real/real_lte' x ('const/real/#slash#' u ('const/real/real_of_num' m))) = (('const/bool/COND' $o) (m = 'const/num/0') ('const/real/real_lte' x (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u ('const/real/real_of_num' 'const/num/0')))) ('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' m) x) u))))).
tt('thm/real/le_int_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/real/real_lte' ('const/real/real_of_num' n) ('const/real/real_of_num' m)) = ('const/arithmetic/<=' n m)))).
tt('thm/real/le_int_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' n)) ('const/real/real_of_num' m)) = $true))).
tt('thm/real/le_int_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/real/real_lte' ('const/real/real_of_num' n) ('const/realax/real_neg' ('const/real/real_of_num' m))) = ((n = 'const/num/0') & (m = 'const/num/0'))))).
tt('thm/real/le_int_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/real/real_lte' ('const/realax/real_neg' ('const/real/real_of_num' n)) ('const/realax/real_neg' ('const/real/real_of_num' m))) = ('const/arithmetic/<=' m n)))).
tt('thm/real/lt_rat_', ax, (![x : 'type/realax/real', u : 'type/realax/real', n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_lt' ('const/real/#slash#' x ('const/real/real_of_num' n)) ('const/real/#slash#' u ('const/real/real_of_num' m))) = (('const/bool/COND' $o) (n = 'const/num/0') ('const/realax/real_lt' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x ('const/real/real_of_num' 'const/num/0'))) ('const/real/#slash#' u ('const/real/real_of_num' m))) (('const/bool/COND' $o) (m = 'const/num/0') ('const/realax/real_lt' ('const/real/#slash#' x ('const/real/real_of_num' n)) (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u ('const/real/real_of_num' 'const/num/0')))) ('const/realax/real_lt' ('const/realax/real_mul' ('const/real/real_of_num' m) x) ('const/realax/real_mul' ('const/real/real_of_num' n) u))))))).
tt('thm/real/lt_ratl_', ax, (![x : 'type/realax/real', u : 'type/realax/real', n : 'type/num/num']: (('const/realax/real_lt' ('const/real/#slash#' x ('const/real/real_of_num' n)) u) = (('const/bool/COND' $o) (n = 'const/num/0') ('const/realax/real_lt' (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' x ('const/real/real_of_num' 'const/num/0'))) u) ('const/realax/real_lt' x ('const/realax/real_mul' ('const/real/real_of_num' n) u)))))).
tt('thm/real/lt_ratr_', ax, (![x : 'type/realax/real', u : 'type/realax/real', m : 'type/num/num']: (('const/realax/real_lt' x ('const/real/#slash#' u ('const/real/real_of_num' m))) = (('const/bool/COND' $o) (m = 'const/num/0') ('const/realax/real_lt' x (('const/marker/unint' 'type/realax/real') ('const/real/#slash#' u ('const/real/real_of_num' 'const/num/0')))) ('const/realax/real_lt' ('const/realax/real_mul' ('const/real/real_of_num' m) x) u))))).
tt('thm/real/lt_int_0', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' n) ('const/real/real_of_num' m)) = ('const/prim_rec/<' n m)))).
tt('thm/real/lt_int_1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' n)) ('const/real/real_of_num' m)) = ((~ (n = 'const/num/0')) | (~ (m = 'const/num/0')))))).
tt('thm/real/lt_int_2', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_lt' ('const/real/real_of_num' n) ('const/realax/real_neg' ('const/real/real_of_num' m))) = $false))).
tt('thm/real/lt_int_e3', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/realax/real_lt' ('const/realax/real_neg' ('const/real/real_of_num' n)) ('const/realax/real_neg' ('const/real/real_of_num' m))) = ('const/prim_rec/<' m n)))).
tt('thm/real/NUM_FLOOR_def_', def, (![x : 'type/realax/real']: (('const/real/NUM_FLOOR' x) = ('const/while/LEAST' (^[n : 'type/num/num']: ('const/real/real_gt' ('const/real/real_of_num' ('const/arithmetic/+' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) x)))))).
tt('thm/real/NUM_CEILING_def_', def, (![x : 'type/realax/real']: (('const/real/NUM_CEILING' x) = ('const/while/LEAST' (^[n : 'type/num/num']: ('const/real/real_lte' x ('const/real/real_of_num' n))))))).
tt('thm/real/NUM_FLOOR_LE_', ax, (![x : 'type/realax/real']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) => ('const/real/real_lte' ('const/real/real_of_num' ('const/real/NUM_FLOOR' x)) x)))).
tt('thm/real/NUM_FLOOR_LE2_', ax, (![y : 'type/realax/real', x : 'type/num/num']: (('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') y) => (('const/arithmetic/<=' x ('const/real/NUM_FLOOR' y)) = ('const/real/real_lte' ('const/real/real_of_num' x) y))))).
tt('thm/real/NUM_FLOOR_LET_', ax, (![y : 'type/num/num', x : 'type/realax/real']: (('const/arithmetic/<=' ('const/real/NUM_FLOOR' x) y) = ('const/realax/real_lt' x ('const/realax/real_add' ('const/real/real_of_num' y) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/real/NUM_FLOOR_DIV_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/real/real_lte' ('const/realax/real_mul' ('const/real/real_of_num' ('const/real/NUM_FLOOR' ('const/real/#slash#' x y))) y) x)))).
tt('thm/real/NUM_FLOOR_DIV_LOWERBOUND_', ax, (![y : 'type/realax/real', x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') y)) => ('const/realax/real_lt' x ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/+' ('const/real/NUM_FLOOR' ('const/real/#slash#' x y)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) y))))).
tt('thm/real/NUM_FLOOR_EQNS_0', ax, (![n : 'type/num/num']: (('const/real/NUM_FLOOR' ('const/real/real_of_num' n)) = n))).
tt('thm/real/NUM_FLOOR_EQNS_e1', ax, (![n : 'type/num/num', m : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' m) => (('const/real/NUM_FLOOR' ('const/real/#slash#' ('const/real/real_of_num' n) ('const/real/real_of_num' m))) = ('const/arithmetic/DIV' n m))))).
tt('thm/real/NUM_FLOOR_LOWER_BOUND_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/realax/real_lt' x ('const/real/real_of_num' n)) = ('const/arithmetic/<=' ('const/real/NUM_FLOOR' ('const/realax/real_add' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) n)))).
tt('thm/real/NUM_FLOOR_upper_bound_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/real/real_lte' ('const/real/real_of_num' n) x) = ('const/prim_rec/<' n ('const/real/NUM_FLOOR' ('const/realax/real_add' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))).
tt('thm/real/LE_NUM_CEILING_', ax, (![x : 'type/realax/real']: ('const/real/real_lte' x ('const/real/real_of_num' ('const/real/NUM_CEILING' x))))).
tt('thm/real/NUM_CEILING_LE_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/real/real_lte' x ('const/real/real_of_num' n)) => ('const/arithmetic/<=' ('const/real/NUM_CEILING' x) n)))).
