Hi muad, muad wrote: > I think I can write such a function in a few different ways, but I don't > know how to prove this code works, could anybody show me how? Why don't you pick a specific implementation first and share it with us? The proof heavily depends on the precise implementation. Kind regards, Martijn.