The answer is either ``the TRS is in
CBN or
``the TRS is not in
CBN; in the latter case an
``-free-term''
*i.e.* a term with no
-needed redex is shown.

The *Call-by-need * command checks membership to
CBN
but with the signature extended with a fresh constant symbol .
Indeed a TRS may be in
CBN with the signature consiting of
all the symbols appearing in its rules but **not** in
CBN 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 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.

2005-02-01