Term Rewriting System R:
[x, y, l]
0(#) -> #
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
sum(nil) -> 0(#)
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> 1(#)
prod(cons(x, l)) -> *(x, prod(l))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
+'(0(x), 0(y)) -> 0'(+(x, y))
+'(0(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(1(x), 1(y)) -> 0'(+(+(x, y), 1(#)))
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 1(y)) -> +'(x, y)
*'(0(x), y) -> 0'(*(x, y))
*'(0(x), y) -> *'(x, y)
*'(1(x), y) -> +'(0(*(x, y)), y)
*'(1(x), y) -> 0'(*(x, y))
*'(1(x), y) -> *'(x, y)
SUM(nil) -> 0'(#)
SUM(cons(x, l)) -> +'(x, sum(l))
SUM(cons(x, l)) -> SUM(l)
PROD(cons(x, l)) -> *'(x, prod(l))
PROD(cons(x, l)) -> PROD(l)
Furthermore, R contains four SCCs.
R
↳DPs
→DP Problem 1
↳Modular Removal of Rules
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳SCP
Dependency Pairs:
+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(0(x), 0(y)) -> +'(x, y)
Rules:
0(#) -> #
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
sum(nil) -> 0(#)
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> 1(#)
prod(cons(x, l)) -> *(x, prod(l))
We have the following set of usable rules:
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
0(#) -> #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#) | = 0_{ }^{ } |
_{ }^{ }POL(0(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(1(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(+(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(+'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {#, 0, 1, +, +'}
No Dependency Pairs can be deleted.
7 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 5
↳Modular Removal of Rules
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳SCP
Dependency Pairs:
+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(0(x), 0(y)) -> +'(x, y)
Rules:
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
0(#) -> #
We have the following set of usable rules:
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
0(#) -> #
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(#) | = 0_{ }^{ } |
_{ }^{ }POL(0(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(1(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(+(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(+'(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {#, 0, 1, +, +'}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 5
↳MRR
...
→DP Problem 6
↳Modular Removal of Rules
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳SCP
Dependency Pair:
+'(0(x), 0(y)) -> +'(x, y)
Rules:
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
0(#) -> #
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(0(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(+'(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {+'}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
+'(0(x), 0(y)) -> +'(x, y)
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.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Size-Change Principle
→DP Problem 3
↳SCP
→DP Problem 4
↳SCP
Dependency Pairs:
*'(1(x), y) -> *'(x, y)
*'(0(x), y) -> *'(x, y)
Rules:
0(#) -> #
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
sum(nil) -> 0(#)
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> 1(#)
prod(cons(x, l)) -> *(x, prod(l))
We number the DPs as follows:
- *'(1(x), y) -> *'(x, y)
- *'(0(x), y) -> *'(x, y)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
0(x_{1}) -> 0(x_{1})
1(x_{1}) -> 1(x_{1})
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳SCP
→DP Problem 3
↳Size-Change Principle
→DP Problem 4
↳SCP
Dependency Pair:
SUM(cons(x, l)) -> SUM(l)
Rules:
0(#) -> #
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
sum(nil) -> 0(#)
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> 1(#)
prod(cons(x, l)) -> *(x, prod(l))
We number the DPs as follows:
- SUM(cons(x, l)) -> SUM(l)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
cons(x_{1}, x_{2}) -> cons(x_{1}, x_{2})
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
→DP Problem 4
↳Size-Change Principle
Dependency Pair:
PROD(cons(x, l)) -> PROD(l)
Rules:
0(#) -> #
+(x, #) -> x
+(#, x) -> x
+(0(x), 0(y)) -> 0(+(x, y))
+(0(x), 1(y)) -> 1(+(x, y))
+(1(x), 0(y)) -> 1(+(x, y))
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
*(#, x) -> #
*(0(x), y) -> 0(*(x, y))
*(1(x), y) -> +(0(*(x, y)), y)
sum(nil) -> 0(#)
sum(cons(x, l)) -> +(x, sum(l))
prod(nil) -> 1(#)
prod(cons(x, l)) -> *(x, prod(l))
We number the DPs as follows:
- PROD(cons(x, l)) -> PROD(l)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
D_{P}: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
cons(x_{1}, x_{2}) -> cons(x_{1}, x_{2})
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:00 minutes