Problem 1: Propagation
Dependency Pair Problem
Dependency Pairs
| length1# | → | length# | | length# | → | length1# |
Rewrite Rules
| from(X) | → | cons(X) | | length | → | 0 |
| length | → | s(length1) | | length1 | → | length |
Original Signature
Termination of terms over the following signature is verified: 0, s, length, from, length1, cons
Strategy
The dependency pairs length1
# → length
# and length
# → length1
# are consolidated into the rule length1
# → length1
# .
This is possible as
- all subterms of length# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in length#, but non-replacing in both length1# and length1#
The dependency pairs length1
# → length
# and length
# → length1
# are consolidated into the rule length1
# → length1
# .
This is possible as
- all subterms of length# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in length#, but non-replacing in both length1# and length1#
The dependency pairs length
# → length1
# and length1
# → length
# are consolidated into the rule length
# → length
# .
This is possible as
- all subterms of length1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in length1#, but non-replacing in both length# and length#
The dependency pairs length
# → length1
# and length1
# → length
# are consolidated into the rule length
# → length
# .
This is possible as
- all subterms of length1# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in length1#, but non-replacing in both length# and length#
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| length1# → length# | length1# → length1# |
| length# → length1# | length# → length# |