Termination w.r.t. Q proof of /tmp/tmpfMlZ9Y/z082.srs

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(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ DependencyPairsProof

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

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

The set Q is empty.
We have obtained the following QTRS:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ RFCMatchBoundsTRSProof

  ↳ DependencyPairsProof

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

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:

a(c(a(x))) → c(a(c(x)))
b(a(a(x))) → b(d(a(x)))
b(a(x)) → a(a(b(x)))
d(d(x)) → b(d(a(x)))
b(b(x)) → c(b(x))
c(d(a(x))) → a(c(x))
c(b(x)) → a(a(a(x)))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

108, 109, 110, 112, 111, 113, 114, 115, 117, 116, 119, 118, 120, 121, 123, 122, 125, 124, 127, 126, 129, 128, 131, 130, 133, 132, 135, 134, 137, 136, 153, 152, 155, 154, 160, 158, 175, 174, 184, 183

Node 108 is start node and node 109 is final node.

Those nodes are connect through the following edges:

108 to 110 labelled a_1(0), c_1(1)
108 to 111 labelled a_1(0)
108 to 113 labelled b_1(0)
108 to 108 labelled c_1(0)
108 to 112 labelled c_1(0)
108 to 122 labelled a_1(1)
108 to 116 labelled a_1(1)
108 to 126 labelled c_1(1)
108 to 134 labelled c_1(2)
109 to 109 labelled #_1(0)
110 to 109 labelled c_1(0)
110 to 115 labelled a_1(1)
110 to 116 labelled a_1(1)
110 to 110 labelled c_1(1)
110 to 128 labelled c_1(2)
110 to 134 labelled c_1(2)
112 to 109 labelled b_1(0), a_1(0)
112 to 118 labelled a_1(1)
112 to 120 labelled b_1(1)
112 to 119 labelled c_1(1)
112 to 110 labelled c_1(1)
112 to 124 labelled a_1(2)
112 to 136 labelled c_1(2)
112 to 152 labelled c_1(3)
111 to 112 labelled a_1(0)
111 to 126 labelled c_1(1)
113 to 114 labelled d_1(0)
114 to 109 labelled a_1(0)
114 to 110 labelled c_1(1)
115 to 109 labelled c_1(1)
115 to 115 labelled a_1(1)
115 to 116 labelled a_1(1)
115 to 110 labelled c_1(1)
115 to 127 labelled c_1(1)
115 to 128 labelled c_1(2)
115 to 134 labelled c_1(2)
115 to 129 labelled c_1(1)
115 to 135 labelled c_1(1)
117 to 109 labelled a_1(1)
117 to 110 labelled c_1(1)
117 to 120 labelled a_1(1)
116 to 117 labelled a_1(1)
116 to 128 labelled c_1(2)
119 to 109 labelled b_1(1)
119 to 118 labelled a_1(1)
119 to 120 labelled b_1(1)
119 to 119 labelled c_1(1)
119 to 124 labelled a_1(2)
119 to 136 labelled c_1(2)
119 to 152 labelled c_1(3)
118 to 119 labelled a_1(1)
118 to 130 labelled c_1(2)
120 to 121 labelled d_1(1)
121 to 109 labelled a_1(1)
121 to 110 labelled c_1(1)
123 to 113 labelled a_1(1)
122 to 123 labelled a_1(1)
125 to 109 labelled a_1(2)
125 to 120 labelled a_1(2)
125 to 110 labelled c_1(1)
124 to 125 labelled a_1(2)
124 to 128 labelled c_1(2)
127 to 116 labelled c_1(1)
127 to 115 labelled c_1(1)
127 to 118 labelled c_1(1)
127 to 124 labelled c_1(1)
127 to 137 labelled c_1(1)
127 to 153 labelled c_1(1)
126 to 127 labelled a_1(1)
126 to 128 labelled c_1(2)
126 to 132 labelled c_1(2)
129 to 116 labelled c_1(2), a_1(1)
129 to 115 labelled c_1(2), a_1(1)
129 to 117 labelled c_1(2)
129 to 109 labelled c_1(2)
129 to 120 labelled c_1(2)
129 to 129 labelled a_1(2)
129 to 125 labelled c_1(2)
129 to 135 labelled c_1(2)
129 to 110 labelled c_1(1)
129 to 128 labelled c_1(2)
129 to 134 labelled c_1(2)
129 to 174 labelled c_1(3)
129 to 152 labelled c_1(3)
129 to 158 labelled c_1(3)
128 to 129 labelled a_1(2)
128 to 128 labelled c_1(2)
128 to 110 labelled c_1(1)
128 to 174 labelled c_1(3)
128 to 152 labelled c_1(3)
128 to 158 labelled c_1(3)
131 to 118 labelled c_1(2)
131 to 124 labelled c_1(2)
131 to 137 labelled c_1(2)
131 to 153 labelled c_1(2)
130 to 131 labelled a_1(2)
130 to 132 labelled c_1(2)
130 to 154 labelled c_1(3)
133 to 119 labelled c_1(2)
133 to 124 labelled a_1(2)
133 to 152 labelled c_1(3)
132 to 133 labelled a_1(2)
132 to 130 labelled c_1(2)
132 to 158 labelled c_1(3)
135 to 129 labelled c_1(2)
134 to 135 labelled a_1(2)
134 to 128 labelled c_1(2)
134 to 152 labelled c_1(3)
137 to 131 labelled c_1(2)
136 to 137 labelled a_1(2)
153 to 129 labelled c_1(3)
153 to 135 labelled c_1(3)
153 to 175 labelled c_1(3)
153 to 160 labelled c_1(3)
152 to 153 labelled a_1(3)
152 to 128 labelled c_1(2)
152 to 152 labelled c_1(3)
155 to 125 labelled c_1(3)
154 to 155 labelled a_1(3)
154 to 174 labelled c_1(3)
160 to 124 labelled c_1(3)
160 to 153 labelled c_1(3)
158 to 160 labelled a_1(3)
158 to 154 labelled c_1(3)
175 to 109 labelled c_1(3)
175 to 120 labelled c_1(3)
175 to 115 labelled a_1(1)
175 to 116 labelled a_1(1)
175 to 129 labelled a_1(2)
175 to 128 labelled c_1(2)
175 to 174 labelled c_1(3)
175 to 134 labelled c_1(2)
175 to 152 labelled c_1(3)
175 to 158 labelled c_1(3)
175 to 110 labelled c_1(1)
174 to 175 labelled a_1(3)
174 to 110 labelled c_1(1)
174 to 128 labelled c_1(2)
174 to 152 labelled c_1(3)
174 to 183 labelled c_1(4)
184 to 175 labelled c_1(4)
184 to 153 labelled c_1(4)
184 to 160 labelled c_1(4)
183 to 184 labelled a_1(4)
183 to 128 labelled c_1(2)
183 to 152 labelled c_1(3)

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(a(b(x1))) → D(b(x1))
B(b(x1)) → B(c(x1))
D(d(x1)) → B(x1)
A(a(b(x1))) → A(d(b(x1)))
D(d(x1)) → A(d(b(x1)))
B(c(x1)) → A(a(x1))
A(b(x1)) → A(x1)
B(c(x1)) → A(x1)
A(c(a(x1))) → A(c(x1))
B(c(x1)) → A(a(a(x1)))
A(b(x1)) → B(a(a(x1)))
A(b(x1)) → A(a(x1))
D(d(x1)) → D(b(x1))
A(d(c(x1))) → A(x1)

The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

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

A(a(b(x1))) → D(b(x1))
B(b(x1)) → B(c(x1))
D(d(x1)) → B(x1)
A(a(b(x1))) → A(d(b(x1)))
D(d(x1)) → A(d(b(x1)))
B(c(x1)) → A(a(x1))
A(b(x1)) → A(x1)
B(c(x1)) → A(x1)
A(c(a(x1))) → A(c(x1))
B(c(x1)) → A(a(a(x1)))
A(b(x1)) → B(a(a(x1)))
A(b(x1)) → A(a(x1))
D(d(x1)) → D(b(x1))
A(d(c(x1))) → A(x1)

The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(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 4 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

          ↳ QDP

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

A(c(a(x1))) → A(c(x1))

The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ QTRS Reverse

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

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

A(c(a(x1))) → A(c(x1))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ QTRS Reverse

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

            ↳ UsableRulesProof

              ↳ QDP

          ↳ QDP

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

A(c(a(x1))) → A(c(x1))

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

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

B(c(x1)) → A(x1)
B(b(x1)) → B(c(x1))
B(c(x1)) → A(a(a(x1)))
A(b(x1)) → B(a(a(x1)))
A(a(b(x1))) → A(d(b(x1)))
A(b(x1)) → A(a(x1))
B(c(x1)) → A(a(x1))
A(d(c(x1))) → A(x1)
A(b(x1)) → A(x1)

The TRS R consists of the following rules:

a(c(a(x1))) → c(a(c(x1)))
a(a(b(x1))) → a(d(b(x1)))
a(b(x1)) → b(a(a(x1)))
d(d(x1)) → a(d(b(x1)))
b(b(x1)) → b(c(x1))
a(d(c(x1))) → c(a(x1))
b(c(x1)) → a(a(a(x1)))

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