Term Rewriting System R:
[k, l, x, y]
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
Termination of R to be shown.
R
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
app(nil, k) -> k
app(l, nil) -> l
plus(0, y) -> y
where the Polynomial interpretation:
| POL(plus(x1, x2)) | = x1 + x2 |
| POL(0) | = 1 |
| POL(cons(x1, x2)) | = x1 + x2 |
| POL(nil) | = 0 |
| POL(sum(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(app(x1, x2)) | = 1 + x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRPolo
→TRS2
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
where the Polynomial interpretation:
| POL(plus(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = 1 + x1 + x2 |
| POL(nil) | = 0 |
| POL(sum(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(app(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
plus(s(x), y) -> s(plus(x, y))
where the Polynomial interpretation:
| POL(plus(x1, x2)) | = 2·x1 + x2 |
| POL(cons(x1, x2)) | = x1 + x2 |
| POL(nil) | = 0 |
| POL(sum(x1)) | = x1 |
| POL(s(x1)) | = 1 + x1 |
| POL(app(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS4
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
app(cons(x, l), k) -> cons(x, app(l, k))
where the Polynomial interpretation:
| POL(cons(x1, x2)) | = 1 + x1 + x2 |
| POL(nil) | = 0 |
| POL(sum(x1)) | = x1 |
| POL(app(x1, x2)) | = 2·x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS5
↳Overlay and local confluence Check
The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳RRRPolo
...
→TRS6
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) -> SUM(cons(x, cons(y, k)))
R contains no SCCs.
Termination of R successfully shown.
Duration:
0:01 minutes