TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60001 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (28ms).
| – Problem 2 was processed with processor ForwardNarrowing (1ms).
| | – Problem 4 was processed with processor ForwardNarrowing (1ms).
| | | – Problem 6 was processed with processor ForwardNarrowing (2ms).
| | | | – Problem 8 was processed with processor ForwardNarrowing (2ms).
| | | | | – Problem 10 was processed with processor ForwardNarrowing (3ms).
| | | | | | – Problem 12 was processed with processor ForwardNarrowing (4ms).
| | | | | | | – Problem 14 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | – Problem 16 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | – Problem 19 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | – Problem 20 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | – Problem 23 was processed with processor ForwardNarrowing (6ms).
| | | | | | | | | | | | – Problem 24 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | – Problem 27 was processed with processor ForwardNarrowing (5ms).
| | | | | | | | | | | | | | – Problem 28 was processed with processor ForwardNarrowing (6ms).
| | | | | | | | | | | | | | | – Problem 31 was processed with processor ForwardNarrowing (8ms).
| | | | | | | | | | | | | | | | – Problem 32 was processed with processor ForwardNarrowing (6ms).
| | | | | | | | | | | | | | | | | – Problem 34 was processed with processor ForwardNarrowing (6ms).
| | | | | | | | | | | | | | | | | | – Problem 36 was processed with processor ForwardNarrowing (8ms).
| | | | | | | | | | | | | | | | | | | – Problem 38 was processed with processor ForwardNarrowing (7ms).
| | | | | | | | | | | | | | | | | | | | – Problem 40 was processed with processor ForwardNarrowing (7ms).
| | | | | | | | | | | | | | | | | | | | | – Problem 42 was processed with processor ForwardNarrowing (62ms).
| | | | | | | | | | | | | | | | | | | | | | – Problem 44 was processed with processor ForwardNarrowing (78ms).
| | | | | | | | | | | | | | | | | | | | | | | – Problem 46 was processed with processor ForwardNarrowing (156ms).
| | | | | | | | | | | | | | | | | | | | | | | | – Problem 48 was processed with processor ForwardNarrowing (264ms).
| | | | | | | | | | | | | | | | | | | | | | | | | – Problem 51 remains open; application of the following processors failed [ForwardNarrowing (303ms), ForwardNarrowing (268ms), ForwardNarrowing (268ms), ForwardNarrowing (272ms), ForwardNarrowing (278ms), ForwardNarrowing (312ms), ForwardNarrowing (284ms), ForwardNarrowing (288ms), ForwardNarrowing (315ms), ForwardNarrowing (285ms), ForwardNarrowing (289ms), ForwardNarrowing (331ms), ForwardNarrowing (301ms), ForwardNarrowing (303ms), ForwardNarrowing (305ms)].
| – Problem 3 was processed with processor ForwardNarrowing (1ms).
| | – Problem 5 was processed with processor ForwardNarrowing (4ms).
| | | – Problem 7 was processed with processor ForwardNarrowing (0ms).
| | | | – Problem 9 was processed with processor ForwardNarrowing (1ms).
| | | | | – Problem 11 was processed with processor ForwardNarrowing (1ms).
| | | | | | – Problem 13 was processed with processor ForwardNarrowing (3ms).
| | | | | | | – Problem 15 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | – Problem 17 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | – Problem 18 was processed with processor ForwardNarrowing (9ms).
| | | | | | | | | | – Problem 21 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | – Problem 22 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | – Problem 25 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | – Problem 26 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | – Problem 29 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | – Problem 30 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | | – Problem 33 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | | | | | – Problem 35 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | | | | – Problem 37 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | | | | | – Problem 39 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | | | | | | | | | | | – Problem 41 was processed with processor ForwardNarrowing (5ms).
| | | | | | | | | | | | | | | | | | | | | – Problem 43 was processed with processor ForwardNarrowing (27ms).
| | | | | | | | | | | | | | | | | | | | | | – Problem 45 was processed with processor ForwardNarrowing (68ms).
| | | | | | | | | | | | | | | | | | | | | | | – Problem 47 was processed with processor ForwardNarrowing (143ms).
| | | | | | | | | | | | | | | | | | | | | | | | – Problem 49 was processed with processor ForwardNarrowing (242ms).
| | | | | | | | | | | | | | | | | | | | | | | | | – Problem 50 remains open; application of the following processors failed [ForwardNarrowing (245ms), ForwardNarrowing (249ms), ForwardNarrowing (288ms), ForwardNarrowing (255ms), ForwardNarrowing (278ms), ForwardNarrowing (259ms), ForwardNarrowing (278ms), ForwardNarrowing (260ms), ForwardNarrowing (268ms), ForwardNarrowing (269ms), ForwardNarrowing (267ms), ForwardNarrowing (269ms), ForwardNarrowing (273ms), ForwardNarrowing (307ms), ForwardNarrowing (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, f(b, f(b, x))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Open Dependency Pair Problem 3
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, x)) | → | f#(a, f(a, f(a, x))) |
| f#(a, f(b, x)) | → | f#(a, f(a, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, f(b, f(b, x))) | | f#(a, f(b, x)) | → | f#(a, f(a, f(a, x))) |
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, x)) | → | f#(a, f(a, x)) |
| f#(b, f(a, x)) | → | f#(b, x) | | f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The following SCCs where found
| f#(a, f(b, x)) → f#(a, f(a, f(a, x))) | f#(a, f(b, x)) → f#(a, x) |
| f#(a, f(b, x)) → f#(a, f(a, x)) |
| f#(b, f(a, x)) → f#(b, f(b, f(b, x))) | f#(b, f(a, x)) → f#(b, x) |
| f#(b, f(a, x)) → f#(b, f(b, x)) |
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, f(b, f(b, x))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a,
x)) → f
#(b, f(b, f(b,
x))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, _x51))))) | |
Thus, the rule f
#(b, f(a,
x)) → f
#(b, f(b, f(b,
x))) is replaced by the following rules:
| f#(b, f(a, f(a, _x51))) → f#(b, f(b, f(b, f(b, f(b, _x51))))) |
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, _x51))) | → | f#(b, f(b, f(b, f(b, f(b, _x51))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a,
_x51))) → f
#(b, f(b, f(b, f(b, f(b,
_x51))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, _x101))))))) | |
Thus, the rule f
#(b, f(a, f(a,
_x51))) → f
#(b, f(b, f(b, f(b, f(b,
_x51))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, _x101)))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, _x101))))))) |
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, _x101)))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, _x101))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a,
_x101)))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x101))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x131))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a,
_x101)))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x101))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, _x131))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x131))))))))) |
Problem 8: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, _x131))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x131))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a,
_x131))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x131))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x181))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a,
_x131))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x131))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, _x181)))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x181))))))))))) |
Problem 10: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, _x181)))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x181))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a,
_x181)))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x181))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x211))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a,
_x181)))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x181))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, _x211))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x211))))))))))))) |
Problem 12: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, _x211))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x211))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a,
_x211))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x211))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x261))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a,
_x211))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x211))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x261)))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x261))))))))))))))) |
Problem 14: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x261)))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x261))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x261)))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x261))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x291))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x261)))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x261))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x291))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x291))))))))))))))))) |
Problem 16: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x291))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x291))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x291))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x291))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x291))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x291))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341)))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341))))))))))))))))))) |
Problem 19: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341)))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x341)))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x341))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x391))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x341)))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x341))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x391))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x391))))))))))))))))))))) |
Problem 20: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x391))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x391))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x391))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x391))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x421))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x391))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x391))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x421)))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x421))))))))))))))))))))))) |
Problem 23: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, x) | | f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x421)))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x421))))))))))))))))))))))) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x421)))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x421))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x451))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x421)))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x421))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x451))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x451))))))))))))))))))))))))) |
Problem 24: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x451))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x451))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x451))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x451))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x501))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x451))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x451))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x501)))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x501))))))))))))))))))))))))))) |
Problem 27: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, x) | | f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x501)))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x501))))))))))))))))))))))))))) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x501)))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x501))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x551))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x501)))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x501))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x551))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x551))))))))))))))))))))))))))))) |
Problem 28: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x551))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x551))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x551))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x551))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x581))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x551))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x551))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x581)))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x581))))))))))))))))))))))))))))))) |
Problem 31: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x581)))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x581))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x581)))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x581))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x631))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x581)))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x581))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x631))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x631))))))))))))))))))))))))))))))))) |
Problem 32: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, x) | | f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x631))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x631))))))))))))))))))))))))))))))))) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x631))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x631))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x661))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x631))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x631))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x661)))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x661))))))))))))))))))))))))))))))))))) |
Problem 34: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x661)))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x661))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x661)))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x661))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x691))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x661)))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x661))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x691))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x691))))))))))))))))))))))))))))))))))))) |
Problem 36: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x691))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x691))))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x691))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x691))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x741))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x691))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x691))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x741)))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x741))))))))))))))))))))))))))))))))))))))) |
Problem 38: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x741)))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x741))))))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x741)))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x741))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x791))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x741)))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x741))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x791))))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x791))))))))))))))))))))))))))))))))))))))))) |
Problem 40: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x791))))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x791))))))))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x791))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x791))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x821))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x791))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x791))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x821)))))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x821))))))))))))))))))))))))))))))))))))))))))) |
Problem 42: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x2021)))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x2021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x2021)))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x2021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x2051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x2021)))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x2021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x2051))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x2051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 44: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x4021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x4021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x4021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x4021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x4051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x4021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x4021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x4051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x4051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 46: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, x)) | → | f#(b, x) | | f#(b, f(a, x)) | → | f#(b, f(b, x)) |
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x6021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x6021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x6021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x6021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x6051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x6021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x6021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x6051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x6051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 48: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x8021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x8021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | | f#(b, f(a, x)) | → | f#(b, x) |
| f#(b, f(a, x)) | → | f#(b, f(b, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x8021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x8021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x8051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x8021)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x8021))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(b, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x8051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x8051))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, f(a, f(a, x))) | | f#(a, f(b, x)) | → | f#(a, x) |
| f#(a, f(b, x)) | → | f#(a, f(a, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b,
x)) → f
#(a, f(a, f(a,
x))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, _x51))))) | |
Thus, the rule f
#(a, f(b,
x)) → f
#(a, f(a, f(a,
x))) is replaced by the following rules:
| f#(a, f(b, f(b, _x51))) → f#(a, f(a, f(a, f(a, f(a, _x51))))) |
Problem 5: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, f(b, _x51))) | → | f#(a, f(a, f(a, f(a, f(a, _x51))))) | | f#(a, f(b, x)) | → | f#(a, x) |
| f#(a, f(b, x)) | → | f#(a, f(a, x)) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b,
_x51))) → f
#(a, f(a, f(a, f(a, f(a,
_x51))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, _x101))))))) | |
Thus, the rule f
#(a, f(b, f(b,
_x51))) → f
#(a, f(a, f(a, f(a, f(a,
_x51))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, _x101)))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, _x101))))))) |
Problem 7: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, x)) | → | f#(a, f(a, x)) |
| f#(a, f(b, f(b, f(b, _x101)))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, _x101))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b,
x)) → f
#(a, f(a,
x)) 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 |
|---|
| f#(a, f(a, f(a, f(a, _x31)))) | |
Thus, the rule f
#(a, f(b,
x)) → f
#(a, f(a,
x)) is replaced by the following rules:
| f#(a, f(b, f(b, _x31))) → f#(a, f(a, f(a, f(a, _x31)))) |
Problem 9: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, _x101)))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, _x101))))))) |
| f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b,
_x101)))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x101))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x131))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b,
_x101)))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x101))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, _x131))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x131))))))))) |
Problem 11: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, _x131))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x131))))))))) |
| f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b,
_x131))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x131))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x181))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b,
_x131))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x131))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, _x181)))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x181))))))))))) |
Problem 13: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, _x181)))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x181))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b,
_x181)))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x181))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x211))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b,
_x181)))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x181))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, _x211))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x211))))))))))))) |
Problem 15: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, _x211))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x211))))))))))))) |
| f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b,
_x211))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x211))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x261))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b,
_x211))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x211))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x261)))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x261))))))))))))))) |
Problem 17: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x261)))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x261))))))))))))))) |
| f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x261)))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x261))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x291))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x261)))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x261))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x291))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x291))))))))))))))))) |
Problem 18: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x291))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x291))))))))))))))))) | | f#(a, f(b, x)) | → | f#(a, x) |
| f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x291))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x291))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x291))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x291))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Problem 21: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, _x31))) | → | f#(a, f(a, f(a, f(a, _x31)))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b,
_x31))) → f
#(a, f(a, f(a, f(a,
_x31)))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, _x81)))))) | |
Thus, the rule f
#(a, f(b, f(b,
_x31))) → f
#(a, f(a, f(a, f(a,
_x31)))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, _x81)))) → f#(a, f(a, f(a, f(a, f(a, f(a, _x81)))))) |
Problem 22: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, _x81)))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, _x81)))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b,
_x81)))) → f
#(a, f(a, f(a, f(a, f(a, f(a,
_x81)))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x111)))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b,
_x81)))) → f
#(a, f(a, f(a, f(a, f(a, f(a,
_x81)))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, _x111))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x111)))))))) |
Problem 25: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, f(b, f(b, f(b, _x111))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x111)))))))) | | f#(a, f(b, x)) | → | f#(a, x) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b,
_x111))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x111)))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x161)))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b,
_x111))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x111)))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, _x161)))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x161)))))))))) |
Problem 26: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, _x161)))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x161)))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b,
_x161)))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x161)))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x191)))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b,
_x161)))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x161)))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, _x191))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x191)))))))))))) |
Problem 29: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, _x191))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x191)))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b,
_x191))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x191)))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x241)))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b,
_x191))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x191)))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x241)))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x241)))))))))))))) |
Problem 30: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x241)))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x241)))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x241)))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x241)))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x271)))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x241)))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x241)))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x271))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x271)))))))))))))))) |
Problem 33: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x271))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x271)))))))))))))))) | | f#(a, f(b, x)) | → | f#(a, x) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x271))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x271)))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x321)))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x271))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x271)))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x321)))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x321)))))))))))))))))) |
Problem 35: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x321)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x321)))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x321)))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x321)))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x371)))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x321)))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x321)))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x371))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x371)))))))))))))))))))) |
Problem 37: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x371))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x371)))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x371))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x371)))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x401)))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x371))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x371)))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x401)))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x401)))))))))))))))))))))) |
Problem 39: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x401)))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x401)))))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x401)))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x401)))))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x431)))))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x401)))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x401)))))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x431))))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x431)))))))))))))))))))))))) |
Problem 41: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x431))))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x431)))))))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x431))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x431)))))))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x481)))))))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x431))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x431)))))))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x481)))))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x481)))))))))))))))))))))))))) |
Problem 43: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x1681)))))))))))))))))))))))))))))))))))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x1681)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x1681)))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x1681)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x1711)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x1681)))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x1681)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x1711))))))))))))))))))))))))))))))))))))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x1711)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 45: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x3701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x3701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x3701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x3701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x3731)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x3701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x3701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x3731))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x3731)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 47: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x5701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x5701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x5701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x5701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x5731)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x5701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x5701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x5731))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x5731)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
Problem 49: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f#(a, f(b, x)) | → | f#(a, x) | | f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x7701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x7701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x341)))))))))) | → | f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x341))))))))))))))))))) |
Rewrite Rules
| f(a, f(b, x)) | → | f(a, f(a, f(a, x))) | | f(b, f(a, x)) | → | f(b, f(b, f(b, x))) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
The right-hand side of the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x7701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x7701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 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 |
|---|
| f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x7731)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | |
Thus, the rule f
#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b,
_x7701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f
#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a,
_x7701)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) is replaced by the following rules:
| f#(a, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, f(b, _x7731))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → f#(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, f(a, _x7731)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |