YES

The TRS could be proven terminating. The proof took 38 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (18ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 4 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

rev#(++(x, y))++#(rev(y), rev(x))rev#(++(x, y))rev#(x)
rev#(++(x, y))rev#(y)++#(x, ++(y, z))++#(++(x, y), z)
++#(.(x, y), z)++#(y, z)++#(x, ++(y, z))++#(x, y)

Rewrite Rules

rev(nil)nilrev(rev(x))x
rev(++(x, y))++(rev(y), rev(x))++(nil, y)y
++(x, nil)x++(.(x, y), z).(x, ++(y, z))
++(x, ++(y, z))++(++(x, y), z)make(x).(x, nil)

Original Signature

Termination of terms over the following signature is verified: rev, ++, ., make, nil

Strategy


The following SCCs where found

++#(x, ++(y, z)) → ++#(++(x, y), z)++#(.(x, y), z) → ++#(y, z)
++#(x, ++(y, z)) → ++#(x, y)

rev#(++(x, y)) → rev#(x)rev#(++(x, y)) → rev#(y)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

rev#(++(x, y))rev#(x)rev#(++(x, y))rev#(y)

Rewrite Rules

rev(nil)nilrev(rev(x))x
rev(++(x, y))++(rev(y), rev(x))++(nil, y)y
++(x, nil)x++(.(x, y), z).(x, ++(y, z))
++(x, ++(y, z))++(++(x, y), z)make(x).(x, nil)

Original Signature

Termination of terms over the following signature is verified: rev, ++, ., make, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

rev#(++(x, y))rev#(x)rev#(++(x, y))rev#(y)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

++#(x, ++(y, z))++#(++(x, y), z)++#(.(x, y), z)++#(y, z)
++#(x, ++(y, z))++#(x, y)

Rewrite Rules

rev(nil)nilrev(rev(x))x
rev(++(x, y))++(rev(y), rev(x))++(nil, y)y
++(x, nil)x++(.(x, y), z).(x, ++(y, z))
++(x, ++(y, z))++(++(x, y), z)make(x).(x, nil)

Original Signature

Termination of terms over the following signature is verified: rev, ++, ., make, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

++#(x, ++(y, z))++#(++(x, y), z)++#(x, ++(y, z))++#(x, y)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

++#(.(x, y), z)++#(y, z)

Rewrite Rules

rev(nil)nilrev(rev(x))x
rev(++(x, y))++(rev(y), rev(x))++(nil, y)y
++(x, nil)x++(.(x, y), z).(x, ++(y, z))
++(x, ++(y, z))++(++(x, y), z)make(x).(x, nil)

Original Signature

Termination of terms over the following signature is verified: rev, ., ++, make, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

++#(.(x, y), z)++#(y, z)