YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

:#(z, +(x, f(y))):#(g(z, y), +(x, a)):#(:(x, y), z):#(x, :(y, z))
:#(:(x, y), z):#(y, z):#(+(x, y), z):#(y, z)
:#(+(x, y), z):#(x, z)

Rewrite Rules

:(:(x, y), z):(x, :(y, z)):(+(x, y), z)+(:(x, z), :(y, z))
:(z, +(x, f(y))):(g(z, y), +(x, a))

Original Signature

Termination of terms over the following signature is verified: f, g, a, :, +

Strategy


The following SCCs where found

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

:(:(x, y), z):(x, :(y, z)):(+(x, y), z)+(:(x, z), :(y, z))
:(z, +(x, f(y))):(g(z, y), +(x, a))

Original Signature

Termination of terms over the following signature is verified: f, g, a, :, +

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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