YES
The TRS could be proven terminating. The proof took 6181 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (429ms).
| – Problem 2 was processed with processor SubtermCriterion (50ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (1406ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (1176ms).
| | | – Problem 6 was processed with processor DependencyGraph (58ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (1359ms).
| | | | | – Problem 8 was processed with processor DependencyGraph (9ms).
| | | | | | – Problem 9 was processed with processor PolynomialLinearRange4iUR (331ms).
| | | | | | | – Problem 11 was processed with processor PolynomialLinearRange4iUR (372ms).
| | | | | | | | – Problem 12 was processed with processor PolynomialLinearRange4iUR (347ms).
| | | | | | | | | – Problem 13 was processed with processor PolynomialLinearRange4iUR (16ms).
| | | | | | | | | | – Problem 14 was processed with processor PolynomialLinearRange4iUR (13ms).
| | | | | | – Problem 10 was processed with processor PolynomialLinearRange4iUR (311ms).
| – Problem 4 was processed with processor SubtermCriterion (32ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Case(m, xi, n), s) | → | Frozen#(m, Sum_sub(xi, s), n, s) |
| Frozen#(m, Sum_constant(Right), n, s) | → | Term_sub#(n, s) | | Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) |
| Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(m, s) | | Sum_sub#(xi, Cons_usual(y, m, s)) | → | Sum_sub#(xi, s) |
| Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(n, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) |
| Concat#(Cons_sum(xi, k, s), t) | → | Concat#(s, t) | | Term_sub#(Case(m, xi, n), s) | → | Sum_sub#(xi, s) |
| Concat#(Cons_usual(x, m, s), t) | → | Term_sub#(m, t) | | Term_sub#(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub#(Term_var(x), s) |
| Term_sub#(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub#(Term_var(x), s) | | Concat#(Concat(s, t), u) | → | Concat#(t, u) |
| Sum_sub#(xi, Cons_sum(psi, k, s)) | → | Sum_sub#(xi, s) | | Frozen#(m, Sum_constant(Left), n, s) | → | Term_sub#(m, s) |
| Concat#(Cons_usual(x, m, s), t) | → | Concat#(s, t) | | Term_sub#(Term_sub(m, s), t) | → | Concat#(s, t) |
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
The following SCCs where found
| Term_sub#(Term_var(x), Cons_usual(y, m, s)) → Term_sub#(Term_var(x), s) | Term_sub#(Term_var(x), Cons_sum(xi, k, s)) → Term_sub#(Term_var(x), s) |
| Term_sub#(Term_app(m, n), s) → Term_sub#(m, s) | Term_sub#(Term_inl(m), s) → Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) → Term_sub#(m, s) | Term_sub#(Case(m, xi, n), s) → Frozen#(m, Sum_sub(xi, s), n, s) |
| Frozen#(m, Sum_constant(Right), n, s) → Term_sub#(n, s) | Term_sub#(Term_inr(m), s) → Term_sub#(m, s) |
| Term_sub#(Term_sub(m, s), t) → Term_sub#(m, Concat(s, t)) | Concat#(Concat(s, t), u) → Concat#(s, Concat(t, u)) |
| Frozen#(m, Sum_term_var(xi), n, s) → Term_sub#(m, s) | Term_sub#(Term_pair(m, n), s) → Term_sub#(n, s) |
| Frozen#(m, Sum_term_var(xi), n, s) → Term_sub#(n, s) | Concat#(Cons_sum(xi, k, s), t) → Concat#(s, t) |
| Concat#(Cons_usual(x, m, s), t) → Term_sub#(m, t) | Concat#(Concat(s, t), u) → Concat#(t, u) |
| Concat#(Cons_usual(x, m, s), t) → Concat#(s, t) | Frozen#(m, Sum_constant(Left), n, s) → Term_sub#(m, s) |
| Term_sub#(Term_sub(m, s), t) → Concat#(s, t) | Term_sub#(Term_app(m, n), s) → Term_sub#(n, s) |
| Sum_sub#(xi, Cons_usual(y, m, s)) → Sum_sub#(xi, s) | Sum_sub#(xi, Cons_sum(psi, k, s)) → Sum_sub#(xi, s) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub#(Term_var(x), s) | | Term_sub#(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub#(Term_var(x), s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| Term_sub#(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub#(Term_var(x), s) | | Term_sub#(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub#(Term_var(x), s) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Case(m, xi, n), s) | → | Frozen#(m, Sum_sub(xi, s), n, s) |
| Frozen#(m, Sum_constant(Right), n, s) | → | Term_sub#(n, s) | | Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) |
| Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(m, s) | | Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(n, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) | | Concat#(Cons_sum(xi, k, s), t) | → | Concat#(s, t) |
| Concat#(Cons_usual(x, m, s), t) | → | Term_sub#(m, t) | | Concat#(Concat(s, t), u) | → | Concat#(t, u) |
| Concat#(Cons_usual(x, m, s), t) | → | Concat#(s, t) | | Frozen#(m, Sum_constant(Left), n, s) | → | Term_sub#(m, s) |
| Term_sub#(Term_sub(m, s), t) | → | Concat#(s, t) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 2z + 2x
- Concat(x,y): 2y + x
- Concat#(x,y): 2x
- Cons_sum(x,y,z): z + 1
- Cons_usual(x,y,z): z + y + 2x
- Frozen(x1,x2,x3,x4): 2x2
- Frozen#(x1,x2,x3,x4): 2x3 + 3x1
- Id: 0
- Left: 3
- Right: 3
- Sum_constant(x): 0
- Sum_sub(x,y): 1
- Sum_term_var(x): 0
- Term_app(x,y): y + 2x
- Term_inl(x): 3x
- Term_inr(x): 2x
- Term_pair(x,y): y + x
- Term_sub(x,y): y + x
- Term_sub#(x,y): 2x
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Concat#(Cons_sum(xi, k, s), t) | → | Concat#(s, t) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Case(m, xi, n), s) | → | Frozen#(m, Sum_sub(xi, s), n, s) |
| Frozen#(m, Sum_constant(Right), n, s) | → | Term_sub#(n, s) | | Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) |
| Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(m, s) | | Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(n, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) | | Concat#(Cons_usual(x, m, s), t) | → | Term_sub#(m, t) |
| Concat#(Concat(s, t), u) | → | Concat#(t, u) | | Frozen#(m, Sum_constant(Left), n, s) | → | Term_sub#(m, s) |
| Concat#(Cons_usual(x, m, s), t) | → | Concat#(s, t) | | Term_sub#(Term_sub(m, s), t) | → | Concat#(s, t) |
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 2z + 2x + 2
- Concat(x,y): y + 2x
- Concat#(x,y): 2x
- Cons_sum(x,y,z): 1
- Cons_usual(x,y,z): z + y + 2x
- Frozen(x1,x2,x3,x4): 0
- Frozen#(x1,x2,x3,x4): 2x3 + 2x1
- Id: 1
- Left: 3
- Right: 2
- Sum_constant(x): 1
- Sum_sub(x,y): 2y + x
- Sum_term_var(x): 3x
- Term_app(x,y): y + 2x
- Term_inl(x): x
- Term_inr(x): 2x
- Term_pair(x,y): y + 2x
- Term_sub(x,y): 2y + x
- Term_sub#(x,y): x
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Term_sub#(Case(m, xi, n), s) | → | Frozen#(m, Sum_sub(xi, s), n, s) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Frozen#(m, Sum_constant(Right), n, s) | → | Term_sub#(n, s) |
| Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) | | Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) |
| Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) | | Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(m, s) |
| Frozen#(m, Sum_term_var(xi), n, s) | → | Term_sub#(n, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) |
| Concat#(Cons_usual(x, m, s), t) | → | Term_sub#(m, t) | | Concat#(Concat(s, t), u) | → | Concat#(t, u) |
| Concat#(Cons_usual(x, m, s), t) | → | Concat#(s, t) | | Frozen#(m, Sum_constant(Left), n, s) | → | Term_sub#(m, s) |
| Term_sub#(Term_sub(m, s), t) | → | Concat#(s, t) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
The following SCCs where found
| Term_sub#(Term_pair(m, n), s) → Term_sub#(n, s) | Term_sub#(Term_app(m, n), s) → Term_sub#(m, s) |
| Term_sub#(Term_inl(m), s) → Term_sub#(m, s) | Term_sub#(Term_pair(m, n), s) → Term_sub#(m, s) |
| Concat#(Cons_usual(x, m, s), t) → Term_sub#(m, t) | Term_sub#(Term_inr(m), s) → Term_sub#(m, s) |
| Concat#(Concat(s, t), u) → Concat#(t, u) | Term_sub#(Term_sub(m, s), t) → Term_sub#(m, Concat(s, t)) |
| Concat#(Concat(s, t), u) → Concat#(s, Concat(t, u)) | Concat#(Cons_usual(x, m, s), t) → Concat#(s, t) |
| Term_sub#(Term_sub(m, s), t) → Concat#(s, t) | Term_sub#(Term_app(m, n), s) → Term_sub#(n, s) |
Problem 7: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) |
| Concat#(Cons_usual(x, m, s), t) | → | Term_sub#(m, t) | | Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) |
| Concat#(Concat(s, t), u) | → | Concat#(t, u) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) | | Concat#(Cons_usual(x, m, s), t) | → | Concat#(s, t) |
| Term_sub#(Term_sub(m, s), t) | → | Concat#(s, t) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): z + 1
- Concat(x,y): 2y + x
- Concat#(x,y): 2x
- Cons_sum(x,y,z): 0
- Cons_usual(x,y,z): z + y + 1
- Frozen(x1,x2,x3,x4): 3x4 + 3x1
- Id: 0
- Left: 3
- Right: 2
- Sum_constant(x): 0
- Sum_sub(x,y): 3x + 3
- Sum_term_var(x): x + 3
- Term_app(x,y): 2y + 2x
- Term_inl(x): x
- Term_inr(x): x
- Term_pair(x,y): y + 2x
- Term_sub(x,y): y + 2x
- Term_sub#(x,y): 2x
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Concat#(Cons_usual(x, m, s), t) | → | Term_sub#(m, t) | | Concat#(Cons_usual(x, m, s), t) | → | Concat#(s, t) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) |
| Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) | | Concat#(Concat(s, t), u) | → | Concat#(t, u) |
| Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Term_sub#(Term_sub(m, s), t) | → | Concat#(s, t) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
The following SCCs where found
| Concat#(Concat(s, t), u) → Concat#(t, u) | Concat#(Concat(s, t), u) → Concat#(s, Concat(t, u)) |
| Term_sub#(Term_app(m, n), s) → Term_sub#(m, s) | Term_sub#(Term_pair(m, n), s) → Term_sub#(n, s) |
| Term_sub#(Term_inl(m), s) → Term_sub#(m, s) | Term_sub#(Term_pair(m, n), s) → Term_sub#(m, s) |
| Term_sub#(Term_inr(m), s) → Term_sub#(m, s) | Term_sub#(Term_sub(m, s), t) → Term_sub#(m, Concat(s, t)) |
| Term_sub#(Term_app(m, n), s) → Term_sub#(n, s) |
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) |
| Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 2y
- Concat(x,y): 3x
- Cons_sum(x,y,z): 3x
- Cons_usual(x,y,z): 2y
- Frozen(x1,x2,x3,x4): 2x2
- Id: 0
- Left: 1
- Right: 3
- Sum_constant(x): 0
- Sum_sub(x,y): y
- Sum_term_var(x): 0
- Term_app(x,y): 2y + 3x
- Term_inl(x): 2x + 1
- Term_inr(x): x
- Term_pair(x,y): y + 2x
- Term_sub(x,y): 2y + x
- Term_sub#(x,y): 2x + 1
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Term_sub#(Term_inl(m), s) | → | Term_sub#(m, s) |
Problem 11: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 2y
- Concat(x,y): 1
- Cons_sum(x,y,z): 3
- Cons_usual(x,y,z): 3x
- Frozen(x1,x2,x3,x4): 3x4 + x3 + 3x1
- Id: 3
- Left: 2
- Right: 0
- Sum_constant(x): x
- Sum_sub(x,y): 3x + 2
- Sum_term_var(x): 2x
- Term_app(x,y): 2y + 2x
- Term_inl(x): 0
- Term_inr(x): x + 1
- Term_pair(x,y): 2y + x
- Term_sub(x,y): y + 2x
- Term_sub#(x,y): x
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Term_sub#(Term_inr(m), s) | → | Term_sub#(m, s) |
Problem 12: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 0
- Concat(x,y): 0
- Cons_sum(x,y,z): 1
- Cons_usual(x,y,z): x + 1
- Frozen(x1,x2,x3,x4): 3x4 + 2x3 + 3x1 + 2
- Id: 1
- Left: 0
- Right: 3
- Sum_constant(x): 2
- Sum_sub(x,y): 3x + 2
- Sum_term_var(x): 2x + 2
- Term_app(x,y): 2y + x
- Term_inl(x): 0
- Term_inr(x): 0
- Term_pair(x,y): 2y + x
- Term_sub(x,y): y + x + 1
- Term_sub#(x,y): 2x
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Term_sub#(Term_sub(m, s), t) | → | Term_sub#(m, Concat(s, t)) |
Problem 13: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) |
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 0
- Concat(x,y): 0
- Cons_sum(x,y,z): 0
- Cons_usual(x,y,z): 0
- Frozen(x1,x2,x3,x4): 0
- Id: 0
- Left: 0
- Right: 0
- Sum_constant(x): 0
- Sum_sub(x,y): 0
- Sum_term_var(x): 0
- Term_app(x,y): 2y + x
- Term_inl(x): 0
- Term_inr(x): 0
- Term_pair(x,y): 2y + x + 1
- Term_sub(x,y): 0
- Term_sub#(x,y): x
- Term_var(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Term_sub#(Term_pair(m, n), s) | → | Term_sub#(n, s) | | Term_sub#(Term_pair(m, n), s) | → | Term_sub#(m, s) |
Problem 14: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 0
- Concat(x,y): 0
- Cons_sum(x,y,z): 0
- Cons_usual(x,y,z): 0
- Frozen(x1,x2,x3,x4): 0
- Id: 0
- Left: 0
- Right: 0
- Sum_constant(x): 0
- Sum_sub(x,y): 0
- Sum_term_var(x): 0
- Term_app(x,y): y + 2x + 1
- Term_inl(x): 0
- Term_inr(x): 0
- Term_pair(x,y): 0
- Term_sub(x,y): 0
- Term_sub#(x,y): x
- Term_var(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Term_sub#(Term_app(m, n), s) | → | Term_sub#(m, s) | | Term_sub#(Term_app(m, n), s) | → | Term_sub#(n, s) |
Problem 10: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| Concat#(Concat(s, t), u) | → | Concat#(t, u) | | Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Polynomial Interpretation
- Case(x,y,z): 0
- Concat(x,y): 2y + x + 1
- Concat#(x,y): x + 1
- Cons_sum(x,y,z): 0
- Cons_usual(x,y,z): 2y
- Frozen(x1,x2,x3,x4): x2
- Id: 0
- Left: 3
- Right: 3
- Sum_constant(x): 0
- Sum_sub(x,y): y
- Sum_term_var(x): 0
- Term_app(x,y): 2x
- Term_inl(x): 0
- Term_inr(x): 0
- Term_pair(x,y): 0
- Term_sub(x,y): x
- Term_var(x): 0
Improved Usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| Concat#(Concat(s, t), u) | → | Concat#(t, u) | | Concat#(Concat(s, t), u) | → | Concat#(s, Concat(t, u)) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| Sum_sub#(xi, Cons_usual(y, m, s)) | → | Sum_sub#(xi, s) | | Sum_sub#(xi, Cons_sum(psi, k, s)) | → | Sum_sub#(xi, s) |
Rewrite Rules
| Term_sub(Case(m, xi, n), s) | → | Frozen(m, Sum_sub(xi, s), n, s) | | Frozen(m, Sum_constant(Left), n, s) | → | Term_sub(m, s) |
| Frozen(m, Sum_constant(Right), n, s) | → | Term_sub(n, s) | | Frozen(m, Sum_term_var(xi), n, s) | → | Case(Term_sub(m, s), xi, Term_sub(n, s)) |
| Term_sub(Term_app(m, n), s) | → | Term_app(Term_sub(m, s), Term_sub(n, s)) | | Term_sub(Term_pair(m, n), s) | → | Term_pair(Term_sub(m, s), Term_sub(n, s)) |
| Term_sub(Term_inl(m), s) | → | Term_inl(Term_sub(m, s)) | | Term_sub(Term_inr(m), s) | → | Term_inr(Term_sub(m, s)) |
| Term_sub(Term_var(x), Id) | → | Term_var(x) | | Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | m |
| Term_sub(Term_var(x), Cons_usual(y, m, s)) | → | Term_sub(Term_var(x), s) | | Term_sub(Term_var(x), Cons_sum(xi, k, s)) | → | Term_sub(Term_var(x), s) |
| Term_sub(Term_sub(m, s), t) | → | Term_sub(m, Concat(s, t)) | | Sum_sub(xi, Id) | → | Sum_term_var(xi) |
| Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_constant(k) | | Sum_sub(xi, Cons_sum(psi, k, s)) | → | Sum_sub(xi, s) |
| Sum_sub(xi, Cons_usual(y, m, s)) | → | Sum_sub(xi, s) | | Concat(Concat(s, t), u) | → | Concat(s, Concat(t, u)) |
| Concat(Cons_usual(x, m, s), t) | → | Cons_usual(x, Term_sub(m, t), Concat(s, t)) | | Concat(Cons_sum(xi, k, s), t) | → | Cons_sum(xi, k, Concat(s, t)) |
| Concat(Id, s) | → | s |
Original Signature
Termination of terms over the following signature is verified: Right, Term_app, Term_sub, Concat, Sum_sub, Cons_sum, Term_var, Left, Frozen, Sum_term_var, Sum_constant, Term_inl, Cons_usual, Case, Id, Term_inr, Term_pair
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| Sum_sub#(xi, Cons_usual(y, m, s)) | → | Sum_sub#(xi, s) | | Sum_sub#(xi, Cons_sum(psi, k, s)) | → | Sum_sub#(xi, s) |