Unchallenged Termination Function

The termination function $\beta_{\mathsf{uc}}$ is defined by $\beta_{\mathsf{uc}}(F,E) = 1$ iff $\mathsf{is}^{\not\leftarrow}(F)$ $\cup$ $\mathsf{is}^{\not\leftrightarrow}(F)$ $= \emptyset$.