YES
The TRS could be proven terminating. The proof took 37 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (16ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| max#(g(g(g(x, y), z), u)) | → | max#(g(g(x, y), z)) | | mem#(g(x, y), z) | → | mem#(x, z) |
| f#(x, g(y, z)) | → | f#(x, y) | | ++#(x, g(y, z)) | → | ++#(x, y) |
| mem#(x, max(x)) | → | null#(x) |
Rewrite Rules
| f(x, nil) | → | g(nil, x) | | f(x, g(y, z)) | → | g(f(x, y), z) |
| ++(x, nil) | → | x | | ++(x, g(y, z)) | → | g(++(x, y), z) |
| null(nil) | → | true | | null(g(x, y)) | → | false |
| mem(nil, y) | → | false | | mem(g(x, y), z) | → | or(=(y, z), mem(x, z)) |
| mem(x, max(x)) | → | not(null(x)) | | max(g(g(nil, x), y)) | → | max'(x, y) |
| max(g(g(g(x, y), z), u)) | → | max'(max(g(g(x, y), z)), u) |
Original Signature
Termination of terms over the following signature is verified: f, g, max, or, true, not, u, mem, false, ++, null, =, max', nil
Strategy
The following SCCs where found
| max#(g(g(g(x, y), z), u)) → max#(g(g(x, y), z)) |
| mem#(g(x, y), z) → mem#(x, z) |
| f#(x, g(y, z)) → f#(x, y) |
| ++#(x, g(y, z)) → ++#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ++#(x, g(y, z)) | → | ++#(x, y) |
Rewrite Rules
| f(x, nil) | → | g(nil, x) | | f(x, g(y, z)) | → | g(f(x, y), z) |
| ++(x, nil) | → | x | | ++(x, g(y, z)) | → | g(++(x, y), z) |
| null(nil) | → | true | | null(g(x, y)) | → | false |
| mem(nil, y) | → | false | | mem(g(x, y), z) | → | or(=(y, z), mem(x, z)) |
| mem(x, max(x)) | → | not(null(x)) | | max(g(g(nil, x), y)) | → | max'(x, y) |
| max(g(g(g(x, y), z), u)) | → | max'(max(g(g(x, y), z)), u) |
Original Signature
Termination of terms over the following signature is verified: f, g, max, or, true, not, u, mem, false, ++, null, =, max', nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ++#(x, g(y, z)) | → | ++#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| max#(g(g(g(x, y), z), u)) | → | max#(g(g(x, y), z)) |
Rewrite Rules
| f(x, nil) | → | g(nil, x) | | f(x, g(y, z)) | → | g(f(x, y), z) |
| ++(x, nil) | → | x | | ++(x, g(y, z)) | → | g(++(x, y), z) |
| null(nil) | → | true | | null(g(x, y)) | → | false |
| mem(nil, y) | → | false | | mem(g(x, y), z) | → | or(=(y, z), mem(x, z)) |
| mem(x, max(x)) | → | not(null(x)) | | max(g(g(nil, x), y)) | → | max'(x, y) |
| max(g(g(g(x, y), z), u)) | → | max'(max(g(g(x, y), z)), u) |
Original Signature
Termination of terms over the following signature is verified: f, g, max, or, true, not, u, mem, false, ++, null, =, max', nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| max#(g(g(g(x, y), z), u)) | → | max#(g(g(x, y), z)) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| mem#(g(x, y), z) | → | mem#(x, z) |
Rewrite Rules
| f(x, nil) | → | g(nil, x) | | f(x, g(y, z)) | → | g(f(x, y), z) |
| ++(x, nil) | → | x | | ++(x, g(y, z)) | → | g(++(x, y), z) |
| null(nil) | → | true | | null(g(x, y)) | → | false |
| mem(nil, y) | → | false | | mem(g(x, y), z) | → | or(=(y, z), mem(x, z)) |
| mem(x, max(x)) | → | not(null(x)) | | max(g(g(nil, x), y)) | → | max'(x, y) |
| max(g(g(g(x, y), z), u)) | → | max'(max(g(g(x, y), z)), u) |
Original Signature
Termination of terms over the following signature is verified: f, g, max, or, true, not, u, mem, false, ++, null, =, max', nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| mem#(g(x, y), z) | → | mem#(x, z) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| f#(x, g(y, z)) | → | f#(x, y) |
Rewrite Rules
| f(x, nil) | → | g(nil, x) | | f(x, g(y, z)) | → | g(f(x, y), z) |
| ++(x, nil) | → | x | | ++(x, g(y, z)) | → | g(++(x, y), z) |
| null(nil) | → | true | | null(g(x, y)) | → | false |
| mem(nil, y) | → | false | | mem(g(x, y), z) | → | or(=(y, z), mem(x, z)) |
| mem(x, max(x)) | → | not(null(x)) | | max(g(g(nil, x), y)) | → | max'(x, y) |
| max(g(g(g(x, y), z), u)) | → | max'(max(g(g(x, y), z)), u) |
Original Signature
Termination of terms over the following signature is verified: f, g, max, or, true, not, u, mem, false, ++, null, =, max', nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| f#(x, g(y, z)) | → | f#(x, y) |