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:

P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof

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

P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → x1

Q is empty.

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

P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1
p(P(x1)) → x1
P(p(x1)) → 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:

P(x1) → Q(Q(p(x1)))
p(p(x1)) → q(q(x1))
p(P(x1)) → x1
P(p(x1)) → x1
Used ordering:
Polynomial interpretation [25]:

POL(P(x1)) = 2 + 2·x1   
POL(Q(x1)) = x1   
POL(p(x1)) = 1 + x1   
POL(q(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof

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

p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → x1

Q is empty.

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

p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))
q(Q(x1)) → x1
Q(q(x1)) → 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:

q(Q(x1)) → x1
Q(q(x1)) → x1
Used ordering:
Polynomial interpretation [25]:

POL(Q(x1)) = x1   
POL(p(x1)) = 1 + 2·x1   
POL(q(x1)) = 1 + 2·x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof

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

p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(x1)))

Q is empty.

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

p(Q(Q(x1))) → Q(Q(p(x1)))
Q(p(q(x1))) → q(p(Q(x1)))
q(q(p(x1))) → p(q(q(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:

Q(p(q(x1))) → q(p(Q(x1)))
Used ordering:
Polynomial interpretation [25]:

POL(Q(x1)) = 2·x1   
POL(p(x1)) = x1   
POL(q(x1)) = 1 + 2·x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof

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

p(Q(Q(x1))) → Q(Q(p(x1)))
q(q(p(x1))) → p(q(q(x1)))

Q is empty.

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

p(Q(Q(x1))) → Q(Q(p(x1)))
q(q(p(x1))) → p(q(q(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:

q(q(p(x1))) → p(q(q(x1)))
Used ordering:
Polynomial interpretation [25]:

POL(Q(x1)) = 2 + 2·x1   
POL(p(x1)) = 2 + 2·x1   
POL(q(x1)) = 1 + 2·x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof

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

p(Q(Q(x1))) → Q(Q(p(x1)))

Q is empty.

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

p(Q(Q(x1))) → Q(Q(p(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:

p(Q(Q(x1))) → Q(Q(p(x1)))
Used ordering:
Polynomial interpretation [25]:

POL(Q(x1)) = 2 + 2·x1   
POL(p(x1)) = 2·x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.