It's hard for me to believe we're five pages in and you still haven't defined your operation.
You have a function  not division, but your new take on it  which takes two arguments and returns a third. Let's call it BillyB(x, y) = z. For which pairs of x and y is BillyB(x, y) defined? When BillyB(x, y) is defined, how can BillyB(x, y) = z be computed? Are there some pairs x and y for which BillyB(x, y) = x/y or BillyB(x, y+1) = x/y?
