YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (6ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U01#(c, x) → T(x)g#(x) → U11#(x, x)
f#(x) → U01#(x, x)U11#(c, x) → T(x)

Rewrite Rules

f(x) → U01(x, x)U01(c, x) → x
g(x) → U11(x, x)U11(c, x) → x
a → ba → c

Original Signature

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

Strategy

Context-sensitive strategy:
μ(b) = μ(c) = μ(a) = μ(a#) = μ(T) = ∅
μ(f) = μ(g) = μ(f#) = μ(U11#) = μ(g#) = μ(U01) = μ(U11) = μ(U01#) = {1}

There are no SCCs!