Term Rewriting System R:
[x, y, z]
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
f(g(f(x))) -> f(h(s(0), x))
f(g(h(x, y))) -> f(h(s(x), y))
f(h(x, h(y, z))) -> f(h(+(x, y), z))
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
+'(x, s(y)) -> +'(x, y)
+'(s(x), y) -> +'(x, y)
+'(x, +(y, z)) -> +'(+(x, y), z)
+'(x, +(y, z)) -> +'(x, y)
F(g(f(x))) -> F(h(s(0), x))
F(g(h(x, y))) -> F(h(s(x), y))
F(h(x, h(y, z))) -> F(h(+(x, y), z))
F(h(x, h(y, z))) -> +'(x, y)
Furthermore, R contains two SCCs.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
Dependency Pairs:
+'(x, +(y, z)) -> +'(x, y)
+'(x, +(y, z)) -> +'(+(x, y), z)
+'(s(x), y) -> +'(x, y)
+'(x, s(y)) -> +'(x, y)
Rules:
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
f(g(f(x))) -> f(h(s(0), x))
f(g(h(x, y))) -> f(h(s(x), y))
f(h(x, h(y, z))) -> f(h(+(x, y), z))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳Size-Change Principle
→DP Problem 2
↳UsableRules
Dependency Pairs:
+'(x, +(y, z)) -> +'(x, y)
+'(x, +(y, z)) -> +'(+(x, y), z)
+'(s(x), y) -> +'(x, y)
+'(x, s(y)) -> +'(x, y)
Rules:
+(x, 0) -> x
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(x, s(y)) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
Strategy:
innermost
We number the DPs as follows:
- +'(x, +(y, z)) -> +'(x, y)
- +'(x, +(y, z)) -> +'(+(x, y), z)
- +'(s(x), y) -> +'(x, y)
- +'(x, s(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:
s(x_{1}) -> s(x_{1})
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
Dependency Pair:
F(h(x, h(y, z))) -> F(h(+(x, y), z))
Rules:
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
f(g(f(x))) -> f(h(s(0), x))
f(g(h(x, y))) -> f(h(s(x), y))
f(h(x, h(y, z))) -> f(h(+(x, y), z))
Strategy:
innermost
As we are in the innermost case, we can delete all 3 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Modular Removal of Rules
Dependency Pair:
F(h(x, h(y, z))) -> F(h(+(x, y), z))
Rules:
+(x, 0) -> x
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(x, s(y)) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
Strategy:
innermost
We have the following set of usable rules:
+(x, 0) -> x
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(x, s(y)) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
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) | = 1_{ }^{ } |
_{ }^{ }POL(h(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(s(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(F(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(+(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {h, s, F, +}
No Dependency Pairs can be deleted.
The following rules can be deleted as they contain symbols in their lhs which do not occur in D:
+(x, 0) -> x
+(0, y) -> y
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳MRR
...
→DP Problem 5
↳Modular Removal of Rules
Dependency Pair:
F(h(x, h(y, z))) -> F(h(+(x, y), z))
Rules:
+(s(x), y) -> s(+(x, y))
+(x, s(y)) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
Strategy:
innermost
We have the following set of usable rules:
+(s(x), y) -> s(+(x, y))
+(x, s(y)) -> s(+(x, y))
+(x, +(y, z)) -> +(+(x, y), z)
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(h(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(s(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(F(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(+(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {h, s, F, +}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:
F(h(x, h(y, z))) -> F(h(+(x, y), z))
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.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes