Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → B(b(a(a(x1))))
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
B(a(a(b(x1)))) → B(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
A(b(a(x1))) → B(a(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → B(b(a(a(x1))))
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
B(a(a(b(x1)))) → B(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
A(b(a(x1))) → B(a(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ RFCMatchBoundsDPProof
↳ QDP
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
B(a(a(b(x1)))) → B(a(b(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 5.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
B(a(a(b(x1)))) → B(a(b(x1)))
To find matches we regarded all rules of R and P:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
B(a(a(b(x1)))) → B(a(b(x1)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
191, 192, 194, 193, 196, 195, 199, 200, 198, 201, 197, 204, 205, 203, 206, 202, 208, 207, 211, 212, 210, 213, 209, 216, 217, 215, 218, 214, 220, 219, 222, 221, 227, 226, 223, 224, 225, 232, 231, 228, 229, 230, 233, 234, 235, 236, 237, 238, 239, 240
Node 191 is start node and node 192 is final node.
Those nodes are connect through the following edges:
- 191 to 193 labelled B_1(0)
- 191 to 197 labelled B_1(1)
- 192 to 192 labelled #_1(0)
- 194 to 192 labelled b_1(0)
- 194 to 195 labelled b_1(1)
- 194 to 207 labelled b_1(2)
- 194 to 202 labelled b_1(2)
- 194 to 214 labelled b_1(3)
- 194 to 219 labelled b_1(3)
- 194 to 209 labelled b_1(3)
- 193 to 194 labelled a_1(0)
- 193 to 197 labelled a_1(1)
- 196 to 192 labelled b_1(1)
- 196 to 195 labelled b_1(1)
- 196 to 207 labelled b_1(2)
- 196 to 202 labelled b_1(2)
- 196 to 214 labelled b_1(3)
- 196 to 219 labelled b_1(3)
- 196 to 209 labelled b_1(3)
- 195 to 196 labelled a_1(1)
- 195 to 197 labelled a_1(1)
- 195 to 202 labelled a_1(2)
- 199 to 200 labelled b_1(1)
- 199 to 195 labelled b_1(1)
- 199 to 207 labelled b_1(2)
- 199 to 202 labelled b_1(2)
- 199 to 206 labelled b_1(2)
- 199 to 209 labelled b_1(3)
- 199 to 214 labelled b_1(3)
- 199 to 219 labelled b_1(3)
- 200 to 201 labelled a_1(1)
- 198 to 199 labelled b_1(1)
- 201 to 192 labelled a_1(1)
- 201 to 197 labelled a_1(1)
- 201 to 196 labelled a_1(1)
- 201 to 202 labelled a_1(2), a_1(1)
- 201 to 208 labelled a_1(1)
- 201 to 203 labelled a_1(1)
- 201 to 214 labelled a_1(1)
- 201 to 215 labelled a_1(1)
- 201 to 209 labelled a_1(1)
- 201 to 220 labelled a_1(1)
- 201 to 210 labelled a_1(1)
- 201 to 219 labelled a_1(1)
- 197 to 198 labelled a_1(1)
- 204 to 205 labelled b_1(2)
- 204 to 221 labelled b_1(3)
- 204 to 207 labelled b_1(2)
- 204 to 214 labelled b_1(3)
- 204 to 213 labelled b_1(3)
- 204 to 219 labelled b_1(3)
- 204 to 233 labelled b_1(4)
- 204 to 209 labelled b_1(3)
- 204 to 223 labelled b_1(4)
- 204 to 228 labelled b_1(4)
- 204 to 231 labelled b_1(4)
- 204 to 239 labelled b_1(5)
- 204 to 237 labelled b_1(5)
- 205 to 206 labelled a_1(2)
- 203 to 204 labelled b_1(2)
- 206 to 197 labelled a_1(2), a_1(1)
- 206 to 196 labelled a_1(2)
- 206 to 202 labelled a_1(2)
- 206 to 208 labelled a_1(2)
- 206 to 209 labelled a_1(3), a_1(2)
- 206 to 214 labelled a_1(3), a_1(2)
- 206 to 220 labelled a_1(2)
- 206 to 215 labelled a_1(2)
- 206 to 219 labelled a_1(3), a_1(2)
- 206 to 210 labelled a_1(2)
- 202 to 203 labelled a_1(2)
- 208 to 199 labelled b_1(2)
- 208 to 195 labelled b_1(2), b_1(1)
- 208 to 192 labelled b_1(2)
- 208 to 219 labelled b_1(3), b_1(2)
- 208 to 207 labelled b_1(2)
- 208 to 214 labelled b_1(3), b_1(2)
- 208 to 202 labelled b_1(2)
- 208 to 209 labelled b_1(3), b_1(2)
- 208 to 216 labelled b_1(2)
- 208 to 211 labelled b_1(2)
- 207 to 208 labelled a_1(2)
- 207 to 197 labelled a_1(1)
- 207 to 202 labelled a_1(2)
- 207 to 214 labelled a_1(3)
- 207 to 209 labelled a_1(3)
- 207 to 219 labelled a_1(3)
- 211 to 212 labelled b_1(3)
- 211 to 235 labelled b_1(4)
- 211 to 221 labelled b_1(3)
- 211 to 207 labelled b_1(2)
- 211 to 214 labelled b_1(3)
- 211 to 233 labelled b_1(4)
- 211 to 209 labelled b_1(3)
- 211 to 219 labelled b_1(3)
- 211 to 223 labelled b_1(4)
- 211 to 228 labelled b_1(4)
- 211 to 239 labelled b_1(5)
- 211 to 237 labelled b_1(5)
- 212 to 213 labelled a_1(3)
- 210 to 211 labelled b_1(3)
- 213 to 208 labelled a_1(3)
- 213 to 202 labelled a_1(2)
- 213 to 214 labelled a_1(3)
- 213 to 209 labelled a_1(3)
- 213 to 228 labelled a_1(4)
- 213 to 197 labelled a_1(1)
- 213 to 233 labelled a_1(4)
- 213 to 219 labelled a_1(3)
- 209 to 210 labelled a_1(3)
- 216 to 217 labelled b_1(3)
- 216 to 231 labelled b_1(4)
- 216 to 219 labelled b_1(3)
- 216 to 233 labelled b_1(4)
- 217 to 218 labelled a_1(3)
- 215 to 216 labelled b_1(3)
- 218 to 202 labelled a_1(3)
- 218 to 203 labelled a_1(3)
- 218 to 220 labelled a_1(3)
- 214 to 215 labelled a_1(3)
- 220 to 204 labelled b_1(3)
- 219 to 220 labelled a_1(3)
- 222 to 207 labelled b_1(3), b_1(2)
- 222 to 233 labelled b_1(4)
- 222 to 199 labelled b_1(3)
- 222 to 195 labelled b_1(3), b_1(1)
- 222 to 192 labelled b_1(3)
- 222 to 202 labelled b_1(3), b_1(2)
- 222 to 219 labelled b_1(3)
- 222 to 214 labelled b_1(3)
- 222 to 209 labelled b_1(3)
- 222 to 231 labelled b_1(4)
- 221 to 222 labelled a_1(3)
- 221 to 202 labelled a_1(2)
- 221 to 209 labelled a_1(3)
- 221 to 214 labelled a_1(3)
- 221 to 223 labelled a_1(4)
- 221 to 228 labelled a_1(4)
- 221 to 197 labelled a_1(1)
- 221 to 233 labelled a_1(4)
- 227 to 214 labelled a_1(4)
- 227 to 234 labelled a_1(4)
- 227 to 209 labelled a_1(4)
- 226 to 227 labelled a_1(4)
- 223 to 224 labelled a_1(4)
- 223 to 233 labelled a_1(4)
- 224 to 225 labelled b_1(4)
- 224 to 219 labelled a_1(4)
- 224 to 209 labelled b_1(4)
- 224 to 232 labelled a_1(4)
- 225 to 226 labelled b_1(4)
- 225 to 237 labelled b_1(5)
- 232 to 220 labelled a_1(4)
- 232 to 215 labelled a_1(4)
- 232 to 204 labelled b_1(4)
- 232 to 210 labelled a_1(4)
- 231 to 232 labelled a_1(4)
- 228 to 229 labelled a_1(4)
- 229 to 230 labelled b_1(4)
- 230 to 231 labelled b_1(4)
- 230 to 233 labelled b_1(4)
- 233 to 234 labelled a_1(4)
- 234 to 216 labelled b_1(4)
- 234 to 211 labelled b_1(4)
- 235 to 236 labelled a_1(4)
- 235 to 228 labelled a_1(4)
- 235 to 233 labelled a_1(4)
- 236 to 219 labelled b_1(4)
- 236 to 214 labelled b_1(4)
- 237 to 238 labelled a_1(5)
- 238 to 211 labelled b_1(5)
- 238 to 216 labelled b_1(5)
- 239 to 240 labelled a_1(5)
- 240 to 230 labelled b_1(5)
- 240 to 204 labelled b_1(5)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
A(b(a(x1))) → A(a(x1))
The remaining pairs can at least be oriented weakly.
A(b(a(x1))) → A(b(b(a(a(x1)))))
Used ordering: Polynomial Order [21,25] with Interpretation:
POL( A(x1) ) = x1
POL( a(x1) ) = 0
POL( b(x1) ) = 1
The following usable rules [17] were oriented:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ RFCMatchBoundsDPProof
↳ QTRS Reverse
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(a(x1)))))
The TRS R consists of the following rules:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
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:
A(b(a(x1))) → A(b(b(a(a(x1)))))
To find matches we regarded all rules of R and P:
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
315, 316, 318, 319, 317, 320, 323, 324, 322, 325, 321, 327, 326, 330, 331, 329, 332, 328, 334, 333, 337, 338, 336, 339, 335, 342, 343, 341, 344, 340, 346, 345, 349, 350, 348, 351, 347, 353, 352, 355, 354, 356, 357, 358, 359
Node 315 is start node and node 316 is final node.
Those nodes are connect through the following edges:
- 315 to 317 labelled A_1(0)
- 316 to 316 labelled #_1(0)
- 318 to 319 labelled b_1(0)
- 318 to 326 labelled b_1(1)
- 318 to 333 labelled b_1(2)
- 318 to 328 labelled b_1(2)
- 318 to 335 labelled b_1(2)
- 319 to 320 labelled a_1(0)
- 317 to 318 labelled b_1(0)
- 320 to 316 labelled a_1(0)
- 320 to 321 labelled a_1(1)
- 323 to 324 labelled b_1(1)
- 323 to 326 labelled b_1(1)
- 323 to 333 labelled b_1(2)
- 323 to 328 labelled b_1(2)
- 323 to 335 labelled b_1(2)
- 324 to 325 labelled a_1(1)
- 322 to 323 labelled b_1(1)
- 325 to 316 labelled a_1(1)
- 325 to 321 labelled a_1(1)
- 321 to 322 labelled a_1(1)
- 327 to 316 labelled b_1(1)
- 327 to 326 labelled b_1(1)
- 327 to 333 labelled b_1(2)
- 327 to 328 labelled b_1(2)
- 327 to 335 labelled b_1(2)
- 326 to 327 labelled a_1(1)
- 326 to 321 labelled a_1(1)
- 326 to 328 labelled a_1(2)
- 326 to 335 labelled a_1(2)
- 330 to 331 labelled b_1(2)
- 330 to 345 labelled b_1(3)
- 330 to 333 labelled b_1(2)
- 330 to 347 labelled b_1(3)
- 330 to 356 labelled b_1(4)
- 330 to 352 labelled b_1(3)
- 330 to 340 labelled b_1(3)
- 331 to 332 labelled a_1(2)
- 331 to 321 labelled a_1(1)
- 331 to 347 labelled a_1(3)
- 331 to 328 labelled a_1(2)
- 331 to 340 labelled a_1(3)
- 331 to 335 labelled a_1(2)
- 329 to 330 labelled b_1(2)
- 332 to 321 labelled a_1(2), a_1(1)
- 332 to 327 labelled a_1(2)
- 332 to 335 labelled a_1(2), b_1(2)
- 332 to 340 labelled a_1(3)
- 332 to 328 labelled a_1(2), b_1(2)
- 332 to 326 labelled b_1(2), b_1(1)
- 332 to 316 labelled b_1(2)
- 332 to 333 labelled b_1(2)
- 332 to 352 labelled b_1(3)
- 332 to 356 labelled b_1(4)
- 328 to 329 labelled a_1(2)
- 334 to 323 labelled b_1(2)
- 333 to 334 labelled a_1(2)
- 337 to 338 labelled b_1(2)
- 337 to 354 labelled b_1(3)
- 337 to 352 labelled b_1(3)
- 337 to 356 labelled b_1(4)
- 338 to 339 labelled a_1(2)
- 336 to 337 labelled b_1(2)
- 339 to 328 labelled a_1(2)
- 339 to 334 labelled a_1(2)
- 339 to 329 labelled a_1(2)
- 339 to 336 labelled a_1(2)
- 335 to 336 labelled a_1(2)
- 342 to 343 labelled b_1(3)
- 342 to 354 labelled b_1(3)
- 342 to 352 labelled b_1(3)
- 342 to 358 labelled b_1(4)
- 342 to 356 labelled b_1(4)
- 343 to 344 labelled a_1(3)
- 341 to 342 labelled b_1(3)
- 344 to 334 labelled a_1(3)
- 344 to 329 labelled a_1(3)
- 344 to 336 labelled a_1(3)
- 344 to 353 labelled a_1(3)
- 344 to 340 labelled a_1(3)
- 344 to 357 labelled a_1(3)
- 340 to 341 labelled a_1(3)
- 346 to 333 labelled b_1(3)
- 346 to 328 labelled b_1(3)
- 345 to 346 labelled a_1(3)
- 345 to 340 labelled a_1(3)
- 349 to 350 labelled b_1(3)
- 350 to 351 labelled a_1(3)
- 348 to 349 labelled b_1(3)
- 351 to 335 labelled a_1(3)
- 351 to 328 labelled a_1(3)
- 347 to 348 labelled a_1(3)
- 353 to 330 labelled b_1(3)
- 353 to 337 labelled b_1(3)
- 353 to 335 labelled b_1(3)
- 352 to 353 labelled a_1(3)
- 352 to 340 labelled a_1(3)
- 355 to 323 labelled b_1(3)
- 354 to 355 labelled a_1(3)
- 356 to 357 labelled a_1(4)
- 357 to 342 labelled b_1(4)
- 358 to 359 labelled a_1(4)
- 358 to 340 labelled a_1(3)
- 359 to 330 labelled b_1(4)
- 359 to 337 labelled b_1(4)
- 359 to 335 labelled b_1(4)
We have reversed the following QTRS:
The set of rules R is
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
The set Q is empty.
We have obtained the following QTRS:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))
The set Q is empty.
We have obtained the following QTRS:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x))) → a(a(b(b(a(a(x))))))
b(a(a(b(x)))) → b(a(b(x)))
Q is empty.