YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor BackwardsNarrowing (9ms).
 |    | – Problem 3 was processed with processor BackwardsNarrowing (6ms).
 |    |    | – Problem 4 was processed with processor BackwardsNarrowing (8ms).
 |    |    |    | – Problem 5 was processed with processor BackwardsNarrowing (6ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

U31#(d, x)T(x)g#(x)h#(x)
U31#(d, x)h#(x)f#(k(a), k(b), x)f#(x, x, x)
g#(x)U31#(h(x), x)U31#(d, x)U32#(h(x), x)

Rewrite Rules

h(d)c(a)h(d)c(b)
f(k(a), k(b), x)f(x, x, x)g(x)U31(h(x), x)
U31(d, x)U32(h(x), x)U32(c(y), x)k(y)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(d) = μ(b) = μ(a) = μ(T) = ∅
μ(g) = μ(U31#) = μ(c) = μ(h#) = μ(g#) = μ(k) = μ(h) = μ(U32#) = μ(U31) = μ(U32) = {1}
μ(f) = μ(f#) = {1, 2, 3}


The following SCCs where found

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

Problem 2: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

h(d)c(a)h(d)c(b)
f(k(a), k(b), x)f(x, x, x)g(x)U31(h(x), x)
U31(d, x)U32(h(x), x)U32(c(y), x)k(y)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(d) = μ(b) = μ(a) = μ(T) = ∅
μ(g) = μ(U31#) = μ(c) = μ(h#) = μ(g#) = μ(k) = μ(h) = μ(U32#) = μ(U31) = μ(U32) = {1}
μ(f) = μ(f#) = {1, 2, 3}


The left-hand side of the rule f#(k(a), k(b), x) → f#(x, x, x) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
f#(U32(c(a), _x22), k(b), x) 
f#(k(a), U32(c(b), _x32), x) 
Thus, the rule f#(k(a), k(b), x) → f#(x, x, x) is replaced by the following rules:
f#(k(a), U32(c(b), _x32), x) → f#(x, x, x)f#(U32(c(a), _x22), k(b), x) → f#(x, x, x)

Problem 3: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

f#(k(a), U32(c(b), _x32), x)f#(x, x, x)f#(U32(c(a), _x22), k(b), x)f#(x, x, x)

Rewrite Rules

h(d)c(a)h(d)c(b)
f(k(a), k(b), x)f(x, x, x)g(x)U31(h(x), x)
U31(d, x)U32(h(x), x)U32(c(y), x)k(y)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(d) = μ(b) = μ(a) = μ(T) = ∅
μ(g) = μ(U31#) = μ(c) = μ(h#) = μ(g#) = μ(k) = μ(h) = μ(U32#) = μ(U31) = μ(U32) = {1}
μ(f) = μ(f#) = {1, 2, 3}


The left-hand side of the rule f#(k(a), U32(c(b), _x32), x) → f#(x, x, x) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
f#(U32(c(a), _x22), U32(c(b), _x32), x)f#(k(a), U32(h(d), _x32), x)
Thus, the rule f#(k(a), U32(c(b), _x32), x) → f#(x, x, x) is replaced by the following rules:
f#(U32(c(a), _x22), U32(c(b), _x32), x) → f#(x, x, x)

Problem 4: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

f#(U32(c(a), _x22), k(b), x)f#(x, x, x)f#(U32(c(a), _x22), U32(c(b), _x32), x)f#(x, x, x)

Rewrite Rules

h(d)c(a)h(d)c(b)
f(k(a), k(b), x)f(x, x, x)g(x)U31(h(x), x)
U31(d, x)U32(h(x), x)U32(c(y), x)k(y)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(d) = μ(b) = μ(a) = μ(T) = ∅
μ(g) = μ(U31#) = μ(c) = μ(h#) = μ(g#) = μ(k) = μ(h) = μ(U32#) = μ(U31) = μ(U32) = {1}
μ(f) = μ(f#) = {1, 2, 3}


The left-hand side of the rule f#(U32(c(a), _x22), k(b), x) → f#(x, x, x) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
f#(U32(c(a), _x22), U32(c(b), _x32), x)f#(U32(h(d), _x22), k(b), x)
Thus, the rule f#(U32(c(a), _x22), k(b), x) → f#(x, x, x) is replaced by the following rules:
f#(U32(c(a), _x22), U32(c(b), _x32), x) → f#(x, x, x)

Problem 5: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

f#(U32(c(a), _x22), U32(c(b), _x32), x)f#(x, x, x)

Rewrite Rules

h(d)c(a)h(d)c(b)
f(k(a), k(b), x)f(x, x, x)g(x)U31(h(x), x)
U31(d, x)U32(h(x), x)U32(c(y), x)k(y)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(d) = μ(b) = μ(a) = μ(T) = ∅
μ(g) = μ(U31#) = μ(c) = μ(h#) = μ(g#) = μ(k) = μ(h) = μ(U32#) = μ(U31) = μ(U32) = {1}
μ(f) = μ(f#) = {1, 2, 3}


The left-hand side of the rule f#(U32(c(a), _x22), U32(c(b), _x32), x) → f#(x, x, x) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
 f#(U32(h(d), _x22), U32(c(b), _x32), x)
 f#(U32(c(a), _x22), U32(h(d), _x32), x)
Thus, the rule f#(U32(c(a), _x22), U32(c(b), _x32), x) → f#(x, x, x) is deleted.