(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
Q is empty.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(g, a(f, a(f, a(f, x))))))
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(f, a(f, a(f, x)))))
A(f, a(f, a(g, a(g, x)))) → A(g, a(f, a(f, a(f, x))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(f, x)
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))
A(f, a(f, a(g, a(g, x)))) → A(f, x)
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
We have to consider all minimal (P,Q,R)-chains.
(7) ATransformationProof (EQUIVALENT transformation)
We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(x)
The TRS R consists of the following rules:
f(f(g(g(x)))) → g(g(g(f(f(f(x))))))
The set Q consists of the following terms:
f(f(g(g(x0))))
We have to consider all minimal (P,Q,R)-chains.
(9) RFCMatchBoundsDPProof (EQUIVALENT transformation)
Finiteness of the DP problem can be shown by a matchbound of 4.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(x)
To find matches we regarded all rules of R and P:
f(f(g(g(x)))) → g(g(g(f(f(f(x))))))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(x)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
9574211, 9574212, 9574214, 9574213, 9574215, 9574216, 9574219, 9574217, 9574218, 9574221, 9574220, 9574222, 9574223, 9574224, 9574225, 9574226, 9574230, 9574231, 9574227, 9574228, 9574229, 9574236, 9574234, 9574235, 9574233, 9574232, 9574237, 9574238, 9574239, 9574240, 9574241, 9574242, 9574243, 9574245, 9574246, 9574247, 9574248, 9574244
Node 9574211 is start node and node 9574212 is final node.
Those nodes are connect through the following edges:
- 9574211 to 9574213 labelled f1_1(0)
- 9574211 to 9574214 labelled f1_1(0)
- 9574211 to 9574212 labelled f1_1(0), f1_1(1)
- 9574211 to 9574218 labelled f1_1(1)
- 9574211 to 9574219 labelled f1_1(1)
- 9574211 to 9574216 labelled f1_1(1), f1_1(2)
- 9574211 to 9574220 labelled f1_1(2)
- 9574211 to 9574221 labelled f1_1(2)
- 9574211 to 9574230 labelled f1_1(2)
- 9574211 to 9574231 labelled f1_1(2)
- 9574211 to 9574222 labelled f1_1(2)
- 9574211 to 9574235 labelled f1_1(3)
- 9574211 to 9574236 labelled f1_1(3)
- 9574211 to 9574224 labelled f1_1(3)
- 9574211 to 9574240 labelled f1_1(3)
- 9574211 to 9574241 labelled f1_1(3)
- 9574211 to 9574228 labelled f1_1(3)
- 9574211 to 9574242 labelled f1_1(4)
- 9574211 to 9574243 labelled f1_1(4)
- 9574211 to 9574238 labelled f1_1(4)
- 9574212 to 9574212 labelled #_1(0)
- 9574214 to 9574212 labelled f_1(0)
- 9574214 to 9574215 labelled g_1(1)
- 9574213 to 9574214 labelled f_1(0)
- 9574213 to 9574215 labelled g_1(1)
- 9574215 to 9574216 labelled g_1(1)
- 9574216 to 9574217 labelled g_1(1)
- 9574219 to 9574212 labelled f_1(1)
- 9574219 to 9574215 labelled g_1(1)
- 9574219 to 9574216 labelled f_1(1)
- 9574217 to 9574218 labelled f_1(1)
- 9574217 to 9574222 labelled g_1(2)
- 9574218 to 9574219 labelled f_1(1)
- 9574218 to 9574215 labelled g_1(1)
- 9574218 to 9574227 labelled g_1(2)
- 9574221 to 9574216 labelled f_1(2)
- 9574220 to 9574221 labelled f_1(2)
- 9574220 to 9574227 labelled g_1(2)
- 9574222 to 9574223 labelled g_1(2)
- 9574223 to 9574224 labelled g_1(2)
- 9574224 to 9574225 labelled f_1(2)
- 9574225 to 9574226 labelled f_1(2)
- 9574225 to 9574227 labelled g_1(2)
- 9574226 to 9574216 labelled f_1(2)
- 9574230 to 9574231 labelled f_1(2)
- 9574230 to 9574232 labelled g_1(3)
- 9574231 to 9574222 labelled f_1(2)
- 9574227 to 9574228 labelled g_1(2)
- 9574228 to 9574229 labelled g_1(2)
- 9574229 to 9574230 labelled f_1(2)
- 9574236 to 9574224 labelled f_1(3)
- 9574236 to 9574237 labelled g_1(3)
- 9574234 to 9574235 labelled f_1(3)
- 9574234 to 9574244 labelled g_1(4)
- 9574235 to 9574236 labelled f_1(3)
- 9574233 to 9574234 labelled g_1(3)
- 9574232 to 9574233 labelled g_1(3)
- 9574237 to 9574238 labelled g_1(3)
- 9574238 to 9574239 labelled g_1(3)
- 9574239 to 9574240 labelled f_1(3)
- 9574240 to 9574241 labelled f_1(3)
- 9574241 to 9574228 labelled f_1(3)
- 9574242 to 9574243 labelled f_1(4)
- 9574243 to 9574238 labelled f_1(4)
- 9574245 to 9574246 labelled g_1(4)
- 9574246 to 9574247 labelled f_1(4)
- 9574247 to 9574248 labelled f_1(4)
- 9574248 to 9574238 labelled f_1(4)
- 9574244 to 9574245 labelled g_1(4)
(10) TRUE