In this talk, I will share the hard journey we experienced in proving the decidability of certain nondeterministic worklist algorithms.