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

0 QTRS
  ↳1 QTRS Reverse (⇔)
    ↳2 QTRS
  ↳3 QTRS Reverse (⇔)
    ↳4 QTRS
  ↳5 QTRSRRRProof (⇔)
    ↳6 QTRS
    ↳7 QTRSRRRProof (⇔)
    ↳8 QTRS
    ↳9 QTRSRRRProof (⇔)
    ↳10 QTRS
    ↳11 DependencyPairsProof (⇔)
    ↳12 QDP
    ↳13 QDPOrderProof (⇔)
    ↳14 QDP
    ↳15 DependencyGraphProof (⇔)
    ↳16 AND
      ↳17 QDP
        ↳18 QDPOrderProof (⇔)
          ↳19 QDP
        ↳20 QDPOrderProof (⇔)
          ↳21 QDP
          ↳22 QDPOrderProof (⇔)
          ↳23 QDP
          ↳24 PisEmptyProof (⇔)
          ↳25 TRUE
      ↳26 QDP
        ↳27 QDPOrderProof (⇔)
        ↳28 QDP
        ↳29 QDPOrderProof (⇔)
        ↳30 QDP
        ↳31 PisEmptyProof (⇔)
        ↳32 TRUE

(0) Obligation:

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

a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
u(a(x)) → x
v(b(x)) → x
w(c(x)) → x
a(u(x)) → x
b(v(x)) → x
c(w(x)) → x

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

b(a(x)) → a(a(b(x)))
c(b(x)) → b(b(c(x)))
a(c(x)) → c(c(a(x)))
a(u(x)) → x
b(v(x)) → x
c(w(x)) → x
u(a(x)) → x
v(b(x)) → x
w(c(x)) → x

Q is empty.

(3) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(4) Obligation:

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

b(a(x)) → a(a(b(x)))
c(b(x)) → b(b(c(x)))
a(c(x)) → c(c(a(x)))
a(u(x)) → x
b(v(x)) → x
c(w(x)) → x
u(a(x)) → x
v(b(x)) → x
w(c(x)) → x

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(a(x1)) = x1   
POL(b(x1)) = x1   
POL(c(x1)) = x1   
POL(u(x1)) = 1 + x1   
POL(v(x1)) = x1   
POL(w(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

u(a(x)) → x
a(u(x)) → x


(6) Obligation:

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

a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
v(b(x)) → x
w(c(x)) → x
b(v(x)) → x
c(w(x)) → x

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(a(x1)) = x1   
POL(b(x1)) = x1   
POL(c(x1)) = x1   
POL(v(x1)) = 1 + x1   
POL(w(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

v(b(x)) → x
b(v(x)) → x


(8) Obligation:

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

a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
w(c(x)) → x
c(w(x)) → x

Q is empty.

(9) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(a(x1)) = x1   
POL(b(x1)) = x1   
POL(c(x1)) = x1   
POL(w(x1)) = 1 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

w(c(x)) → x
c(w(x)) → x


(10) Obligation:

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

a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(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(b(x)) → B(a(a(x)))
A(b(x)) → A(a(x))
A(b(x)) → A(x)
B(c(x)) → C(b(b(x)))
B(c(x)) → B(b(x))
B(c(x)) → B(x)
C(a(x)) → A(c(c(x)))
C(a(x)) → C(c(x))
C(a(x)) → C(x)

The TRS R consists of the following rules:

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

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


C(a(x)) → A(c(c(x)))
C(a(x)) → C(c(x))
C(a(x)) → C(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( A(x1) ) = 1


POL( B(x1) ) = 1


POL( C(x1) ) = x1 + 1


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


POL( c(x1) ) = x1


POL( a(x1) ) = x1 + 1



The following usable rules [FROCOS05] were oriented:

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

(14) Obligation:

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

A(b(x)) → B(a(a(x)))
A(b(x)) → A(a(x))
A(b(x)) → A(x)
B(c(x)) → C(b(b(x)))
B(c(x)) → B(b(x))
B(c(x)) → B(x)

The TRS R consists of the following rules:

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

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

(15) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.

(16) Complex Obligation (AND)

(17) Obligation:

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

B(c(x)) → B(x)
B(c(x)) → B(b(x))

The TRS R consists of the following rules:

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

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


B(c(x)) → B(x)
B(c(x)) → B(b(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( B(x1) ) = x1 + 1


POL( b(x1) ) = x1


POL( c(x1) ) = x1 + 1


POL( a(x1) ) = 1



The following usable rules [FROCOS05] were oriented:

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

(19) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

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

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


B(c(x)) → B(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(B(x1)) =
/0A\
\-I/
 +
/1A0A\
\-I-I/
·x1

POL(c(x1)) =
/0A\
\0A/
 +
/1A1A\
\0A1A/
·x1

POL(b(x1)) =
/0A\
\-I/
 +
/-I1A\
\-I0A/
·x1

POL(a(x1)) =
/1A\
\0A/
 +
/-I-I\
\-I-I/
·x1

The following usable rules [FROCOS05] were oriented:

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

(21) Obligation:

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

B(c(x)) → B(b(x))

The TRS R consists of the following rules:

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

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

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


B(c(x)) → B(b(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( B(x1) ) = x1 + 1


POL( b(x1) ) = x1


POL( c(x1) ) = x1 + 1


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



The following usable rules [FROCOS05] were oriented:

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

(23) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

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

(24) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(25) TRUE

(26) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


A(b(x)) → A(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(A(x1)) =
/0A\
\-I/
 +
/1A-I\
\-I-I/
·x1

POL(b(x1)) =
/0A\
\0A/
 +
/1A1A\
\0A1A/
·x1

POL(a(x1)) =
/0A\
\-I/
 +
/0A1A\
\-I0A/
·x1

POL(c(x1)) =
/0A\
\-I/
 +
/-I-I\
\-I-I/
·x1

The following usable rules [FROCOS05] were oriented:

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

(28) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


A(b(x)) → A(a(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( A(x1) ) = x1 + 1


POL( b(x1) ) = x1 + 1


POL( c(x1) ) = 1


POL( a(x1) ) = x1



The following usable rules [FROCOS05] were oriented:

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

(30) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

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

(31) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(32) TRUE