(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(y, f(x, y)) → f(f(a, y), f(a, x))
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(x, y)) → F(f(a, y), f(a, x))
F(y, f(x, y)) → F(a, y)
F(y, f(x, y)) → F(a, x)
The TRS R consists of the following rules:
f(y, f(x, y)) → f(f(a, y), f(a, x))
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(x, y)) → F(a, y)
F(y, f(x, y)) → F(a, x)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
| POL(F(x1, x2)) = | 1A | + | -I | · | x1 | + | 2A | · | 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(x, y)) → f(f(a, y), f(a, x))
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(y, f(x, y)) → F(f(a, y), f(a, x))
The TRS R consists of the following rules:
f(y, f(x, y)) → f(f(a, y), f(a, x))
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 1 for the Rule:
F(y, f(x, y)) → F(f(a, y), f(a, x))
by considering the usable rules:
f(y, f(x, y)) → f(f(a, y), f(a, x))
The compatible tree automaton used to show the Match-(raise-)DP-Boundedness is represented by:
final states : [0]
transitions:
#0() → 3
f0(2, 3) → 11
F0(1, 4) → 0
f0(2, 1) → 12
f0(2, 2) → 13
F0(5, 6) → 0
f0(7, 8) → 11
f0(9, 8) → 11
f0(2, 7) → 13
f0(7, 10) → 14
f0(2, 9) → 13
f0(2, 8) → 12
f0(2, 5) → 12
f0(2, 10) → 12
f0(11, 8) → 11
f0(11, 10) → 14
f0(2, 11) → 13
f0(7, 11) → 11
f0(9, 11) → 11
f0(12, 8) → 11
f0(12, 10) → 14
f0(2, 12) → 13
f0(13, 8) → 11
f0(13, 10) → 14
f0(2, 13) → 13
f0(7, 13) → 14
f0(14, 8) → 11
f0(14, 10) → 14
f0(2, 14) → 13
f0(7, 14) → 14
f0(9, 14) → 11
f0(11, 11) → 11
f0(11, 13) → 14
f0(11, 14) → 14
f0(12, 11) → 11
f0(13, 11) → 11
f0(14, 11) → 11
f0(12, 13) → 14
f0(12, 14) → 14
f0(13, 13) → 14
f0(13, 14) → 14
f0(14, 13) → 14
f0(14, 14) → 14
F0(11, 4) → 0
F0(11, 6) → 0
F0(1, 11) → 0
F0(12, 6) → 0
F0(13, 6) → 0
F0(5, 13) → 0
F0(14, 4) → 0
F0(14, 6) → 0
F0(1, 14) → 0
F0(5, 14) → 0
F0(11, 11) → 0
F0(11, 13) → 0
F0(11, 14) → 0
F0(14, 11) → 0
F0(12, 13) → 0
F0(12, 14) → 0
F0(13, 13) → 0
F0(13, 14) → 0
F0(14, 13) → 0
F0(14, 14) → 0
f0(16, 11) → 21
f0(15, 17) → 14
f0(16, 12) → 17
f0(16, 13) → 17
f0(16, 14) → 17
f0(16, 2) → 21
a1() → 22
f1(19, 11) → 23
F1(18, 20) → 0
f1(19, 12) → 23
f1(19, 13) → 23
f1(19, 14) → 23
f1(19, 2) → 20
f0(16, 11) → 17
f0(16, 14) → 21
f0(21, 17) → 14
f0(15, 21) → 14
f0(22, 3) → 11
f0(22, 1) → 12
f0(22, 2) → 24
f0(22, 7) → 13
f0(22, 9) → 13
f0(22, 8) → 12
f0(22, 5) → 12
f0(22, 10) → 12
f0(22, 11) → 24
f0(22, 12) → 25
f0(22, 13) → 25
f0(22, 14) → 25
f0(2, 22) → 13
f0(16, 22) → 21
f0(22, 11) → 25
f0(22, 12) → 13
f0(22, 14) → 24
f0(21, 21) → 14
f0(22, 22) → 24
f0(22, 11) → 13
f0(22, 13) → 13
f0(22, 14) → 13
F1(23, 20) → 0
F1(18, 23) → 0
F1(23, 23) → 0
f1(22, 11) → 23
f1(22, 12) → 23
f1(22, 13) → 23
f1(22, 14) → 23
f1(22, 2) → 20
f1(19, 22) → 20
f1(22, 22) → 20
f0(24, 8) → 11
f0(24, 10) → 14
f0(24, 11) → 11
f0(24, 13) → 14
f0(24, 14) → 14
f0(24, 17) → 14
f0(2, 24) → 13
f0(7, 24) → 14
f0(11, 24) → 14
f0(12, 24) → 14
f0(13, 24) → 14
f0(14, 24) → 14
f0(15, 24) → 14
f0(16, 24) → 17
f0(25, 8) → 11
f0(25, 10) → 14
f0(25, 11) → 11
f0(25, 13) → 14
f0(25, 14) → 14
f0(2, 25) → 13
f0(7, 25) → 14
f0(11, 25) → 14
f0(12, 25) → 14
f0(13, 25) → 14
f0(14, 25) → 14
f0(15, 25) → 14
f0(16, 25) → 17
f0(24, 24) → 14
f0(24, 25) → 14
f0(25, 24) → 14
f0(25, 25) → 14
F0(24, 6) → 0
F0(24, 13) → 0
F0(24, 14) → 0
F0(5, 24) → 0
F0(11, 24) → 0
F0(12, 24) → 0
F0(13, 24) → 0
F0(14, 24) → 0
F0(25, 6) → 0
F0(25, 13) → 0
F0(25, 14) → 0
F0(5, 25) → 0
F0(11, 25) → 0
F0(12, 25) → 0
F0(13, 25) → 0
F0(14, 25) → 0
F0(24, 24) → 0
F0(24, 25) → 0
F0(25, 24) → 0
F0(25, 25) → 0
f1(19, 24) → 23
f1(19, 25) → 23
(6) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
f(y, f(x, y)) → f(f(a, y), f(a, x))
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