For a model checking problem, I'm attempting to emulate integer division without actually using division, having access only to integer addition, subtraction, multiplication and case analysis. No non-integer operations are permitted, all possible results will be integers as well.
I can generate a finite amount of cases using a preprocessor and the amount of possible denominators is quite small.
The formula I'm trying to implement looks like this: $$\dfrac{\sum_{i=0}^{x} a(i) \times \sum_{j=0}^{y} b(j)}{(x+1) \times (y+1)}$$
Where $x$ can change and $y$ is a constant, both are natural numbers. $a$ and $b$ can be considered to be vectors of natural numbers. I cannot use any kind of loops or the sum operator here, but using case analysis, the numerator can be generated like this:
$$num = \begin{cases} a(0) + b(0) + \ldots + b(m) & x = 0, y = m\\ a(0) + a(1) + b(0) + \ldots + b(m) & x = 1, y = m\\ \ldots& \\ a(0) + \ldots + a(n) + b(0) + \ldots + b(m) & x = n, y = m\\ \end{cases}$$
Generating the denominator itself is also quite straightforward using a similar case analysis.
My question is now whether it is possible to implement a division algorithm in a semi-controlled environment like this, using only the operators mentioned above. The amount of possible denominators is very limited since $y$ is constant and $x$ will be very small. The preprocessor knows the value $y$ as well as the maximum value for $x$. The actual contents of $a$ and $b$ cannot be accessed beforehand, but statements like $-a(0)-2 \times b(0)$ accessing the values can be generated and used in cases.