Membership to CBN

One can check membership to CBN$_\alpha$ for the current TRS $\mathcal{R}$ and the current approximation $\alpha$ by using the Call-by-need command.

The answer is either ``the TRS is in CBN$_\alpha$ or ``the TRS is not in CBN$_\alpha$; in the latter case an ``$\alpha$-free-term'' i.e. a term with no $\mathcal{R}_\alpha$-needed redex is shown.

The Call-by-need command checks membership to CBN$_\alpha$ but with the signature extended with a fresh constant symbol . Indeed a TRS may be in CBN$_\alpha$ with the signature consiting of all the symbols appearing in its rules but not in CBN$_\alpha$ with the same signature extended by just one fresh symbol. The preservation of membership thru ``signature extension'' has been investigated in [5].

Note that the membership to CBN$_\alpha$ problem having a double exponential time complexity, may run for a very long time for big TRS.
Use the Stop button to stop the computation.