I'm trying to reduce one calculation in an iterative Successive Over-Relaxation procedure for a program I'm writing. The code that works does this calculation:
$$ s = \left\lfloor\frac{b + \left\lfloor\frac{2^{16}-1}{4}\right\rfloor}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor $$
Now, I think that the following two properties of floors/ceilings and modulus division hold up (or at least I couldn't find a contradicting set of inputs):
$$ \forall x\in\mathbb{N},y\in\mathbb{N}\left(\left\lfloor\frac{x-1}{y}\right\rfloor = \frac{x-y}{y} \leftrightarrow x\mod y = 0\right)\\ \forall x\in\mathbb{N},y\in\mathbb{N}\left(\left\lfloor\frac{x+y-1}{y}\right\rfloor=\left\lceil\frac{x}{y}\right\rceil\right) $$
So, according to the first property, because $2^{16}\mod4=0$, I can rewrite the above as:
$$ s=\left\lfloor\frac{b+\frac{2^{16}-4}{4}}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor = \left\lfloor\frac{b+\frac{2^{16}}{4}-1}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor $$
and since, again, $2^{16}\mod4=0$, it must be true that $\frac{2^{16}}{4}=\left\lfloor\frac{2^{16}}{4}\right\rfloor$, and so by the second property this can be re-written as:
$$ s=\left\lceil\frac{b}{\frac{2^{16}}{4}}\right\rceil = \left\lceil\frac{b}{2^{14}}\right\rceil $$
This usually gets me the right answer, but sometimes I get erroneous outputs, and I'm trying to eliminate this simplification of the original as the cause. Are those two properties really true? Or did I mess up in the actual simplification somewhere? Or is it actually fine and the flaw is probably elsewhere?
Bonus Question
Should those statements above be written as $\forall x\in\mathbb{N},y\in\mathbb{N}$ or $\forall(x,y)\in\mathbb{N}^2$? Or are those equivalent? I'll edit my question as appropriate/if needed according to any comments on the formatting.
$\newcommand{\fl}[1]{\left\lfloor #1 \right\rfloor}$ $\newcommand{\ce}[1]{\left\lceil #1 \right\rceil}$
The first claim is correct, if you assume that $x \geq y$.
Proof of 1: For ($\implies$), $\frac{x-y}{y}$ must be an integer, so $x$ is a multiple of $y$, in other words $x \equiv 0 \ (\textrm{mod}\ y)$. For ($\impliedby$), note that $x=ky$, so $\frac{x-y}{y}=k-1$, and $\left\lfloor \frac{x - 1}{y} \right\rfloor = \left\lfloor k - \frac{1}{y} \right\rfloor = k - 1$ whenever $y$ is positive.
The second claim is also true. Proof:
Case 1: $\fl{\frac{x}{y}} = \frac{x}{y} = \ce{\frac{x}{y}}$. Since $0 < \frac{1}{y} < 1, \fl{\frac{x}{y}} - 1 < \frac{x}{y} - \frac{1}{y} < \ce{\frac{x}{y}}$, and so $\fl{\frac{x}{y} - \frac{1}{y}} + 1 = \ce{\frac{x}{y}}$.
Case 2: $\frac{x}{y} - \frac{1}{y} < \fl{\frac{x}{y}}$: Note that $\fl{\frac{x}{y}} \leq \frac{x}{y}$. Together with the assumption, this implies that $\fl{\frac{x}{y}} = \frac{x}{y}$, reducing to case 1.
Case 3: $\fl{\frac{x}{y}} \leq \frac{x}{y} - \frac{1}{y} < \frac{x}{y} < \ce{\frac{x}{y}}$: The result is obvious.
So I don't know what's wrong with your simulation. It should work fine.