Term Rewriting System R:
[x, y, z]
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(x, g(y)) -> F(h(x), i(x, y))
F(x, g(y)) -> I(x, y)
I(x, j(y, z)) -> J(g(y), i(x, z))
I(x, j(y, z)) -> I(x, z)
I(h(x), j(j(y, z), 0)) -> J(i(h(x), j(y, z)), i(x, j(y, z)))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
J(g(x), g(y)) -> J(x, y)
Furthermore, R contains three SCCs.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
→DP Problem 2
↳MRR
→DP Problem 3
↳Inst
Dependency Pair:
J(g(x), g(y)) -> J(x, y)
Rules:
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
We number the DPs as follows:
- J(g(x), g(y)) -> J(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:
g(x_{1}) -> g(x_{1})
We obtain no new DP problems.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Modular Removal of Rules
→DP Problem 3
↳Inst
Dependency Pairs:
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(x, j(y, z)) -> I(x, z)
Rules:
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
We have the following set of usable rules:
j(g(x), g(y)) -> g(j(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}-compatible order: Polynomial ordering.
Polynomial interpretation:
_{ }^{ }POL(I(x_{1}, x_{2})) | = 1 + x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(0) | = 0_{ }^{ } |
_{ }^{ }POL(g(x_{1})) | = x_{1}_{ }^{ } |
_{ }^{ }POL(h(x_{1})) | = 1 + x_{1}_{ }^{ } |
_{ }^{ }POL(j(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I, g, h, j}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
4 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 4
↳Modular Removal of Rules
→DP Problem 3
↳Inst
Dependency Pair:
I(x, j(y, z)) -> I(x, z)
Rule:
j(g(x), g(y)) -> g(j(x, y))
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(I(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
_{ }^{ }POL(j(x_{1}, x_{2})) | = x_{1} + x_{2}_{ }^{ } |
We have the following set D of usable symbols: {I}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
I(x, j(y, z)) -> I(x, 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.
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳Instantiation Transformation
Dependency Pair:
F(x, g(y)) -> F(h(x), i(x, y))
Rules:
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule
F(x, g(y)) -> F(h(x), i(x, y))
one new Dependency Pair
is created:
F(h(x''''), g(y')) -> F(h(h(x'''')), i(h(x''''), y'))
The transformation is resulting in one new DP problem:
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳MRR
→DP Problem 3
↳Inst
→DP Problem 5
↳Remaining Obligation(s)
The following remains to be proven:
Dependency Pair:
F(h(x''''), g(y')) -> F(h(h(x'''')), i(h(x''''), y'))
Rules:
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))
The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
1:00 minutes