YES
The TRS could be proven terminating. The proof took 1712 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (24ms).
| – Problem 2 was processed with processor ForwardNarrowing (8ms).
| | – Problem 3 was processed with processor ForwardNarrowing (5ms).
| | | – Problem 4 was processed with processor ForwardNarrowing (7ms).
| | | | – Problem 5 was processed with processor ForwardNarrowing (2ms).
| | | | | – Problem 6 was processed with processor ForwardNarrowing (3ms).
| | | | | | – Problem 7 was processed with processor ForwardNarrowing (4ms).
| | | | | | | – Problem 8 was processed with processor ForwardNarrowing (8ms).
| | | | | | | | – Problem 9 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | – Problem 10 was processed with processor ForwardNarrowing (37ms).
| | | | | | | | | | – Problem 11 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | – Problem 12 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | – Problem 13 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | – Problem 14 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | – Problem 15 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | – Problem 16 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | – Problem 17 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | – Problem 18 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | – Problem 19 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | – Problem 20 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | – Problem 21 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | | | | | | | – Problem 22 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | – Problem 23 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | – Problem 24 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | – Problem 25 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | – Problem 26 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 27 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 28 was processed with processor BackwardInstantiation (6ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 29 was processed with processor Propagation (2ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 30 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 31 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 32 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 33 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 34 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 35 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 36 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 37 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 38 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 39 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 40 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 41 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 42 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 43 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 44 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 45 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 46 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 47 was processed with processor ForwardNarrowing (0ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 48 was processed with processor ForwardNarrowing (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| A# | → | a# | | g#(d, e) | → | A# |
| f#(x) | → | U71#(x, x) | | U71#(d, x) | → | T(x) |
| A# | → | h#(f(a), f(b)) | | A# | → | f#(b) |
| A# | → | b# | | h#(x, x) | → | g#(x, x) |
| A# | → | f#(a) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The following SCCs where found
| g#(d, e) → A# | A# → h#(f(a), f(b)) |
| h#(x, x) → g#(x, x) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(f(a), f(b)) |
| h#(x, x) | → | g#(x, x) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(a), f(b)) is 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 |
|---|
| h#(f(a), U71(b, b)) | |
| h#(f(a), f(d)) | |
| h#(f(d), f(b)) | |
| h#(f(e), f(b)) | |
| h#(U71(a, a), f(b)) | |
| h#(f(a), f(e)) | |
Thus, the rule A
# → h
#(f(a), f(b)) is replaced by the following rules:
| A# → h#(f(a), U71(b, b)) | A# → h#(f(a), f(e)) |
| A# → h#(f(d), f(b)) | A# → h#(f(e), f(b)) |
| A# → h#(f(a), f(d)) | A# → h#(U71(a, a), f(b)) |
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(f(a), U71(b, b)) | | A# | → | h#(f(a), f(e)) |
| g#(d, e) | → | A# | | A# | → | h#(f(d), f(b)) |
| A# | → | h#(f(e), f(b)) | | A# | → | h#(f(a), f(d)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(U71(a, a), f(b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(a),
U71(b, b)) is 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 |
|---|
| h#(f(a), U71(d, b)) | h#(f(a), U71(e, b)) |
| h#(U71(a, a), U71(b, b)) | |
| h#(f(d), U71(b, b)) | |
| h#(f(e), U71(b, b)) | |
Thus, the rule A
# → h
#(f(a),
U71(b, b)) is replaced by the following rules:
| A# → h#(f(d), U71(b, b)) | A# → h#(f(e), U71(b, b)) |
| A# → h#(U71(a, a), U71(b, b)) | A# → h#(f(a), U71(d, b)) |
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(f(a), f(e)) | | A# | → | h#(f(d), U71(b, b)) |
| g#(d, e) | → | A# | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), f(b)) | | A# | → | h#(f(e), f(b)) |
| A# | → | h#(U71(a, a), U71(b, b)) | | A# | → | h#(f(a), f(d)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(a, a), f(b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(d),
U71(b, b)) is 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 |
|---|
| h#(f(d), U71(d, b)) | h#(f(d), U71(e, b)) |
| h#(U71(d, d), U71(b, b)) | |
Thus, the rule A
# → h
#(f(d),
U71(b, b)) is replaced by the following rules:
| A# → h#(f(d), U71(d, b)) | A# → h#(U71(d, d), U71(b, b)) |
Problem 5: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(f(a), f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| g#(d, e) | → | A# | | A# | → | h#(f(d), f(b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), f(b)) | | A# | → | h#(f(a), f(d)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(a), f(e)) is 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 |
|---|
| h#(f(e), f(e)) | h#(f(a), U71(e, e)) |
| h#(f(d), f(e)) | |
| h#(U71(a, a), f(e)) | |
Thus, the rule A
# → h
#(f(a), f(e)) is replaced by the following rules:
| A# → h#(U71(a, a), f(e)) | A# → h#(f(e), f(e)) |
| A# → h#(f(d), f(e)) |
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(U71(a, a), f(e)) |
| A# | → | h#(f(d), f(b)) | | A# | → | h#(f(e), f(b)) |
| A# | → | h#(f(a), f(d)) | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(d), f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(a, a), f(e)) is 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 |
|---|
| h#(U71(a, a), U71(e, e)) | h#(U71(e, a), f(e)) |
| h#(U71(d, a), f(e)) | |
Thus, the rule A
# → h
#(
U71(a, a), f(e)) is replaced by the following rules:
| A# → h#(U71(d, a), f(e)) | A# → h#(U71(a, a), U71(e, e)) |
Problem 7: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(U71(d, a), f(e)) |
| A# | → | h#(f(d), f(b)) | | A# | → | h#(f(e), f(b)) |
| A# | → | h#(f(a), f(d)) | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(d), f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(d, a), f(e)) is 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 |
|---|
| h#(a, f(e)) | h#(U71(d, a), U71(e, e)) |
Thus, the rule A
# → h
#(
U71(d, a), f(e)) is replaced by the following rules:
Problem 8: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(f(d), f(b)) |
| A# | → | h#(f(e), f(b)) | | A# | → | h#(f(a), f(d)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(d), f(e)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(d), f(b)) is 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 |
|---|
| h#(U71(d, d), f(b)) | |
| h#(f(d), f(e)) | |
| h#(f(d), U71(b, b)) | |
| h#(f(d), f(d)) | |
Thus, the rule A
# → h
#(f(d), f(b)) is replaced by the following rules:
| A# → h#(f(d), U71(b, b)) | A# → h#(U71(d, d), f(b)) |
| A# → h#(f(d), f(e)) | A# → h#(f(d), f(d)) |
Problem 9: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(f(d), U71(b, b)) | | g#(d, e) | → | A# |
| A# | → | h#(f(e), f(b)) | | A# | → | h#(f(a), f(d)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(d), f(e)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(d),
U71(b, b)) is 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 |
|---|
| h#(f(d), U71(d, b)) | h#(f(d), U71(e, b)) |
| h#(U71(d, d), U71(b, b)) | |
Thus, the rule A
# → h
#(f(d),
U71(b, b)) is replaced by the following rules:
| A# → h#(f(d), U71(d, b)) | A# → h#(U71(d, d), U71(b, b)) |
Problem 10: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(f(e), f(b)) |
| A# | → | h#(f(a), f(d)) | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(d), f(e)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(f(d), U71(d, b)) |
| A# | → | h#(U71(a, a), U71(b, b)) | | A# | → | h#(U71(a, a), U71(e, e)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(e), f(b)) is 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 |
|---|
| h#(f(e), f(d)) | h#(U71(e, e), f(b)) |
| h#(f(e), f(e)) | |
| h#(f(e), U71(b, b)) | |
Thus, the rule A
# → h
#(f(e), f(b)) is replaced by the following rules:
| A# → h#(f(e), U71(b, b)) | A# → h#(f(e), f(d)) |
| A# → h#(f(e), f(e)) |
Problem 11: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(f(a), f(d)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(d), f(e)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), f(d)) | | A# | → | h#(U71(a, a), U71(e, e)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(U71(d, d), f(b)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(a), f(d)) is 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 |
|---|
| h#(f(e), f(d)) | |
| h#(U71(a, a), f(d)) | |
| h#(f(d), f(d)) | |
| h#(f(a), U71(d, d)) | |
Thus, the rule A
# → h
#(f(a), f(d)) is replaced by the following rules:
| A# → h#(f(e), f(d)) | A# → h#(U71(a, a), f(d)) |
| A# → h#(f(d), f(d)) | A# → h#(f(a), U71(d, d)) |
Problem 12: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(d), f(e)) | | A# | → | h#(f(a), U71(d, d)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), f(d)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(d, d), f(b)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(d), f(e)) is 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 |
|---|
| h#(U71(d, d), f(e)) | h#(f(d), U71(e, e)) |
Thus, the rule A
# → h
#(f(d), f(e)) is replaced by the following rules:
Problem 13: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(U71(d, d), f(e)) | | A# | → | h#(f(a), U71(d, d)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), f(d)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(d, d), f(e)) is 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 |
|---|
| h#(U71(d, d), U71(e, e)) | |
| h#(d, f(e)) | |
Thus, the rule A
# → h
#(
U71(d, d), f(e)) is replaced by the following rules:
| A# → h#(U71(d, d), U71(e, e)) | A# → h#(d, f(e)) |
Problem 14: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(a), U71(d, d)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(f(d), U71(d, b)) |
| A# | → | h#(U71(a, a), U71(b, b)) | | A# | → | h#(f(e), f(d)) |
| A# | → | h#(U71(a, a), f(d)) | | A# | → | h#(U71(a, a), U71(e, e)) |
| A# | → | h#(U71(d, d), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(d, d), f(b)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(d, f(e)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(a),
U71(d, d)) is 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 |
|---|
| h#(f(d), U71(d, d)) | |
| h#(f(e), U71(d, d)) | |
| h#(U71(a, a), U71(d, d)) | |
| h#(f(a), d) | |
Thus, the rule A
# → h
#(f(a),
U71(d, d)) is replaced by the following rules:
| A# → h#(U71(a, a), U71(d, d)) | A# → h#(f(a), d) |
| A# → h#(f(e), U71(d, d)) | A# → h#(f(d), U71(d, d)) |
Problem 15: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(a), d) | | A# | → | h#(U71(a, a), U71(d, d)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), U71(d, d)) | | A# | → | h#(f(e), f(d)) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(U71(d, d), U71(e, e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(a), d) is 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 |
|---|
| h#(f(e), d) | |
| h#(U71(a, a), d) | |
| h#(f(d), d) | |
Thus, the rule A
# → h
#(f(a), d) is replaced by the following rules:
| A# → h#(f(e), d) | A# → h#(U71(a, a), d) |
| A# → h#(f(d), d) |
Problem 16: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(f(e), d) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(U71(a, a), d) |
| A# | → | h#(f(d), d) | | A# | → | h#(U71(a, a), U71(d, d)) |
| A# | → | h#(a, f(e)) | | A# | → | h#(f(e), U71(b, b)) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), U71(d, d)) | | A# | → | h#(f(e), f(d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(U71(d, d), U71(e, e)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(e), d) is 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 |
|---|
| | h#(U71(e, e), d) |
Thus, the rule A
# → h
#(f(e), d) is deleted.
Problem 17: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(U71(a, a), d) | | A# | → | h#(f(d), d) |
| A# | → | h#(U71(a, a), U71(d, d)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(f(d), U71(d, b)) |
| A# | → | h#(U71(a, a), U71(b, b)) | | A# | → | h#(f(e), U71(d, d)) |
| A# | → | h#(f(e), f(d)) | | A# | → | h#(f(d), U71(d, d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(U71(d, d), U71(e, e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(d, f(e)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(U71(d, d), f(b)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(a, a), d) is 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 |
|---|
| h#(U71(d, a), d) | h#(U71(e, a), d) |
Thus, the rule A
# → h
#(
U71(a, a), d) is replaced by the following rules:
Problem 18: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(U71(d, a), d) | | A# | → | h#(f(d), d) |
| A# | → | h#(U71(a, a), U71(d, d)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(f(d), U71(d, b)) |
| A# | → | h#(U71(a, a), U71(b, b)) | | A# | → | h#(f(e), U71(d, d)) |
| A# | → | h#(f(e), f(d)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(U71(a, a), U71(e, e)) |
| A# | → | h#(U71(d, d), U71(e, e)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(U71(d, d), f(b)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(d, f(e)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(d, a), d) is 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 |
|---|
| h#(a, d) | |
Thus, the rule A
# → h
#(
U71(d, a), d) is replaced by the following rules:
Problem 19: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(a, d) | | g#(d, e) | → | A# |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(d), d) |
| A# | → | h#(U71(a, a), U71(d, d)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(f(d), U71(d, b)) |
| A# | → | h#(U71(a, a), U71(b, b)) | | A# | → | h#(f(e), U71(d, d)) |
| A# | → | h#(f(e), f(d)) | | A# | → | h#(U71(a, a), U71(e, e)) |
| A# | → | h#(U71(a, a), f(d)) | | A# | → | h#(f(d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(U71(d, d), U71(e, e)) |
| A# | → | h#(f(a), U71(d, b)) | | A# | → | h#(d, f(e)) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(U71(d, d), f(b)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(a, d) is 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 |
|---|
| h#(e, d) | |
| h#(d, d) | |
Thus, the rule A
# → h
#(a, d) is replaced by the following rules:
| A# → h#(e, d) | A# → h#(d, d) |
Problem 20: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(d, d) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(d), d) |
| A# | → | h#(U71(a, a), U71(d, d)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(e, d) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), U71(d, d)) | | A# | → | h#(f(e), f(d)) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(U71(d, d), U71(e, e)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(d), d) is 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 |
|---|
| h#(U71(d, d), d) | |
Thus, the rule A
# → h
#(f(d), d) is replaced by the following rules:
Problem 21: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | A# | | A# | → | h#(d, d) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(U71(a, a), U71(d, d)) |
| A# | → | h#(U71(d, d), d) | | A# | → | h#(a, f(e)) |
| A# | → | h#(f(e), U71(b, b)) | | A# | → | h#(e, d) |
| A# | → | h#(f(d), U71(d, b)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(f(e), U71(d, d)) | | A# | → | h#(f(e), f(d)) |
| A# | → | h#(U71(a, a), U71(e, e)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(U71(d, d), U71(e, e)) | | A# | → | h#(f(a), U71(d, b)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(U71(d, d), f(b)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(a, a),
U71(d, d)) is 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 |
|---|
| h#(U71(e, a), U71(d, d)) | |
| h#(U71(a, a), d) | |
| h#(U71(d, a), U71(d, d)) | |
Thus, the rule A
# → h
#(
U71(a, a),
U71(d, d)) is replaced by the following rules:
| A# → h#(U71(d, a), U71(d, d)) | A# → h#(U71(a, a), d) |
| A# → h#(U71(e, a), U71(d, d)) |
Problem 22: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(d, d) | | A# | → | h#(U71(d, a), d) |
| A# | → | h#(U71(d, a), e) | | A# | → | h#(a, b) |
| A# | → | h#(e, e) | | g#(d, e) | → | A# |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(U71(a, a), U71(e, b)) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(U71(a, a), d) |
| A# | → | h#(U71(e, e), U71(d, b)) | | A# | → | h#(U71(e, a), U71(d, d)) |
| A# | → | h#(U71(a, a), U71(d, d)) | | A# | → | h#(d, b) |
| A# | → | h#(d, U71(d, b)) | | A# | → | h#(a, U71(d, d)) |
| A# | → | h#(d, f(b)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(U71(d, d), U71(d, b)) | | A# | → | h#(U71(d, a), f(d)) |
| A# | → | h#(e, d) | | A# | → | h#(U71(a, a), U71(d, b)) |
| A# | → | h#(f(e), U71(d, d)) | | A# | → | h#(f(d), b) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(a, U71(b, b)) |
| A# | → | h#(f(e), b) | | A# | → | h#(U71(d, d), U71(e, e)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), b) |
| A# | → | h#(a, e) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(d, a), d) is 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 |
|---|
| h#(a, d) | |
Thus, the rule A
# → h
#(
U71(d, a), d) is replaced by the following rules:
Problem 23: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(a, d) | | A# | → | h#(e, e) |
| g#(d, e) | → | A# | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(d, d) | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(a, f(d)) | | A# | → | h#(a, U71(d, d)) |
| A# | → | h#(e, d) | | A# | → | h#(U71(a, a), U71(d, b)) |
| A# | → | h#(f(e), U71(d, d)) | | A# | → | h#(a, U71(b, b)) |
| A# | → | h#(f(d), b) | | A# | → | h#(f(d), U71(d, d)) |
| A# | → | h#(f(e), b) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(U71(d, d), U71(e, e)) | | A# | → | h#(f(a), b) |
| A# | → | h#(U71(a, a), f(b)) | | A# | → | h#(d, f(e)) |
| A# | → | h#(a, e) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(a, d) is 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 |
|---|
| h#(e, d) | |
| h#(d, d) | |
Thus, the rule A
# → h
#(a, d) is replaced by the following rules:
| A# → h#(e, d) | A# → h#(d, d) |
Problem 24: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(e, e) | | g#(d, e) | → | A# |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(d, d) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(d, U71(d, b)) |
| A# | → | h#(f(d), U71(d, d)) | | A# | → | h#(f(e), b) |
| A# | → | h#(e, U71(d, b)) | | A# | → | h#(U71(d, d), U71(e, e)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(a), b) |
| A# | → | h#(d, f(e)) | | A# | → | h#(U71(a, a), f(b)) |
| A# | → | h#(a, e) | | A# | → | h#(e, f(d)) |
| A# | → | h#(f(d), f(d)) | | A# | → | h#(U71(d, d), U71(b, b)) |
| A# | → | h#(U71(d, d), e) | | A# | → | h#(a, U71(d, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(d,
U71(d, b)) is 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 |
|---|
| h#(d, b) | |
Thus, the rule A
# → h
#(d,
U71(d, b)) is replaced by the following rules:
Problem 25: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(U71(d, a), b) | | A# | → | h#(e, e) |
| g#(d, e) | → | A# | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(d, d) | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(a, f(b)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(U71(d, a), f(d)) | | A# | → | h#(U71(a, a), U71(b, b)) |
| A# | → | h#(a, U71(b, b)) | | A# | → | h#(U71(a, a), f(d)) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(a, e) |
| A# | → | h#(a, b) | | A# | → | h#(e, f(d)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) | | A# | → | h#(U71(d, d), e) |
| A# | → | h#(a, U71(d, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(
U71(d, a), b) is 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 |
|---|
| h#(U71(d, a), d) | |
| h#(U71(d, a), e) | |
| h#(a, b) | |
Thus, the rule A
# → h
#(
U71(d, a), b) is replaced by the following rules:
| A# → h#(U71(d, a), e) | A# → h#(a, b) |
| A# → h#(U71(d, a), d) |
Problem 26: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(e, e) | | g#(d, e) | → | A# |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(d, d) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(d, b) |
| A# | → | h#(a, U71(d, d)) | | A# | → | h#(a, f(e)) |
| A# | → | h#(d, f(b)) | | A# | → | h#(e, d) |
| A# | → | h#(U71(d, a), f(d)) | | A# | → | h#(U71(a, a), U71(d, b)) |
| A# | → | h#(a, U71(b, b)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(d, f(e)) | | A# | → | h#(a, e) |
| A# | → | h#(e, f(d)) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(d, b) is 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 |
|---|
| h#(d, e) | |
| h#(d, d) | |
Thus, the rule A
# → h
#(d, b) is replaced by the following rules:
| A# → h#(d, e) | A# → h#(d, d) |
Problem 27: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(e, e) | | A# | → | h#(e, U71(d, d)) |
| g#(d, e) | → | A# | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(d, d) | | h#(x, x) | → | g#(x, x) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(d, f(e)) |
| A# | → | h#(a, b) | | A# | → | h#(f(d), f(d)) |
| A# | → | h#(U71(d, d), U71(b, b)) | | A# | → | h#(a, U71(d, b)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(e,
U71(d, d)) is 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 |
|---|
| h#(e, d) | |
Thus, the rule A
# → h
#(e,
U71(d, d)) is replaced by the following rules:
Problem 28: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(e, e) | | g#(d, e) | → | A# |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(d, d) |
| h#(x, x) | → | g#(x, x) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule h
#(
x,
x) → g
#(
x,
x) on dependency pair chains it holds that:
- h#(x, x) matches r,
- all variables of h#(x, x) are embedded in constructor contexts, i.e., each subterm of h#(x, x), containing a variable is rooted by a constructor symbol.
Thus, h
#(
x,
x) → g
#(
x,
x) is replaced by instances determined through the above matching. These instances are:
| h#(f(d), f(d)) → g#(f(d), f(d)) | h#(d, d) → g#(d, d) |
| h#(e, e) → g#(e, e) | h#(f(e), f(e)) → g#(f(e), f(e)) |
| h#(U71(d, d), U71(d, d)) → g#(U71(d, d), U71(d, d)) |
Problem 29: Propagation
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(e, e) | | h#(f(d), f(d)) | → | g#(f(d), f(d)) |
| g#(d, e) | → | A# | | h#(d, d) | → | g#(d, d) |
| h#(e, e) | → | g#(e, e) | | h#(f(e), f(e)) | → | g#(f(e), f(e)) |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(d, d) |
| A# | → | h#(f(e), f(e)) | | A# | → | h#(f(d), f(d)) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The dependency pairs A
# → h
#(e, e) and h
#(e, e) → g
#(e, e) are consolidated into the rule A
# → g
#(e, e) .
This is possible as
- all subterms of h#(e, e) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in h#(e, e), but non-replacing in both A# and g#(e, e)
The dependency pairs g
#(d, e) → A
# and A
# → h
#(e, e) are consolidated into the rule g
#(d, e) → h
#(e, e) .
This is possible as
- all subterms of A# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in A#, but non-replacing in both g#(d, e) and h#(e, e)
The dependency pairs g
#(d, e) → A
# and A
# → h
#(e, e) are consolidated into the rule g
#(d, e) → h
#(e, e) .
This is possible as
- all subterms of A# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in A#, but non-replacing in both g#(d, e) and h#(e, e)
The dependency pairs g
#(d, e) → A
# and A
# → h
#(e, e) are consolidated into the rule g
#(d, e) → h
#(e, e) .
This is possible as
- all subterms of A# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in A#, but non-replacing in both g#(d, e) and h#(e, e)
The dependency pairs g
#(d, e) → A
# and A
# → h
#(e, e) are consolidated into the rule g
#(d, e) → h
#(e, e) .
This is possible as
- all subterms of A# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in A#, but non-replacing in both g#(d, e) and h#(e, e)
The dependency pairs g
#(d, e) → A
# and A
# → h
#(e, e) are consolidated into the rule g
#(d, e) → h
#(e, e) .
This is possible as
- all subterms of A# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in A#, but non-replacing in both g#(d, e) and h#(e, e)
The dependency pairs g
#(d, e) → A
# and A
# → h
#(e, e) are consolidated into the rule g
#(d, e) → h
#(e, e) .
This is possible as
- all subterms of A# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in A#, but non-replacing in both g#(d, e) and h#(e, e)
The dependency pairs A
# → h
#(d, d) and h
#(d, d) → g
#(d, d) are consolidated into the rule A
# → g
#(d, d) .
This is possible as
- all subterms of h#(d, d) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in h#(d, d), but non-replacing in both A# and g#(d, d)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| A# → h#(e, e) | g#(d, e) → h#(e, e) |
| h#(d, d) → g#(d, d) | A# → g#(e, e) |
| g#(d, e) → A# | A# → g#(d, d) |
| h#(e, e) → g#(e, e) | |
| A# → h#(d, d) | |
Problem 30: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(d, e) | → | h#(e, e) | | h#(f(d), f(d)) | → | g#(f(d), f(d)) |
| h#(f(e), f(e)) | → | g#(f(e), f(e)) | | A# | → | g#(e, e) |
| A# | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule g
#(d, e) → h
#(e, e) is 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 |
|---|
Thus, the rule g
#(d, e) → h
#(e, e) is deleted.
Problem 31: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(f(d), f(d)) | | A# | → | g#(e, e) |
| h#(f(e), f(e)) | → | g#(f(e), f(e)) | | A# | → | g#(d, d) |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(f(e), f(e)) |
| A# | → | h#(f(d), f(d)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(f(d), f(d)) is 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 |
|---|
| g#(U71(d, d), f(d)) | |
| g#(f(d), U71(d, d)) | |
Thus, the rule h
#(f(d), f(d)) → g
#(f(d), f(d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(f(d), U71(d, d)) | h#(f(d), f(d)) → g#(U71(d, d), f(d)) |
Problem 32: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(f(d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(U71(d, d), f(d)) |
| h#(f(e), f(e)) | → | g#(f(e), f(e)) | | A# | → | g#(e, e) |
| A# | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(f(d),
U71(d, d)) is 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 |
|---|
| g#(U71(d, d), U71(d, d)) | |
| g#(f(d), d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(f(d),
U71(d, d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(U71(d, d), U71(d, d)) | h#(f(d), f(d)) → g#(f(d), d) |
Problem 33: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(U71(d, d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(U71(d, d), f(d)) |
| A# | → | g#(e, e) | | h#(f(e), f(e)) | → | g#(f(e), f(e)) |
| A# | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| A# | → | h#(f(d), f(d)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(
U71(d, d),
U71(d, d)) is 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 |
|---|
| g#(U71(d, d), d) | |
| g#(d, U71(d, d)) | |
Thus, the rule h
#(f(d), f(d)) → g
#(
U71(d, d),
U71(d, d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(U71(d, d), d) | h#(f(d), f(d)) → g#(d, U71(d, d)) |
Problem 34: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(U71(d, d), d) | | h#(f(d), f(d)) | → | g#(U71(d, d), f(d)) |
| h#(f(d), f(d)) | → | g#(d, U71(d, d)) | | h#(f(e), f(e)) | → | g#(f(e), f(e)) |
| A# | → | g#(e, e) | | A# | → | g#(d, d) |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(
U71(d, d), d) is 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 |
|---|
| g#(d, d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(
U71(d, d), d) is replaced by the following rules:
| h#(f(d), f(d)) → g#(d, d) |
Problem 35: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(d, U71(d, d)) | | h#(f(d), f(d)) | → | g#(U71(d, d), f(d)) |
| A# | → | g#(e, e) | | h#(f(e), f(e)) | → | g#(f(e), f(e)) |
| A# | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| h#(f(d), f(d)) | → | g#(d, d) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | A# | → | h#(f(d), f(d)) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(
U71(d, d), f(d)) is 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 |
|---|
| g#(U71(d, d), U71(d, d)) | |
| g#(d, f(d)) | |
Thus, the rule h
#(f(d), f(d)) → g
#(
U71(d, d), f(d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(U71(d, d), U71(d, d)) | h#(f(d), f(d)) → g#(d, f(d)) |
Problem 36: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(U71(d, d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(d, U71(d, d)) |
| h#(f(e), f(e)) | → | g#(f(e), f(e)) | | A# | → | g#(e, e) |
| h#(f(d), f(d)) | → | g#(d, f(d)) | | A# | → | g#(d, d) |
| h#(f(d), f(d)) | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) | | A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(
U71(d, d),
U71(d, d)) is 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 |
|---|
| g#(U71(d, d), d) | |
| g#(d, U71(d, d)) | |
Thus, the rule h
#(f(d), f(d)) → g
#(
U71(d, d),
U71(d, d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(U71(d, d), d) | h#(f(d), f(d)) → g#(d, U71(d, d)) |
Problem 37: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(U71(d, d), d) | | h#(f(d), f(d)) | → | g#(d, U71(d, d)) |
| h#(f(d), f(d)) | → | g#(d, f(d)) | | A# | → | g#(e, e) |
| h#(f(e), f(e)) | → | g#(f(e), f(e)) | | A# | → | g#(d, d) |
| A# | → | h#(U71(d, d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(d, d) |
| A# | → | h#(f(e), f(e)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| A# | → | h#(f(d), f(d)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(
U71(d, d), d) is 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 |
|---|
| g#(d, d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(
U71(d, d), d) is replaced by the following rules:
| h#(f(d), f(d)) → g#(d, d) |
Problem 38: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(d, U71(d, d)) | | h#(f(e), f(e)) | → | g#(f(e), f(e)) |
| A# | → | g#(e, e) | | h#(f(d), f(d)) | → | g#(d, f(d)) |
| A# | → | g#(d, d) | | h#(f(d), f(d)) | → | g#(d, d) |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(d,
U71(d, d)) is 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 |
|---|
| g#(d, d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(d,
U71(d, d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(d, d) |
Problem 39: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(d, f(d)) | | A# | → | g#(e, e) |
| h#(f(e), f(e)) | → | g#(f(e), f(e)) | | A# | → | g#(d, d) |
| A# | → | h#(U71(d, d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(d, d) |
| A# | → | h#(f(e), f(e)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| A# | → | h#(f(d), f(d)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(e), f(e)) → g
#(f(e), f(e)) is 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 |
|---|
| | g#(U71(e, e), f(e)) |
| | g#(f(e), U71(e, e)) |
Thus, the rule h
#(f(e), f(e)) → g
#(f(e), f(e)) is deleted.
Problem 40: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | g#(e, e) | | h#(f(d), f(d)) | → | g#(d, f(d)) |
| A# | → | g#(d, d) | | h#(f(d), f(d)) | → | g#(d, d) |
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(d, f(d)) is 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 |
|---|
| g#(d, U71(d, d)) | |
Thus, the rule h
#(f(d), f(d)) → g
#(d, f(d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(d, U71(d, d)) |
Problem 41: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(d, U71(d, d)) | | A# | → | g#(e, e) |
| A# | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| h#(f(d), f(d)) | → | g#(d, d) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | A# | → | h#(f(d), f(d)) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(d,
U71(d, d)) is 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 |
|---|
| g#(d, d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(d,
U71(d, d)) is replaced by the following rules:
| h#(f(d), f(d)) → g#(d, d) |
Problem 42: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | g#(e, e) | | A# | → | g#(d, d) |
| h#(f(d), f(d)) | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) | | A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → g
#(e, e) is 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 |
|---|
Thus, the rule A
# → g
#(e, e) is deleted.
Problem 43: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| h#(f(d), f(d)) | → | g#(d, d) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | A# | → | h#(f(d), f(d)) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → g
#(d, d) is 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 |
|---|
Thus, the rule A
# → g
#(d, d) is deleted.
Problem 44: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(d, d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(e), f(e)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) | | A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(d, d) is 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 |
|---|
Thus, the rule h
#(f(d), f(d)) → g
#(d, d) is deleted.
Problem 45: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(U71(d, d), U71(d, d)) | | A# | → | h#(f(e), f(e)) |
| h#(f(d), f(d)) | → | g#(f(d), d) | | A# | → | h#(f(d), f(d)) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule A
# → h
#(f(e), f(e)) is 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 |
|---|
| | h#(f(e), U71(e, e)) |
| | h#(U71(e, e), f(e)) |
Thus, the rule A
# → h
#(f(e), f(e)) is deleted.
Problem 46: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(U71(d, d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(f(d), d) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) | | A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(f(d), d) is 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 |
|---|
| g#(U71(d, d), d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(f(d), d) is replaced by the following rules:
| h#(f(d), f(d)) → g#(U71(d, d), d) |
Problem 47: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| h#(f(d), f(d)) | → | g#(U71(d, d), d) | | A# | → | h#(U71(d, d), U71(d, d)) |
| A# | → | h#(f(d), f(d)) | | h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(
U71(d, d), d) is 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 |
|---|
| g#(d, d) | |
Thus, the rule h
#(f(d), f(d)) → g
#(
U71(d, d), d) is replaced by the following rules:
| h#(f(d), f(d)) → g#(d, d) |
Problem 48: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| A# | → | h#(U71(d, d), U71(d, d)) | | h#(f(d), f(d)) | → | g#(d, d) |
| h#(U71(d, d), U71(d, d)) | → | g#(U71(d, d), U71(d, d)) | | A# | → | h#(f(d), f(d)) |
Rewrite Rules
| a | → | d | | b | → | d |
| a | → | e | | b | → | e |
| A | → | h(f(a), f(b)) | | h(x, x) | → | g(x, x) |
| g(d, e) | → | A | | f(x) | → | U71(x, x) |
| U71(d, x) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, e, b, A, a, h
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(A) = μ(a) = μ(a#) = μ(T) = μ(A#) = μ(b#) = ∅
μ(f) = μ(f#) = μ(U71) = μ(U71#) = {1}
μ(g) = μ(h#) = μ(g#) = μ(h) = {1, 2}
The right-hand side of the rule h
#(f(d), f(d)) → g
#(d, d) is 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 |
|---|
Thus, the rule h
#(f(d), f(d)) → g
#(d, d) is deleted.