Termination w.r.t. Q proof of /tmp/tmpy1QwAm/z083.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(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

Q is empty.

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

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

Used ordering:
Polynomial interpretation [25]:

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Used ordering: POLO with Polynomial interpretation [25]:

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

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

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

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

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPToSRSProof

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPToSRSProof

                                    ↳ QTRS

                                      ↳ QTRS Reverse

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

                ↳ QDP

                  ↳ RuleRemovalProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ Narrowing

                            ↳ QDP

                              ↳ DependencyGraphProof

                                ↳ QDP

                                  ↳ QDPToSRSProof

                                    ↳ QTRS

                                      ↳ QTRS Reverse

                                        ↳ QTRS

                                          ↳ RFCMatchBoundsTRSProof

              ↳ UsableRulesProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1428, 1429, 1430, 1431, 1432, 1434, 1435, 1433, 1436, 1437, 1440, 1441, 1438, 1439, 1442, 1443, 1444, 1445, 1446, 1448, 1449, 1447, 1450, 1453, 1454, 1451, 1452, 1455, 1456, 1457, 1458, 1459, 1460, 1461, 1462

Node 1428 is start node and node 1429 is final node.

Those nodes are connect through the following edges:

1428 to 1430 labelled b_1(0), d_1(0)
1428 to 1433 labelled d_1(0)
1428 to 1436 labelled c_1(0)
1428 to 1438 labelled d_1(0)
1428 to 1445 labelled c_1(1)
1428 to 1459 labelled b_1(1)
1429 to 1429 labelled #_1(0), d_1(0)
1430 to 1431 labelled d_1(0)
1430 to 1429 labelled b_1(0)
1430 to 1442 labelled b_1(1)
1430 to 1445 labelled c_1(1)
1430 to 1461 labelled b_1(2)
1431 to 1432 labelled c_1(0)
1431 to 1429 labelled c_1(0)
1431 to 1447 labelled d_1(1)
1431 to 1450 labelled b_1(1), d_1(1)
1431 to 1451 labelled d_1(1)
1431 to 1445 labelled c_1(1)
1432 to 1429 labelled D_1(0)
1434 to 1435 labelled b_1(0)
1435 to 1429 labelled D_1(0)
1433 to 1434 labelled b_1(0)
1436 to 1437 labelled b_1(0)
1437 to 1429 labelled a_1(0)
1440 to 1441 labelled b_1(0)
1441 to 1429 labelled D_1(0)
1438 to 1439 labelled b_1(0)
1438 to 1455 labelled b_1(1)
1439 to 1440 labelled d_1(0)
1442 to 1443 labelled d_1(1)
1443 to 1444 labelled c_1(1)
1443 to 1429 labelled c_1(1)
1443 to 1447 labelled d_1(1)
1443 to 1450 labelled b_1(1), d_1(1)
1443 to 1451 labelled d_1(1)
1443 to 1445 labelled c_1(1)
1444 to 1429 labelled D_1(1)
1445 to 1446 labelled b_1(1)
1446 to 1429 labelled a_1(1)
1448 to 1449 labelled b_1(1)
1448 to 1429 labelled d_1(1)
1449 to 1429 labelled D_1(1)
1447 to 1448 labelled b_1(1)
1447 to 1442 labelled b_1(1)
1447 to 1461 labelled b_1(2)
1450 to 1429 labelled b_1(1)
1450 to 1442 labelled b_1(1)
1450 to 1445 labelled c_1(1)
1450 to 1461 labelled b_1(2)
1453 to 1454 labelled b_1(1)
1454 to 1429 labelled D_1(1)
1451 to 1452 labelled b_1(1)
1451 to 1457 labelled b_1(2)
1452 to 1453 labelled d_1(1)
1455 to 1456 labelled d_1(1)
1456 to 1441 labelled c_1(1)
1457 to 1458 labelled d_1(2)
1458 to 1454 labelled c_1(2)
1459 to 1460 labelled d_1(1)
1460 to 1450 labelled c_1(1)
1461 to 1462 labelled d_1(2)
1462 to 1450 labelled c_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

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ UsableRulesProof

              ↳ UsableRulesProof

                ↳ QDP

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is

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

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

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

The set Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ QTRS Reverse

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

    ↳ QTRS

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

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

Q is empty.