NFP Category

The NFP category deals with the normal form property of first-order term rewrite systems. It is a component category of the UN category.

Input

The input is a TRS, specified in basic TRS format or in extended TRS format.

Problem

A TRS has the normal form property (NFP) if any term convertible to a normal form reaches that normal form. The problem is to answer the question whether the input TRS is NFP or not.

Problem Selection

See the corresponding section of UN category.

Output Format

The output format should follow the same rules as for the TRS category.

Scoring

The scoring is the same as for the TRS category.