Arbitraryness

The approximated TRS is arbitrary if there exists a term $t \in \mathcal{T}(\mathcal{F})$ such that $t \to_{\mathcal{R}_\alpha,\mathcal{F}\cup \{ @ \}} @$. If the approximated TRS $\mathcal{R}_\alpha$ is arbitrary a witness term $t$ is given. One can check whether the current approximated TRS $\mathcal{R}_\alpha$ is arbitrary by using the Arbitrary command of the Approx-TRS menu.