(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a12(a12(a12(a12(x)))) → x
a13(a13(a13(a13(x)))) → x
a14(a14(a14(a14(x)))) → x
a15(a15(a15(a15(x)))) → x
a16(a16(a16(a16(x)))) → x
a23(a23(a23(a23(x)))) → x
a24(a24(a24(a24(x)))) → x
a25(a25(a25(a25(x)))) → x
a26(a26(a26(a26(x)))) → x
a34(a34(a34(a34(x)))) → x
a35(a35(a35(a35(x)))) → x
a36(a36(a36(a36(x)))) → x
a45(a45(a45(a45(x)))) → x
a46(a46(a46(a46(x)))) → x
a56(a56(a56(a56(x)))) → x
a13(a13(x)) → a12(a12(a23(a23(a12(a12(x))))))
a14(a14(x)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x))))))))))
a15(a15(x)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x))))))))))))))
a16(a16(x)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x))))))))))))))))))
a24(a24(x)) → a23(a23(a34(a34(a23(a23(x))))))
a25(a25(x)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x))))))))))
a26(a26(x)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x))))))))))))))
a35(a35(x)) → a34(a34(a45(a45(a34(a34(x))))))
a36(a36(x)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x))))))))))
a46(a46(x)) → a45(a45(a56(a56(a45(a45(x))))))
a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x)))))))))))) → x
a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x)))))))))))) → x
a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x)))))))))))) → x
a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x)))))))))))) → x
a12(a12(a34(a34(x)))) → a34(a34(a12(a12(x))))
a12(a12(a45(a45(x)))) → a45(a45(a12(a12(x))))
a12(a12(a56(a56(x)))) → a56(a56(a12(a12(x))))
a23(a23(a45(a45(x)))) → a45(a45(a23(a23(x))))
a23(a23(a56(a56(x)))) → a56(a56(a23(a23(x))))
a34(a34(a56(a56(x)))) → a56(a56(a34(a34(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:
a12(a12(a12(a12(x)))) → x
a13(a13(a13(a13(x)))) → x
a14(a14(a14(a14(x)))) → x
a15(a15(a15(a15(x)))) → x
a16(a16(a16(a16(x)))) → x
a23(a23(a23(a23(x)))) → x
a24(a24(a24(a24(x)))) → x
a25(a25(a25(a25(x)))) → x
a26(a26(a26(a26(x)))) → x
a34(a34(a34(a34(x)))) → x
a35(a35(a35(a35(x)))) → x
a36(a36(a36(a36(x)))) → x
a45(a45(a45(a45(x)))) → x
a46(a46(a46(a46(x)))) → x
a56(a56(a56(a56(x)))) → x
a13(a13(x)) → a12(a12(a23(a23(a12(a12(x))))))
a14(a14(x)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x))))))))))
a15(a15(x)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x))))))))))))))
a16(a16(x)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x))))))))))))))))))
a24(a24(x)) → a23(a23(a34(a34(a23(a23(x))))))
a25(a25(x)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x))))))))))
a26(a26(x)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x))))))))))))))
a35(a35(x)) → a34(a34(a45(a45(a34(a34(x))))))
a36(a36(x)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x))))))))))
a46(a46(x)) → a45(a45(a56(a56(a45(a45(x))))))
a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(x)))))))))))) → x
a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(x)))))))))))) → x
a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(x)))))))))))) → x
a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(x)))))))))))) → x
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(a12(x1)) = x1
POL(a13(x1)) = 2 + x1
POL(a14(x1)) = 4 + x1
POL(a15(x1)) = 6 + x1
POL(a16(x1)) = 9 + x1
POL(a23(x1)) = 1 + x1
POL(a24(x1)) = 4 + x1
POL(a25(x1)) = 6 + x1
POL(a26(x1)) = 8 + x1
POL(a34(x1)) = 1 + x1
POL(a35(x1)) = 4 + x1
POL(a36(x1)) = 6 + x1
POL(a45(x1)) = 1 + x1
POL(a46(x1)) = 4 + x1
POL(a56(x1)) = 1 + x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a13(a13(a13(a13(x)))) → x
a14(a14(a14(a14(x)))) → x
a15(a15(a15(a15(x)))) → x
a16(a16(a16(a16(x)))) → x
a23(a23(a23(a23(x)))) → x
a24(a24(a24(a24(x)))) → x
a25(a25(a25(a25(x)))) → x
a26(a26(a26(a26(x)))) → x
a34(a34(a34(a34(x)))) → x
a35(a35(a35(a35(x)))) → x
a36(a36(a36(a36(x)))) → x
a45(a45(a45(a45(x)))) → x
a46(a46(a46(a46(x)))) → x
a56(a56(a56(a56(x)))) → x
a13(a13(x)) → a12(a12(a23(a23(a12(a12(x))))))
a14(a14(x)) → a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x))))))))))
a15(a15(x)) → a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x))))))))))))))
a16(a16(x)) → a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x))))))))))))))))))
a24(a24(x)) → a23(a23(a34(a34(a23(a23(x))))))
a25(a25(x)) → a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x))))))))))
a26(a26(x)) → a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x))))))))))))))
a35(a35(x)) → a34(a34(a45(a45(a34(a34(x))))))
a36(a36(x)) → a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x))))))))))
a46(a46(x)) → a45(a45(a56(a56(a45(a45(x))))))
a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(x)))))))))))) → x
a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(x)))))))))))) → x
a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(x)))))))))))) → x
a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(x)))))))))))) → x
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a12(a12(a12(a12(x)))) → x
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(a12(x1)) = 1 + x1
POL(a23(x1)) = x1
POL(a34(x1)) = x1
POL(a45(x1)) = x1
POL(a56(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a12(a12(a12(a12(x)))) → x
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
(7) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A34(a34(a12(a12(x)))) → A34(a34(x))
A34(a34(a12(a12(x)))) → A34(x)
A45(a45(a12(a12(x)))) → A45(a45(x))
A45(a45(a12(a12(x)))) → A45(x)
A56(a56(a12(a12(x)))) → A56(a56(x))
A56(a56(a12(a12(x)))) → A56(x)
A45(a45(a23(a23(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(x)
A56(a56(a23(a23(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(x)
A56(a56(a34(a34(x)))) → A34(a34(a56(a56(x))))
A56(a56(a34(a34(x)))) → A34(a56(a56(x)))
A56(a56(a34(a34(x)))) → A56(a56(x))
A56(a56(a34(a34(x)))) → A56(x)
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 2 less nodes.
(10) Complex Obligation (AND)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A45(a45(a12(a12(x)))) → A45(x)
A45(a45(a12(a12(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(x)
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A45(a45(a12(a12(x)))) → A45(x)
A45(a45(a12(a12(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(x)
The TRS R consists of the following rules:
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(14) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(15) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A45(a45(a12(a12(x)))) → A45(x)
A45(a45(a12(a12(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(x)
The TRS R consists of the following rules:
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
The set Q consists of the following terms:
a45(a45(a12(a12(x0))))
a45(a45(a23(a23(x0))))
We have to consider all minimal (P,Q,R)-chains.
(16) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
A45(a45(a12(a12(x)))) → A45(x)
A45(a45(a12(a12(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(a45(x))
A45(a45(a23(a23(x)))) → A45(x)
Strictly oriented rules of the TRS R:
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
Used ordering: Polynomial interpretation [POLO]:
POL(A45(x1)) = 2·x1
POL(a12(x1)) = 2 + 2·x1
POL(a23(x1)) = 3 + 3·x1
POL(a45(x1)) = 3 + 3·x1
(17) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
The set Q consists of the following terms:
a45(a45(a12(a12(x0))))
a45(a45(a23(a23(x0))))
We have to consider all minimal (P,Q,R)-chains.
(18) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(19) YES
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A34(a34(a12(a12(x)))) → A34(x)
A34(a34(a12(a12(x)))) → A34(a34(x))
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A34(a34(a12(a12(x)))) → A34(x)
A34(a34(a12(a12(x)))) → A34(a34(x))
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A34(a34(a12(a12(x)))) → A34(x)
A34(a34(a12(a12(x)))) → A34(a34(x))
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
The set Q consists of the following terms:
a34(a34(a12(a12(x0))))
We have to consider all minimal (P,Q,R)-chains.
(25) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
A34(a34(a12(a12(x)))) → A34(x)
Used ordering: Polynomial interpretation [POLO]:
POL(A34(x1)) = 2·x1
POL(a12(x1)) = x1
POL(a34(x1)) = 1 + 2·x1
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A34(a34(a12(a12(x)))) → A34(a34(x))
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
The set Q consists of the following terms:
a34(a34(a12(a12(x0))))
We have to consider all minimal (P,Q,R)-chains.
(27) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
A34(a34(a12(a12(x)))) → A34(a34(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(A34(x1)) = x1
POL(a12(x1)) = 1 + x1
POL(a34(x1)) = x1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
(28) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
The set Q consists of the following terms:
a34(a34(a12(a12(x0))))
We have to consider all minimal (P,Q,R)-chains.
(29) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(30) YES
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A56(a56(a12(a12(x)))) → A56(x)
A56(a56(a12(a12(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(x)
A56(a56(a34(a34(x)))) → A56(a56(x))
A56(a56(a34(a34(x)))) → A56(x)
The TRS R consists of the following rules:
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
a45(a45(a12(a12(x)))) → a12(a12(a45(a45(x))))
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a45(a45(a23(a23(x)))) → a23(a23(a45(a45(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(32) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(33) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A56(a56(a12(a12(x)))) → A56(x)
A56(a56(a12(a12(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(x)
A56(a56(a34(a34(x)))) → A56(a56(x))
A56(a56(a34(a34(x)))) → A56(x)
The TRS R consists of the following rules:
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(34) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
A56(a56(a12(a12(x)))) → A56(x)
A56(a56(a12(a12(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(a56(x))
A56(a56(a23(a23(x)))) → A56(x)
A56(a56(a34(a34(x)))) → A56(a56(x))
A56(a56(a34(a34(x)))) → A56(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
(35) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
a56(a56(a12(a12(x)))) → a12(a12(a56(a56(x))))
a56(a56(a23(a23(x)))) → a23(a23(a56(a56(x))))
a56(a56(a34(a34(x)))) → a34(a34(a56(a56(x))))
a34(a34(a12(a12(x)))) → a12(a12(a34(a34(x))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(36) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(37) YES