next up previous
Next: Term Menu Up: Approx Trs Menu Previous: Preservation of the set

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.



Irene DURAND
2005-02-01