Termination w.r.t. Q proof of /tmp/tmp8aMo7Y/dup12.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:

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

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ RRRPoloQTRSProof

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

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

Q is empty.

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

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

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

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

Used ordering:
Polynomial interpretation [25]:

POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 2 + 2·x₁
POL(c(x₁)) = 2 + 2·x₁
POL(d(x₁)) = x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

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

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

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

The TRS R consists of the following rules:

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

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

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

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

The TRS R consists of the following rules:

b(b(d(d(b(b(x1)))))) → c(c(d(d(b(b(x1))))))
a(a(d(d(x1)))) → d(d(c(c(x1))))
b(b(b(b(b(b(x1)))))) → a(a(b(b(c(c(x1))))))
d(d(c(c(x1)))) → b(b(d(d(x1))))
d(d(c(c(x1)))) → d(d(b(b(d(d(x1))))))
d(d(a(a(c(c(x1)))))) → b(b(b(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 1 SCC with 12 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

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

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

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

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

              ↳ UsableRulesProof

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

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(x1)

Used ordering: POLO with Polynomial interpretation [25]:

POL(D(x₁)) = x₁
POL(a(x₁)) = 1 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(c(x₁)) = 1 + 2·x₁
POL(d(x₁)) = x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

              ↳ UsableRulesProof

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

D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))

The TRS R consists of the following rules:

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

D(d(c(c(x1)))) → D(b(b(d(d(x1)))))

The remaining pairs can at least be oriented weakly.

D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))

Used ordering: Polynomial Order [21,25] with Interpretation:

POL( c(x₁) ) = max{0, -1}

POL( d(x₁) ) = 1

POL( b(x₁) ) = max{0, -1}

POL( D(x₁) ) = x₁ + 1

POL( a(x₁) ) = max{0, -1}

The following usable rules [17] were oriented:

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

              ↳ UsableRulesProof

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

D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(d(c(c(x1)))) → D(d(b(b(d(d(x1)))))) at position [0] we obtained the following new rules:

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(b(b(b(b(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

              ↳ UsableRulesProof

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

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(b(b(b(b(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(d(c(c(a(a(c(c(x0)))))))) → D(d(b(b(b(b(b(b(x0)))))))) at position [0] we obtained the following new rules:

D(d(c(c(a(a(c(c(b(b(b(b(b(x0))))))))))))) → D(d(b(b(b(b(b(a(a(b(b(c(c(x0)))))))))))))
D(d(c(c(a(a(c(c(b(b(b(x0))))))))))) → D(d(b(b(b(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(a(a(c(c(b(d(d(b(b(x0))))))))))))) → D(d(b(b(b(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(a(a(c(c(b(x0))))))))) → D(d(b(a(a(b(b(c(c(x0)))))))))
D(d(c(c(a(a(c(c(b(b(b(b(x0)))))))))))) → D(d(b(b(b(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(a(a(c(c(d(d(b(b(x0)))))))))))) → D(d(b(b(b(b(c(c(d(d(b(b(x0))))))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(a(a(b(b(c(c(x0))))))))
D(d(c(c(a(a(c(c(b(b(x0)))))))))) → D(d(b(b(a(a(b(b(c(c(x0))))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

              ↳ UsableRulesProof

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

D(d(c(c(a(a(c(c(b(b(b(x0))))))))))) → D(d(b(b(b(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(a(a(c(c(b(d(d(b(b(x0))))))))))))) → D(d(b(b(b(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(a(a(c(c(b(x0))))))))) → D(d(b(a(a(b(b(c(c(x0)))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(a(a(c(c(x0)))))))) → D(d(a(a(b(b(c(c(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(a(a(c(c(b(b(b(b(b(x0))))))))))))) → D(d(b(b(b(b(b(a(a(b(b(c(c(x0)))))))))))))
D(d(c(c(a(a(c(c(b(b(b(b(x0)))))))))))) → D(d(b(b(b(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(a(a(c(c(d(d(b(b(x0)))))))))))) → D(d(b(b(b(b(c(c(d(d(b(b(x0))))))))))))
D(d(c(c(a(a(c(c(b(b(x0)))))))))) → D(d(b(b(a(a(b(b(c(c(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 8 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

              ↳ UsableRulesProof

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

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0)))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule D(d(c(c(d(a(a(c(c(x0))))))))) → D(d(b(b(d(b(b(b(b(x0))))))))) at position [0] we obtained the following new rules:

D(d(c(c(d(a(a(c(c(b(b(x0))))))))))) → D(d(b(b(d(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(d(a(a(c(c(b(d(d(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(c(c(d(d(b(b(x0))))))))))))))
D(d(c(c(d(a(a(c(c(d(d(b(b(x0))))))))))))) → D(d(b(b(d(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(x0)))))))))))) → D(d(b(b(d(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(a(a(b(b(c(c(x0))))))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(x0))))))))))))) → D(d(b(b(d(b(b(a(a(b(b(c(c(x0)))))))))))))

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

              ↳ UsableRulesProof

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

D(d(c(c(d(a(a(c(c(d(d(b(b(x0))))))))))))) → D(d(b(b(d(b(b(c(c(d(d(b(b(x0)))))))))))))
D(d(c(c(d(a(a(c(c(b(d(d(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(c(c(d(d(b(b(x0))))))))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(b(x0)))))))))))))) → D(d(b(b(d(b(b(b(a(a(b(b(c(c(x0))))))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(d(a(a(c(c(b(b(b(b(x0))))))))))))) → D(d(b(b(d(b(b(a(a(b(b(c(c(x0)))))))))))))
D(d(c(c(d(a(a(c(c(b(b(x0))))))))))) → D(d(b(b(d(a(a(b(b(c(c(x0)))))))))))
D(d(c(c(d(a(a(c(c(b(b(b(x0)))))))))))) → D(d(b(b(d(b(a(a(b(b(c(c(x0))))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

              ↳ UsableRulesProof

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

D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(b(b(d(d(x0)))))))))
D(d(c(c(d(c(c(x0))))))) → D(d(b(b(d(d(d(b(b(d(d(x0)))))))))))
D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R. Interpretation over the domain with elements from 0 to 1.c: 0
D: 0
a: 0
b: 0
d: 1 + x₀
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.1(d.0(d.1(x0))))))))))
D.1(d.0(c.0(c.0(b.0(b.1(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.1(x0))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.0(d.1(d.0(x0))))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))))
D.1(d.0(c.0(c.0(b.0(b.0(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.0(d.1(d.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.1(d.0(d.1(x0))))))))

The TRS R consists of the following rules:

b.0(b.0(b.0(b.0(b.0(b.0(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.0(x1))))))
b.0(b.0(d.1(d.0(b.0(b.0(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.0(x1))))))
d.1(d.0(a.0(a.0(c.0(c.0(x1)))))) → b.0(b.0(b.0(b.0(x1))))
d.1(d.0(c.0(c.1(x1)))) → b.0(b.1(d.0(d.1(x1))))
b.0(b.0(d.1(d.0(b.0(b.1(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.1(x1))))))
d.1(d.0(a.0(a.0(c.0(c.1(x1)))))) → b.0(b.0(b.0(b.1(x1))))
d.1(d.0(c.0(c.1(x1)))) → d.1(d.0(b.0(b.1(d.0(d.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → b.0(b.0(d.1(d.0(x1))))
b.0(b.0(b.0(b.0(b.0(b.1(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → d.1(d.0(b.0(b.0(d.1(d.0(x1))))))

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                              ↳ SemLabProof2

              ↳ UsableRulesProof

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

D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.1(d.0(d.1(x0))))))))))
D.1(d.0(c.0(c.0(b.0(b.1(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.1(x0))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.0(d.1(d.0(x0))))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.0(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.0(d.1(d.0(x0)))))))))))
D.1(d.0(c.0(c.0(b.0(b.0(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(d.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.0(d.1(d.0(x0))))))))
D.1(d.0(c.0(c.1(d.0(c.0(c.1(x0))))))) → D.1(d.0(b.0(b.1(d.0(b.0(b.1(d.0(d.1(x0)))))))))
D.1(d.0(c.0(c.0(c.0(c.1(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.1(d.0(d.1(x0))))))))

The TRS R consists of the following rules:

b.0(b.0(b.0(b.0(b.0(b.0(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.0(x1))))))
b.0(b.0(d.1(d.0(b.0(b.0(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.0(x1))))))
d.1(d.0(a.0(a.0(c.0(c.0(x1)))))) → b.0(b.0(b.0(b.0(x1))))
d.1(d.0(c.0(c.1(x1)))) → b.0(b.1(d.0(d.1(x1))))
b.0(b.0(d.1(d.0(b.0(b.1(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.1(x1))))))
d.1(d.0(a.0(a.0(c.0(c.1(x1)))))) → b.0(b.0(b.0(b.1(x1))))
d.1(d.0(c.0(c.1(x1)))) → d.1(d.0(b.0(b.1(d.0(d.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → b.0(b.0(d.1(d.0(x1))))
b.0(b.0(b.0(b.0(b.0(b.1(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → d.1(d.0(b.0(b.0(d.1(d.0(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 7 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                              ↳ SemLabProof2

              ↳ UsableRulesProof

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

D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(d.1(d.0(b.0(b.0(d.1(d.0(x0))))))))))
D.1(d.0(c.0(c.0(b.0(b.0(x0)))))) → D.1(d.0(c.0(c.0(d.1(d.0(b.0(b.0(x0))))))))
D.1(d.0(c.0(c.0(c.0(c.0(x0)))))) → D.1(d.0(b.0(b.0(b.0(b.0(d.1(d.0(x0))))))))

The TRS R consists of the following rules:

b.0(b.0(b.0(b.0(b.0(b.0(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.0(x1))))))
b.0(b.0(d.1(d.0(b.0(b.0(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.0(x1))))))
d.1(d.0(a.0(a.0(c.0(c.0(x1)))))) → b.0(b.0(b.0(b.0(x1))))
d.1(d.0(c.0(c.1(x1)))) → b.0(b.1(d.0(d.1(x1))))
b.0(b.0(d.1(d.0(b.0(b.1(x1)))))) → c.0(c.0(d.1(d.0(b.0(b.1(x1))))))
d.1(d.0(a.0(a.0(c.0(c.1(x1)))))) → b.0(b.0(b.0(b.1(x1))))
d.1(d.0(c.0(c.1(x1)))) → d.1(d.0(b.0(b.1(d.0(d.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → b.0(b.0(d.1(d.0(x1))))
b.0(b.0(b.0(b.0(b.0(b.1(x1)))))) → a.0(a.0(b.0(b.0(c.0(c.1(x1))))))
d.1(d.0(c.0(c.0(x1)))) → d.1(d.0(b.0(b.0(d.1(d.0(x1))))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
As can be seen after transforming the QDP problem by semantic labelling [33] and then some rule deleting processors, only certain labelled rules and pairs can be used. Hence, we only have to consider all unlabelled pairs and rules (without the decreasing rules for quasi-models).

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

                                                ↳ QDP

                                                  ↳ QDPToSRSProof

              ↳ UsableRulesProof

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

D(d(c(c(b(b(x0)))))) → D(d(c(c(d(d(b(b(x0))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(d(d(b(b(d(d(x0))))))))))
D(d(c(c(c(c(x0)))))) → D(d(b(b(b(b(d(d(x0))))))))

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The finiteness of this DP problem is implied by strong termination of a SRS due to [12].

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

                                                ↳ QDP

                                                  ↳ QDPToSRSProof

                                                    ↳ QTRS

                                                      ↳ QTRS Reverse

              ↳ UsableRulesProof

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ SemLabProof

                                              ↳ SemLabProof2

                                                ↳ QDP

                                                  ↳ QDPToSRSProof

                                                    ↳ QTRS

                                                      ↳ QTRS Reverse

                                                        ↳ QTRS

                                                          ↳ RFCMatchBoundsTRSProof

              ↳ UsableRulesProof

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

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

Q is empty.

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

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

5748, 5749, 5754, 5753, 5752, 5751, 5750, 5761, 5762, 5760, 5757, 5758, 5756, 5763, 5759, 5755, 5764, 5765, 5766, 5767, 5768, 5773, 5774, 5772, 5771, 5770, 5775, 5769, 5776, 5777, 5782, 5781, 5778, 5779, 5780, 5785, 5784, 5783, 5790, 5789, 5788, 5787, 5786, 5791, 5792, 5793, 5794, 5795, 5796, 5797, 5802, 5801, 5798, 5799, 5800, 5809, 5810, 5808, 5805, 5806, 5804, 5811, 5807, 5803, 5816, 5817, 5815, 5814, 5813, 5818, 5812, 5821, 5820, 5819, 5825, 5826, 5829, 5828, 5827, 5830, 5831, 5832, 5833, 5834, 5840, 5841, 5844, 5843, 5842

Node 5748 is start node and node 5749 is final node.

Those nodes are connect through the following edges:

5748 to 5750 labelled c_1(0)
5748 to 5755 labelled d_1(0)
5748 to 5764 labelled b_1(0)
5748 to 5769 labelled d_1(0)
5748 to 5776 labelled b_1(0)
5748 to 5783 labelled b_1(0)
5748 to 5786 labelled c_1(1)
5748 to 5830 labelled b_1(1)
5749 to 5749 labelled #_1(0)
5754 to 5749 labelled a_1(0)
5753 to 5754 labelled a_1(0)
5752 to 5753 labelled b_1(0)
5751 to 5752 labelled b_1(0)
5750 to 5751 labelled c_1(0)
5761 to 5762 labelled b_1(0)
5762 to 5763 labelled d_1(0)
5760 to 5761 labelled b_1(0)
5757 to 5758 labelled b_1(0)
5757 to 5749 labelled b_1(0)
5757 to 5786 labelled c_1(1)
5757 to 5791 labelled b_1(1)
5757 to 5796 labelled b_1(1)
5757 to 5840 labelled b_1(2)
5758 to 5759 labelled d_1(0)
5756 to 5757 labelled b_1(0)
5756 to 5786 labelled c_1(1)
5756 to 5791 labelled b_1(1)
5756 to 5796 labelled b_1(1)
5756 to 5840 labelled b_1(2)
5763 to 5749 labelled D_1(0)
5759 to 5760 labelled d_1(0)
5759 to 5749 labelled d_1(0)
5755 to 5756 labelled d_1(0)
5764 to 5765 labelled b_1(0)
5765 to 5766 labelled d_1(0)
5766 to 5767 labelled d_1(0)
5767 to 5768 labelled c_1(0)
5767 to 5803 labelled d_1(1)
5767 to 5812 labelled d_1(1)
5767 to 5819 labelled b_1(1)
5767 to 5786 labelled c_1(1)
5768 to 5749 labelled c_1(0)
5768 to 5803 labelled d_1(1)
5768 to 5812 labelled d_1(1)
5768 to 5819 labelled b_1(1)
5768 to 5786 labelled c_1(1)
5773 to 5774 labelled b_1(0)
5774 to 5775 labelled d_1(0)
5772 to 5773 labelled b_1(0)
5771 to 5772 labelled b_1(0)
5770 to 5771 labelled b_1(0)
5775 to 5749 labelled D_1(0)
5769 to 5770 labelled d_1(0)
5776 to 5777 labelled b_1(0)
5777 to 5778 labelled d_1(0)
5782 to 5749 labelled D_1(0)
5781 to 5782 labelled d_1(0)
5778 to 5779 labelled d_1(0)
5779 to 5780 labelled c_1(0)
5780 to 5781 labelled c_1(0)
5785 to 5749 labelled b_1(0)
5785 to 5786 labelled c_1(1)
5785 to 5791 labelled b_1(1)
5785 to 5796 labelled b_1(1)
5785 to 5840 labelled b_1(2)
5784 to 5785 labelled b_1(0)
5784 to 5786 labelled c_1(1)
5784 to 5791 labelled b_1(1)
5784 to 5796 labelled b_1(1)
5784 to 5840 labelled b_1(2)
5783 to 5784 labelled b_1(0)
5783 to 5786 labelled c_1(1)
5790 to 5749 labelled a_1(1)
5789 to 5790 labelled a_1(1)
5788 to 5789 labelled b_1(1)
5787 to 5788 labelled b_1(1)
5786 to 5787 labelled c_1(1)
5791 to 5792 labelled b_1(1)
5792 to 5793 labelled d_1(1)
5793 to 5794 labelled d_1(1)
5794 to 5795 labelled c_1(1)
5794 to 5803 labelled d_1(1)
5794 to 5812 labelled d_1(1)
5794 to 5819 labelled b_1(1)
5794 to 5786 labelled c_1(1)
5795 to 5749 labelled c_1(1)
5795 to 5803 labelled d_1(1)
5795 to 5812 labelled d_1(1)
5795 to 5819 labelled b_1(1)
5795 to 5786 labelled c_1(1)
5796 to 5797 labelled b_1(1)
5797 to 5798 labelled d_1(1)
5802 to 5749 labelled D_1(1)
5801 to 5802 labelled d_1(1)
5798 to 5799 labelled d_1(1)
5799 to 5800 labelled c_1(1)
5800 to 5801 labelled c_1(1)
5800 to 5762 labelled c_1(1)
5809 to 5810 labelled b_1(1)
5810 to 5811 labelled d_1(1)
5808 to 5809 labelled b_1(1)
5805 to 5806 labelled b_1(1)
5805 to 5749 labelled b_1(1)
5805 to 5786 labelled c_1(1)
5805 to 5791 labelled b_1(1)
5805 to 5796 labelled b_1(1)
5805 to 5840 labelled b_1(2)
5806 to 5807 labelled d_1(1)
5804 to 5805 labelled b_1(1)
5804 to 5786 labelled c_1(1)
5804 to 5791 labelled b_1(1)
5804 to 5796 labelled b_1(1)
5804 to 5825 labelled b_1(2)
5804 to 5840 labelled b_1(2)
5811 to 5749 labelled D_1(1)
5807 to 5808 labelled d_1(1)
5807 to 5749 labelled d_1(1)
5803 to 5804 labelled d_1(1)
5816 to 5817 labelled b_1(1)
5817 to 5818 labelled d_1(1)
5815 to 5816 labelled b_1(1)
5814 to 5815 labelled b_1(1)
5813 to 5814 labelled b_1(1)
5818 to 5749 labelled D_1(1)
5812 to 5813 labelled d_1(1)
5821 to 5749 labelled b_1(1)
5821 to 5786 labelled c_1(1)
5821 to 5791 labelled b_1(1)
5821 to 5796 labelled b_1(1)
5821 to 5840 labelled b_1(2)
5820 to 5821 labelled b_1(1)
5820 to 5786 labelled c_1(1)
5820 to 5791 labelled b_1(1)
5820 to 5796 labelled b_1(1)
5820 to 5840 labelled b_1(2)
5819 to 5820 labelled b_1(1)
5819 to 5786 labelled c_1(1)
5825 to 5826 labelled b_1(2)
5826 to 5827 labelled d_1(2)
5829 to 5810 labelled c_1(2)
5828 to 5829 labelled c_1(2)
5827 to 5828 labelled d_1(2)
5830 to 5831 labelled b_1(1)
5831 to 5832 labelled d_1(1)
5832 to 5833 labelled d_1(1)
5833 to 5834 labelled c_1(1)
5834 to 5820 labelled c_1(1)
5840 to 5841 labelled b_1(2)
5841 to 5842 labelled d_1(2)
5844 to 5820 labelled c_1(2)
5843 to 5844 labelled c_1(2)
5842 to 5843 labelled d_1(2)

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

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

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

D(d(c(c(x1)))) → D(d(x1))
D(d(c(c(x1)))) → D(b(b(d(d(x1)))))
D(d(c(c(x1)))) → D(d(b(b(d(d(x1))))))
D(d(c(c(x1)))) → D(x1)

The TRS R consists of the following rules:

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

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