<apply>
<floor/>
<ci> a </ci>
</apply>
<apply>
<forall/>
<bvar>
<ci> a </ci>
</bvar>
<apply>
<and/>
<apply>
<leq/>
<apply>
<floor/>
<ci>a</ci>
</apply>
<ci>a</ci>
</apply>
<apply>
<lt/>
<ci>a</ci>
<apply>
<plus/>
<apply>
<floor/>
<ci>a</ci>
</apply>
<cn>1</cn>
</apply>
</apply>
</apply>
</apply>