How can I prove or disprove that the following function is bijection? For a research project, I tried to prove or disprove that a function called xxhash128_low is a bijection from 64 bit unsigned integer to 64 bit unsigned integer. I have shown that it is sufficient to prove that the following critical code is a bijection:
Input: a 64-bit integer x
0. Let c=0x9e3779b185ebcaa7
1. Let x_low= the 8-low bytes of c*x.
2. Let x_high= the 8-high bytes of c*x.
3. w= x_high+2*x_low.
4  y= shift right 3 bits of w.
5. return x_low XOR y.

What I have proved till now: returning only the low 64 bits, x_low, can be shown to be a permutation. Also, y can be expressed as a function of x_low (i.e., y=f(x_low)).
Originally, the hash function was defined as follows:

Input: a 64-bit unsigned integer $x$.
Calculate $(9E3779B185EBCB87)_{16} \cdot x = 2^{64} x_h + x_l$, where $x_l,x_h$ are 64-bit unsigned integers.
Output $x_l \oplus \lfloor (x_h + 2x_l)/8 \rfloor$.

Under this definition, there is a collision: both $(2DCE4F983BBEB685)_{16}$ and $(72E04DBED1540FE1)_{16}$ map to $(A5C53FE6E277BD92)_{16}$.
You can find such collisions using a cycle detection algorithm.