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(b(x1)) → C(x1)
b(c(x1)) → A(x1)
c(a(x1)) → B(x1)
A(C(x1)) → b(x1)
C(B(x1)) → a(x1)
B(A(x1)) → c(x1)
a(a(a(a(x1)))) → A(A(A(x1)))
A(A(A(A(x1)))) → a(a(a(x1)))
b(b(b(b(x1)))) → B(B(B(x1)))
B(B(B(B(x1)))) → b(b(b(x1)))
c(c(c(c(x1)))) → C(C(C(x1)))
C(C(C(C(x1)))) → c(c(c(x1)))
B(a(a(a(x1)))) → c(A(A(A(x1))))
A(A(A(b(x1)))) → a(a(a(C(x1))))
C(b(b(b(x1)))) → a(B(B(B(x1))))
B(B(B(c(x1)))) → b(b(b(A(x1))))
A(c(c(c(x1)))) → b(C(C(C(x1))))
C(C(C(a(x1)))) → c(c(c(B(x1))))
a(A(x1)) → x1
A(a(x1)) → x1
b(B(x1)) → x1
B(b(x1)) → x1
c(C(x1)) → x1
C(c(x1)) → x1
Q is empty.
↳ QTRS
↳ RRRPoloQTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(x1)) → C(x1)
b(c(x1)) → A(x1)
c(a(x1)) → B(x1)
A(C(x1)) → b(x1)
C(B(x1)) → a(x1)
B(A(x1)) → c(x1)
a(a(a(a(x1)))) → A(A(A(x1)))
A(A(A(A(x1)))) → a(a(a(x1)))
b(b(b(b(x1)))) → B(B(B(x1)))
B(B(B(B(x1)))) → b(b(b(x1)))
c(c(c(c(x1)))) → C(C(C(x1)))
C(C(C(C(x1)))) → c(c(c(x1)))
B(a(a(a(x1)))) → c(A(A(A(x1))))
A(A(A(b(x1)))) → a(a(a(C(x1))))
C(b(b(b(x1)))) → a(B(B(B(x1))))
B(B(B(c(x1)))) → b(b(b(A(x1))))
A(c(c(c(x1)))) → b(C(C(C(x1))))
C(C(C(a(x1)))) → c(c(c(B(x1))))
a(A(x1)) → x1
A(a(x1)) → x1
b(B(x1)) → x1
B(b(x1)) → x1
c(C(x1)) → x1
C(c(x1)) → x1
Q is empty.
The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(x1)) → C(x1)
b(c(x1)) → A(x1)
c(a(x1)) → B(x1)
A(C(x1)) → b(x1)
C(B(x1)) → a(x1)
B(A(x1)) → c(x1)
a(a(a(a(x1)))) → A(A(A(x1)))
A(A(A(A(x1)))) → a(a(a(x1)))
b(b(b(b(x1)))) → B(B(B(x1)))
B(B(B(B(x1)))) → b(b(b(x1)))
c(c(c(c(x1)))) → C(C(C(x1)))
C(C(C(C(x1)))) → c(c(c(x1)))
B(a(a(a(x1)))) → c(A(A(A(x1))))
A(A(A(b(x1)))) → a(a(a(C(x1))))
C(b(b(b(x1)))) → a(B(B(B(x1))))
B(B(B(c(x1)))) → b(b(b(A(x1))))
A(c(c(c(x1)))) → b(C(C(C(x1))))
C(C(C(a(x1)))) → c(c(c(B(x1))))
a(A(x1)) → x1
A(a(x1)) → x1
b(B(x1)) → x1
B(b(x1)) → x1
c(C(x1)) → x1
C(c(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:
a(b(x1)) → C(x1)
b(c(x1)) → A(x1)
c(a(x1)) → B(x1)
A(C(x1)) → b(x1)
C(B(x1)) → a(x1)
B(A(x1)) → c(x1)
a(a(a(a(x1)))) → A(A(A(x1)))
A(A(A(A(x1)))) → a(a(a(x1)))
b(b(b(b(x1)))) → B(B(B(x1)))
B(B(B(B(x1)))) → b(b(b(x1)))
c(c(c(c(x1)))) → C(C(C(x1)))
C(C(C(C(x1)))) → c(c(c(x1)))
a(A(x1)) → x1
A(a(x1)) → x1
b(B(x1)) → x1
B(b(x1)) → x1
c(C(x1)) → x1
C(c(x1)) → x1
Used ordering:
Polynomial interpretation [25]:
POL(A(x1)) = 1 + 2·x1
POL(B(x1)) = 1 + 2·x1
POL(C(x1)) = 1 + 2·x1
POL(a(x1)) = 1 + 2·x1
POL(b(x1)) = 1 + 2·x1
POL(c(x1)) = 1 + 2·x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
B(a(a(a(x1)))) → c(A(A(A(x1))))
A(A(A(b(x1)))) → a(a(a(C(x1))))
C(b(b(b(x1)))) → a(B(B(B(x1))))
B(B(B(c(x1)))) → b(b(b(A(x1))))
A(c(c(c(x1)))) → b(C(C(C(x1))))
C(C(C(a(x1)))) → c(c(c(B(x1))))
Q is empty.
The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:
B(a(a(a(x1)))) → c(A(A(A(x1))))
A(A(A(b(x1)))) → a(a(a(C(x1))))
C(b(b(b(x1)))) → a(B(B(B(x1))))
B(B(B(c(x1)))) → b(b(b(A(x1))))
A(c(c(c(x1)))) → b(C(C(C(x1))))
C(C(C(a(x1)))) → c(c(c(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(a(a(x1)))) → c(A(A(A(x1))))
A(A(A(b(x1)))) → a(a(a(C(x1))))
C(b(b(b(x1)))) → a(B(B(B(x1))))
B(B(B(c(x1)))) → b(b(b(A(x1))))
A(c(c(c(x1)))) → b(C(C(C(x1))))
C(C(C(a(x1)))) → c(c(c(B(x1))))
Used ordering:
Polynomial interpretation [25]:
POL(A(x1)) = 2·x1
POL(B(x1)) = 1 + 2·x1
POL(C(x1)) = 2·x1
POL(a(x1)) = 2 + 2·x1
POL(b(x1)) = 2 + 2·x1
POL(c(x1)) = 1 + 2·x1
↳ 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.