tt('type/ieee/ccode', ty, $t).
tt('type/ieee/float', ty, $t).
tt('type/ieee/roundmode', ty, $t).
tt('const/ieee/Eq', ty, 'type/ieee/ccode').
tt('const/ieee/Exponent', ty, ('type/ieee/float' > 'type/num/num')).
tt('const/ieee/Finite', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Float', ty, ('type/realax/real' > 'type/ieee/float')).
tt('const/ieee/Fraction', ty, ('type/ieee/float' > 'type/num/num')).
tt('const/ieee/Gt', ty, 'type/ieee/ccode').
tt('const/ieee/Infinity', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Isdenormal', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Isintegral', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Isnan', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Isnormal', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Iszero', ty, ('type/ieee/float' > $o)).
tt('const/ieee/Lt', ty, 'type/ieee/ccode').
tt('const/ieee/Minus_infinity', ty, 'type/ieee/float').
tt('const/ieee/Minus_zero', ty, 'type/ieee/float').
tt('const/ieee/Plus_infinity', ty, 'type/ieee/float').
tt('const/ieee/Plus_zero', ty, 'type/ieee/float').
tt('const/ieee/ROUNDFLOAT', ty, ('type/ieee/float' > 'type/ieee/float')).
tt('const/ieee/Sign', ty, ('type/ieee/float' > 'type/num/num')).
tt('const/ieee/To_nearest', ty, 'type/ieee/roundmode').
tt('const/ieee/To_ninfinity', ty, 'type/ieee/roundmode').
tt('const/ieee/To_pinfinity', ty, 'type/ieee/roundmode').
tt('const/ieee/Ulp', ty, ('type/ieee/float' > 'type/realax/real')).
tt('const/ieee/Un', ty, 'type/ieee/ccode').
tt('const/ieee/Val', ty, ('type/ieee/float' > 'type/realax/real')).
tt('const/ieee/bias', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/ieee/bottomfloat', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/ccode2num', ty, ('type/ieee/ccode' > 'type/num/num')).
tt('const/ieee/ccode_CASE', ty, ![A : $t]: ('type/ieee/ccode' > (A > (A > (A > (A > A)))))).
tt('const/ieee/ccode_size', ty, ('type/ieee/ccode' > 'type/num/num')).
tt('const/ieee/closest', ty, ![A : $t]: ((A > 'type/realax/real') > ((A > $o) > ((A > $o) > ('type/realax/real' > A))))).
tt('const/ieee/defloat', ty, ('type/ieee/float' > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/emax', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/ieee/encoding', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/num/num'))).
tt('const/ieee/exponent', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/num/num')).
tt('const/ieee/expwidth', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/ieee/fadd', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')) > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('const/ieee/fcompare', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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')) > 'type/ieee/ccode')))).
tt('const/ieee/fdiv', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')) > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('const/ieee/feq', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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')) > $o)))).
tt('const/ieee/fge', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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')) > $o)))).
tt('const/ieee/fgt', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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')) > $o)))).
tt('const/ieee/fintrnd', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')))))).
tt('const/ieee/fle', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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')) > $o)))).
tt('const/ieee/float', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/ieee/float')).
tt('const/ieee/float_To_zero', ty, 'type/ieee/roundmode').
tt('const/ieee/float_abs', ty, ('type/ieee/float' > 'type/ieee/float')).
tt('const/ieee/float_add', ty, ('type/ieee/float' > ('type/ieee/float' > 'type/ieee/float'))).
tt('const/ieee/float_div', ty, ('type/ieee/float' > ('type/ieee/float' > 'type/ieee/float'))).
tt('const/ieee/float_eq', ty, ('type/ieee/float' > ('type/ieee/float' > $o))).
tt('const/ieee/float_format', ty, ('type/pair/prod' 'type/num/num' 'type/num/num')).
tt('const/ieee/float_ge', ty, ('type/ieee/float' > ('type/ieee/float' > $o))).
tt('const/ieee/float_gt', ty, ('type/ieee/float' > ('type/ieee/float' > $o))).
tt('const/ieee/float_le', ty, ('type/ieee/float' > ('type/ieee/float' > $o))).
tt('const/ieee/float_lt', ty, ('type/ieee/float' > ('type/ieee/float' > $o))).
tt('const/ieee/float_mul', ty, ('type/ieee/float' > ('type/ieee/float' > 'type/ieee/float'))).
tt('const/ieee/float_neg', ty, ('type/ieee/float' > 'type/ieee/float')).
tt('const/ieee/float_rem', ty, ('type/ieee/float' > ('type/ieee/float' > 'type/ieee/float'))).
tt('const/ieee/float_sqrt', ty, ('type/ieee/float' > 'type/ieee/float')).
tt('const/ieee/float_sub', ty, ('type/ieee/float' > ('type/ieee/float' > 'type/ieee/float'))).
tt('const/ieee/flt', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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')) > $o)))).
tt('const/ieee/fmul', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')) > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('const/ieee/fneg', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')))))).
tt('const/ieee/fraction', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/num/num')).
tt('const/ieee/fracwidth', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/ieee/frem', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')) > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('const/ieee/fsqrt', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')))))).
tt('const/ieee/fsub', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > (('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')) > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))))))).
tt('const/ieee/intround', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > ('type/realax/real' > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))))).
tt('const/ieee/is_closest', ty, ![A : $t]: ((A > 'type/realax/real') > ((A > $o) > ('type/realax/real' > (A > $o))))).
tt('const/ieee/is_denormal', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_double', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)).
tt('const/ieee/is_double_extended', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)).
tt('const/ieee/is_finite', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_infinity', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_integral', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_nan', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_normal', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_single', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)).
tt('const/ieee/is_single_extended', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > $o)).
tt('const/ieee/is_valid', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/is_zero', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > $o))).
tt('const/ieee/largest', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/realax/real')).
tt('const/ieee/minus', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('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'))))).
tt('const/ieee/minus_infinity', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/minus_zero', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/num2ccode', ty, ('type/num/num' > 'type/ieee/ccode')).
tt('const/ieee/num2roundmode', ty, ('type/num/num' > 'type/ieee/roundmode')).
tt('const/ieee/plus_infinity', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/plus_zero', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/rem', ty, ('type/realax/real' > ('type/realax/real' > 'type/realax/real'))).
tt('const/ieee/round', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/ieee/roundmode' > ('type/realax/real' > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))))).
tt('const/ieee/roundmode2num', ty, ('type/ieee/roundmode' > 'type/num/num')).
tt('const/ieee/roundmode_CASE', ty, ![A : $t]: ('type/ieee/roundmode' > (A > (A > (A > (A > A)))))).
tt('const/ieee/roundmode_size', ty, ('type/ieee/roundmode' > 'type/num/num')).
tt('const/ieee/sign', ty, (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/num/num')).
tt('const/ieee/some_nan', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/threshold', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/realax/real')).
tt('const/ieee/topfloat', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))).
tt('const/ieee/ulp', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'))).
tt('const/ieee/valof', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > (('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) > 'type/realax/real'))).
tt('const/ieee/wordlength', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > 'type/num/num')).
tt('const/ieee/zerosign', ty, (('type/pair/prod' 'type/num/num' 'type/num/num') > ('type/num/num' > (('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')))))).
tt('thm/ieee/expwidth_', def, (![ew : 'type/num/num', fw : 'type/num/num']: (('const/ieee/expwidth' (('const/pair/,' 'type/num/num' 'type/num/num') ew fw)) = ew))).
tt('thm/ieee/fracwidth_', def, (![ew : 'type/num/num', fw : 'type/num/num']: (('const/ieee/fracwidth' (('const/pair/,' 'type/num/num' 'type/num/num') ew fw)) = fw))).
tt('thm/ieee/wordlength_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/wordlength' X) = ('const/arithmetic/+' ('const/arithmetic/+' ('const/ieee/expwidth' X) ('const/ieee/fracwidth' X)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/ieee/emax_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/emax' X) = ('const/arithmetic/-' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/expwidth' X)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/ieee/bias_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/bias' X) = ('const/arithmetic/-' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/-' ('const/ieee/expwidth' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))).
tt('thm/ieee/is_single_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/is_single' X) = ((('const/ieee/expwidth' X) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (('const/ieee/wordlength' X) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/ieee/is_double_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/is_double' X) = ((('const/ieee/expwidth' X) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & (('const/ieee/wordlength' X) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))).
tt('thm/ieee/is_single_extended_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/is_single_extended' X) = (('const/arithmetic/>=' ('const/ieee/expwidth' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))))) & ('const/arithmetic/>=' ('const/ieee/wordlength' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))).
tt('thm/ieee/is_double_extended_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/is_double_extended' X) = (('const/arithmetic/>=' ('const/ieee/expwidth' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ('const/arithmetic/>=' ('const/ieee/wordlength' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))).
tt('thm/ieee/sign_', def, (![s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/ieee/sign' (('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))) = s))).
tt('thm/ieee/exponent_', def, (![s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/ieee/exponent' (('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))) = e))).
tt('thm/ieee/fraction_', def, (![s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/ieee/fraction' (('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))) = f))).
tt('thm/ieee/is_nan_', def, (![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_nan' X a) = ((('const/ieee/exponent' a) = ('const/ieee/emax' X)) & (~ (('const/ieee/fraction' a) = 'const/num/0')))))).
tt('thm/ieee/is_infinity_', def, (![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_infinity' X a) = ((('const/ieee/exponent' a) = ('const/ieee/emax' X)) & (('const/ieee/fraction' a) = 'const/num/0'))))).
tt('thm/ieee/is_normal_', def, (![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_normal' X a) = (('const/prim_rec/<' 'const/num/0' ('const/ieee/exponent' a)) & ('const/prim_rec/<' ('const/ieee/exponent' a) ('const/ieee/emax' X)))))).
tt('thm/ieee/is_denormal_', def, (![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_denormal' X a) = ((('const/ieee/exponent' a) = 'const/num/0') & (~ (('const/ieee/fraction' a) = 'const/num/0')))))).
tt('thm/ieee/is_zero_', def, (![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_zero' X a) = ((('const/ieee/exponent' a) = 'const/num/0') & (('const/ieee/fraction' a) = 'const/num/0'))))).
tt('thm/ieee/is_valid_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/ieee/is_valid' X (('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/prim_rec/<' s ('const/num/SUC' ('const/num/SUC' 'const/num/0'))) & (('const/prim_rec/<' e ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/expwidth' X))) & ('const/prim_rec/<' f ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/fracwidth' X)))))))).
tt('thm/ieee/is_finite_', def, (![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_finite' X a) = (('const/ieee/is_valid' X a) & (('const/ieee/is_normal' X a) | (('const/ieee/is_denormal' X a) | ('const/ieee/is_zero' X a))))))).
tt('thm/ieee/plus_infinity_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/plus_infinity' X) = (('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') ('const/ieee/emax' X) 'const/num/0'))))).
tt('thm/ieee/minus_infinity_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/minus_infinity' X) = (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/pair/,' 'type/num/num' 'type/num/num') ('const/ieee/emax' X) 'const/num/0'))))).
tt('thm/ieee/plus_zero_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/plus_zero' X) = (('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') 'const/num/0' 'const/num/0'))))).
tt('thm/ieee/minus_zero_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/minus_zero' X) = (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/pair/,' 'type/num/num' 'type/num/num') 'const/num/0' 'const/num/0'))))).
tt('thm/ieee/topfloat_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/topfloat' X) = (('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') ('const/arithmetic/-' ('const/ieee/emax' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/-' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/fracwidth' X)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/ieee/bottomfloat_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/bottomfloat' X) = (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) (('const/pair/,' 'type/num/num' 'type/num/num') ('const/arithmetic/-' ('const/ieee/emax' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/arithmetic/-' ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/fracwidth' X)) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/ieee/minus_', def, (![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/minus' X a) = (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/ieee/sign' a)) (('const/pair/,' 'type/num/num' 'type/num/num') ('const/ieee/exponent' a) ('const/ieee/fraction' a)))))).
tt('thm/ieee/encoding_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/ieee/encoding' X (('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/arithmetic/+' ('const/arithmetic/+' ('const/arithmetic/*' s ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/arithmetic/-' ('const/ieee/wordlength' X) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/arithmetic/*' e ('const/arithmetic/EXP' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')) ('const/ieee/fracwidth' X)))) f)))).
tt('thm/ieee/valof_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), s : 'type/num/num', e : 'type/num/num', f : 'type/num/num']: (('const/ieee/valof' X (('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/bool/COND' 'type/realax/real') (e = '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')))) s) ('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' f) ('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')))) s) ('const/real/#slash#' ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) e) ('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' f) ('const/real/pow' ('const/real/real_of_num' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) ('const/ieee/fracwidth' X))))))))).
tt('thm/ieee/largest_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/largest' X) = ('const/realax/real_mul' ('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' X) ('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/ieee/bias' X))) ('const/real/real_sub' ('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/ieee/fracwidth' X)))))))).
tt('thm/ieee/threshold_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/threshold' X) = ('const/realax/real_mul' ('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' X) ('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/ieee/bias' X))) ('const/real/real_sub' ('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/num/SUC' ('const/ieee/fracwidth' X))))))))).
tt('thm/ieee/ulp_', def, (![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/ulp' X a) = ('const/real/real_sub' ('const/ieee/valof' X (('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') ('const/ieee/exponent' a) ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) ('const/ieee/valof' X (('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') ('const/ieee/exponent' a) 'const/num/0'))))))).
tt('thm/ieee/roundmode_TY_DEF_', def, (?[rep : ('type/ieee/roundmode' > 'type/num/num')]: (('const/bool/TYPE_DEFINITION' 'type/num/num' 'type/ieee/roundmode') (^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) rep))).
tt('thm/ieee/roundmode_BIJ_0', def, (![a : 'type/ieee/roundmode']: (('const/ieee/num2roundmode' ('const/ieee/roundmode2num' a)) = a))).
tt('thm/ieee/roundmode_BIJ_e1', def, (![r : 'type/num/num']: (((^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) r) = (('const/ieee/roundmode2num' ('const/ieee/num2roundmode' r)) = r)))).
tt('thm/ieee/num2roundmode_roundmode2num_', ax, (![a : 'type/ieee/roundmode']: (('const/ieee/num2roundmode' ('const/ieee/roundmode2num' a)) = a))).
tt('thm/ieee/roundmode2num_num2roundmode_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (('const/ieee/roundmode2num' ('const/ieee/num2roundmode' r)) = r)))).
tt('thm/ieee/num2roundmode_11_', ax, (![r : 'type/num/num', 'r\'' : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (('const/prim_rec/<' 'r\'' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => ((('const/ieee/num2roundmode' r) = ('const/ieee/num2roundmode' 'r\'')) = (r = 'r\'')))))).
tt('thm/ieee/roundmode2num_11_', ax, (![a : 'type/ieee/roundmode', 'a\'' : 'type/ieee/roundmode']: ((('const/ieee/roundmode2num' a) = ('const/ieee/roundmode2num' 'a\'')) = (a = 'a\'')))).
tt('thm/ieee/num2roundmode_ONTO_', ax, (![a : 'type/ieee/roundmode']: (?[r : 'type/num/num']: ((a = ('const/ieee/num2roundmode' r)) & ('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/ieee/roundmode2num_ONTO_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (?[a : 'type/ieee/roundmode']: (r = ('const/ieee/roundmode2num' a)))))).
tt('thm/ieee/num2roundmode_thm_0', ax, (('const/ieee/num2roundmode' 'const/num/0') = 'const/ieee/To_nearest')).
tt('thm/ieee/num2roundmode_thm_1', ax, (('const/ieee/num2roundmode' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = 'const/ieee/float_To_zero')).
tt('thm/ieee/num2roundmode_thm_2', ax, (('const/ieee/num2roundmode' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = 'const/ieee/To_pinfinity')).
tt('thm/ieee/num2roundmode_thm_e3', ax, (('const/ieee/num2roundmode' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = 'const/ieee/To_ninfinity')).
tt('thm/ieee/roundmode2num_thm_0', ax, (('const/ieee/roundmode2num' 'const/ieee/To_nearest') = 'const/num/0')).
tt('thm/ieee/roundmode2num_thm_1', ax, (('const/ieee/roundmode2num' 'const/ieee/float_To_zero') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/ieee/roundmode2num_thm_2', ax, (('const/ieee/roundmode2num' 'const/ieee/To_pinfinity') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))).
tt('thm/ieee/roundmode2num_thm_e3', ax, (('const/ieee/roundmode2num' 'const/ieee/To_ninfinity') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/ieee/roundmode_EQ_roundmode_', ax, (![a : 'type/ieee/roundmode', 'a\'' : 'type/ieee/roundmode']: ((a = 'a\'') = (('const/ieee/roundmode2num' a) = ('const/ieee/roundmode2num' 'a\''))))).
tt('thm/ieee/roundmode_size_def_', def, (![x : 'type/ieee/roundmode']: (('const/ieee/roundmode_size' x) = 'const/num/0'))).
tt('thm/ieee/roundmode_CASE_', def, ![A : $t]: (![x : 'type/ieee/roundmode', v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/roundmode_CASE' A) x v0 v1 v2 v3) = ((^[m : 'type/num/num']: (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) v0 (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v1 (('const/bool/COND' A) (m = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v2 v3)))) ('const/ieee/roundmode2num' x))))).
tt('thm/ieee/roundmode_case_def_0', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/roundmode_CASE' A) 'const/ieee/To_nearest' v0 v1 v2 v3) = v0))).
tt('thm/ieee/roundmode_case_def_1', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/roundmode_CASE' A) 'const/ieee/float_To_zero' v0 v1 v2 v3) = v1))).
tt('thm/ieee/roundmode_case_def_2', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/roundmode_CASE' A) 'const/ieee/To_pinfinity' v0 v1 v2 v3) = v2))).
tt('thm/ieee/roundmode_case_def_e3', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/roundmode_CASE' A) 'const/ieee/To_ninfinity' v0 v1 v2 v3) = v3))).
tt('thm/ieee/datatype_roundmode_', ax, (![roundmode : ('type/ieee/roundmode' > ('type/ieee/roundmode' > ('type/ieee/roundmode' > ('type/ieee/roundmode' > $o))))]: (('const/bool/DATATYPE' $o) (roundmode 'const/ieee/To_nearest' 'const/ieee/float_To_zero' 'const/ieee/To_pinfinity' 'const/ieee/To_ninfinity')))).
tt('thm/ieee/roundmode_distinct_0', ax, (~ ('const/ieee/To_nearest' = 'const/ieee/float_To_zero'))).
tt('thm/ieee/roundmode_distinct_1', ax, (~ ('const/ieee/To_nearest' = 'const/ieee/To_pinfinity'))).
tt('thm/ieee/roundmode_distinct_2', ax, (~ ('const/ieee/To_nearest' = 'const/ieee/To_ninfinity'))).
tt('thm/ieee/roundmode_distinct_3', ax, (~ ('const/ieee/float_To_zero' = 'const/ieee/To_pinfinity'))).
tt('thm/ieee/roundmode_distinct_4', ax, (~ ('const/ieee/float_To_zero' = 'const/ieee/To_ninfinity'))).
tt('thm/ieee/roundmode_distinct_e5', ax, (~ ('const/ieee/To_pinfinity' = 'const/ieee/To_ninfinity'))).
tt('thm/ieee/roundmode_case_cong_', ax, ![A : $t]: (!['v3\'' : A, 'v2\'' : A, 'v1\'' : A, 'v0\'' : A, M : 'type/ieee/roundmode', 'M\'' : 'type/ieee/roundmode', v0 : A, v1 : A, v2 : A, v3 : A]: (((M = 'M\'') & ((('M\'' = 'const/ieee/To_nearest') => (v0 = 'v0\'')) & ((('M\'' = 'const/ieee/float_To_zero') => (v1 = 'v1\'')) & ((('M\'' = 'const/ieee/To_pinfinity') => (v2 = 'v2\'')) & (('M\'' = 'const/ieee/To_ninfinity') => (v3 = 'v3\'')))))) => ((('const/ieee/roundmode_CASE' A) M v0 v1 v2 v3) = (('const/ieee/roundmode_CASE' A) 'M\'' 'v0\'' 'v1\'' 'v2\'' 'v3\''))))).
tt('thm/ieee/roundmode_nchotomy_', ax, (![a : 'type/ieee/roundmode']: ((a = 'const/ieee/To_nearest') | ((a = 'const/ieee/float_To_zero') | ((a = 'const/ieee/To_pinfinity') | (a = 'const/ieee/To_ninfinity')))))).
tt('thm/ieee/roundmode_Axiom_', ax, ![A : $t]: (![x0 : A, x1 : A, x2 : A, x3 : A]: (?[f : ('type/ieee/roundmode' > A)]: (((f 'const/ieee/To_nearest') = x0) & (((f 'const/ieee/float_To_zero') = x1) & (((f 'const/ieee/To_pinfinity') = x2) & ((f 'const/ieee/To_ninfinity') = x3))))))).
tt('thm/ieee/roundmode_induction_', ax, (![P : ('type/ieee/roundmode' > $o)]: (((P 'const/ieee/To_nearest') & ((P 'const/ieee/To_ninfinity') & ((P 'const/ieee/To_pinfinity') & (P 'const/ieee/float_To_zero')))) => (![a : 'type/ieee/roundmode']: (P a))))).
tt('thm/ieee/is_closest_', def, ![A : $t]: (![v : (A > 'type/realax/real'), s : (A > $o), x : 'type/realax/real', a : A]: ((('const/ieee/is_closest' A) v s x a) = ((('const/bool/IN' A) a s) & (![b : A]: ((('const/bool/IN' A) b s) => ('const/real/real_lte' ('const/real/abs' ('const/real/real_sub' (v a) x)) ('const/real/abs' ('const/real/real_sub' (v b) x))))))))).
tt('thm/ieee/closest_', def, ![A : $t]: (![v : (A > 'type/realax/real'), p : (A > $o), s : (A > $o), x : 'type/realax/real']: ((('const/ieee/closest' A) v p s x) = (('const/min/@' A) (^[a : A]: ((('const/ieee/is_closest' A) v s x a) & ((?[b : A]: ((('const/ieee/is_closest' A) v s x b) & (p b))) => (p a)))))))).
tt('thm/ieee/round_def_0', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/round' X 'const/ieee/To_nearest' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_lte' x ('const/realax/real_neg' ('const/ieee/threshold' X))) ('const/ieee/minus_infinity' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_ge' x ('const/ieee/threshold' X)) ('const/ieee/plus_infinity' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: ('const/arithmetic/EVEN' ('const/ieee/fraction' 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_finite' X a)))) x)))))).
tt('thm/ieee/round_def_1', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/round' X 'const/ieee/float_To_zero' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/realax/real_lt' x ('const/realax/real_neg' ('const/ieee/largest' X))) ('const/ieee/bottomfloat' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_gt' x ('const/ieee/largest' X)) ('const/ieee/topfloat' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[x0 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: $true) (('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/real/real_lte' ('const/real/abs' ('const/ieee/valof' X a)) ('const/real/abs' x)))))) x)))))).
tt('thm/ieee/round_def_2', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/round' X 'const/ieee/To_pinfinity' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/realax/real_lt' x ('const/realax/real_neg' ('const/ieee/largest' X))) ('const/ieee/bottomfloat' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_gt' x ('const/ieee/largest' X)) ('const/ieee/plus_infinity' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[x0 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: $true) (('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/real/real_ge' ('const/ieee/valof' X a) x))))) x)))))).
tt('thm/ieee/round_def_e3', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/round' X 'const/ieee/To_ninfinity' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/realax/real_lt' x ('const/realax/real_neg' ('const/ieee/largest' X))) ('const/ieee/minus_infinity' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_gt' x ('const/ieee/largest' X)) ('const/ieee/topfloat' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[x0 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: $true) (('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/real/real_lte' ('const/ieee/valof' X a) x))))) x)))))).
tt('thm/ieee/is_integral_', def, (![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_integral' X a) = (('const/ieee/is_finite' X a) & (?[n : 'type/num/num']: (('const/real/abs' ('const/ieee/valof' X a)) = ('const/real/real_of_num' n))))))).
tt('thm/ieee/intround_def_0', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/intround' X 'const/ieee/To_nearest' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_lte' x ('const/realax/real_neg' ('const/ieee/threshold' X))) ('const/ieee/minus_infinity' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_ge' x ('const/ieee/threshold' X)) ('const/ieee/plus_infinity' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (?[n : 'type/num/num']: (('const/arithmetic/EVEN' n) & (('const/real/abs' ('const/ieee/valof' X a)) = ('const/real/real_of_num' n))))) (('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_integral' X a)))) x)))))).
tt('thm/ieee/intround_def_1', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/intround' X 'const/ieee/float_To_zero' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/realax/real_lt' x ('const/realax/real_neg' ('const/ieee/largest' X))) ('const/ieee/bottomfloat' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_gt' x ('const/ieee/largest' X)) ('const/ieee/topfloat' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[x0 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: $true) (('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_integral' X a) & ('const/real/real_lte' ('const/real/abs' ('const/ieee/valof' X a)) ('const/real/abs' x)))))) x)))))).
tt('thm/ieee/intround_def_2', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/intround' X 'const/ieee/To_pinfinity' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/realax/real_lt' x ('const/realax/real_neg' ('const/ieee/largest' X))) ('const/ieee/bottomfloat' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_gt' x ('const/ieee/largest' X)) ('const/ieee/plus_infinity' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[x0 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: $true) (('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_integral' X a) & ('const/real/real_ge' ('const/ieee/valof' X a) x))))) x)))))).
tt('thm/ieee/intround_def_e3', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), x : 'type/realax/real']: (('const/ieee/intround' X 'const/ieee/To_ninfinity' x) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/realax/real_lt' x ('const/realax/real_neg' ('const/ieee/largest' X))) ('const/ieee/minus_infinity' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/real/real_gt' x ('const/ieee/largest' X)) ('const/ieee/topfloat' X) (('const/ieee/closest' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/valof' X) (^[x0 : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: $true) (('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_integral' X a) & ('const/real/real_lte' ('const/ieee/valof' X a) x))))) x)))))).
tt('thm/ieee/some_nan_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num')]: (('const/ieee/some_nan' X) = (('const/min/@' ('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_nan' X a)))))).
tt('thm/ieee/zerosign_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), s : 'type/num/num', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/zerosign' X s a) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_zero' X a) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (s = 'const/num/0') ('const/ieee/plus_zero' X) ('const/ieee/minus_zero' X)) a)))).
tt('thm/ieee/rem_', def, (![x : 'type/realax/real', y : 'type/realax/real']: (('const/ieee/rem' x y) = (('const/bool/LET' 'type/realax/real' 'type/realax/real') (^[n : 'type/realax/real']: ('const/real/real_sub' x ('const/realax/real_mul' n y))) (('const/ieee/closest' 'type/realax/real') ('const/combin/I' 'type/realax/real') (^[x0 : 'type/realax/real']: (?[n : 'type/num/num']: (('const/arithmetic/EVEN' n) & (('const/real/abs' x0) = ('const/real/real_of_num' n))))) (('const/pred_set/GSPEC' 'type/realax/real' 'type/realax/real') (^[x0 : 'type/realax/real']: (('const/pair/,' 'type/realax/real' $o) x0 (?[n : 'type/num/num']: (('const/real/abs' x0) = ('const/real/real_of_num' n)))))) ('const/real/#slash#' x y)))))).
tt('thm/ieee/fintrnd_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fintrnd' X m a) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_nan' X a) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X a) a ('const/ieee/zerosign' X ('const/ieee/sign' a) ('const/ieee/intround' X m ('const/ieee/valof' X a)))))))).
tt('thm/ieee/fadd_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fadd' X m a b) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_nan' X a) | (('const/ieee/is_nan' X b) | (('const/ieee/is_infinity' X a) & (('const/ieee/is_infinity' X b) & (~ (('const/ieee/sign' a) = ('const/ieee/sign' b))))))) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X a) a (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X b) b ('const/ieee/zerosign' X (('const/bool/COND' 'type/num/num') (('const/ieee/is_zero' X a) & (('const/ieee/is_zero' X b) & (('const/ieee/sign' a) = ('const/ieee/sign' b)))) ('const/ieee/sign' a) (('const/bool/COND' 'type/num/num') (m = 'const/ieee/To_ninfinity') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) 'const/num/0')) ('const/ieee/round' X m ('const/realax/real_add' ('const/ieee/valof' X a) ('const/ieee/valof' X b)))))))))).
tt('thm/ieee/fsub_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fsub' X m a b) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_nan' X a) | (('const/ieee/is_nan' X b) | (('const/ieee/is_infinity' X a) & (('const/ieee/is_infinity' X b) & (('const/ieee/sign' a) = ('const/ieee/sign' b)))))) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X a) a (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X b) ('const/ieee/minus' X b) ('const/ieee/zerosign' X (('const/bool/COND' 'type/num/num') (('const/ieee/is_zero' X a) & (('const/ieee/is_zero' X b) & (~ (('const/ieee/sign' a) = ('const/ieee/sign' b))))) ('const/ieee/sign' a) (('const/bool/COND' 'type/num/num') (m = 'const/ieee/To_ninfinity') ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) 'const/num/0')) ('const/ieee/round' X m ('const/real/real_sub' ('const/ieee/valof' X a) ('const/ieee/valof' X b)))))))))).
tt('thm/ieee/fmul_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fmul' X m a b) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_nan' X a) | (('const/ieee/is_nan' X b) | ((('const/ieee/is_zero' X a) & ('const/ieee/is_infinity' X b)) | (('const/ieee/is_infinity' X a) & ('const/ieee/is_zero' X b))))) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_infinity' X a) | ('const/ieee/is_infinity' X b)) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/sign' a) = ('const/ieee/sign' b)) ('const/ieee/plus_infinity' X) ('const/ieee/minus_infinity' X)) ('const/ieee/zerosign' X (('const/bool/COND' 'type/num/num') (('const/ieee/sign' a) = ('const/ieee/sign' b)) 'const/num/0' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/ieee/round' X m ('const/realax/real_mul' ('const/ieee/valof' X a) ('const/ieee/valof' X b))))))))).
tt('thm/ieee/fdiv_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fdiv' X m a b) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_nan' X a) | (('const/ieee/is_nan' X b) | ((('const/ieee/is_zero' X a) & ('const/ieee/is_zero' X b)) | (('const/ieee/is_infinity' X a) & ('const/ieee/is_infinity' X b))))) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_infinity' X a) | ('const/ieee/is_zero' X b)) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/sign' a) = ('const/ieee/sign' b)) ('const/ieee/plus_infinity' X) ('const/ieee/minus_infinity' X)) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X b) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/sign' a) = ('const/ieee/sign' b)) ('const/ieee/plus_zero' X) ('const/ieee/minus_zero' X)) ('const/ieee/zerosign' X (('const/bool/COND' 'type/num/num') (('const/ieee/sign' a) = ('const/ieee/sign' b)) 'const/num/0' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/ieee/round' X m ('const/real/#slash#' ('const/ieee/valof' X a) ('const/ieee/valof' X b)))))))))).
tt('thm/ieee/fsqrt_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fsqrt' X m a) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_nan' X a) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_zero' X a) | (('const/ieee/is_infinity' X a) & (('const/ieee/sign' a) = 'const/num/0'))) a (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/sign' a) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) ('const/ieee/some_nan' X) ('const/ieee/zerosign' X ('const/ieee/sign' a) ('const/ieee/round' X m ('const/transc/sqrt' ('const/ieee/valof' X a)))))))))).
tt('thm/ieee/frem_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/frem' X m a b) = (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) (('const/ieee/is_nan' X a) | (('const/ieee/is_nan' X b) | (('const/ieee/is_infinity' X a) | ('const/ieee/is_zero' X b)))) ('const/ieee/some_nan' X) (('const/bool/COND' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))) ('const/ieee/is_infinity' X b) a ('const/ieee/zerosign' X ('const/ieee/sign' a) ('const/ieee/round' X m ('const/ieee/rem' ('const/ieee/valof' X a) ('const/ieee/valof' X b))))))))).
tt('thm/ieee/fneg_', def, (![X : ('type/pair/prod' 'type/num/num' 'type/num/num'), m : 'type/ieee/roundmode', a : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fneg' X m a) = (('const/pair/,' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) ('const/arithmetic/-' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) ('const/ieee/sign' a)) (('const/pair/,' 'type/num/num' 'type/num/num') ('const/ieee/exponent' a) ('const/ieee/fraction' a)))))).
tt('thm/ieee/ccode_TY_DEF_', def, (?[rep : ('type/ieee/ccode' > 'type/num/num')]: (('const/bool/TYPE_DEFINITION' 'type/num/num' 'type/ieee/ccode') (^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) rep))).
tt('thm/ieee/ccode_BIJ_0', def, (![a : 'type/ieee/ccode']: (('const/ieee/num2ccode' ('const/ieee/ccode2num' a)) = a))).
tt('thm/ieee/ccode_BIJ_e1', def, (![r : 'type/num/num']: (((^[n : 'type/num/num']: ('const/prim_rec/<' n ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) r) = (('const/ieee/ccode2num' ('const/ieee/num2ccode' r)) = r)))).
tt('thm/ieee/num2ccode_ccode2num_', ax, (![a : 'type/ieee/ccode']: (('const/ieee/num2ccode' ('const/ieee/ccode2num' a)) = a))).
tt('thm/ieee/ccode2num_num2ccode_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (('const/ieee/ccode2num' ('const/ieee/num2ccode' r)) = r)))).
tt('thm/ieee/num2ccode_11_', ax, (![r : 'type/num/num', 'r\'' : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => (('const/prim_rec/<' 'r\'' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) => ((('const/ieee/num2ccode' r) = ('const/ieee/num2ccode' 'r\'')) = (r = 'r\'')))))).
tt('thm/ieee/ccode2num_11_', ax, (![a : 'type/ieee/ccode', 'a\'' : 'type/ieee/ccode']: ((('const/ieee/ccode2num' a) = ('const/ieee/ccode2num' 'a\'')) = (a = 'a\'')))).
tt('thm/ieee/num2ccode_ONTO_', ax, (![a : 'type/ieee/ccode']: (?[r : 'type/num/num']: ((a = ('const/ieee/num2ccode' r)) & ('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))).
tt('thm/ieee/ccode2num_ONTO_', ax, (![r : 'type/num/num']: (('const/prim_rec/<' r ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (?[a : 'type/ieee/ccode']: (r = ('const/ieee/ccode2num' a)))))).
tt('thm/ieee/num2ccode_thm_0', ax, (('const/ieee/num2ccode' 'const/num/0') = 'const/ieee/Gt')).
tt('thm/ieee/num2ccode_thm_1', ax, (('const/ieee/num2ccode' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) = 'const/ieee/Lt')).
tt('thm/ieee/num2ccode_thm_2', ax, (('const/ieee/num2ccode' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) = 'const/ieee/Eq')).
tt('thm/ieee/num2ccode_thm_e3', ax, (('const/ieee/num2ccode' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = 'const/ieee/Un')).
tt('thm/ieee/ccode2num_thm_0', ax, (('const/ieee/ccode2num' 'const/ieee/Gt') = 'const/num/0')).
tt('thm/ieee/ccode2num_thm_1', ax, (('const/ieee/ccode2num' 'const/ieee/Lt') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))).
tt('thm/ieee/ccode2num_thm_2', ax, (('const/ieee/ccode2num' 'const/ieee/Eq') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO')))).
tt('thm/ieee/ccode2num_thm_e3', ax, (('const/ieee/ccode2num' 'const/ieee/Un') = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))).
tt('thm/ieee/ccode_EQ_ccode_', ax, (![a : 'type/ieee/ccode', 'a\'' : 'type/ieee/ccode']: ((a = 'a\'') = (('const/ieee/ccode2num' a) = ('const/ieee/ccode2num' 'a\''))))).
tt('thm/ieee/ccode_size_def_', def, (![x : 'type/ieee/ccode']: (('const/ieee/ccode_size' x) = 'const/num/0'))).
tt('thm/ieee/ccode_CASE_', def, ![A : $t]: (![x : 'type/ieee/ccode', v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/ccode_CASE' A) x v0 v1 v2 v3) = ((^[m : 'type/num/num']: (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))) v0 (('const/bool/COND' A) ('const/prim_rec/<' m ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v1 (('const/bool/COND' A) (m = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT2' 'const/arithmetic/ZERO'))) v2 v3)))) ('const/ieee/ccode2num' x))))).
tt('thm/ieee/ccode_case_def_0', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/ccode_CASE' A) 'const/ieee/Gt' v0 v1 v2 v3) = v0))).
tt('thm/ieee/ccode_case_def_1', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/ccode_CASE' A) 'const/ieee/Lt' v0 v1 v2 v3) = v1))).
tt('thm/ieee/ccode_case_def_2', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/ccode_CASE' A) 'const/ieee/Eq' v0 v1 v2 v3) = v2))).
tt('thm/ieee/ccode_case_def_e3', ax, ![A : $t]: (![v0 : A, v1 : A, v2 : A, v3 : A]: ((('const/ieee/ccode_CASE' A) 'const/ieee/Un' v0 v1 v2 v3) = v3))).
tt('thm/ieee/datatype_ccode_', ax, (![ccode : ('type/ieee/ccode' > ('type/ieee/ccode' > ('type/ieee/ccode' > ('type/ieee/ccode' > $o))))]: (('const/bool/DATATYPE' $o) (ccode 'const/ieee/Gt' 'const/ieee/Lt' 'const/ieee/Eq' 'const/ieee/Un')))).
tt('thm/ieee/ccode_distinct_0', ax, (~ ('const/ieee/Gt' = 'const/ieee/Lt'))).
tt('thm/ieee/ccode_distinct_1', ax, (~ ('const/ieee/Gt' = 'const/ieee/Eq'))).
tt('thm/ieee/ccode_distinct_2', ax, (~ ('const/ieee/Gt' = 'const/ieee/Un'))).
tt('thm/ieee/ccode_distinct_3', ax, (~ ('const/ieee/Lt' = 'const/ieee/Eq'))).
tt('thm/ieee/ccode_distinct_4', ax, (~ ('const/ieee/Lt' = 'const/ieee/Un'))).
tt('thm/ieee/ccode_distinct_e5', ax, (~ ('const/ieee/Eq' = 'const/ieee/Un'))).
tt('thm/ieee/ccode_case_cong_', ax, ![A : $t]: (!['v3\'' : A, 'v2\'' : A, 'v1\'' : A, 'v0\'' : A, M : 'type/ieee/ccode', 'M\'' : 'type/ieee/ccode', v0 : A, v1 : A, v2 : A, v3 : A]: (((M = 'M\'') & ((('M\'' = 'const/ieee/Gt') => (v0 = 'v0\'')) & ((('M\'' = 'const/ieee/Lt') => (v1 = 'v1\'')) & ((('M\'' = 'const/ieee/Eq') => (v2 = 'v2\'')) & (('M\'' = 'const/ieee/Un') => (v3 = 'v3\'')))))) => ((('const/ieee/ccode_CASE' A) M v0 v1 v2 v3) = (('const/ieee/ccode_CASE' A) 'M\'' 'v0\'' 'v1\'' 'v2\'' 'v3\''))))).
tt('thm/ieee/ccode_nchotomy_', ax, (![a : 'type/ieee/ccode']: ((a = 'const/ieee/Gt') | ((a = 'const/ieee/Lt') | ((a = 'const/ieee/Eq') | (a = 'const/ieee/Un')))))).
tt('thm/ieee/ccode_Axiom_', ax, ![A : $t]: (![x0 : A, x1 : A, x2 : A, x3 : A]: (?[f : ('type/ieee/ccode' > A)]: (((f 'const/ieee/Gt') = x0) & (((f 'const/ieee/Lt') = x1) & (((f 'const/ieee/Eq') = x2) & ((f 'const/ieee/Un') = x3))))))).
tt('thm/ieee/ccode_induction_', ax, (![P : ('type/ieee/ccode' > $o)]: (((P 'const/ieee/Eq') & ((P 'const/ieee/Gt') & ((P 'const/ieee/Lt') & (P 'const/ieee/Un')))) => (![a : 'type/ieee/ccode']: (P a))))).
tt('thm/ieee/fcompare_', def, (![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')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fcompare' X a b) = (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_nan' X a) | ('const/ieee/is_nan' X b)) 'const/ieee/Un' (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_infinity' X a) & (('const/ieee/sign' a) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_infinity' X b) & (('const/ieee/sign' b) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/ieee/Eq' 'const/ieee/Lt') (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_infinity' X a) & (('const/ieee/sign' a) = 'const/num/0')) (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_infinity' X b) & (('const/ieee/sign' b) = 'const/num/0')) 'const/ieee/Eq' 'const/ieee/Gt') (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_infinity' X b) & (('const/ieee/sign' b) = ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) 'const/ieee/Gt' (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/is_infinity' X b) & (('const/ieee/sign' b) = 'const/num/0')) 'const/ieee/Lt' (('const/bool/COND' 'type/ieee/ccode') ('const/realax/real_lt' ('const/ieee/valof' X a) ('const/ieee/valof' X b)) 'const/ieee/Lt' (('const/bool/COND' 'type/ieee/ccode') (('const/ieee/valof' X a) = ('const/ieee/valof' X b)) 'const/ieee/Eq' 'const/ieee/Gt')))))))))).
tt('thm/ieee/flt_', def, (![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')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/flt' X a b) = (('const/ieee/fcompare' X a b) = 'const/ieee/Lt')))).
tt('thm/ieee/fle_', def, (![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')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fle' X a b) = ((('const/ieee/fcompare' X a b) = 'const/ieee/Lt') | (('const/ieee/fcompare' X a b) = 'const/ieee/Eq'))))).
tt('thm/ieee/fgt_', def, (![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')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fgt' X a b) = (('const/ieee/fcompare' X a b) = 'const/ieee/Gt')))).
tt('thm/ieee/fge_', def, (![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')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/fge' X a b) = ((('const/ieee/fcompare' X a b) = 'const/ieee/Gt') | (('const/ieee/fcompare' X a b) = 'const/ieee/Eq'))))).
tt('thm/ieee/feq_', def, (![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')), b : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/feq' X a b) = (('const/ieee/fcompare' X a b) = 'const/ieee/Eq')))).
tt('thm/ieee/float_format_', def, ('const/ieee/float_format' = (('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')))))))).
tt('thm/ieee/float_TY_DEF_', def, (?[rep : ('type/ieee/float' > ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')))]: (('const/bool/TYPE_DEFINITION' ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num')) 'type/ieee/float') ('const/ieee/is_valid' 'const/ieee/float_format') rep))).
tt('thm/ieee/float_tybij_0', def, (![a : 'type/ieee/float']: (('const/ieee/float' ('const/ieee/defloat' a)) = a))).
tt('thm/ieee/float_tybij_e1', def, (![r : ('type/pair/prod' 'type/num/num' ('type/pair/prod' 'type/num/num' 'type/num/num'))]: (('const/ieee/is_valid' 'const/ieee/float_format' r) = (('const/ieee/defloat' ('const/ieee/float' r)) = r)))).
tt('thm/ieee/Val_', def, (![a : 'type/ieee/float']: (('const/ieee/Val' a) = ('const/ieee/valof' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Float_', def, (![x : 'type/realax/real']: (('const/ieee/Float' x) = ('const/ieee/float' ('const/ieee/round' 'const/ieee/float_format' 'const/ieee/To_nearest' x))))).
tt('thm/ieee/Sign_', def, (![a : 'type/ieee/float']: (('const/ieee/Sign' a) = ('const/ieee/sign' ('const/ieee/defloat' a))))).
tt('thm/ieee/Exponent_', def, (![a : 'type/ieee/float']: (('const/ieee/Exponent' a) = ('const/ieee/exponent' ('const/ieee/defloat' a))))).
tt('thm/ieee/Fraction_', def, (![a : 'type/ieee/float']: (('const/ieee/Fraction' a) = ('const/ieee/fraction' ('const/ieee/defloat' a))))).
tt('thm/ieee/Ulp_', def, (![a : 'type/ieee/float']: (('const/ieee/Ulp' a) = ('const/ieee/ulp' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Isnan_', def, (![a : 'type/ieee/float']: (('const/ieee/Isnan' a) = ('const/ieee/is_nan' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Infinity_', def, (![a : 'type/ieee/float']: (('const/ieee/Infinity' a) = ('const/ieee/is_infinity' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Isnormal_', def, (![a : 'type/ieee/float']: (('const/ieee/Isnormal' a) = ('const/ieee/is_normal' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Isdenormal_', def, (![a : 'type/ieee/float']: (('const/ieee/Isdenormal' a) = ('const/ieee/is_denormal' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Iszero_', def, (![a : 'type/ieee/float']: (('const/ieee/Iszero' a) = ('const/ieee/is_zero' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Finite_', def, (![a : 'type/ieee/float']: (('const/ieee/Finite' a) = (('const/ieee/Isnormal' a) | (('const/ieee/Isdenormal' a) | ('const/ieee/Iszero' a)))))).
tt('thm/ieee/Isintegral_', def, (![a : 'type/ieee/float']: (('const/ieee/Isintegral' a) = ('const/ieee/is_integral' 'const/ieee/float_format' ('const/ieee/defloat' a))))).
tt('thm/ieee/Plus_zero_', def, ('const/ieee/Plus_zero' = ('const/ieee/float' ('const/ieee/plus_zero' 'const/ieee/float_format')))).
tt('thm/ieee/Minus_zero_', def, ('const/ieee/Minus_zero' = ('const/ieee/float' ('const/ieee/minus_zero' 'const/ieee/float_format')))).
tt('thm/ieee/Minus_infinity_', def, ('const/ieee/Minus_infinity' = ('const/ieee/float' ('const/ieee/minus_infinity' 'const/ieee/float_format')))).
tt('thm/ieee/Plus_infinity_', def, ('const/ieee/Plus_infinity' = ('const/ieee/float' ('const/ieee/plus_infinity' 'const/ieee/float_format')))).
tt('thm/ieee/float_add_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_add' a b) = ('const/ieee/float' ('const/ieee/fadd' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a) ('const/ieee/defloat' b)))))).
tt('thm/ieee/float_sub_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_sub' a b) = ('const/ieee/float' ('const/ieee/fsub' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a) ('const/ieee/defloat' b)))))).
tt('thm/ieee/float_mul_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_mul' a b) = ('const/ieee/float' ('const/ieee/fmul' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a) ('const/ieee/defloat' b)))))).
tt('thm/ieee/float_div_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_div' a b) = ('const/ieee/float' ('const/ieee/fdiv' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a) ('const/ieee/defloat' b)))))).
tt('thm/ieee/float_rem_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_rem' a b) = ('const/ieee/float' ('const/ieee/frem' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a) ('const/ieee/defloat' b)))))).
tt('thm/ieee/float_sqrt_', def, (![a : 'type/ieee/float']: (('const/ieee/float_sqrt' a) = ('const/ieee/float' ('const/ieee/fsqrt' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a)))))).
tt('thm/ieee/ROUNDFLOAT_', def, (![a : 'type/ieee/float']: (('const/ieee/ROUNDFLOAT' a) = ('const/ieee/float' ('const/ieee/fintrnd' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a)))))).
tt('thm/ieee/float_lt_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_lt' a b) = ('const/ieee/flt' 'const/ieee/float_format' ('const/ieee/defloat' a) ('const/ieee/defloat' b))))).
tt('thm/ieee/float_le_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_le' a b) = ('const/ieee/fle' 'const/ieee/float_format' ('const/ieee/defloat' a) ('const/ieee/defloat' b))))).
tt('thm/ieee/float_gt_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_gt' a b) = ('const/ieee/fgt' 'const/ieee/float_format' ('const/ieee/defloat' a) ('const/ieee/defloat' b))))).
tt('thm/ieee/float_ge_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_ge' a b) = ('const/ieee/fge' 'const/ieee/float_format' ('const/ieee/defloat' a) ('const/ieee/defloat' b))))).
tt('thm/ieee/float_eq_', def, (![a : 'type/ieee/float', b : 'type/ieee/float']: (('const/ieee/float_eq' a b) = ('const/ieee/feq' 'const/ieee/float_format' ('const/ieee/defloat' a) ('const/ieee/defloat' b))))).
tt('thm/ieee/float_neg_', def, (![a : 'type/ieee/float']: (('const/ieee/float_neg' a) = ('const/ieee/float' ('const/ieee/fneg' 'const/ieee/float_format' 'const/ieee/To_nearest' ('const/ieee/defloat' a)))))).
tt('thm/ieee/float_abs_', def, (![a : 'type/ieee/float']: (('const/ieee/float_abs' a) = (('const/bool/COND' 'type/ieee/float') ('const/ieee/float_ge' a 'const/ieee/Plus_zero') a ('const/ieee/float_neg' a))))).
