Term Rewriting System R:
[X]
f(a, a) -> f(a, b)
f(a, b) -> f(s(a), c)
f(s(X), c) -> f(X, c)
f(c, c) -> f(a, a)
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(a, a) -> F(a, b)
F(a, b) -> F(s(a), c)
F(s(X), c) -> F(X, c)
F(c, c) -> F(a, a)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pairs:
F(c, c) -> F(a, a)
F(s(X), c) -> F(X, c)
F(a, b) -> F(s(a), c)
F(a, a) -> F(a, b)
Rules:
f(a, a) -> f(a, b)
f(a, b) -> f(s(a), c)
f(s(X), c) -> f(X, c)
f(c, c) -> f(a, a)
Strategy:
innermost
As we are in the innermost case, we can delete all 4 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Negative Polynomial Order
Dependency Pairs:
F(c, c) -> F(a, a)
F(s(X), c) -> F(X, c)
F(a, b) -> F(s(a), c)
F(a, a) -> F(a, b)
Rule:
none
Strategy:
innermost
The following Dependency Pair can be strictly oriented using the given order.
F(c, c) -> F(a, a)
There are no usable rules (regarding the implicit AFS).
Used ordering:
Polynomial Order with Interpretation:
POL( F(x_{1}, x_{2}) ) = x_{1}
POL( c ) = 1
POL( a ) = 0
POL( s(x_{1}) ) = x_{1}
This results in one new DP problem.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 3
↳Dependency Graph
Dependency Pairs:
F(s(X), c) -> F(X, c)
F(a, b) -> F(s(a), c)
F(a, a) -> F(a, b)
Rule:
none
Strategy:
innermost
Using the Dependency Graph the DP problem was split into 1 DP problems.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 4
↳Size-Change Principle
Dependency Pair:
F(s(X), c) -> F(X, c)
Rule:
none
Strategy:
innermost
We number the DPs as follows:
- F(s(X), c) -> F(X, c)
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.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes