Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(x, a(a(b(b(y))))) → f(a(a(a(b(b(b(x)))))), y)
f(a(x), y) → f(x, a(y))
f(b(x), y) → f(x, b(y))

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is none

The TRS R 2 is

f(x, a(a(b(b(y))))) → f(a(a(a(b(b(b(x)))))), y)
f(a(x), y) → f(x, a(y))
f(b(x), y) → f(x, b(y))

The signature Sigma is {f}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(x, a(a(b(b(y))))) → f(a(a(a(b(b(b(x)))))), y)
f(a(x), y) → f(x, a(y))
f(b(x), y) → f(x, b(y))

The set Q consists of the following terms:

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

(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:

F(x, a(a(b(b(y))))) → F(a(a(a(b(b(b(x)))))), y)
F(a(x), y) → F(x, a(y))
F(b(x), y) → F(x, b(y))

The TRS R consists of the following rules:

f(x, a(a(b(b(y))))) → f(a(a(a(b(b(b(x)))))), y)
f(a(x), y) → f(x, a(y))
f(b(x), y) → f(x, b(y))

The set Q consists of the following terms:

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

We have to consider all minimal (P,Q,R)-chains.

(5) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(x, a(a(b(b(y))))) → F(a(a(a(b(b(b(x)))))), y)
F(a(x), y) → F(x, a(y))
F(b(x), y) → F(x, b(y))

R is empty.
The set Q consists of the following terms:

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

We have to consider all minimal (P,Q,R)-chains.

(7) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(x, a(a(b(b(y))))) → F(a(a(a(b(b(b(x)))))), y)
F(a(x), y) → F(x, a(y))
F(b(x), y) → F(x, b(y))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(9) QDPToSRSProof (SOUND transformation)

The finiteness of this DP problem is implied by strong termination of a SRS due to [UNKNOWN].

(10) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

Q is empty.

(11) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

A(a(b(b(x)))) → A(a(a(x)))
A(a(b(b(x)))) → A(a(x))
A(a(b(b(x)))) → A(x)

The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

A(a(b(b(x)))) → A(a(a(x)))
A(a(b(b(x)))) → A(a(x))
A(a(b(b(x)))) → A(x)

The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

The set Q consists of the following terms:

a(a(b(b(x0))))

We have to consider all minimal (P,Q,R)-chains.

(15) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule A(a(b(b(x)))) → A(a(a(x))) at position [0] we obtained the following new rules [LPAR04]:

A(a(b(b(b(b(x0)))))) → A(b(b(b(a(a(a(x0)))))))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

A(a(b(b(x)))) → A(a(x))
A(a(b(b(x)))) → A(x)
A(a(b(b(b(b(x0)))))) → A(b(b(b(a(a(a(x0)))))))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))

The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

The set Q consists of the following terms:

a(a(b(b(x0))))

We have to consider all minimal (P,Q,R)-chains.

(17) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

A(a(b(b(x)))) → A(x)
A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))

The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

The set Q consists of the following terms:

a(a(b(b(x0))))

We have to consider all minimal (P,Q,R)-chains.

(19) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule A(a(b(b(x)))) → A(x) we obtained the following new rules [LPAR04]:

A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))
A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

The TRS R consists of the following rules:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))

The set Q consists of the following terms:

a(a(b(b(x0))))

We have to consider all minimal (P,Q,R)-chains.

(21) 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:

A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))
A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

To find matches we regarded all rules of R and P:

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))
A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))
A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

9575030, 9575031, 9575032, 9575038, 9575039, 9575035, 9575036, 9575033, 9575034, 9575037, 9575045, 9575043, 9575044, 9575040, 9575041, 9575042, 9575047, 9575048, 9575046, 9575049, 9575050, 9575051, 9575052, 9575054, 9575055, 9575056, 9575057, 9575053, 9575060, 9575061, 9575062, 9575063, 9575059, 9575058, 9575064, 9575067, 9575068, 9575065, 9575069, 9575066, 9575072, 9575073, 9575076, 9575075, 9575074, 9575071, 9575070, 9575077, 9575079, 9575080, 9575078, 9575082, 9575081, 9575086, 9575087, 9575084, 9575085, 9575083, 9575090, 9575091, 9575088, 9575092, 9575089, 9575093, 9575094, 9575095, 9575096, 9575097, 9575102, 9575101, 9575098, 9575099, 9575100, 9575105, 9575106, 9575108, 9575109, 9575107, 9575103, 9575104, 9575110, 9575115, 9575111, 9575112, 9575113, 9575114, 9575117, 9575118, 9575119, 9575120, 9575116

Node 9575030 is start node and node 9575031 is final node.

Those nodes are connect through the following edges:

• 9575030 to 9575032 labelled A_1(0)
• 9575030 to 9575033 labelled A_1(0)
• 9575030 to 9575040 labelled A_1(0)
• 9575030 to 9575050 labelled A_1(1)
• 9575030 to 9575051 labelled A_1(1)
• 9575030 to 9575058 labelled A_1(1)
• 9575030 to 9575061 labelled A_1(1)
• 9575030 to 9575056 labelled A_1(1)
• 9575030 to 9575064 labelled A_1(2)
• 9575030 to 9575055 labelled A_1(1)
• 9575030 to 9575070 labelled A_1(2)
• 9575030 to 9575077 labelled A_1(3)
• 9575030 to 9575097 labelled A_1(3)
• 9575030 to 9575086 labelled A_1(2)
• 9575030 to 9575080 labelled A_1(2)
• 9575030 to 9575103 labelled A_1(3)
• 9575030 to 9575110 labelled A_1(4)
• 9575030 to 9575109 labelled A_1(3)
• 9575030 to 9575115 labelled A_1(3)
• 9575031 to 9575031 labelled #_1(0)
• 9575032 to 9575031 labelled a_1(0)
• 9575032 to 9575046 labelled b_1(1)
• 9575038 to 9575039 labelled a_1(0)
• 9575038 to 9575046 labelled b_1(1)
• 9575039 to 9575031 labelled a_1(0)
• 9575039 to 9575046 labelled b_1(1)
• 9575035 to 9575036 labelled b_1(0)
• 9575035 to 9575031 labelled b_1(0)
• 9575036 to 9575037 labelled b_1(0)
• 9575033 to 9575034 labelled a_1(0)
• 9575034 to 9575035 labelled b_1(0)
• 9575037 to 9575038 labelled a_1(0)
• 9575037 to 9575065 labelled b_1(1)
• 9575045 to 9575031 labelled b_1(0)
• 9575043 to 9575044 labelled a_1(0)
• 9575044 to 9575045 labelled b_1(0)
• 9575040 to 9575041 labelled a_1(0)
• 9575041 to 9575042 labelled b_1(0)
• 9575042 to 9575043 labelled b_1(0)
• 9575047 to 9575048 labelled b_1(1)
• 9575048 to 9575049 labelled a_1(1)
• 9575048 to 9575078 labelled b_1(2)
• 9575046 to 9575047 labelled b_1(1)
• 9575049 to 9575050 labelled a_1(1)
• 9575049 to 9575046 labelled b_1(1)
• 9575049 to 9575083 labelled b_1(2)
• 9575050 to 9575031 labelled a_1(1)
• 9575050 to 9575036 labelled a_1(1)
• 9575050 to 9575043 labelled a_1(1)
• 9575050 to 9575046 labelled b_1(1)
• 9575050 to 9575065 labelled a_1(1)
• 9575051 to 9575052 labelled a_1(1)
• 9575052 to 9575053 labelled b_1(1)
• 9575054 to 9575055 labelled b_1(1)
• 9575055 to 9575056 labelled a_1(1)
• 9575055 to 9575078 labelled b_1(2)
• 9575056 to 9575057 labelled a_1(1)
• 9575056 to 9575046 labelled b_1(1)
• 9575057 to 9575031 labelled a_1(1)
• 9575057 to 9575046 labelled b_1(1)
• 9575053 to 9575054 labelled b_1(1)
• 9575053 to 9575031 labelled b_1(1)
• 9575060 to 9575061 labelled b_1(1)
• 9575061 to 9575062 labelled a_1(1)
• 9575062 to 9575063 labelled b_1(1)
• 9575063 to 9575031 labelled b_1(1)
• 9575059 to 9575060 labelled b_1(1)
• 9575058 to 9575059 labelled a_1(1)
• 9575064 to 9575031 labelled a_1(2)
• 9575064 to 9575061 labelled a_1(2)
• 9575064 to 9575054 labelled a_1(2)
• 9575064 to 9575046 labelled b_1(1)
• 9575064 to 9575047 labelled a_1(2)
• 9575064 to 9575072 labelled b_1(2)
• 9575064 to 9575078 labelled a_1(2)
• 9575064 to 9575067 labelled a_1(2)
• 9575064 to 9575098 labelled b_1(2)
• 9575067 to 9575068 labelled a_1(1)
• 9575068 to 9575069 labelled a_1(1)
• 9575068 to 9575088 labelled b_1(2)
• 9575065 to 9575066 labelled b_1(1)
• 9575069 to 9575047 labelled a_1(1)
• 9575066 to 9575067 labelled b_1(1)
• 9575072 to 9575073 labelled b_1(2)
• 9575072 to 9575031 labelled b_1(2)
• 9575073 to 9575074 labelled b_1(2)
• 9575076 to 9575031 labelled a_1(2)
• 9575076 to 9575046 labelled b_1(1)
• 9575075 to 9575076 labelled a_1(2)
• 9575075 to 9575046 labelled b_1(1)
• 9575074 to 9575075 labelled a_1(2)
• 9575074 to 9575078 labelled b_1(2)
• 9575071 to 9575072 labelled b_1(2)
• 9575070 to 9575071 labelled a_1(2)
• 9575077 to 9575073 labelled a_1(3)
• 9575077 to 9575031 labelled a_1(3)
• 9575077 to 9575046 labelled b_1(1)
• 9575077 to 9575078 labelled a_1(3)
• 9575079 to 9575080 labelled b_1(2)
• 9575080 to 9575081 labelled a_1(2)
• 9575078 to 9575079 labelled b_1(2)
• 9575082 to 9575047 labelled a_1(2)
• 9575081 to 9575082 labelled a_1(2)
• 9575081 to 9575088 labelled b_1(2)
• 9575086 to 9575087 labelled a_1(2)
• 9575087 to 9575067 labelled a_1(2)
• 9575087 to 9575098 labelled b_1(2)
• 9575084 to 9575085 labelled b_1(2)
• 9575085 to 9575086 labelled a_1(2)
• 9575085 to 9575111 labelled b_1(3)
• 9575083 to 9575084 labelled b_1(2)
• 9575090 to 9575091 labelled a_1(2)
• 9575091 to 9575092 labelled a_1(2)
• 9575091 to 9575093 labelled b_1(3)
• 9575088 to 9575089 labelled b_1(2)
• 9575092 to 9575078 labelled a_1(2)
• 9575089 to 9575090 labelled b_1(2)
• 9575093 to 9575094 labelled b_1(3)
• 9575094 to 9575095 labelled b_1(3)
• 9575095 to 9575096 labelled a_1(3)
• 9575095 to 9575116 labelled b_1(4)
• 9575096 to 9575097 labelled a_1(3)
• 9575097 to 9575080 labelled a_1(3)
• 9575097 to 9575105 labelled b_1(3)
• 9575102 to 9575089 labelled a_1(2)
• 9575101 to 9575102 labelled a_1(2)
• 9575098 to 9575099 labelled b_1(2)
• 9575099 to 9575100 labelled b_1(2)
• 9575100 to 9575101 labelled a_1(2)
• 9575105 to 9575106 labelled b_1(3)
• 9575105 to 9575089 labelled b_1(3)
• 9575106 to 9575107 labelled b_1(3)
• 9575108 to 9575109 labelled a_1(3)
• 9575109 to 9575089 labelled a_1(3)
• 9575107 to 9575108 labelled a_1(3)
• 9575103 to 9575104 labelled a_1(3)
• 9575104 to 9575105 labelled b_1(3)
• 9575110 to 9575089 labelled a_1(4)
• 9575110 to 9575106 labelled a_1(4)
• 9575115 to 9575099 labelled a_1(3)
• 9575111 to 9575112 labelled b_1(3)
• 9575112 to 9575113 labelled b_1(3)
• 9575113 to 9575114 labelled a_1(3)
• 9575114 to 9575115 labelled a_1(3)
• 9575117 to 9575118 labelled b_1(4)
• 9575118 to 9575119 labelled a_1(4)
• 9575119 to 9575120 labelled a_1(4)
• 9575120 to 9575089 labelled a_1(4)
• 9575120 to 9575106 labelled a_1(4)
• 9575116 to 9575117 labelled b_1(4)

(22) TRUE