YES
The TRS could be proven terminating. The proof took 1033 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (102ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (345ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (257ms).
| | | – Problem 6 was processed with processor DependencyGraph (36ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (63ms).
| | | | | – Problem 8 was processed with processor DependencyGraph (0ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, h) | | reach#(x, y, edge(u, v, i), h) | → | eq#(x, u) |
| if_reach_1#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, edge(u, v, h)) | | if_reach_1#(true, x, y, edge(u, v, i), h) | → | if_reach_2#(eq(y, v), x, y, edge(u, v, i), h) |
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | union#(i, h) | | eq#(s(x), s(y)) | → | eq#(x, y) |
| if_reach_1#(true, x, y, edge(u, v, i), h) | → | eq#(y, v) | | if_reach_2#(false, x, y, edge(u, v, i), h) | → | or#(reach(x, y, i, h), reach(v, y, union(i, h), empty)) |
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(v, y, union(i, h), empty) | | reach#(x, y, edge(u, v, i), h) | → | if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
| union#(edge(x, y, i), h) | → | union#(i, h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, 0, edge, s, or, union, empty, true, false, if_reach_2, if_reach_1, eq
Strategy
The following SCCs where found
| eq#(s(x), s(y)) → eq#(x, y) |
| if_reach_2#(false, x, y, edge(u, v, i), h) → reach#(x, y, i, h) | if_reach_1#(false, x, y, edge(u, v, i), h) → reach#(x, y, i, edge(u, v, h)) |
| if_reach_1#(true, x, y, edge(u, v, i), h) → if_reach_2#(eq(y, v), x, y, edge(u, v, i), h) | if_reach_2#(false, x, y, edge(u, v, i), h) → reach#(v, y, union(i, h), empty) |
| reach#(x, y, edge(u, v, i), h) → if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
| union#(edge(x, y, i), h) → union#(i, h) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, h) | | if_reach_1#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, edge(u, v, h)) |
| if_reach_1#(true, x, y, edge(u, v, i), h) | → | if_reach_2#(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(v, y, union(i, h), empty) |
| reach#(x, y, edge(u, v, i), h) | → | if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, 0, edge, s, or, union, empty, true, false, if_reach_2, if_reach_1, eq
Strategy
Polynomial Interpretation
- 0: 1
- edge(x,y,z): z + y + 2x + 2
- empty: 1
- eq(x,y): y + x
- false: 0
- if_reach_1(x1,x2,x3,x4,x5): 0
- if_reach_1#(x1,x2,x3,x4,x5): x5 + x4
- if_reach_2(x1,x2,x3,x4,x5): 0
- if_reach_2#(x1,x2,x3,x4,x5): x5 + x4
- or(x,y): 0
- reach(x1,x2,x3,x4): 0
- reach#(x1,x2,x3,x4): x4 + x3
- s(x): x + 1
- true: 0
- union(x,y): y + x + 1
Improved Usable rules
| union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) | | union(empty, h) | → | h |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, h) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if_reach_1#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, edge(u, v, h)) | | if_reach_1#(true, x, y, edge(u, v, i), h) | → | if_reach_2#(eq(y, v), x, y, edge(u, v, i), h) |
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(v, y, union(i, h), empty) | | reach#(x, y, edge(u, v, i), h) | → | if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, edge, 0, s, or, union, empty, if_reach_2, false, true, if_reach_1, eq
Strategy
Polynomial Interpretation
- 0: 2
- edge(x,y,z): z + 2
- empty: 0
- eq(x,y): y
- false: 0
- if_reach_1(x1,x2,x3,x4,x5): 0
- if_reach_1#(x1,x2,x3,x4,x5): x5 + x4
- if_reach_2(x1,x2,x3,x4,x5): 0
- if_reach_2#(x1,x2,x3,x4,x5): x5 + x4
- or(x,y): 0
- reach(x1,x2,x3,x4): 0
- reach#(x1,x2,x3,x4): x4 + x3
- s(x): 3x + 2
- true: 0
- union(x,y): y + x
Improved Usable rules
| union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) | | union(empty, h) | → | h |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if_reach_2#(false, x, y, edge(u, v, i), h) | → | reach#(v, y, union(i, h), empty) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if_reach_1#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, edge(u, v, h)) | | if_reach_1#(true, x, y, edge(u, v, i), h) | → | if_reach_2#(eq(y, v), x, y, edge(u, v, i), h) |
| reach#(x, y, edge(u, v, i), h) | → | if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, 0, edge, s, or, union, empty, true, false, if_reach_2, if_reach_1, eq
Strategy
The following SCCs where found
| if_reach_1#(false, x, y, edge(u, v, i), h) → reach#(x, y, i, edge(u, v, h)) | reach#(x, y, edge(u, v, i), h) → if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if_reach_1#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, edge(u, v, h)) | | reach#(x, y, edge(u, v, i), h) | → | if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, 0, edge, s, or, union, empty, true, false, if_reach_2, if_reach_1, eq
Strategy
Polynomial Interpretation
- 0: 1
- edge(x,y,z): z + 2
- empty: 0
- eq(x,y): 2y + 1
- false: 0
- if_reach_1(x1,x2,x3,x4,x5): 0
- if_reach_1#(x1,x2,x3,x4,x5): x4
- if_reach_2(x1,x2,x3,x4,x5): 0
- or(x,y): 0
- reach(x1,x2,x3,x4): 0
- reach#(x1,x2,x3,x4): x3
- s(x): 1
- true: 2
- union(x,y): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if_reach_1#(false, x, y, edge(u, v, i), h) | → | reach#(x, y, i, edge(u, v, h)) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| reach#(x, y, edge(u, v, i), h) | → | if_reach_1#(eq(x, u), x, y, edge(u, v, i), h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, edge, 0, s, or, union, empty, if_reach_2, false, true, if_reach_1, eq
Strategy
There are no SCCs!
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| union#(edge(x, y, i), h) | → | union#(i, h) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, 0, edge, s, or, union, empty, true, false, if_reach_2, if_reach_1, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| union#(edge(x, y, i), h) | → | union#(i, h) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(x), s(y)) | → | eq#(x, y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| or(true, y) | → | true | | or(false, y) | → | y |
| union(empty, h) | → | h | | union(edge(x, y, i), h) | → | edge(x, y, union(i, h)) |
| reach(x, y, empty, h) | → | false | | reach(x, y, edge(u, v, i), h) | → | if_reach_1(eq(x, u), x, y, edge(u, v, i), h) |
| if_reach_1(true, x, y, edge(u, v, i), h) | → | if_reach_2(eq(y, v), x, y, edge(u, v, i), h) | | if_reach_2(true, x, y, edge(u, v, i), h) | → | true |
| if_reach_2(false, x, y, edge(u, v, i), h) | → | or(reach(x, y, i, h), reach(v, y, union(i, h), empty)) | | if_reach_1(false, x, y, edge(u, v, i), h) | → | reach(x, y, i, edge(u, v, h)) |
Original Signature
Termination of terms over the following signature is verified: reach, 0, edge, s, or, union, empty, true, false, if_reach_2, if_reach_1, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(x), s(y)) | → | eq#(x, y) |