* Category type

demonstration category for CoCo 2016

* Problem and Semantics

Our problem is to check ground confluence of many-sorted TRSs. 
A many-sorted TRS R is ground confluent if R is confluent on the 
set of ground terms. For many-sorted TRSs, we refer e.g. Section 6.5.6 of
the book: Terese, Term Rewriting Systems, Cambridge University Press, 2003.

* Input and Input format

The input of the problem is a many-sorted TRS. To declare many-sorted TRSs, 
we add the following changes to the specification of first-order TRSs 
(in old TPDB format):

(i) Add sorted function declaration.
Thus, decl is replaced as follows:
...........
decl ::= VAR varlist | RULES listofrules | FUN funlist | id anylist
varlist ::=  | id varlist
funlist ::=  | fun funlist
fun ::= id : sort
sort ::= id | idlist -> id
idlist ::= id | id , idlist
...........
Furthermore, id should not contain ':'.

* Example

(FUN
  b: 0
  c: 1
  f: 0 -> 0
  g: 0 -> 1
  h: 1, 1 -> 2
)
(VAR
  x
)
(RULES
  g(b) -> g(f(f(f(f(b)))))
  f(f(x)) -> b
  f(b) -> b
  g(f(b)) -> c
  h(x,g(b)) -> h(c,c)
  h(c,x) -> h(c,g(f(f(b))))
)