\begin{aligned}
S_0 &= &\mu&\\
S_1 &= \{ &\langle rdi, rdi, rax\rangle \in S_0 \}\\
S_2 &= \{ &\langle mod(4 \cdot rdi, 2^{64}), r12, rax \rangle \mid \langle rdi, r12, rax \rangle \in S_1\}\\
S_3 &= \{ &\langle rdi, r12, rax' \rangle \mid \langle rdi, r12, rax \rangle \in S_2,\\
	&&rax' \in [0, 2^{64-1}]\\
\end{aligned}