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 Terms | Irrelevant 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 Terms | Irrelevant 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 Terms | Irrelevant 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 Terms | Irrelevant 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.