Term Rewriting System R:
[x]
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(0) -> 0
bits(s(x)) -> s(bits(half(s(x))))
Termination of R to be shown.
TRS
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
bits(0) -> 0
where the Polynomial interpretation:
| POL(0) | = 0 |
| POL(bits(x1)) | = 1 + x1 |
| POL(s(x1)) | = x1 |
| POL(half(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳RRRPolo
→TRS2
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
HALF(s(s(x))) -> HALF(x)
BITS(s(x)) -> BITS(half(s(x)))
BITS(s(x)) -> HALF(s(x))
Furthermore, R contains two SCCs.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳Non-Overlappingness Check
→DP Problem 2
↳NOC
Dependency Pair:
HALF(s(s(x))) -> HALF(x)
Rules:
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(s(x)) -> s(bits(half(s(x))))
R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle:
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
...
→DP Problem 3
↳Usable Rules (Innermost)
→DP Problem 2
↳NOC
Dependency Pair:
HALF(s(s(x))) -> HALF(x)
Rules:
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(s(x)) -> s(bits(half(s(x))))
Strategy:
innermost
As we are in the innermost case, we can delete all 4 non-usable-rules.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
...
→DP Problem 4
↳Modular Removal of Rules
→DP Problem 2
↳NOC
Dependency Pair:
HALF(s(s(x))) -> HALF(x)
Rule:
none
Strategy:
innermost
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(HALF(x1)) | = x1 |
| POL(s(x1)) | = x1 |
We have the following set D of usable symbols: {HALF}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
HALF(s(s(x))) -> HALF(x)
No Rules can be deleted.
After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
→DP Problem 2
↳Non-Overlappingness Check
Dependency Pair:
BITS(s(x)) -> BITS(half(s(x)))
Rules:
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(s(x)) -> s(bits(half(s(x))))
R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle:
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
→DP Problem 2
↳NOC
...
→DP Problem 5
↳Usable Rules (Innermost)
Dependency Pair:
BITS(s(x)) -> BITS(half(s(x)))
Rules:
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(s(x)) -> s(bits(half(s(x))))
Strategy:
innermost
As we are in the innermost case, we can delete all 1 non-usable-rules.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
→DP Problem 2
↳NOC
...
→DP Problem 6
↳Modular Removal of Rules
Dependency Pair:
BITS(s(x)) -> BITS(half(s(x)))
Rules:
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
Strategy:
innermost
We have the following set of usable rules:
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(BITS(x1)) | = x1 |
| POL(0) | = 1 |
| POL(s(x1)) | = 2·x1 |
| POL(half(x1)) | = x1 |
We have the following set D of usable symbols: {BITS, 0, s, half}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
half(s(0)) -> 0
The result of this processor delivers one new DP problem.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
→DP Problem 2
↳NOC
...
→DP Problem 7
↳Modular Removal of Rules
Dependency Pair:
BITS(s(x)) -> BITS(half(s(x)))
Rules:
half(0) -> 0
half(s(s(x))) -> s(half(x))
Strategy:
innermost
We have the following set of usable rules:
half(0) -> 0
half(s(s(x))) -> s(half(x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(BITS(x1)) | = 1 + x1 |
| POL(0) | = 0 |
| POL(s(x1)) | = 1 + x1 |
| POL(half(x1)) | = x1 |
We have the following set D of usable symbols: {BITS, 0, s, half}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
half(s(s(x))) -> s(half(x))
The result of this processor delivers one new DP problem.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
→DP Problem 2
↳NOC
...
→DP Problem 8
↳Modular Removal of Rules
Dependency Pair:
BITS(s(x)) -> BITS(half(s(x)))
Rule:
half(0) -> 0
Strategy:
innermost
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(BITS(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(half(x1)) | = x1 |
We have the following set D of usable symbols: {BITS, s, half}
No Dependency Pairs can be deleted.
1 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
TRS
↳RRRPolo
→TRS2
↳DPs
→DP Problem 1
↳NOC
→DP Problem 2
↳NOC
...
→DP Problem 9
↳Dependency Graph
Dependency Pair:
BITS(s(x)) -> BITS(half(s(x)))
Rule:
none
Strategy:
innermost
Using the Dependency Graph resulted in no new DP problems.
Termination of R successfully shown.
Duration:
0:01 minutes