YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(a, empty)g#(a, empty)g#(cons(x, k), d)g#(k, cons(x, d))
f#(a, cons(x, k))f#(cons(x, a), k)

Rewrite Rules

f(a, empty)g(a, empty)f(a, cons(x, k))f(cons(x, a), k)
g(empty, d)dg(cons(x, k), d)g(k, cons(x, d))

Original Signature

Termination of terms over the following signature is verified: f, g, empty, cons

Strategy


The following SCCs where found

g#(cons(x, k), d) → g#(k, cons(x, d))

f#(a, cons(x, k)) → f#(cons(x, a), k)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

f#(a, cons(x, k))f#(cons(x, a), k)

Rewrite Rules

f(a, empty)g(a, empty)f(a, cons(x, k))f(cons(x, a), k)
g(empty, d)dg(cons(x, k), d)g(k, cons(x, d))

Original Signature

Termination of terms over the following signature is verified: f, g, empty, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

f#(a, cons(x, k))f#(cons(x, a), k)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

g#(cons(x, k), d)g#(k, cons(x, d))

Rewrite Rules

f(a, empty)g(a, empty)f(a, cons(x, k))f(cons(x, a), k)
g(empty, d)dg(cons(x, k), d)g(k, cons(x, d))

Original Signature

Termination of terms over the following signature is verified: f, g, empty, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

g#(cons(x, k), d)g#(k, cons(x, d))