Term Rewriting System R:
[x, y]
top(sent(x)) -> top(check(rest(x)))
rest(nil) -> sent(nil)
rest(cons(x, y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x, y)) -> cons(check(x), y)
check(cons(x, y)) -> cons(x, check(y))
check(cons(x, y)) -> cons(x, y)
Termination of R to be shown.
R
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
rest(cons(x, y)) -> sent(y)
where the Polynomial interpretation:
| POL(top(x1)) | = 1 + x1 |
| POL(rest(x1)) | = x1 |
| POL(cons(x1, x2)) | = 1 + x1 + x2 |
| POL(check(x1)) | = x1 |
| POL(nil) | = 0 |
| POL(sent(x1)) | = x1 |
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:
check(cons(x, y)) -> cons(x, check(y))
check(cons(x, y)) -> cons(x, y)
check(cons(x, y)) -> cons(check(x), y)
where the Polynomial interpretation:
| POL(top(x1)) | = 2 + x1 |
| POL(rest(x1)) | = x1 |
| POL(cons(x1, x2)) | = 1 + x1 + x2 |
| POL(check(x1)) | = 2·x1 |
| POL(nil) | = 0 |
| POL(sent(x1)) | = 2·x1 |
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
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
CHECK(sent(x)) -> CHECK(x)
CHECK(rest(x)) -> REST(check(x))
CHECK(rest(x)) -> CHECK(x)
TOP(sent(x)) -> TOP(check(rest(x)))
TOP(sent(x)) -> CHECK(rest(x))
TOP(sent(x)) -> REST(x)
Furthermore, R contains two SCCs.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳DPs
...
→DP Problem 1
↳Size-Change Principle
Dependency Pairs:
CHECK(rest(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)
Rules:
rest(nil) -> sent(nil)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
top(sent(x)) -> top(check(rest(x)))
We number the DPs as follows:
- CHECK(rest(x)) -> CHECK(x)
- CHECK(sent(x)) -> CHECK(x)
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:
rest(x1) -> rest(x1)
sent(x1) -> sent(x1)
We obtain no new DP problems.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳DPs
...
→DP Problem 2
↳Modular Removal of Rules
Dependency Pair:
TOP(sent(x)) -> TOP(check(rest(x)))
Rules:
rest(nil) -> sent(nil)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
top(sent(x)) -> top(check(rest(x)))
We have the following set of usable rules:
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
rest(nil) -> sent(nil)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(rest(x1)) | = x1 |
| POL(check(x1)) | = x1 |
| POL(nil) | = 0 |
| POL(TOP(x1)) | = 1 + x1 |
| POL(sent(x1)) | = x1 |
We have the following set D of usable symbols: {rest, nil, check, TOP, sent}
No Dependency Pairs can be deleted.
1 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳RRRPolo
→TRS2
↳RRRPolo
→TRS3
↳DPs
...
→DP Problem 3
↳RFC Match Bounds
Dependency Pair:
TOP(sent(x)) -> TOP(check(rest(x)))
Rules:
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
rest(nil) -> sent(nil)
Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 2.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
24, 25, 26, 27, 28, 29, 30, 31, 32, 33
Node 24 is start node and node 25 is final node.
Those nodes are connect through the following edges:
- 25 to 25 labelled #(0)
- 24 to 26 labelled TOP(0)
- 26 to 27 labelled check(0)
- 27 to 25 labelled rest(0)
- 27 to 28 labelled sent(1)
- 28 to 25 labelled nil(1)
- 26 to 29 labelled rest(1)
- 29 to 25 labelled check(1)
- 26 to 30 labelled sent(1)
- 30 to 28 labelled check(1)
- 29 to 29 labelled rest(1)
- 29 to 29 labelled sent(1)
- 24 to 31 labelled TOP(1)
- 31 to 32 labelled check(1)
- 32 to 30 labelled rest(1)
- 31 to 33 labelled rest(2)
- 33 to 30 labelled check(2)
Termination of R successfully shown.
Duration:
0:00 minutes