The term {tt (floor $tau$)} denotes the largest integer less than the object denoted by $tau$.
(=> (Floor $X $Y) (Integer $Y))