&gt; If you guard break with if then you also need to prove if the &quot;if&quot; condition does indeed provide a dataflow path to break.<p>In <i>all</i> cases, for <i>all</i> possible inputs.<p>On the other hand, if that&#x27;s what your for loop looks like, you probably have the same problem of proving that your recursion terminates (in all cases, for all possible inputs).