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 .
Note that the membership to
having a double exponential time complexity,
may run for a very long time for big TRS.
Use the Stop button to stop the computation.