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.