YES
0 QTRS
↳1 QTRSRRRProof (⇔, 75 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 0 ms)
↳6 QTRS
↳7 DependencyPairsProof (⇔, 15 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 21 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 AND
↳13 QDP
↳14 QDPOrderProof (⇔, 6 ms)
↳15 QDP
↳16 PisEmptyProof (⇔, 0 ms)
↳17 YES
↳18 QDP
↳19 QDPOrderProof (⇔, 4 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
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
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
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
u(a(x)) → x
a(u(x)) → x
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
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(c(x1)) = x1
POL(v(x1)) = 1 + x1
POL(w(x1)) = x1
v(b(x)) → x
b(v(x)) → x
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
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(c(x1)) = x1
POL(w(x1)) = 1 + x1
w(c(x)) → x
c(w(x)) → x
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
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)
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
B(c(x)) → C(b(b(x)))
C(a(x)) → C(c(x))
C(a(x)) → C(x)
POL(A(x1)) = 1
POL(B(x1)) = 1
POL(C(x1)) = x1
POL(a(x1)) = 1 + x1
POL(b(x1)) = 0
POL(c(x1)) = x1
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
a(b(x)) → b(a(a(x)))
A(b(x)) → B(a(a(x)))
A(b(x)) → A(a(x))
A(b(x)) → A(x)
B(c(x)) → B(b(x))
B(c(x)) → B(x)
C(a(x)) → A(c(c(x)))
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
B(c(x)) → B(x)
B(c(x)) → B(b(x))
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
B(c(x)) → B(x)
B(c(x)) → B(b(x))
POL(B(x1)) = x1
POL(a(x1)) = 1
POL(b(x1)) = x1
POL(c(x1)) = 1 + x1
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
a(b(x)) → b(a(a(x)))
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
A(b(x)) → A(x)
A(b(x)) → A(a(x))
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(b(x)) → A(x)
A(b(x)) → A(a(x))
POL(A(x1)) = x1
POL(a(x1)) = x1
POL(b(x1)) = 1 + x1
POL(c(x1)) = 1
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))
a(b(x)) → b(a(a(x)))
a(b(x)) → b(a(a(x)))
b(c(x)) → c(b(b(x)))
c(a(x)) → a(c(c(x)))