* Category type

demonstration category for CoCo 2016

* Problem and Semantics

The problem is to check unique normalization of first-order term rewrite
systems. To prevent a proliferation of categories, we propose to consider
all the following properties in one category:

- UN : from any term we can reach at most one normal form
- UNC: any two convertible normal forms are equal
- NFP: any term convertible to a normal form reaches that normal form
- CR : any two convertible terms are joinable

(Recall that CR implies NFP, NFP implies UNC and UNC implies UN. CR is
included because we expect that UN tools will be based on confluence
tools.)

* Input format

The input uses TPDB format as in the Cops database,

https://www.lri.fr/~marche/tpdb/format.html

* Output

The first line of the output is one of the following

- NO       - if the system does not have the UN property
- MAYBE    - if the answer is unknown
- YES      - if the system is uniquely normalizing (UN)
- YES(UNC) - if the system has the unique normal form property (UNC)
- YES(NFP) - if the system has the normal form property (NFP)
- YES(CR)  - if the system is confluent (CR)

The remainder of the output should contain a justification of the
answer as text, as usual.

* Example

(source: http://cops.uibk.ac.at/problems/55.trs)

(VAR x y z)
(RULES
  Ap(Ap(Ap(S,x),y),z) -> Ap(Ap(x,z),Ap(y,z))
  Ap(Ap(K,x),y) -> x
  Ap(I,x) -> x
  Dh(z,z) -> z
)
(COMMENT from p.246 of \cite{Klop80})