Updated: Aug 04, 2014

Implemented Procedure (Ver. 1.0)

The tool takes a CTRS R as input, and then starts the following process:

  1. If R is a normal 1-CTRS, then go to the next step; otherwise, return UNSUPPORTED.
  2. If R satisfies the following, then return NO, and otherwise, go to the next step:
  3. If R is a TRS, then let R' be R; if R is weak left-linear, then let R' be a TRS obtained by applying the optimized SR transformation [Serbanuta & Rosu, RTA 2006] to R, while the special bracket symbol and its rewrite rules are not introduced whenever R is a constructor system; otherwise, return MAYBE.
  4. If R' satisfies one of the following (i.e., R' is confluent), then return YES, and otherwise, return MAYBE: