Term Rewriting System R:
[x]
a(f, a(g, a(f, x))) -> a(f, a(g, a(g, a(f, x))))
a(g, a(f, a(g, x))) -> a(g, a(f, a(f, a(g, x))))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
A(f, a(g, a(f, x))) -> A(f, a(g, a(g, a(f, x))))
A(f, a(g, a(f, x))) -> A(g, a(g, a(f, x)))
A(g, a(f, a(g, x))) -> A(g, a(f, a(f, a(g, x))))
A(g, a(f, a(g, x))) -> A(f, a(f, a(g, x)))
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Modular Removal of Rules
Dependency Pairs:
A(g, a(f, a(g, x))) -> A(f, a(f, a(g, x)))
A(g, a(f, a(g, x))) -> A(g, a(f, a(f, a(g, x))))
A(f, a(g, a(f, x))) -> A(g, a(g, a(f, x)))
A(f, a(g, a(f, x))) -> A(f, a(g, a(g, a(f, x))))
Rules:
a(f, a(g, a(f, x))) -> a(f, a(g, a(g, a(f, x))))
a(g, a(f, a(g, x))) -> a(g, a(f, a(f, a(g, x))))
The original DP problem is in applicative form. Its DPs and usable rules are the following.
A(g, a(f, a(g, x))) -> A(f, a(f, a(g, x)))
A(g, a(f, a(g, x))) -> A(g, a(f, a(f, a(g, x))))
A(f, a(g, a(f, x))) -> A(g, a(g, a(f, x)))
A(f, a(g, a(f, x))) -> A(f, a(g, a(g, a(f, x))))
a(f, a(g, a(f, x))) -> a(f, a(g, a(g, a(f, x))))
a(g, a(f, a(g, x))) -> a(g, a(f, a(f, a(g, x))))
It is proper and hence, it can be A-transformed which results in the DP problem
G(f(g(x))) -> F(f(g(x)))
G(f(g(x))) -> G(f(f(g(x))))
F(g(f(x))) -> G(g(f(x)))
F(g(f(x))) -> F(g(g(f(x))))
f(g(f(x))) -> f(g(g(f(x))))
g(f(g(x))) -> g(f(f(g(x))))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(g(x1)) | = x1 |
| POL(G(x1)) | = x1 |
| POL(f(x1)) | = x1 |
| POL(F(x1)) | = x1 |
We have the following set D of usable symbols: {g, G, F, f}
No Dependency Pairs can be deleted.
No Rules can be deleted.
The result of this processor delivers one new DP problem.
Note that we keep the A-transformed DP problem as result of this processor.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Negative Polynomial Order
Dependency Pairs:
G(f(g(x))) -> F(f(g(x)))
G(f(g(x))) -> G(f(f(g(x))))
F(g(f(x))) -> G(g(f(x)))
F(g(f(x))) -> F(g(g(f(x))))
Rules:
f(g(f(x))) -> f(g(g(f(x))))
g(f(g(x))) -> g(f(f(g(x))))
The following Dependency Pair can be strictly oriented using the given order.
G(f(g(x))) -> F(f(g(x)))
Moreover, the following usable rules (regarding the implicit AFS) are oriented.
f(g(f(x))) -> f(g(g(f(x))))
g(f(g(x))) -> g(f(f(g(x))))
Used ordering:
Polynomial Order with Interpretation:
POL( G(x1) ) = 1
POL( F(x1) ) = x1
POL( f(x1) ) = 0
POL( g(x1) ) = 1
This results in one new DP problem.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Neg POLO
...
→DP Problem 3
↳Dependency Graph
Dependency Pairs:
G(f(g(x))) -> G(f(f(g(x))))
F(g(f(x))) -> G(g(f(x)))
F(g(f(x))) -> F(g(g(f(x))))
Rules:
f(g(f(x))) -> f(g(g(f(x))))
g(f(g(x))) -> g(f(f(g(x))))
Using the Dependency Graph the DP problem was split into 2 DP problems.
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Neg POLO
...
→DP Problem 4
↳RFC Match Bounds
Dependency Pair:
G(f(g(x))) -> G(f(f(g(x))))
Rules:
f(g(f(x))) -> f(g(g(f(x))))
g(f(g(x))) -> g(f(f(g(x))))
Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 2.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65
Node 49 is start node and node 50 is final node.
Those nodes are connect through the following edges:
- 50 to 50 labelled #(0)
- 49 to 51 labelled G(0)
- 51 to 52 labelled f(0)
- 52 to 53 labelled f(0)
- 53 to 50 labelled g(0)
- 53 to 54 labelled g(1)
- 54 to 55 labelled f(1)
- 55 to 56 labelled f(1)
- 56 to 50 labelled g(1)
- 52 to 57 labelled f(1)
- 57 to 58 labelled g(1)
- 58 to 59 labelled g(1)
- 59 to 50 labelled f(1)
- 59 to 57 labelled f(1)
- 56 to 54 labelled g(1)
- 58 to 54 labelled g(1)
- 55 to 57 labelled f(1)
- 58 to 60 labelled g(2)
- 60 to 61 labelled f(2)
- 61 to 62 labelled f(2)
- 62 to 58 labelled g(2)
- 55 to 63 labelled f(2)
- 63 to 64 labelled g(2)
- 64 to 65 labelled g(2)
- 65 to 55 labelled f(2)
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Neg POLO
...
→DP Problem 5
↳RFC Match Bounds
Dependency Pair:
F(g(f(x))) -> F(g(g(f(x))))
Rules:
f(g(f(x))) -> f(g(g(f(x))))
g(f(g(x))) -> g(f(f(g(x))))
Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 2.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82
Node 66 is start node and node 67 is final node.
Those nodes are connect through the following edges:
- 67 to 67 labelled #(0)
- 66 to 68 labelled F(0)
- 68 to 69 labelled g(0)
- 69 to 70 labelled g(0)
- 70 to 67 labelled f(0)
- 70 to 71 labelled f(1)
- 71 to 72 labelled g(1)
- 72 to 73 labelled g(1)
- 73 to 67 labelled f(1)
- 69 to 74 labelled g(1)
- 74 to 75 labelled f(1)
- 75 to 76 labelled f(1)
- 76 to 67 labelled g(1)
- 76 to 74 labelled g(1)
- 73 to 71 labelled f(1)
- 75 to 71 labelled f(1)
- 72 to 74 labelled g(1)
- 75 to 77 labelled f(2)
- 77 to 78 labelled g(2)
- 78 to 79 labelled g(2)
- 79 to 75 labelled f(2)
- 72 to 80 labelled g(2)
- 80 to 81 labelled f(2)
- 81 to 82 labelled f(2)
- 82 to 72 labelled g(2)
Termination of R successfully shown.
Duration:
0:00 minutes