Term Rewriting System R:
[y, x]
int(0, 0) -> .(0, nil)
int(0, s(y)) -> .(0, int(s(0), s(y)))
int(s(x), 0) -> nil
int(s(x), s(y)) -> intlist(int(x, y))
intlist(nil) -> nil
intlist(.(x, y)) -> .(s(x), intlist(y))
Termination of R to be shown.
R
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
int(0, 0) -> .(0, nil)
int(s(x), 0) -> nil
where the Polynomial interpretation:
| POL(int_list(x1)) | = x1 |
| POL(0) | = 0 |
| POL(int(x1, x2)) | = 1 + x1 + x2 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(.(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
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
intlist(nil) -> nil
where the Polynomial interpretation:
| POL(int_list(x1)) | = 2·x1 |
| POL(0) | = 0 |
| POL(int(x1, x2)) | = x1 + x2 |
| POL(nil) | = 1 |
| POL(s(x1)) | = 2·x1 |
| POL(.(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
↳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
↳OC
...
→TRS4
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
INT(s(x), s(y)) -> INTLIST(int(x, y))
INT(s(x), s(y)) -> INT(x, y)
INT(0, s(y)) -> INT(s(0), s(y))
INTLIST(.(x, y)) -> INTLIST(y)
Furthermore, R contains two SCCs.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳OC
...
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pair:
INTLIST(.(x, y)) -> INTLIST(y)
Rules:
int(s(x), s(y)) -> intlist(int(x, y))
int(0, s(y)) -> .(0, int(s(0), s(y)))
intlist(.(x, y)) -> .(s(x), intlist(y))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳OC
...
→DP Problem 3
↳Size-Change Principle
Dependency Pair:
INTLIST(.(x, y)) -> INTLIST(y)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- INTLIST(.(x, y)) -> INTLIST(y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
.(x1, x2) -> .(x1, x2)
We obtain no new DP problems.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳OC
...
→DP Problem 2
↳Usable Rules (Innermost)
Dependency Pairs:
INT(0, s(y)) -> INT(s(0), s(y))
INT(s(x), s(y)) -> INT(x, y)
Rules:
int(s(x), s(y)) -> intlist(int(x, y))
int(0, s(y)) -> .(0, int(s(0), s(y)))
intlist(.(x, y)) -> .(s(x), intlist(y))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳OC
...
→DP Problem 4
↳Size-Change Principle
Dependency Pairs:
INT(0, s(y)) -> INT(s(0), s(y))
INT(s(x), s(y)) -> INT(x, y)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- INT(0, s(y)) -> INT(s(0), s(y))
- INT(s(x), s(y)) -> INT(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x1) -> s(x1)
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes