YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

i(0) → 0+(0, y) → y
+(x, 0) → xi(i(x)) → x
+(i(x), x) → 0+(x, i(x)) → 0
i(+(x, y)) → +(i(x), i(y))+(x, +(y, z)) → +(+(x, y), z)
+(+(x, i(y)), y) → x+(+(x, y), i(y)) → x

Original Signature

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

Strategy

The following SCCs where found

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

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

i(0) → 0+(0, y) → y
+(x, 0) → xi(i(x)) → x
+(i(x), x) → 0+(x, i(x)) → 0
i(+(x, y)) → +(i(x), i(y))+(x, +(y, z)) → +(+(x, y), z)
+(+(x, i(y)), y) → x+(+(x, y), i(y)) → x

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:

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

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

i(0) → 0+(0, y) → y
+(x, 0) → xi(i(x)) → x
+(i(x), x) → 0+(x, i(x)) → 0
i(+(x, y)) → +(i(x), i(y))+(x, +(y, z)) → +(+(x, y), z)
+(+(x, i(y)), y) → x+(+(x, y), i(y)) → x

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, y), z)+#(x, +(y, z)) → +#(x, y)