Updated:
Aug 04, 2014

## Implemented Procedure (Ver. 1.0)

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

- If
`R` is a normal 1-CTRS, then go to the next step;
otherwise, return `UNSUPPORTED`

.
- If
`R` satisfies the following, then return `NO`

, and
otherwise, go to the next step:
- there exists an unconditional critical pair (
`s`, `t`) of `R` such that
`s` and `t` are different strongly irreducible ground terms of `R`.

- 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`

.
- If
`R'` satisfies one of the following (i.e., `R'` is confluent), then
return `YES`

,
and otherwise, return `MAYBE`

:
`R'` is orthogonal,
or
`R'` satisfies one of the following (i.e., `R'` is terminating),
`R'` has no dependency pair,
or
`R'` ⊆ ≥ and `DP`(`R'`) ⊆ > where
`s` ≥ `t` iff |`s`| ≥ |`t`|
and ∀`x`∈`V`. |`s`|_{x} ≥ |`t`|_{x}
and
`s` > `t` iff |`s`| > |`t`|
and ∀`x`∈`V`. |`s`|_{x} ≥ |`t`|_{x}

(see [Baader & Nipkow, 92, Example 5.2.2]),

and
all the critical pairs of `R'` are joinable.