(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(y, f(y, x)) → f(f(a, y), f(a, y))
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(y, f(y, x)) → F(f(a, y), f(a, y))
F(y, f(y, x)) → F(a, y)
The TRS R consists of the following rules:
f(y, f(y, x)) → f(f(a, y), f(a, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(y, f(y, x)) → F(a, y)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
| POL(F(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
| POL(f(x1, x2)) = | 1A | + | 1A | · | x1 | + | 1A | · | x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
f(y, f(y, x)) → f(f(a, y), f(a, y))
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(y, f(y, x)) → F(f(a, y), f(a, y))
The TRS R consists of the following rules:
f(y, f(y, x)) → f(f(a, y), f(a, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) QDPBoundsTAProof (EQUIVALENT transformation)
The DP-Problem (P, R) could be shown to be Match-(raise-)DP-Bounded [TAB_NONLEFTLINEAR] by 2 for the Rule:
F(y, f(y, x)) → F(f(a, y), f(a, y))
by considering the usable rules:
f(y, f(y, x)) → f(f(a, y), f(a, y))
The compatible tree automaton used to show the Match-(raise-)DP-Boundedness is represented by:
final states : [2]
transitions:
f0(0, 0) → 0
f0(1, 0) → 0
f0(0, 1) → 0
f0(1, 1) → 0
F0(0, 0) → 2
F0(1, 0) → 2
F0(0, 1) → 2
F0(1, 1) → 2
f1(4, 0) → 7
F1(3, 5) → 2
f1(4, 1) → 7
f0(6, 0) → 0
f0(6, 1) → 0
f0(0, 6) → 0
f0(1, 6) → 0
f0(6, 6) → 0
F0(6, 0) → 2
F0(6, 1) → 2
F0(0, 6) → 2
F0(1, 6) → 2
F0(6, 6) → 2
F1(7, 5) → 2
F1(3, 7) → 2
F1(7, 7) → 2
f1(6, 0) → 10
f1(6, 1) → 10
f1(4, 6) → 11
f1(6, 6) → 15
f1(8, 9) → 10
f0(10, 0) → 0
f0(10, 1) → 0
f0(10, 6) → 0
f0(0, 10) → 0
f0(1, 10) → 0
f0(6, 10) → 0
f0(10, 10) → 0
F0(10, 0) → 2
F0(10, 1) → 2
F0(10, 6) → 2
F0(0, 10) → 2
F0(1, 10) → 2
F0(6, 10) → 2
F0(10, 10) → 2
F1(10, 5) → 2
F1(10, 7) → 2
F1(3, 10) → 2
F1(7, 10) → 2
F1(11, 5) → 2
F1(11, 7) → 2
F1(3, 11) → 2
F1(7, 11) → 2
F1(10, 10) → 2
F1(10, 11) → 2
F1(11, 10) → 2
F1(11, 11) → 2
f1(4, 10) → 7
f1(6, 10) → 10
f1(11, 9) → 10
f1(8, 11) → 10
f1(11, 11) → 10
a2() → 16
f2(13, 11) → 17
F2(12, 14) → 2
f0(15, 0) → 0
f0(15, 1) → 0
f0(15, 6) → 0
f0(15, 10) → 0
f0(0, 15) → 0
f0(1, 15) → 0
f0(6, 15) → 0
f0(10, 15) → 0
f0(16, 0) → 0
f0(16, 1) → 0
f0(16, 6) → 0
f0(16, 10) → 0
f0(0, 16) → 0
f0(1, 16) → 0
f0(6, 16) → 0
f0(10, 16) → 0
f0(15, 15) → 0
f0(15, 16) → 0
f0(16, 15) → 0
f0(16, 16) → 0
F0(15, 0) → 2
F0(15, 1) → 2
F0(15, 6) → 2
F0(15, 10) → 2
F0(0, 15) → 2
F0(1, 15) → 2
F0(6, 15) → 2
F0(10, 15) → 2
F0(16, 0) → 2
F0(16, 1) → 2
F0(16, 6) → 2
F0(16, 10) → 2
F0(0, 16) → 2
F0(1, 16) → 2
F0(6, 16) → 2
F0(10, 16) → 2
F0(15, 15) → 2
F0(15, 16) → 2
F0(16, 15) → 2
F0(16, 16) → 2
F1(15, 5) → 2
F1(15, 7) → 2
F1(15, 10) → 2
F1(15, 11) → 2
F1(3, 15) → 2
F1(7, 15) → 2
F1(10, 15) → 2
F1(11, 15) → 2
F1(15, 15) → 2
f1(15, 9) → 10
f1(15, 11) → 10
f1(4, 15) → 7
f1(6, 15) → 10
f1(8, 15) → 10
f1(11, 15) → 10
f1(16, 0) → 10
f1(16, 1) → 10
f1(16, 6) → 15
f1(16, 10) → 10
f1(4, 16) → 11
f1(6, 16) → 15
f1(15, 15) → 10
f1(16, 15) → 10
f1(16, 16) → 15
F2(17, 14) → 2
F2(12, 17) → 2
F2(17, 17) → 2
f2(13, 15) → 17
f2(16, 11) → 17
f2(16, 15) → 20
f2(13, 16) → 21
f2(18, 19) → 20
f0(20, 0) → 0
f0(20, 1) → 0
f0(20, 6) → 0
f0(20, 10) → 0
f0(20, 15) → 0
f0(20, 16) → 0
f0(0, 20) → 0
f0(1, 20) → 0
f0(6, 20) → 0
f0(10, 20) → 0
f0(15, 20) → 0
f0(16, 20) → 0
f0(20, 20) → 0
F0(20, 0) → 2
F0(20, 1) → 2
F0(20, 6) → 2
F0(20, 10) → 2
F0(20, 15) → 2
F0(20, 16) → 2
F0(0, 20) → 2
F0(1, 20) → 2
F0(6, 20) → 2
F0(10, 20) → 2
F0(15, 20) → 2
F0(16, 20) → 2
F0(20, 20) → 2
F1(20, 5) → 2
F1(20, 7) → 2
F1(20, 10) → 2
F1(20, 11) → 2
F1(20, 15) → 2
F1(3, 20) → 2
F1(7, 20) → 2
F1(10, 20) → 2
F1(11, 20) → 2
F1(15, 20) → 2
F1(20, 20) → 2
f1(4, 20) → 7
f1(6, 20) → 10
f1(16, 20) → 10
F2(20, 14) → 2
F2(20, 17) → 2
F2(12, 20) → 2
F2(17, 20) → 2
F2(20, 20) → 2
f2(16, 16) → 22
f2(21, 19) → 17
f2(18, 21) → 17
f2(21, 21) → 17
f0(22, 0) → 0
f0(22, 1) → 0
f0(22, 6) → 0
f0(22, 10) → 0
f0(22, 15) → 0
f0(22, 16) → 0
f0(22, 20) → 0
f0(0, 22) → 0
f0(1, 22) → 0
f0(6, 22) → 0
f0(10, 22) → 0
f0(15, 22) → 0
f0(16, 22) → 0
f0(20, 22) → 0
f0(22, 22) → 0
F0(22, 0) → 2
F0(22, 1) → 2
F0(22, 6) → 2
F0(22, 10) → 2
F0(22, 15) → 2
F0(22, 16) → 2
F0(22, 20) → 2
F0(0, 22) → 2
F0(1, 22) → 2
F0(6, 22) → 2
F0(10, 22) → 2
F0(15, 22) → 2
F0(16, 22) → 2
F0(20, 22) → 2
F0(22, 22) → 2
F1(22, 5) → 2
F1(22, 7) → 2
F1(22, 10) → 2
F1(22, 11) → 2
F1(22, 15) → 2
F1(22, 20) → 2
F1(3, 22) → 2
F1(7, 22) → 2
F1(10, 22) → 2
F1(11, 22) → 2
F1(15, 22) → 2
F1(20, 22) → 2
F1(22, 22) → 2
f1(22, 9) → 10
f1(22, 11) → 10
f1(22, 15) → 10
f1(4, 22) → 7
f1(6, 22) → 10
f1(8, 22) → 10
f1(11, 22) → 10
f1(15, 22) → 10
f1(16, 22) → 10
f1(22, 22) → 10
f2(16, 15) → 17
f2(16, 16) → 21
f2(21, 19) → 20
f2(18, 21) → 20
f2(22, 19) → 20
f2(22, 21) → 17
f2(13, 22) → 17
f2(16, 22) → 20
f2(18, 22) → 20
f2(21, 22) → 17
f2(16, 22) → 17
f2(21, 21) → 20
f2(21, 22) → 20
f2(22, 21) → 20
f2(22, 22) → 20
(6) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
f(y, f(y, x)) → f(f(a, y), f(a, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(8) YES