YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

+(x, 0)x+(x, i(x))0
+(+(x, y), z)+(x, +(y, z))*(x, +(y, z))+(*(x, y), *(x, z))
*(+(x, y), z)+(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: 0, *, +, i

Strategy


The following SCCs where found

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

+(x, 0)x+(x, i(x))0
+(+(x, y), z)+(x, +(y, z))*(x, +(y, z))+(*(x, y), *(x, z))
*(+(x, y), z)+(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: 0, *, +, i

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

+(x, 0)x+(x, i(x))0
+(+(x, y), z)+(x, +(y, z))*(x, +(y, z))+(*(x, y), *(x, z))
*(+(x, y), z)+(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: 0, *, +, i

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

+(x, 0)x+(x, i(x))0
+(+(x, y), z)+(x, +(y, z))*(x, +(y, z))+(*(x, y), *(x, z))
*(+(x, y), z)+(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: 0, *, +, i

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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