(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:
7414841, 7414842, 7414843, 7414844, 7414845, 7414846, 7414850, 7414851, 7414848, 7414849, 7414847, 7414852, 7414853, 7414858, 7414854, 7414855, 7414857, 7414856, 7414859, 7414860, 7414863, 7414861, 7414862, 7414864, 7414865, 7414870, 7414869, 7414866, 7414867, 7414868, 7414874, 7414875, 7414871, 7414872, 7414873, 7414876, 7414877, 7414878, 7414881, 7414882, 7414880, 7414879
Node 7414841 is start node and node 7414842 is final node.
Those nodes are connect through the following edges:
- 7414841 to 7414843 labelled f1_1(0)
- 7414841 to 7414844 labelled f1_1(0)
- 7414841 to 7414842 labelled f1_1(0), f1_1(1)
- 7414841 to 7414845 labelled f1_1(1)
- 7414841 to 7414846 labelled f1_1(1)
- 7414841 to 7414850 labelled f1_1(1)
- 7414841 to 7414851 labelled f1_1(1)
- 7414841 to 7414848 labelled f1_1(1), f1_1(2)
- 7414841 to 7414852 labelled f1_1(2)
- 7414841 to 7414853 labelled f1_1(2)
- 7414841 to 7414854 labelled f1_1(2)
- 7414841 to 7414864 labelled f1_1(3)
- 7414841 to 7414865 labelled f1_1(3)
- 7414841 to 7414856 labelled f1_1(3)
- 7414841 to 7414874 labelled f1_1(3)
- 7414841 to 7414875 labelled f1_1(3)
- 7414841 to 7414860 labelled f1_1(3)
- 7414841 to 7414876 labelled f1_1(4)
- 7414841 to 7414877 labelled f1_1(4)
- 7414841 to 7414872 labelled f1_1(4)
- 7414842 to 7414842 labelled #_1(0)
- 7414843 to 7414844 labelled f_1(0)
- 7414843 to 7414847 labelled g_1(1)
- 7414844 to 7414842 labelled f_1(0)
- 7414844 to 7414847 labelled g_1(1)
- 7414845 to 7414846 labelled f_1(1)
- 7414845 to 7414847 labelled g_1(1)
- 7414846 to 7414842 labelled f_1(1)
- 7414846 to 7414847 labelled g_1(1)
- 7414850 to 7414851 labelled f_1(1)
- 7414850 to 7414847 labelled g_1(1)
- 7414850 to 7414859 labelled g_1(2)
- 7414851 to 7414842 labelled f_1(1)
- 7414851 to 7414847 labelled g_1(1)
- 7414851 to 7414848 labelled f_1(1)
- 7414848 to 7414849 labelled g_1(1)
- 7414849 to 7414850 labelled f_1(1)
- 7414849 to 7414854 labelled g_1(2)
- 7414847 to 7414848 labelled g_1(1)
- 7414852 to 7414853 labelled f_1(2)
- 7414852 to 7414859 labelled g_1(2)
- 7414852 to 7414866 labelled g_1(3)
- 7414853 to 7414848 labelled f_1(2)
- 7414853 to 7414854 labelled f_1(2)
- 7414858 to 7414848 labelled f_1(2)
- 7414854 to 7414855 labelled g_1(2)
- 7414855 to 7414856 labelled g_1(2)
- 7414857 to 7414858 labelled f_1(2)
- 7414857 to 7414859 labelled g_1(2)
- 7414856 to 7414857 labelled f_1(2)
- 7414859 to 7414860 labelled g_1(2)
- 7414860 to 7414861 labelled g_1(2)
- 7414863 to 7414854 labelled f_1(2)
- 7414861 to 7414862 labelled f_1(2)
- 7414862 to 7414863 labelled f_1(2)
- 7414862 to 7414866 labelled g_1(3)
- 7414864 to 7414865 labelled f_1(3)
- 7414865 to 7414856 labelled f_1(3)
- 7414865 to 7414871 labelled g_1(3)
- 7414870 to 7414856 labelled f_1(3)
- 7414870 to 7414871 labelled g_1(3)
- 7414869 to 7414870 labelled f_1(3)
- 7414866 to 7414867 labelled g_1(3)
- 7414867 to 7414868 labelled g_1(3)
- 7414868 to 7414869 labelled f_1(3)
- 7414868 to 7414878 labelled g_1(4)
- 7414874 to 7414875 labelled f_1(3)
- 7414875 to 7414860 labelled f_1(3)
- 7414871 to 7414872 labelled g_1(3)
- 7414872 to 7414873 labelled g_1(3)
- 7414873 to 7414874 labelled f_1(3)
- 7414876 to 7414877 labelled f_1(4)
- 7414877 to 7414872 labelled f_1(4)
- 7414878 to 7414879 labelled g_1(4)
- 7414881 to 7414882 labelled f_1(4)
- 7414882 to 7414872 labelled f_1(4)
- 7414880 to 7414881 labelled f_1(4)
- 7414879 to 7414880 labelled g_1(4)
(10) TRUE