tt('const/float/error', ty, ('type/realax/real' > 'type/realax/real')).
tt('const/float/normalizes', ty, ('type/realax/real' > $o)).
tt('thm/float/TWO_EXP_GE_1_', ax, (![n : 'type/num/num']: ('const/arithmetic/<=' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)))).
tt('thm/float/egtff_', ax, (('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/float/ftt_', ax, (('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))).
tt('thm/float/tpetfs_', ax, (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))).
tt('thm/float/egt1_', ax, ('const/realax/real_lt' ('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/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))).
tt('thm/float/temonz_', ax, (~ (('const/arithmetic/-' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = 'const/num/0'))).
tt('thm/float/tteettto_', ax, (('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) = ('const/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/float/tptteteesze_', ax, (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))))))))))))))))).
tt('thm/float/tfflttfs_', ax, ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))).
tt('thm/float/inv23gt0_', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/float/v23not0_', ax, (~ (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/float/v127not0_', ax, (~ (('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/float/noteteeszegtz_', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))))))))))))))))).
tt('thm/float/lt1eqmul_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ('const/realax/real_lt' ('const/realax/real_mul' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))))))))))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))).
tt('thm/float/twogz_', ax, (![n : 'type/num/num']: ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) n)))).
tt('thm/float/not2eqz_', ax, (~ (('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = ('const/real/real_of_num' 'const/num/0')))).
tt('thm/float/tittfittt_', ax, (('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) = ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))).
tt('thm/float/ttpinv_', ax, (('const/realax/real_mul' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))).
tt('thm/float/RRRC1_', ax, ('const/real/real_lte' ('const/realax/real_mul' ('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/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))))))))))))) ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/real_sub' ('const/realax/real_mul' ('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/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('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/float/RRRC2_', ax, ('const/real/real_lte' ('const/real/real_sub' ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/RRRC3_', ax, ('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/RRRC4_', ax, (('const/real/real_sub' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
tt('thm/float/RRRC5_', ax, ('const/realax/real_lt' ('const/realax/inv' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/real/real_sub' ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/RRRC6_', ax, ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/RRRC7_', ax, ('const/realax/real_lt' ('const/real/real_sub' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/RRRC8_', ax, (('const/real/real_sub' ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
tt('thm/float/RRRC9_', ax, ('const/realax/real_lt' ('const/real/real_sub' ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
tt('thm/float/RRRC10_', ax, ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/real_sub' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))).
tt('thm/float/RRRC11_', ax, ('const/realax/real_lt' ('const/realax/real_mul' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/sucminmullt_', ax, ('const/realax/real_lt' ('const/realax/real_mul' ('const/real/real_sub' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))).
tt('thm/float/SIGN_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/sign' a) = (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a)))).
tt('thm/float/EXPONENT_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/exponent' a) = (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a))))).
tt('thm/float/FRACTION_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fraction' a) = (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a))))).
tt('thm/float/IS_VALID_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/is_valid' X a) = (('const/prim_rec/<' ('const/ieee/sign' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) & (('const/prim_rec/<' ('const/ieee/exponent' a) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/expwidth' X))) & ('const/prim_rec/<' ('const/ieee/fraction' a) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/fracwidth' X)))))))).
tt('thm/float/VALOF_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/valof' X a) = (('const/bool/COND' 'type/realax/real') (('const/ieee/exponent' a) = 'const/num/0') ('const/realax/real_mul' ('const/realax/real_mul' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/ieee/sign' a)) ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/ieee/bias' X)))) ('const/real/#slash#' ('const/real/real_of_num' ('const/ieee/fraction' a)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/ieee/fracwidth' X)))) ('const/realax/real_mul' ('const/realax/real_mul' ('const/real/pow' ('const/realax/real_neg' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/ieee/sign' a)) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/ieee/exponent' a)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/ieee/bias' X)))) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/#slash#' ('const/real/real_of_num' ('const/ieee/fraction' a)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/ieee/fracwidth' X))))))))).
tt('thm/float/IS_VALID_DEFLOAT_', ax, (![a : 'type/ieee/float']: ('const/ieee/is_valid' 'const/ieee/float_format' ('const/ieee/defloat' a)))).
tt('thm/float/ADD_SUB2_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/-' ('const/arithmetic/+' m n) m) = n))).
tt('thm/float/REAL_OF_NUM_SUB_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/arithmetic/<=' m n) => (('const/real/real_sub' ('const/real/real_of_num' n) ('const/real/real_of_num' m)) = ('const/real/real_of_num' ('const/arithmetic/-' n m)))))).
tt('thm/float/IS_FINITE_ALT1_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: ((('const/ieee/is_normal' 'const/ieee/float_format' a) | (('const/ieee/is_denormal' 'const/ieee/float_format' a) | ('const/ieee/is_zero' 'const/ieee/float_format' a))) = ('const/prim_rec/<' ('const/ieee/exponent' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/float/IS_FINITE_ALT_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/is_finite' 'const/ieee/float_format' a) = (('const/ieee/is_valid' 'const/ieee/float_format' a) & ('const/prim_rec/<' ('const/ieee/exponent' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))).
tt('thm/float/IS_FINITE_EXPLICIT_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/is_finite' 'const/ieee/float_format' a) = (('const/prim_rec/<' ('const/ieee/sign' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) & (('const/prim_rec/<' ('const/ieee/exponent' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) & ('const/prim_rec/<' ('const/ieee/fraction' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))))))))))))))))).
tt('thm/float/LT_SUC_LE_', ax, (![m : 'type/num/num', n : 'type/num/num']: (('const/prim_rec/<' m ('const/num/SUC' n)) = ('const/arithmetic/<=' m n)))).
tt('thm/float/FLOAT_CASES_', ax, (![a : 'type/ieee/float']: (('const/ieee/Isnan' a) | (('const/ieee/Infinity' a) | (('const/ieee/Isnormal' a) | (('const/ieee/Isdenormal' a) | ('const/ieee/Iszero' a))))))).
tt('thm/float/FLOAT_CASES_FINITE_', ax, (![a : 'type/ieee/float']: (('const/ieee/Isnan' a) | (('const/ieee/Infinity' a) | ('const/ieee/Finite' a))))).
tt('thm/float/FLOAT_DISTINCT_0', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnan' a) & ('const/ieee/Infinity' a))))).
tt('thm/float/FLOAT_DISTINCT_1', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnan' a) & ('const/ieee/Isnormal' a))))).
tt('thm/float/FLOAT_DISTINCT_2', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnan' a) & ('const/ieee/Isdenormal' a))))).
tt('thm/float/FLOAT_DISTINCT_3', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnan' a) & ('const/ieee/Iszero' a))))).
tt('thm/float/FLOAT_DISTINCT_4', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Infinity' a) & ('const/ieee/Isnormal' a))))).
tt('thm/float/FLOAT_DISTINCT_5', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Infinity' a) & ('const/ieee/Isdenormal' a))))).
tt('thm/float/FLOAT_DISTINCT_6', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Infinity' a) & ('const/ieee/Iszero' a))))).
tt('thm/float/FLOAT_DISTINCT_7', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnormal' a) & ('const/ieee/Isdenormal' a))))).
tt('thm/float/FLOAT_DISTINCT_8', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnormal' a) & ('const/ieee/Iszero' a))))).
tt('thm/float/FLOAT_DISTINCT_e9', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isdenormal' a) & ('const/ieee/Iszero' a))))).
tt('thm/float/FLOAT_DISTINCT_FINITE_0', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnan' a) & ('const/ieee/Infinity' a))))).
tt('thm/float/FLOAT_DISTINCT_FINITE_1', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Isnan' a) & ('const/ieee/Finite' a))))).
tt('thm/float/FLOAT_DISTINCT_FINITE_e2', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/Infinity' a) & ('const/ieee/Finite' a))))).
tt('thm/float/FLOAT_INFINITIES_SIGNED_0', ax, (('const/ieee/sign' ('const/ieee/defloat' 'const/ieee/Plus_infinity')) = 'const/num/0')).
tt('thm/float/FLOAT_INFINITIES_SIGNED_e1', ax, (('const/ieee/sign' ('const/ieee/defloat' 'const/ieee/Minus_infinity')) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/float/INFINITY_IS_INFINITY_0', ax, ('const/ieee/Infinity' 'const/ieee/Plus_infinity')).
tt('thm/float/INFINITY_IS_INFINITY_e1', ax, ('const/ieee/Infinity' 'const/ieee/Minus_infinity')).
tt('thm/float/ZERO_IS_ZERO_0', ax, ('const/ieee/Iszero' 'const/ieee/Plus_zero')).
tt('thm/float/ZERO_IS_ZERO_e1', ax, ('const/ieee/Iszero' 'const/ieee/Minus_zero')).
tt('thm/float/INFINITY_NOT_NAN_0', ax, (~ ('const/ieee/Isnan' 'const/ieee/Plus_infinity'))).
tt('thm/float/INFINITY_NOT_NAN_e1', ax, (~ ('const/ieee/Isnan' 'const/ieee/Minus_infinity'))).
tt('thm/float/ZERO_NOT_NAN_0', ax, (~ ('const/ieee/Isnan' 'const/ieee/Plus_zero'))).
tt('thm/float/ZERO_NOT_NAN_e1', ax, (~ ('const/ieee/Isnan' 'const/ieee/Minus_zero'))).
tt('thm/float/FLOAT_INFINITIES_', ax, (![a : 'type/ieee/float']: (('const/ieee/Infinity' a) = (('const/ieee/float_eq' a 'const/ieee/Plus_infinity') | ('const/ieee/float_eq' a 'const/ieee/Minus_infinity'))))).
tt('thm/float/FLOAT_INFINITES_DISTINCT_', ax, (![a : 'type/ieee/float']: (~ (('const/ieee/float_eq' a 'const/ieee/Plus_infinity') & ('const/ieee/float_eq' a 'const/ieee/Minus_infinity'))))).
tt('thm/float/FLOAT_LT_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & ('const/ieee/Finite' b)) => (('const/ieee/float_lt' a b) = ('const/realax/real_lt' ('const/ieee/Val' a) ('const/ieee/Val' b)))))).
tt('thm/float/FLOAT_GT_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & ('const/ieee/Finite' b)) => (('const/ieee/float_gt' a b) = ('const/real/real_gt' ('const/ieee/Val' a) ('const/ieee/Val' b)))))).
tt('thm/float/FLOAT_LE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & ('const/ieee/Finite' b)) => (('const/ieee/float_le' a b) = ('const/real/real_lte' ('const/ieee/Val' a) ('const/ieee/Val' b)))))).
tt('thm/float/FLOAT_GE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & ('const/ieee/Finite' b)) => (('const/ieee/float_ge' a b) = ('const/real/real_ge' ('const/ieee/Val' a) ('const/ieee/Val' b)))))).
tt('thm/float/FLOAT_EQ_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & ('const/ieee/Finite' b)) => (('const/ieee/float_eq' a b) = (('const/ieee/Val' a) = ('const/ieee/Val' b)))))).
tt('thm/float/FLOAT_EQ_REFL_', ax, (![a : 'type/ieee/float']: (('const/ieee/float_eq' a a) = (~ ('const/ieee/Isnan' a))))).
tt('thm/float/EXP_GT_ZERO_', ax, (![n : 'type/num/num']: ('const/prim_rec/<' 'const/num/0' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) n)))).
tt('thm/float/IS_VALID_SPECIAL_0', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/ieee/is_valid' X ('const/ieee/minus_infinity' X)))).
tt('thm/float/IS_VALID_SPECIAL_1', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/ieee/is_valid' X ('const/ieee/plus_infinity' X)))).
tt('thm/float/IS_VALID_SPECIAL_2', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/ieee/is_valid' X ('const/ieee/topfloat' X)))).
tt('thm/float/IS_VALID_SPECIAL_3', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/ieee/is_valid' X ('const/ieee/bottomfloat' X)))).
tt('thm/float/IS_VALID_SPECIAL_4', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/ieee/is_valid' X ('const/ieee/plus_zero' X)))).
tt('thm/float/IS_VALID_SPECIAL_e5', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ('const/ieee/is_valid' X ('const/ieee/minus_zero' X)))).
tt('thm/float/IS_CLOSEST_EXISTS_', ax, (![v : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'), x : 'type/realax/real', s : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o)]: ((('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) s) => ((~ (s = ('const/pred_set/EMPTY' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))) => (?[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/is_closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v s x a)))))).
tt('thm/float/CLOSEST_IS_EVERYTHING_', ax, (![v : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'), p : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o), s : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o), x : 'type/realax/real']: ((('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) s) => ((~ (s = ('const/pred_set/EMPTY' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))) => ((('const/ieee/is_closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v s x (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v p s x)) & ((?[b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: ((('const/ieee/is_closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v s x b) & (p b))) => (p (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v p s x)))))))).
tt('thm/float/CLOSEST_IN_SET_', ax, (![v : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'), p : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o), x : 'type/realax/real', s : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o)]: ((('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) s) => ((~ (s = ('const/pred_set/EMPTY' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))) => (('const/bool/IN' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v p s x) s))))).
tt('thm/float/CLOSEST_IS_CLOSEST_', ax, (![v : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'), p : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o), x : 'type/realax/real', s : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o)]: ((('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) s) => ((~ (s = ('const/pred_set/EMPTY' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))) => (('const/ieee/is_closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v s x (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v p s x)))))).
tt('thm/float/FLOAT_FIRSTCROSS1_', ax, (![x : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((?['x\'' : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: ((x = (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[x0 : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[y : 'type/num/num', z : 'type/num/num']: (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x0 (('const/pair/,' 'type/num/num' 'type/num/num') y z))))) 'x\'')) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'') m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'')) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'')) p))))) => (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x) m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x)) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x)) p)))))).
tt('thm/float/FLOAT_FIRSTCROSS2_', ax, (![x : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x) m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x)) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x)) p))) => (?['x\'' : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: ((x = (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[x0 : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[y : 'type/num/num', z : 'type/num/num']: (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x0 (('const/pair/,' 'type/num/num' 'type/num/num') y z))))) 'x\'')) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'') m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'')) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'')) p)))))))).
tt('thm/float/FLOAT_FIRSTCROSS3_', ax, (![x : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x) m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x)) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x)) p))) = (?['x\'' : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: ((x = (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[x0 : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[y : 'type/num/num', z : 'type/num/num']: (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x0 (('const/pair/,' 'type/num/num' 'type/num/num') y z))))) 'x\'')) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'') m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'')) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'x\'')) p)))))))).
tt('thm/float/FLOAT_FIRSTCROSS_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: ((('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a) m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a)) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a)) p)))))) = (('const/pred_set/IMAGE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pair/UNCURRY' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num') ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[x : 'type/num/num']: (('const/pair/UNCURRY' 'type/num/num' 'type/num/num' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[y : 'type/num/num', z : 'type/num/num']: (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) x (('const/pair/,' 'type/num/num' 'type/num/num') y z)))))) (('const/pred_set/CROSS' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) (('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[x : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) x ('const/prim_rec/<' x m)))) (('const/pred_set/CROSS' 'type/num/num' 'type/num/num') (('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[y : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) y ('const/prim_rec/<' y n)))) (('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[z : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) z ('const/prim_rec/<' z p)))))))))).
tt('thm/float/FLOAT_COUNTINDUCT_0', ax, ((('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[x : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) x ('const/prim_rec/<' x 'const/num/0')))) = ('const/pred_set/EMPTY' 'type/num/num'))).
tt('thm/float/FLOAT_COUNTINDUCT_e1', ax, (![n : 'type/num/num']: ((('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[x : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) x ('const/prim_rec/<' x ('const/num/SUC' n))))) = (('const/pred_set/INSERT' 'type/num/num') n (('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[x : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) x ('const/prim_rec/<' x n)))))))).
tt('thm/float/FLOAT_FINITECOUNT_', ax, (![n : 'type/num/num']: (('const/pred_set/FINITE' 'type/num/num') (('const/pred_set/GSPEC' 'type/num/num' 'type/num/num') (^[x : 'type/num/num']: (('const/pair/,' 'type/num/num' $o) x ('const/prim_rec/<' x n))))))).
tt('thm/float/FINITE_R3_', ax, (![m : 'type/num/num', n : 'type/num/num', p : 'type/num/num']: (('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a) m) & (('const/prim_rec/<' (('const/pair/FST' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a)) n) & ('const/prim_rec/<' (('const/pair/SND' 'type/num/num' 'type/num/num') (('const/pair/SND' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) a)) p))))))))).
tt('thm/float/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/float/IS_VALID_FINITE_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_valid' X a))))))).
tt('thm/float/FLOAT_IS_FINITE_SUBSET_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/pred_set/SUBSET' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a)))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_valid' X a))))))).
tt('thm/float/MATCH_FLOAT_FINITE_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: ((('const/pred_set/SUBSET' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a)))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_valid' X a))))) => (('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a)))))))).
tt('thm/float/IS_FINITE_FINITE_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/pred_set/FINITE' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a))))))).
tt('thm/float/IS_VALID_NONEMPTY_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (~ ((('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_valid' X a)))) = ('const/pred_set/EMPTY' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('thm/float/IS_FINITE_NONEMPTY_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (~ ((('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a)))) = ('const/pred_set/EMPTY' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('thm/float/IS_FINITE_CLOSEST_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), v : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'), p : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o), x : 'type/realax/real']: ('const/ieee/is_finite' X (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v p (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a)))) x)))).
tt('thm/float/IS_VALID_CLOSEST_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), v : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'), p : (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o), x : 'type/realax/real']: ('const/ieee/is_valid' X (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) v p (('const/pred_set/GSPEC' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/pair/,' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) $o) a ('const/ieee/is_finite' X a)))) x)))).
tt('thm/float/IS_VALID_ROUND_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: ('const/ieee/is_valid' X ('const/ieee/round' X 'const/ieee/To_nearest' x)))).
tt('thm/float/DEFLOAT_FLOAT_ROUND_', ax, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/defloat' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) = ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x)))).
tt('thm/float/DEFLOAT_FLOAT_ZEROSIGN_ROUND_', ax, (![x : 'type/realax/real', b : 'type/num/num']: (('const/ieee/defloat' ('const/ieee/float' ('const/ieee/zerosign' 'const/ieee/float_format' b ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x)))) = ('const/ieee/zerosign' 'const/ieee/float_format' b ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))))).
tt('thm/float/VALOF_DEFLOAT_FLOAT_ZEROSIGN_ROUND_', ax, (![x : 'type/realax/real', b : 'type/num/num']: (('const/ieee/valof' 'const/ieee/float_format' ('const/ieee/defloat' ('const/ieee/float' ('const/ieee/zerosign' 'const/ieee/float_format' b ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))))) = ('const/ieee/valof' 'const/ieee/float_format' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))))).
tt('thm/float/REAL_ABS_NUM_', ax, (![n : 'type/num/num']: (('const/real/abs' ('const/real/real_of_num' n)) = ('const/real/real_of_num' n)))).
tt('thm/float/REAL_ABS_POW_', ax, (![x : 'type/realax/real', n : 'type/num/num']: (('const/real/abs' ('const/real/pow' x n)) = ('const/real/pow' ('const/real/abs' x) n)))).
tt('thm/float/ISFINITE_', ax, (![a : 'type/ieee/float']: (('const/ieee/Finite' a) = ('const/ieee/is_finite' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/float/REAL_ABS_INV_', ax, (![x : 'type/realax/real']: (('const/real/abs' ('const/realax/inv' x)) = ('const/realax/inv' ('const/real/abs' x))))).
tt('thm/float/REAL_ABS_DIV_', ax, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/real/abs' ('const/real/#slash#' x y)) = ('const/real/#slash#' ('const/real/abs' x) ('const/real/abs' y))))).
tt('thm/float/VAL_FINITE_', ax, (![a : 'type/ieee/float']: (('const/ieee/Finite' a) => ('const/real/real_lte' ('const/real/abs' ('const/ieee/Val' a)) ('const/ieee/largest' 'const/ieee/float_format'))))).
tt('thm/float/ISFINITE_LEMMA_', ax, (![s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: ((('const/prim_rec/<' s ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) & (('const/prim_rec/<' e ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) & ('const/prim_rec/<' f ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) => (('const/ieee/Finite' ('const/ieee/float' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') e f)))) & ('const/ieee/is_valid' 'const/ieee/float_format' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') e f))))))).
tt('thm/float/FLOAT_THRESHOLD_EXPLICIT_', ax, (('const/ieee/threshold' 'const/ieee/float_format') = ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
tt('thm/float/VAL_THRESHOLD_', ax, (![a : 'type/ieee/float']: (('const/ieee/Finite' a) => ('const/realax/real_lt' ('const/real/abs' ('const/ieee/Val' a)) ('const/ieee/threshold' 'const/ieee/float_format'))))).
tt('thm/float/error_def_', def, (![x : 'type/realax/real']: (('const/float/error' x) = ('const/real/real_sub' ('const/ieee/Val' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) x)))).
tt('thm/float/BOUND_AT_WORST_LEMMA_', ax, (![a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')) & ('const/ieee/is_finite' 'const/ieee/float_format' a)) => ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/valof' 'const/ieee/float_format' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x)) x)) ('const/real/abs' ('const/real/real_sub' ('const/ieee/valof' 'const/ieee/float_format' a) x)))))).
tt('thm/float/ERROR_AT_WORST_LEMMA_', ax, (![a : 'type/ieee/float', x : 'type/realax/real']: ((('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')) & ('const/ieee/Finite' a)) => ('const/real/real_lte' ('const/real/abs' ('const/float/error' x)) ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' a) x)))))).
tt('thm/float/ERROR_IS_ZERO_', ax, (![a : 'type/ieee/float', x : 'type/realax/real']: ((('const/ieee/Finite' a) & (('const/ieee/Val' a) = x)) => (('const/float/error' x) = ('const/real/real_of_num' 'const/num/0'))))).
tt('thm/float/REAL_LT_LCANCEL_IMP_', 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/float/REAL_OF_NUM_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/float/ERROR_BOUND_LEMMA1_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('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'))))) => (?[n : 'type/num/num']: (('const/prim_rec/<' n ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & (('const/real/real_lte' ('const/real/#slash#' ('const/real/real_of_num' n) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) x) & ('const/realax/real_lt' x ('const/real/#slash#' ('const/real/real_of_num' ('const/num/SUC' n)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))))).
tt('thm/float/ERROR_BOUND_LEMMA2_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('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'))))) => (?[n : 'type/num/num']: (('const/arithmetic/<=' n ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' x ('const/real/#slash#' ('const/real/real_of_num' n) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/float/ERROR_BOUND_LEMMA3_', 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/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) => (?[n : 'type/num/num']: (('const/arithmetic/<=' n ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/#slash#' ('const/real/real_of_num' n) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) x)) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/float/ERROR_BOUND_LEMMA4_', 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/realax/real_lt' x ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) => (?[e : 'type/num/num', f : 'type/num/num']: (('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' ('const/ieee/float' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'const/num/0' (('const/pair/,' 'type/num/num' 'type/num/num') e f)))) x)) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/prim_rec/<' f ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ((e = ('const/ieee/bias' 'const/ieee/float_format')) | ((e = ('const/num/SUC' ('const/ieee/bias' 'const/ieee/float_format'))) & (f = 'const/num/0'))))))))).
tt('thm/float/ERROR_BOUND_LEMMA5_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/real/abs' x)) & ('const/realax/real_lt' ('const/real/abs' x) ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) => (?[s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' ('const/ieee/float' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') e f)))) x)) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/prim_rec/<' s ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) & (('const/prim_rec/<' f ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ((e = ('const/ieee/bias' 'const/ieee/float_format')) | ((e = ('const/num/SUC' ('const/ieee/bias' 'const/ieee/float_format'))) & (f = 'const/num/0')))))))))).
tt('thm/float/REAL_MUL_AC_0', ax, (![n : 'type/realax/real', m : 'type/realax/real']: (('const/realax/real_mul' m n) = ('const/realax/real_mul' n m)))).
tt('thm/float/REAL_MUL_AC_1', ax, (![p : 'type/realax/real', n : 'type/realax/real', m : 'type/realax/real']: (('const/realax/real_mul' ('const/realax/real_mul' m n) p) = ('const/realax/real_mul' m ('const/realax/real_mul' n p))))).
tt('thm/float/REAL_MUL_AC_e2', ax, (![p : 'type/realax/real', n : 'type/realax/real', m : 'type/realax/real']: (('const/realax/real_mul' m ('const/realax/real_mul' n p)) = ('const/realax/real_mul' n ('const/realax/real_mul' m p))))).
tt('thm/float/REAL_LE_LCANCEL_IMP_', 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/float/ERROR_BOUND_LEMMA6_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))) => (?[n : 'type/num/num']: (('const/arithmetic/<=' n ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' x ('const/real/#slash#' ('const/realax/real_mul' ('const/real/#slash#' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) ('const/real/real_of_num' n)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))))).
tt('thm/float/EXP_LT_0_', ax, (![n : 'type/num/num', x : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' ('const/arithmetic/EXP' x n)) = ((~ (x = 'const/num/0')) | (n = 'const/num/0'))))).
tt('thm/float/ERROR_BOUND_LEMMA7_', ax, (![x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x) & ('const/realax/real_lt' x ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))) => (?[e : 'type/num/num', f : 'type/num/num']: (('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' ('const/ieee/float' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'const/num/0' (('const/pair/,' 'type/num/num' 'type/num/num') e f)))) x)) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) & (('const/prim_rec/<' f ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ((e = 'const/num/0') | ((e = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (f = 'const/num/0'))))))))).
tt('thm/float/ERROR_BOUND_LEMMA8_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' x) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))) => (?[s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' ('const/ieee/float' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') e f)))) x)) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) & (('const/prim_rec/<' s ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) & (('const/prim_rec/<' f ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) & ((e = 'const/num/0') | ((e = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) & (f = 'const/num/0')))))))))).
tt('thm/float/VALOF_SCALE_UP_', ax, (![s : 'type/num/num', e : 'type/num/num', k : 'type/num/num', f : 'type/num/num']: ((~ (e = 'const/num/0')) => (('const/ieee/valof' 'const/ieee/float_format' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/+' e k) f))) = ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k) ('const/ieee/valof' 'const/ieee/float_format' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') e f)))))))).
tt('thm/float/VALOF_SCALE_DOWN_', ax, (![s : 'type/num/num', e : 'type/num/num', k : 'type/num/num', f : 'type/num/num']: (('const/prim_rec/<' k e) => (('const/ieee/valof' 'const/ieee/float_format' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/-' e k) f))) = ('const/realax/real_mul' ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k)) ('const/ieee/valof' 'const/ieee/float_format' (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) s (('const/pair/,' 'type/num/num' 'type/num/num') e f)))))))).
tt('thm/float/REAL_LT_RCANCEL_IMP_', 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/float/REAL_LE_RCANCEL_IMP_', 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/float/REAL_POW_EQ_0_', ax, (![x : 'type/realax/real', n : 'type/num/num']: ((('const/real/pow' x n) = ('const/real/real_of_num' 'const/num/0')) = ((x = ('const/real/real_of_num' 'const/num/0')) & (~ (n = 'const/num/0')))))).
tt('thm/float/REAL_POW_LE_1_', ax, (![n : 'type/num/num', 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 n))))).
tt('thm/float/REAL_POW_MONO_', ax, (![m : 'type/num/num', n : 'type/num/num', x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) x) & ('const/arithmetic/<=' m n)) => ('const/real/real_lte' ('const/real/pow' x m) ('const/real/pow' x n))))).
tt('thm/float/ERROR_BOUND_BIG1_', ax, (![x : 'type/realax/real', k : 'type/num/num']: ((('const/real/real_lte' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k) ('const/real/abs' x)) & (('const/realax/real_lt' ('const/real/abs' x) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' k))) & ('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')))) => (?[a : 'type/ieee/float']: (('const/ieee/Finite' a) & ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' a) x)) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/float/ERROR_BOUND_BIG_', ax, (![k : 'type/num/num', x : 'type/realax/real']: ((('const/real/real_lte' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k) ('const/real/abs' x)) & (('const/realax/real_lt' ('const/real/abs' x) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' k))) & ('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')))) => ('const/real/real_lte' ('const/real/abs' ('const/float/error' x)) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/REAL_LE_INV2_', 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' x y)) => ('const/real/real_lte' ('const/realax/inv' y) ('const/realax/inv' x))))).
tt('thm/float/ERROR_BOUND_SMALL1_', ax, (![x : 'type/realax/real', k : 'type/num/num']: ((('const/real/real_lte' ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' k))) ('const/real/abs' x)) & (('const/realax/real_lt' ('const/real/abs' x) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k))) & ('const/prim_rec/<' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))) => (?[a : 'type/ieee/float']: (('const/ieee/Finite' a) & ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' a) x)) ('const/realax/inv' ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' k)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))))).
tt('thm/float/ERROR_BOUND_SMALL_', ax, (![k : 'type/num/num', x : 'type/realax/real']: ((('const/real/real_lte' ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' k))) ('const/real/abs' x)) & (('const/realax/real_lt' ('const/real/abs' x) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) k))) & ('const/prim_rec/<' k ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))) => ('const/real/real_lte' ('const/real/abs' ('const/float/error' x)) ('const/realax/inv' ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' k)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))).
tt('thm/float/ERROR_BOUND_TINY_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' x) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))) => ('const/real/real_lte' ('const/real/abs' ('const/float/error' x)) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))).
tt('thm/float/ERROR_BOUND_NORM_STRONG_', ax, (![x : 'type/realax/real', j : 'type/num/num']: ((('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')) & ('const/realax/real_lt' ('const/real/abs' x) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' j)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))) => ('const/real/real_lte' ('const/real/abs' ('const/float/error' x)) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) j) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))))).
tt('thm/float/normalizes_', def, (![x : 'type/realax/real']: (('const/float/normalizes' x) = (('const/real/real_lte' ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/-' ('const/ieee/bias' 'const/ieee/float_format') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/real/abs' x)) & ('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')))))).
tt('thm/float/THRESHOLD_MUL_LT_', ax, ('const/realax/real_lt' ('const/realax/real_mul' ('const/ieee/threshold' 'const/ieee/float_format') ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))).
tt('thm/float/THRESHOLD_LT_POW_INV_', ax, ('const/realax/real_lt' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ('const/realax/real_mul' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/realax/inv' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))).
tt('thm/float/LT_THRESHOLD_LT_POW_INV_', ax, (![x : 'type/realax/real']: (('const/realax/real_lt' x ('const/ieee/threshold' (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) => ('const/realax/real_lt' x ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/-' ('const/ieee/emax' (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))) ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))))))).
tt('thm/float/REAL_POS_IN_BINADE_', ax, (![x : 'type/realax/real']: ((('const/float/normalizes' x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') x)) => (?[j : 'type/num/num']: (('const/arithmetic/<=' j ('const/arithmetic/-' ('const/ieee/emax' 'const/ieee/float_format') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) & (('const/real/real_lte' ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) j) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) x) & ('const/realax/real_lt' x ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' j)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))))))).
tt('thm/float/REAL_NEG_IN_BINADE_', ax, (![x : 'type/realax/real']: ((('const/float/normalizes' x) & ('const/real/real_lte' ('const/real/real_of_num' 'const/num/0') ('const/realax/real_neg' x))) => (?[j : 'type/num/num']: (('const/arithmetic/<=' j ('const/arithmetic/-' ('const/ieee/emax' 'const/ieee/float_format') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) & (('const/real/real_lte' ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) j) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/realax/real_neg' x)) & ('const/realax/real_lt' ('const/realax/real_neg' x) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' j)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))))))).
tt('thm/float/REAL_IN_BINADE_', ax, (![x : 'type/realax/real']: (('const/float/normalizes' x) => (?[j : 'type/num/num']: (('const/arithmetic/<=' j ('const/arithmetic/-' ('const/ieee/emax' 'const/ieee/float_format') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))) & (('const/real/real_lte' ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) j) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))))))) ('const/real/abs' x)) & ('const/realax/real_lt' ('const/real/abs' x) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/num/SUC' j)) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))))))))))).
tt('thm/float/ERROR_BOUND_NORM_STRONG_NORMALIZE_', ax, (![x : 'type/realax/real']: (('const/float/normalizes' x) => (?[j : 'type/num/num']: ('const/real/real_lte' ('const/real/abs' ('const/float/error' x)) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) j) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))))).
tt('thm/float/RELATIVE_ERROR_POS_', ax, (![x : 'type/realax/real']: ((('const/float/normalizes' x) & ('const/realax/real_lt' ('const/real/real_of_num' 'const/num/0') x)) => (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) = ('const/realax/real_mul' x ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e)))))))).
tt('thm/float/RELATIVE_ERROR_NEG_', ax, (![x : 'type/realax/real']: ((('const/float/normalizes' x) & ('const/realax/real_lt' x ('const/real/real_of_num' 'const/num/0'))) => (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) = ('const/realax/real_mul' x ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e)))))))).
tt('thm/float/RELATIVE_ERROR_ZERO_', ax, (![x : 'type/realax/real']: ((('const/float/normalizes' x) & (x = ('const/real/real_of_num' 'const/num/0'))) => (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) = ('const/realax/real_mul' x ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e)))))))).
tt('thm/float/RELATIVE_ERROR_', ax, (![x : 'type/realax/real']: (('const/float/normalizes' x) => (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) = ('const/realax/real_mul' x ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e)))))))).
tt('thm/float/DEFLOAT_FLOAT_ZEROSIGN_ROUND_FINITE_', ax, (![b : 'type/num/num', x : 'type/realax/real']: (('const/realax/real_lt' ('const/real/abs' x) ('const/ieee/threshold' 'const/ieee/float_format')) => ('const/ieee/is_finite' 'const/ieee/float_format' ('const/ieee/defloat' ('const/ieee/float' ('const/ieee/zerosign' 'const/ieee/float_format' b ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x)))))))).
tt('thm/float/FLOAT_SUB_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' a) ('const/ieee/Val' b))) ('const/ieee/threshold' 'const/ieee/float_format')))) => (('const/ieee/Finite' ('const/ieee/float_sub' a b)) & (('const/ieee/Val' ('const/ieee/float_sub' a b)) = ('const/realax/real_add' ('const/real/real_sub' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/float/error' ('const/real/real_sub' ('const/ieee/Val' a) ('const/ieee/Val' b))))))))).
tt('thm/float/FLOAT_MUL_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/realax/real_lt' ('const/real/abs' ('const/realax/real_mul' ('const/ieee/Val' a) ('const/ieee/Val' b))) ('const/ieee/threshold' 'const/ieee/float_format')))) => (('const/ieee/Finite' ('const/ieee/float_mul' a b)) & (('const/ieee/Val' ('const/ieee/float_mul' a b)) = ('const/realax/real_add' ('const/realax/real_mul' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/float/error' ('const/realax/real_mul' ('const/ieee/Val' a) ('const/ieee/Val' b))))))))).
tt('thm/float/FLOAT_DIV_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ((~ ('const/ieee/Iszero' b)) & ('const/realax/real_lt' ('const/real/abs' ('const/real/#slash#' ('const/ieee/Val' a) ('const/ieee/Val' b))) ('const/ieee/threshold' 'const/ieee/float_format'))))) => (('const/ieee/Finite' ('const/ieee/float_div' a b)) & (('const/ieee/Val' ('const/ieee/float_div' a b)) = ('const/realax/real_add' ('const/real/#slash#' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/float/error' ('const/real/#slash#' ('const/ieee/Val' a) ('const/ieee/Val' b))))))))).
tt('thm/float/Val_FLOAT_ROUND_VALOF_', ax, (![x : 'type/realax/real']: (('const/ieee/Val' ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))) = ('const/ieee/valof' 'const/ieee/float_format' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))))).
tt('thm/float/FLOAT_ADD_RELATIVE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/float/normalizes' ('const/realax/real_add' ('const/ieee/Val' a) ('const/ieee/Val' b))))) => (('const/ieee/Finite' ('const/ieee/float_add' a b)) & (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float_add' a b)) = ('const/realax/real_mul' ('const/realax/real_add' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e))))))))).
tt('thm/float/FLOAT_SUB_RELATIVE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/float/normalizes' ('const/real/real_sub' ('const/ieee/Val' a) ('const/ieee/Val' b))))) => (('const/ieee/Finite' ('const/ieee/float_sub' a b)) & (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float_sub' a b)) = ('const/realax/real_mul' ('const/real/real_sub' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e))))))))).
tt('thm/float/FLOAT_MUL_RELATIVE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/float/normalizes' ('const/realax/real_mul' ('const/ieee/Val' a) ('const/ieee/Val' b))))) => (('const/ieee/Finite' ('const/ieee/float_mul' a b)) & (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float_mul' a b)) = ('const/realax/real_mul' ('const/realax/real_mul' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e))))))))).
tt('thm/float/FLOAT_DIV_RELATIVE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ((~ ('const/ieee/Iszero' b)) & ('const/float/normalizes' ('const/real/#slash#' ('const/ieee/Val' a) ('const/ieee/Val' b)))))) => (('const/ieee/Finite' ('const/ieee/float_div' a b)) & (?[e : 'type/realax/real']: (('const/real/real_lte' ('const/real/abs' e) ('const/real/#slash#' ('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'))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))))))) & (('const/ieee/Val' ('const/ieee/float_div' a b)) = ('const/realax/real_mul' ('const/real/#slash#' ('const/ieee/Val' a) ('const/ieee/Val' b)) ('const/realax/real_add' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) e))))))))).
tt('thm/float/FLOAT_ADD_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/realax/real_lt' ('const/real/abs' ('const/realax/real_add' ('const/ieee/Val' a) ('const/ieee/Val' b))) ('const/ieee/threshold' 'const/ieee/float_format')))) => ('const/ieee/Finite' ('const/ieee/float_add' a b))))).
tt('thm/float/FLOAT_SUB_FINITE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/realax/real_lt' ('const/real/abs' ('const/real/real_sub' ('const/ieee/Val' a) ('const/ieee/Val' b))) ('const/ieee/threshold' 'const/ieee/float_format')))) => ('const/ieee/Finite' ('const/ieee/float_sub' a b))))).
tt('thm/float/FLOAT_MUL_FINITE_', ax, (![a : 'type/ieee/float', b : 'type/ieee/float']: ((('const/ieee/Finite' a) & (('const/ieee/Finite' b) & ('const/realax/real_lt' ('const/real/abs' ('const/realax/real_mul' ('const/ieee/Val' a) ('const/ieee/Val' b))) ('const/ieee/threshold' 'const/ieee/float_format')))) => ('const/ieee/Finite' ('const/ieee/float_mul' a b))))).
