NO
The TRS could be proven non-terminating. The proof took 52080 ms.
The following reduction sequence is a witness for non-termination:
hamming# →* hamming#
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1156ms).
| – Problem 2 was processed with processor ForwardInstantiation (10ms).
| | – Problem 4 was processed with processor ForwardNarrowing (1ms).
| | | – Problem 5 was processed with processor ForwardNarrowing (2ms).
| | | | – Problem 6 was processed with processor ForwardNarrowing (14ms).
| | | | | – Problem 9 was processed with processor ForwardNarrowing (6ms).
| | | | | | – Problem 10 was processed with processor ForwardNarrowing (2ms).
| | | | | | | – Problem 11 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | – Problem 12 was processed with processor ForwardNarrowing (5ms).
| | | | | | | | | – Problem 14 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | – Problem 16 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | – Problem 17 was processed with processor ForwardInstantiation (21ms).
| | | | | | | | | | | | – Problem 18 remains open; application of the following processors failed [Propagation (5ms), ForwardNarrowing (3ms), BackwardInstantiation (7ms), ForwardInstantiation (5ms), Propagation (3ms), ForwardNarrowing (3ms), ForwardNarrowing (3ms), ForwardNarrowing (2ms), BackwardInstantiation (8ms), ForwardInstantiation (11ms), Propagation (3ms)].
| | – Problem 7 remains open; application of the following processors failed [Propagation (7ms), BackwardsNarrowing (9ms), BackwardsNarrowing (5ms), BackwardsNarrowing (4ms), BackwardInstantiation (5ms), ForwardInstantiation (10ms), Propagation (4ms), BackwardsNarrowing (2ms), BackwardInstantiation (5ms), ForwardInstantiation (24ms), Propagation (3ms)].
| – Problem 3 was processed with processor Propagation (5ms).
| | – Problem 8 was processed with processor BackwardsNarrowing (1ms).
| | | – Problem 13 was processed with processor BackwardsNarrowing (0ms).
| | | | – Problem 15 remains open; application of the following processors failed [BackwardsNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms), BackwardsNarrowing (0ms), BackwardInstantiation (2ms), ForwardInstantiation (18ms), Propagation (1ms)].
| | – Problem 19 was processed with processor Propagation (2ms).
| | | – Problem 20 was processed with processor ForwardNarrowing (0ms).
| | | | – Problem 21 was processed with processor ForwardNarrowing (0ms).
| | | | | – Problem 22 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (0ms), ForwardInstantiation (0ms), Propagation (0ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | list2# | → | app#(map, app(mult, app(s, app(s, app(s, 0))))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(lt, x) |
| hamming# | → | app#(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) | | hamming# | → | app#(merge, list1) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | hamming# | → | app#(cons, app(s, 0)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(if, app(app(eq, x), y)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(map, f) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(cons, y) | | list3# | → | app#(s, app(s, app(s, 0))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) |
| list1# | → | hamming# | | app#(app(mult, app(s, x)), y) | → | app#(plus, y) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) |
| list2# | → | hamming# | | list1# | → | app#(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list1# | → | app#(s, app(s, 0)) | | list2# | → | app#(s, 0) |
| list1# | → | app#(map, app(mult, app(s, app(s, 0)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) |
| app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(cons, app(f, x)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) | | list3# | → | app#(s, 0) |
| list3# | → | app#(s, app(s, app(s, app(s, 0)))) | | hamming# | → | list2# |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(eq, x) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) | | list1# | → | app#(mult, app(s, app(s, 0))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), xs) | | app#(app(lt, app(s, x)), app(s, y)) | → | app#(lt, x) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(merge, xs) | | hamming# | → | app#(app(merge, list2), list3) |
| list3# | → | app#(mult, app(s, app(s, app(s, app(s, app(s, 0)))))) | | hamming# | → | app#(s, 0) |
| list3# | → | app#(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) | | hamming# | → | app#(app(merge, list1), app(app(merge, list2), list3)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(if, app(app(lt, x), y)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| hamming# | → | list1# | | app#(app(plus, app(s, x)), y) | → | app#(s, app(app(plus, x), y)) |
| hamming# | → | app#(merge, list2) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(cons, x) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) | | list1# | → | app#(s, 0) |
| hamming# | → | list3# | | list2# | → | app#(s, app(s, 0)) |
| list2# | → | app#(s, app(s, app(s, 0))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), ys)) |
| app#(app(plus, app(s, x)), y) | → | app#(plus, x) | | list2# | → | app#(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) |
| list2# | → | app#(mult, app(s, app(s, app(s, 0)))) | | app#(app(mult, app(s, x)), y) | → | app#(mult, x) |
| list3# | → | app#(s, app(s, app(s, app(s, app(s, 0))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(merge, app(app(cons, x), xs)) | | list3# | → | app#(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))) |
| list3# | → | app#(s, app(s, 0)) | | list3# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The following SCCs where found
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(lt, x), y) |
| app#(app(map, f), app(app(cons, x), xs)) → app#(f, x) | app#(app(map, f), app(app(cons, x), xs)) → app#(app(cons, app(f, x)), app(app(map, f), xs)) |
| app#(app(mult, app(s, x)), y) → app#(app(mult, x), y) | app#(app(mult, app(s, x)), y) → app#(app(plus, y), app(app(mult, x), y)) |
| app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(cons, x), app(app(merge, xs), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(merge, xs), app(app(cons, y), ys)) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(merge, app(app(cons, x), xs)), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(cons, x), xs) | app#(app(map, f), app(app(cons, x), xs)) → app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(cons, y), ys) |
| app#(app(plus, app(s, x)), y) → app#(app(plus, x), y) | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app#(app(eq, x), y) |
| hamming# → list2# | list2# → hamming# |
| hamming# → list1# | list1# → hamming# |
| hamming# → list3# | list3# → hamming# |
Problem 2: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), xs) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) |
| app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
Instantiation
For all potential successors l → r of the rule app
#(app(map,
f), app(app(cons,
x),
xs)) → app
#(
f,
x) on dependency pair chains it holds that:
- app#(f, x) matches l,
- all variables of app#(f, x) are embedded in constructor contexts, i.e., each subterm of app#(f, x) containing a variable is rooted by a constructor symbol.
Thus, app
#(app(map,
f), app(app(cons,
x),
xs)) → app
#(
f,
x) is replaced by instances determined through the above matching. These instances are:
| app#(app(map, app(plus, app(s, _x))), app(app(cons, x), xs)) → app#(app(plus, app(s, _x)), x) | app#(app(map, app(lt, app(s, _x))), app(app(cons, app(s, _y)), xs)) → app#(app(lt, app(s, _x)), app(s, _y)) |
| app#(app(map, app(mult, app(s, _x))), app(app(cons, x), xs)) → app#(app(mult, app(s, _x)), x) | app#(app(map, app(map, _f)), app(app(cons, app(app(cons, _x), _xs)), xs)) → app#(app(map, _f), app(app(cons, _x), _xs)) |
| app#(app(map, app(merge, app(app(cons, _x), _xs))), app(app(cons, app(app(cons, _y), _ys)), xs)) → app#(app(merge, app(app(cons, _x), _xs)), app(app(cons, _y), _ys)) |
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), xs) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | | app#(app(merge, app(app(cons, x), _x31)), app(app(cons, y), nil)) | → | app#(app(cons, x), _x31) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | | app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) | | app#(app(merge, app(app(cons, x), nil)), app(app(cons, y), _x31)) | → | app#(app(cons, x), _x31) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) |
| app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
x),
xs) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
x),
xs) is deleted.
Problem 5: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), _x31)), app(app(cons, y), nil)) | → | app#(app(cons, x), _x31) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) |
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), nil)), app(app(cons, y), _x31)) | → | app#(app(cons, x), _x31) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) | | app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
_x31)), app(app(cons,
y), nil)) → app
#(app(cons,
x),
_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 |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x),
_x31)), app(app(cons,
y), nil)) → app
#(app(cons,
x),
_x31) is deleted.
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | | app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) | | app#(app(merge, app(app(cons, x), nil)), app(app(cons, y), _x31)) | → | app#(app(cons, x), _x31) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) |
| app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x), nil)), app(app(cons,
y),
_x31)) → app
#(app(cons,
x),
_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 |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x), nil)), app(app(cons,
y),
_x31)) → app
#(app(cons,
x),
_x31) is deleted.
Problem 9: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | | app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) | | app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
y), app(app(merge, app(app(cons,
x),
xs)),
ys)) 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 |
|---|
| app#(app(cons, y), app(app(cons, x), xs)) | |
| app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | |
Thus, the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
y), app(app(merge, app(app(cons,
x),
xs)),
ys)) is replaced by the following rules:
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), nil)) → app#(app(cons, y), app(app(cons, x), xs)) | app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) → app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
Problem 10: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), nil)) | → | app#(app(cons, y), app(app(cons, x), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) | | app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) |
| app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) | | app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) |
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) | | app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) |
| app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y), nil)) → app
#(app(cons,
y), app(app(cons,
x),
xs)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y), nil)) → app
#(app(cons,
y), app(app(cons,
x),
xs)) is deleted.
Problem 11: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | | app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, y), ys) |
| app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
y),
ys) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
y),
ys) is deleted.
Problem 12: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) |
| app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) | | app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) |
| app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) | | app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))) | | app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) |
| app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
x), app(app(merge,
xs), app(app(cons,
y),
ys))) 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 |
|---|
| app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | |
| app#(app(cons, x), app(app(cons, y), ys)) | |
Thus, the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(cons,
x), app(app(merge,
xs), app(app(cons,
y),
ys))) is replaced by the following rules:
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, _x33), _x31)) → app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | app#(app(merge, app(app(cons, x), nil)), app(app(cons, y), ys)) → app#(app(cons, x), app(app(cons, y), ys)) |
Problem 14: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, _x33), _x31)) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) | | app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) |
| app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) | | app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) |
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) | | app#(app(merge, app(app(cons, x), nil)), app(app(cons, y), ys)) | → | app#(app(cons, x), app(app(cons, y), ys)) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x), nil)), app(app(cons,
y),
ys)) → app
#(app(cons,
x), app(app(cons,
y),
ys)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x), nil)), app(app(cons,
y),
ys)) → app
#(app(cons,
x), app(app(cons,
y),
ys)) is deleted.
Problem 16: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, _x33), _x31)) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) | | app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) |
| app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) | | app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) |
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) |
| app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(eq, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The right-hand side of the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(eq,
x),
y) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule app
#(app(merge, app(app(cons,
x),
xs)), app(app(cons,
y),
ys)) → app
#(app(eq,
x),
y) is deleted.
Problem 17: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, _x33), _x31)) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))) | | app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(cons, app(f, x)), app(app(map, f), xs)) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(f, x) | | app#(app(mult, app(s, x)), y) | → | app#(app(plus, y), app(app(mult, x), y)) |
| app#(app(mult, app(s, x)), y) | → | app#(app(mult, x), y) | | app#(app(lt, app(s, x)), app(s, y)) | → | app#(app(lt, x), y) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), app(app(cons, y), ys)) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, app(app(cons, x), xs)), ys) |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))) |
| app#(app(merge, app(app(cons, x), app(app(cons, _x34), _x32))), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, x), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(merge, xs), ys) |
| app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))) | | app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) | → | app#(app(cons, y), app(app(app(if, app(app(lt, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), app(app(cons, _x33), _x31)))), app(app(app(if, app(app(eq, _x34), _x33)), app(app(cons, _x34), app(app(merge, _x32), _x31))), app(app(cons, _x33), app(app(merge, app(app(cons, _x34), _x32)), _x31))))) |
| app#(app(plus, app(s, x)), y) | → | app#(app(plus, x), y) | | app#(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app#(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
Instantiation
For all potential successors l → r of the rule app
#(app(map,
f), app(app(cons,
x),
xs)) → app
#(
f,
x) on dependency pair chains it holds that:
- app#(f, x) matches l,
- all variables of app#(f, x) are embedded in constructor contexts, i.e., each subterm of app#(f, x) containing a variable is rooted by a constructor symbol.
Thus, app
#(app(map,
f), app(app(cons,
x),
xs)) → app
#(
f,
x) is replaced by instances determined through the above matching. These instances are:
| app#(app(map, app(merge, app(app(cons, _x), app(app(cons, __x34), __x32)))), app(app(cons, app(app(cons, _y), app(app(cons, __x33), __x31))), xs)) → app#(app(merge, app(app(cons, _x), app(app(cons, __x34), __x32))), app(app(cons, _y), app(app(cons, __x33), __x31))) | app#(app(map, app(plus, app(s, _x))), app(app(cons, x), xs)) → app#(app(plus, app(s, _x)), x) |
| app#(app(map, app(lt, app(s, _x))), app(app(cons, app(s, _y)), xs)) → app#(app(lt, app(s, _x)), app(s, _y)) | app#(app(map, app(merge, app(app(cons, _x), app(app(cons, __x34), __x32)))), app(app(cons, app(app(cons, __x33), __x31)), xs)) → app#(app(merge, app(app(cons, _x), app(app(cons, __x34), __x32))), app(app(cons, __x33), __x31)) |
| app#(app(map, app(mult, app(s, _x))), app(app(cons, x), xs)) → app#(app(mult, app(s, _x)), x) | app#(app(map, app(map, _f)), app(app(cons, app(app(cons, _x), _xs)), xs)) → app#(app(map, _f), app(app(cons, _x), _xs)) |
| app#(app(map, app(merge, app(app(cons, _x), _xs))), app(app(cons, app(app(cons, _y), _ys)), xs)) → app#(app(merge, app(app(cons, _x), _xs)), app(app(cons, _y), _ys)) | app#(app(map, app(merge, app(app(cons, _x34), _x32))), app(app(cons, app(app(cons, y), app(app(cons, _x33), _x31))), xs)) → app#(app(merge, app(app(cons, _x34), _x32)), app(app(cons, y), app(app(cons, _x33), _x31))) |
Problem 3: Propagation
Dependency Pair Problem
Dependency Pairs
| hamming# | → | list2# | | list2# | → | hamming# |
| hamming# | → | list1# | | list1# | → | hamming# |
| hamming# | → | list3# | | list3# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The dependency pairs hamming
# → list2
# and list2
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list2
# and list2
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list2
# and list2
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list2
# and list2
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list2
# and list2
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list2
# and list2
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both hamming# and hamming#
The dependency pairs list2
# → hamming
# and hamming
# → list2
# are consolidated into the rule list2
# → list2
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both list2# and list2#
The dependency pairs list2
# → hamming
# and hamming
# → list2
# are consolidated into the rule list2
# → list2
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both list2# and list2#
The dependency pairs hamming
# → list1
# and list1
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list1#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list1
# and list1
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list1#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list1
# and list1
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list1#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list1
# and list1
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list1#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list1
# and list1
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list1#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list1
# and list1
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list1#, but non-replacing in both hamming# and hamming#
The dependency pairs list1
# → hamming
# and hamming
# → list2
# are consolidated into the rule list1
# → list2
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both list1# and list2#
The dependency pairs hamming
# → list3
# and list3
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list3# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list3#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list3
# and list3
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list3# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list3#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list3
# and list3
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list3# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list3#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list3
# and list3
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list3# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list3#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list3
# and list3
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list3# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list3#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → list3
# and list3
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of list3# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list3#, but non-replacing in both hamming# and hamming#
The dependency pairs list3
# → hamming
# and hamming
# → list2
# are consolidated into the rule list3
# → list2
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both list3# and list2#
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| hamming# → list2# | list3# → list2# |
| list2# → hamming# | list2# → list2# |
| hamming# → list1# | list1# → list2# |
| list1# → hamming# | hamming# → hamming# |
| hamming# → list3# | |
| list3# → hamming# | |
Problem 8: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| list3# | → | list2# | | list2# | → | list2# |
| list1# | → | list2# | | hamming# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The left-hand side of the rule list3
# → list2
# is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule list3
# → list2
# is deleted.
Problem 13: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| list2# | → | list2# | | list1# | → | list2# |
| hamming# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The left-hand side of the rule list1
# → list2
# is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule list1
# → list2
# is deleted.
Problem 19: Propagation
Dependency Pair Problem
Dependency Pairs
| list3# | → | list2# | | list2# | → | list2# |
| list1# | → | list2# | | hamming# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The dependency pairs list3
# → list2
# and list2
# → list2
# are consolidated into the rule list3
# → list2
# .
This is possible as
- all subterms of list2# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in list2#, but non-replacing in both list3# and list2#
The dependency pairs hamming
# → hamming
# and hamming
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → hamming
# and hamming
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → hamming
# and hamming
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both hamming# and hamming#
The dependency pairs hamming
# → hamming
# and hamming
# → hamming
# are consolidated into the rule hamming
# → hamming
# .
This is possible as
- all subterms of hamming# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in hamming#, but non-replacing in both hamming# and hamming#
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| list3# → list2# | list3# → list2# |
| list2# → list2# | hamming# → hamming# |
| hamming# → hamming# | |
Problem 20: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| list3# | → | list2# | | list1# | → | list2# |
| hamming# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, cons, nil, eq
Strategy
The right-hand side of the rule list3
# → list2
# is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule list3
# → list2
# is deleted.
Problem 21: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| list1# | → | list2# | | hamming# | → | hamming# |
Rewrite Rules
| app(app(app(if, true), xs), ys) | → | xs | | app(app(app(if, false), xs), ys) | → | ys |
| app(app(lt, app(s, x)), app(s, y)) | → | app(app(lt, x), y) | | app(app(lt, 0), app(s, y)) | → | true |
| app(app(lt, y), 0) | → | false | | app(app(eq, x), x) | → | true |
| app(app(eq, app(s, x)), 0) | → | false | | app(app(eq, 0), app(s, x)) | → | false |
| app(app(merge, xs), nil) | → | xs | | app(app(merge, nil), ys) | → | ys |
| app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) | → | app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))) | | app(app(map, f), nil) | → | nil |
| app(app(map, f), app(app(cons, x), xs)) | → | app(app(cons, app(f, x)), app(app(map, f), xs)) | | app(app(mult, 0), x) | → | 0 |
| app(app(mult, app(s, x)), y) | → | app(app(plus, y), app(app(mult, x), y)) | | app(app(plus, 0), x) | → | 0 |
| app(app(plus, app(s, x)), y) | → | app(s, app(app(plus, x), y)) | | list1 | → | app(app(map, app(mult, app(s, app(s, 0)))), hamming) |
| list2 | → | app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming) | | list3 | → | app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming) |
| hamming | → | app(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3))) |
Original Signature
Termination of terms over the following signature is verified: plus, app, mult, merge, true, lt, list2, list3, 0, s, list1, if, map, false, hamming, eq, nil, cons
Strategy
The right-hand side of the rule list1
# → list2
# is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule list1
# → list2
# is deleted.