(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) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
f1(
f(
g(
g(
x)))) →
f1(
f(
f(
x))) at position [0] we obtained the following new rules [LPAR04]:
f1(f(g(g(g(g(x0)))))) → f1(g(g(g(f(f(f(x0))))))) → f1(f(g(g(g(g(x0)))))) → f1(g(g(g(f(f(f(x0)))))))
f1(f(g(g(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0)))))))) → f1(f(g(g(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0))))))))
(10) 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(x)
f1(f(g(g(g(g(x0)))))) → f1(g(g(g(f(f(f(x0)))))))
f1(f(g(g(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0))))))))
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.
(11) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
f1(f(g(g(x)))) → f1(x)
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0))))))))
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.
(13) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
f1(
f(
g(
g(
x)))) →
f1(
x) we obtained the following new rules [LPAR04]:
f1(f(g(g(f(g(g(y_0))))))) → f1(f(g(g(y_0)))) → f1(f(g(g(f(g(g(y_0))))))) → f1(f(g(g(y_0))))
f1(f(g(g(f(g(g(f(g(g(y_0)))))))))) → f1(f(g(g(f(g(g(y_0))))))) → f1(f(g(g(f(g(g(f(g(g(y_0)))))))))) → f1(f(g(g(f(g(g(y_0)))))))
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0))))))))
f1(f(g(g(f(g(g(y_0))))))) → f1(f(g(g(y_0))))
f1(f(g(g(f(g(g(f(g(g(y_0)))))))))) → f1(f(g(g(f(g(g(y_0)))))))
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.
(15) 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(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0))))))))
f1(f(g(g(f(g(g(y_0))))))) → f1(f(g(g(y_0))))
f1(f(g(g(f(g(g(f(g(g(y_0)))))))))) → f1(f(g(g(f(g(g(y_0)))))))
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(f(g(g(x0))))))) → f1(f(g(g(g(f(f(f(x0))))))))
f1(f(g(g(f(g(g(y_0))))))) → f1(f(g(g(y_0))))
f1(f(g(g(f(g(g(f(g(g(y_0)))))))))) → f1(f(g(g(f(g(g(y_0)))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241
Node 151 is start node and node 152 is final node.
Those nodes are connected through the following edges:
- 151 to 153 labelled f1_1(0)
- 151 to 154 labelled f1_1(0)
- 151 to 161 labelled f1_1(0)
- 151 to 171 labelled f1_1(1)
- 151 to 172 labelled f1_1(1)
- 151 to 179 labelled f1_1(1)
- 151 to 170 labelled f1_1(1)
- 151 to 185 labelled f1_1(2)
- 151 to 191 labelled f1_1(2)
- 151 to 203 labelled f1_1(3)
- 151 to 200 labelled f1_1(2)
- 151 to 219 labelled f1_1(3)
- 151 to 225 labelled f1_1(3)
- 151 to 231 labelled f1_1(4)
- 152 to 152 labelled #_1(0)
- 153 to 152 labelled f_1(0)
- 153 to 167 labelled g_1(1)
- 154 to 155 labelled f_1(0)
- 155 to 156 labelled g_1(0)
- 156 to 157 labelled g_1(0)
- 156 to 152 labelled g_1(0)
- 157 to 158 labelled g_1(0)
- 158 to 159 labelled f_1(0)
- 158 to 186 labelled g_1(1)
- 159 to 160 labelled f_1(0)
- 159 to 167 labelled g_1(1)
- 160 to 152 labelled f_1(0)
- 160 to 167 labelled g_1(1)
- 161 to 162 labelled f_1(0)
- 162 to 163 labelled g_1(0)
- 163 to 164 labelled g_1(0)
- 164 to 165 labelled f_1(0)
- 165 to 166 labelled g_1(0)
- 166 to 152 labelled g_1(0)
- 167 to 168 labelled g_1(1)
- 168 to 169 labelled g_1(1)
- 169 to 170 labelled f_1(1)
- 169 to 198 labelled g_1(2)
- 170 to 171 labelled f_1(1)
- 170 to 167 labelled g_1(1)
- 170 to 204 labelled g_1(2)
- 171 to 152 labelled f_1(1)
- 171 to 157 labelled f_1(1)
- 171 to 164 labelled f_1(1)
- 171 to 167 labelled g_1(1)
- 171 to 186 labelled f_1(1)
- 172 to 173 labelled f_1(1)
- 173 to 174 labelled g_1(1)
- 174 to 175 labelled g_1(1)
- 174 to 152 labelled g_1(1)
- 175 to 176 labelled g_1(1)
- 176 to 177 labelled f_1(1)
- 176 to 198 labelled g_1(2)
- 177 to 178 labelled f_1(1)
- 177 to 167 labelled g_1(1)
- 178 to 152 labelled f_1(1)
- 178 to 167 labelled g_1(1)
- 179 to 180 labelled f_1(1)
- 180 to 181 labelled g_1(1)
- 181 to 182 labelled g_1(1)
- 182 to 183 labelled f_1(1)
- 183 to 184 labelled g_1(1)
- 184 to 152 labelled g_1(1)
- 185 to 175 labelled f_1(2)
- 185 to 152 labelled f_1(2)
- 185 to 182 labelled f_1(2)
- 185 to 167 labelled g_1(1)
- 185 to 168 labelled f_1(2)
- 185 to 193 labelled g_1(2)
- 185 to 188 labelled f_1(2)
- 185 to 198 labelled f_1(2)
- 186 to 187 labelled g_1(1)
- 187 to 188 labelled g_1(1)
- 188 to 189 labelled f_1(1)
- 189 to 190 labelled f_1(1)
- 189 to 209 labelled g_1(2)
- 190 to 168 labelled f_1(1)
- 191 to 192 labelled f_1(2)
- 192 to 193 labelled g_1(2)
- 193 to 194 labelled g_1(2)
- 193 to 152 labelled g_1(2)
- 194 to 195 labelled g_1(2)
- 195 to 196 labelled f_1(2)
- 195 to 198 labelled g_1(2)
- 196 to 197 labelled f_1(2)
- 196 to 167 labelled g_1(1)
- 197 to 152 labelled f_1(2)
- 197 to 167 labelled g_1(1)
- 197 to 210 labelled f_1(2)
- 198 to 199 labelled g_1(2)
- 199 to 200 labelled g_1(2)
- 200 to 201 labelled f_1(2)
- 201 to 202 labelled f_1(2)
- 201 to 209 labelled g_1(2)
- 202 to 168 labelled f_1(2)
- 203 to 194 labelled f_1(3)
- 203 to 152 labelled f_1(3)
- 203 to 167 labelled g_1(1)
- 203 to 200 labelled f_1(3)
- 203 to 198 labelled f_1(3)
- 203 to 221 labelled g_1(3)
- 204 to 205 labelled g_1(2)
- 205 to 206 labelled g_1(2)
- 206 to 207 labelled f_1(2)
- 206 to 226 labelled g_1(3)
- 207 to 208 labelled f_1(2)
- 208 to 188 labelled f_1(2)
- 208 to 193 labelled g_1(2)
- 209 to 210 labelled g_1(2)
- 210 to 211 labelled g_1(2)
- 211 to 212 labelled f_1(2)
- 212 to 213 labelled f_1(2)
- 212 to 214 labelled g_1(3)
- 213 to 198 labelled f_1(2)
- 214 to 215 labelled g_1(3)
- 215 to 216 labelled g_1(3)
- 216 to 217 labelled f_1(3)
- 216 to 237 labelled g_1(4)
- 217 to 218 labelled f_1(3)
- 218 to 200 labelled f_1(3)
- 218 to 221 labelled g_1(3)
- 219 to 220 labelled f_1(3)
- 220 to 221 labelled g_1(3)
- 221 to 222 labelled g_1(3)
- 221 to 210 labelled g_1(3)
- 222 to 223 labelled g_1(3)
- 223 to 224 labelled f_1(3)
- 224 to 225 labelled f_1(3)
- 225 to 210 labelled f_1(3)
- 226 to 227 labelled g_1(3)
- 227 to 228 labelled g_1(3)
- 228 to 229 labelled f_1(3)
- 228 to 198 labelled g_1(2)
- 229 to 230 labelled f_1(3)
- 229 to 167 labelled g_1(1)
- 229 to 232 labelled g_1(3)
- 230 to 194 labelled f_1(3)
- 230 to 152 labelled f_1(3)
- 230 to 167 labelled g_1(1)
- 231 to 222 labelled f_1(4)
- 231 to 210 labelled f_1(4)
- 232 to 233 labelled g_1(3)
- 233 to 234 labelled g_1(3)
- 234 to 235 labelled f_1(3)
- 235 to 236 labelled f_1(3)
- 235 to 214 labelled g_1(3)
- 236 to 198 labelled f_1(3)
- 237 to 238 labelled g_1(4)
- 238 to 239 labelled g_1(4)
- 239 to 240 labelled f_1(4)
- 240 to 241 labelled f_1(4)
- 241 to 222 labelled f_1(4)
- 241 to 210 labelled f_1(4)
(16) YES