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(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
The set Q is empty.
We have obtained the following QTRS:
a(a(a(a(x)))) → b(b(b(b(b(b(a(a(x))))))))
a(a(b(b(x)))) → c(c(b(b(b(b(x))))))
c(c(b(b(b(b(a(a(x)))))))) → b(b(a(a(a(a(a(a(x))))))))
The set Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(a(x)))) → b(b(b(b(b(b(a(a(x))))))))
a(a(b(b(x)))) → c(c(b(b(b(b(x))))))
c(c(b(b(b(b(a(a(x)))))))) → b(b(a(a(a(a(a(a(x))))))))
Q is empty.
We have reversed the following QTRS:
The set of rules R is
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
The set Q is empty.
We have obtained the following QTRS:
a(a(a(a(x)))) → b(b(b(b(b(b(a(a(x))))))))
a(a(b(b(x)))) → c(c(b(b(b(b(x))))))
c(c(b(b(b(b(a(a(x)))))))) → b(b(a(a(a(a(a(a(x))))))))
The set Q is empty.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(a(a(x)))) → b(b(b(b(b(b(a(a(x))))))))
a(a(b(b(x)))) → c(c(b(b(b(b(x))))))
c(c(b(b(b(b(a(a(x)))))))) → b(b(a(a(a(a(a(a(x))))))))
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:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
B(b(a(a(x1)))) → B(b(b(c(c(x1)))))
B(b(a(a(x1)))) → B(c(c(x1)))
A(a(a(a(x1)))) → B(b(x1))
B(b(a(a(x1)))) → B(b(c(c(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → B(x1)
A(a(a(a(x1)))) → B(b(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
A(a(b(b(b(b(c(c(x1)))))))) → B(b(x1))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(a(a(x1)))) → B(b(b(b(b(b(x1))))))
A(a(a(a(x1)))) → A(b(b(b(b(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(a(a(x1)))) → A(a(b(b(b(b(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(a(a(x1)))) → B(x1)
A(a(a(a(x1)))) → B(b(b(b(b(x1)))))
B(b(a(a(x1)))) → B(b(b(b(c(c(x1))))))
A(a(a(a(x1)))) → B(b(b(x1)))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
B(b(a(a(x1)))) → B(b(b(c(c(x1)))))
B(b(a(a(x1)))) → B(c(c(x1)))
A(a(a(a(x1)))) → B(b(x1))
B(b(a(a(x1)))) → B(b(c(c(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → B(x1)
A(a(a(a(x1)))) → B(b(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
A(a(b(b(b(b(c(c(x1)))))))) → B(b(x1))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(a(a(x1)))) → B(b(b(b(b(b(x1))))))
A(a(a(a(x1)))) → A(b(b(b(b(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(a(a(x1)))) → A(a(b(b(b(b(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(a(a(x1)))) → B(x1)
A(a(a(a(x1)))) → B(b(b(b(b(x1)))))
B(b(a(a(x1)))) → B(b(b(b(c(c(x1))))))
A(a(a(a(x1)))) → B(b(b(x1)))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 12 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(a(a(x1)))) → A(b(b(b(b(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(a(a(x1)))) → A(a(b(b(b(b(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(a(a(x1)))) → A(b(b(b(b(b(b(x1))))))) at position [0] we obtained the following new rules:
A(a(a(a(a(a(x0)))))) → A(b(b(b(b(b(b(b(b(c(c(x0)))))))))))
A(a(a(a(b(a(a(x0))))))) → A(b(b(b(b(b(b(b(b(b(c(c(x0))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(a(a(b(a(a(x0))))))) → A(b(b(b(b(b(b(b(b(b(c(c(x0))))))))))))
A(a(a(a(x1)))) → A(a(b(b(b(b(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(a(a(a(a(x0)))))) → A(b(b(b(b(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(a(a(x1)))) → A(a(b(b(b(b(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(a(a(x1)))) → A(a(b(b(b(b(b(b(x1)))))))) at position [0] we obtained the following new rules:
A(a(a(a(a(a(x0)))))) → A(a(b(b(b(b(b(b(b(b(c(c(x0))))))))))))
A(a(a(a(b(a(a(x0))))))) → A(a(b(b(b(b(b(b(b(b(b(c(c(x0)))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(a(a(a(a(x0)))))) → A(a(b(b(b(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(a(a(b(a(a(x0))))))) → A(a(b(b(b(b(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1)))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(x1)))))))) → A(b(b(x1))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(b(b(b(b(c(c(x0)))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(b(b(b(b(b(c(c(x0))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(b(b(b(b(c(c(x0)))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(b(b(b(b(b(c(c(x0))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(a(b(b(x1)))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1)))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(a(b(b(x1))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(a(b(b(x1)))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(b(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(b(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 1 less node.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1)))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(x1)))))))) → A(a(a(b(b(x1))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(b(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(b(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 1 less node.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(a(b(b(y0)))))))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(b(b(b(b(b(b(a(b(b(b(b(b(c(c(x0)))))))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(b(b(a(b(b(b(b(c(c(x0))))))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(b(b(b(b(b(b(a(b(b(b(b(b(c(c(x0)))))))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(b(b(a(b(b(b(b(c(c(x0))))))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(b(a(a(y0))))))))))) → A(a(a(b(b(b(b(b(b(a(b(b(b(b(b(c(c(y0)))))))))))))))))
A(a(b(b(b(b(c(c(b(a(a(y0))))))))))) → A(a(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(y0)))))))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(b(a(a(y0))))))))))) → A(a(a(b(b(b(b(b(b(a(b(b(b(b(b(c(c(y0)))))))))))))))))
A(a(b(b(b(b(c(c(b(a(a(y0))))))))))) → A(a(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(y0)))))))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(a(b(b(b(b(b(b(b(b(y0)))))))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(b(b(b(b(b(b(c(c(x0))))))))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(x0)))))))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(x0)))))))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(b(b(b(b(b(b(c(c(x0))))))))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(a(a(b(b(b(b(b(c(c(x0)))))))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(b(a(a(y0))))))))))) → A(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(y0))))))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(a(a(y0))))))))))) → A(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(y0))))))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 1 less node.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(a(b(b(b(b(c(c(y0)))))))) → A(a(a(b(b(b(b(b(b(b(b(y0))))))))))) at position [0] we obtained the following new rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(b(b(b(b(b(b(c(c(x0)))))))))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(x0))))))))))))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(b(b(b(b(b(b(c(c(x0)))))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(a(a(x0))))))))))) → A(a(a(b(b(b(b(b(b(b(b(b(b(b(c(c(x0))))))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(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 2 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ SemLabProof
Q DP problem:
The TRS P consists of the following rules:
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(b(b(b(b(c(c(x0))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(b(b(x0)))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(b(b(b(b(c(c(x0)))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(b(b(x0))))))))))
A(a(b(b(b(b(c(c(x1)))))))) → A(a(b(b(x1))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(b(b(b(b(c(c(x0)))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(a(a(a(b(b(x0))))))))))))
A(a(b(b(b(b(c(c(a(a(x0)))))))))) → A(a(a(a(a(a(b(b(b(b(c(c(x0))))))))))))
A(a(b(b(b(b(c(c(b(b(c(c(x0)))))))))))) → A(a(a(a(a(a(a(b(b(x0)))))))))
The TRS R consists of the following rules:
a(a(a(a(x1)))) → a(a(b(b(b(b(b(b(x1))))))))
b(b(a(a(x1)))) → b(b(b(b(c(c(x1))))))
a(a(b(b(b(b(c(c(x1)))))))) → a(a(a(a(a(a(b(b(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R.
Interpretation over the domain with elements from 0 to 1.c: 0
a: 0
A: 0
b: 1
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → A.0(a.1(b.1(b.1(x1))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → A.0(a.1(b.1(b.0(x1))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0))))))))))
The TRS R consists of the following rules:
b.1(b.0(a.0(a.1(x1)))) → b.1(b.1(b.1(b.0(c.0(c.1(x1))))))
a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x1))))))))
a.0(a.0(a.0(a.0(x1)))) → a.0(a.1(b.1(b.1(b.1(b.1(b.1(b.0(x1))))))))
a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x1))))))))
b.1(b.0(a.0(a.0(x1)))) → b.1(b.1(b.1(b.0(c.0(c.0(x1))))))
a.0(a.0(a.0(a.1(x1)))) → a.0(a.1(b.1(b.1(b.1(b.1(b.1(b.1(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → A.0(a.1(b.1(b.1(x1))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0)))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.1(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → A.0(a.1(b.1(b.0(x1))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(b.1(b.0(c.0(c.0(x0)))))))))))) → A.0(a.0(a.0(a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0))))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.1(x0)))))))))) → A.0(a.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x0)))))))))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(a.0(a.0(x0)))))))))) → A.0(a.0(a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x0))))))))))
The TRS R consists of the following rules:
b.1(b.0(a.0(a.1(x1)))) → b.1(b.1(b.1(b.0(c.0(c.1(x1))))))
a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x1))))))))
a.0(a.0(a.0(a.0(x1)))) → a.0(a.1(b.1(b.1(b.1(b.1(b.1(b.0(x1))))))))
a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x1))))))))
b.1(b.0(a.0(a.0(x1)))) → b.1(b.1(b.1(b.0(c.0(c.0(x1))))))
a.0(a.0(a.0(a.1(x1)))) → a.0(a.1(b.1(b.1(b.1(b.1(b.1(b.1(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 16 less nodes.
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
Q DP problem:
The TRS P consists of the following rules:
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → A.0(a.1(b.1(b.0(x1))))
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → A.0(a.1(b.1(b.1(x1))))
The TRS R consists of the following rules:
b.1(b.0(a.0(a.1(x1)))) → b.1(b.1(b.1(b.0(c.0(c.1(x1))))))
a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.1(x1))))))))
a.0(a.0(a.0(a.0(x1)))) → a.0(a.1(b.1(b.1(b.1(b.1(b.1(b.0(x1))))))))
a.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → a.0(a.0(a.0(a.0(a.0(a.1(b.1(b.0(x1))))))))
b.1(b.0(a.0(a.0(x1)))) → b.1(b.1(b.1(b.0(c.0(c.0(x1))))))
a.0(a.0(a.0(a.1(x1)))) → a.0(a.1(b.1(b.1(b.1(b.1(b.1(b.1(x1))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.1(x1)))))))) → A.0(a.1(b.1(b.1(x1))))
The following rules are removed from R:
b.1(b.0(a.0(a.1(x1)))) → b.1(b.1(b.1(b.0(c.0(c.1(x1))))))
b.1(b.0(a.0(a.0(x1)))) → b.1(b.1(b.1(b.0(c.0(c.0(x1))))))
Used ordering: POLO with Polynomial interpretation [25]:
POL(A.0(x1)) = x1
POL(a.0(x1)) = 1 + x1
POL(a.1(x1)) = 1 + x1
POL(b.0(x1)) = x1
POL(b.1(x1)) = x1
POL(c.0(x1)) = x1
POL(c.1(x1)) = 1 + x1
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A.0(a.1(b.1(b.1(b.1(b.0(c.0(c.0(x1)))))))) → A.0(a.1(b.1(b.0(x1))))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.