UNR Category

The UNR category deals with the unique normal form property with respect to reduction of first-order term rewrite systems. It is a component category of UN category.

Input

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

Problem

A TRS has the unique normal form property with respect to reduction (UNR) if from any term we can reach at most one normal form. The problem is to answer the question whether the input TRS is UNR or not.

Problem Selection

See the corresponding section of UN category.

Output Format

The output format should follow the same rule as that of the TRS category.

Scoring

The scoring is the same as for the TRS category.