The term {tt (integer-decode-float $tau$)} denotes the significand of the object denoted by $tau$.
(=> (Integer-Decode-Float $X $Y) (Integer $Y))