(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(f(x, a), y) → f(y, f(x, 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(f(x, a), y) → F(y, f(x, y))
F(f(x, a), y) → F(x, y)
The TRS R consists of the following rules:
f(f(x, a), y) → f(y, f(x, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
F(
f(
x,
a),
y) →
F(
y,
f(
x,
y)) we obtained the following new rules [LPAR04]:
F(f(x0, a), f(y_0, a)) → F(f(y_0, a), f(x0, f(y_0, a)))
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(f(x, a), y) → F(x, y)
F(f(x0, a), f(y_0, a)) → F(f(y_0, a), f(x0, f(y_0, a)))
The TRS R consists of the following rules:
f(f(x, a), y) → f(y, f(x, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
F(
f(
x,
a),
y) →
F(
x,
y) we obtained the following new rules [LPAR04]:
F(f(f(y_0, a), a), x1) → F(f(y_0, a), x1)
F(f(f(y_0, a), a), f(y_1, a)) → F(f(y_0, a), f(y_1, a))
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(f(x0, a), f(y_0, a)) → F(f(y_0, a), f(x0, f(y_0, a)))
F(f(f(y_0, a), a), x1) → F(f(y_0, a), x1)
F(f(f(y_0, a), a), f(y_1, a)) → F(f(y_0, a), f(y_1, a))
The TRS R consists of the following rules:
f(f(x, a), y) → f(y, f(x, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
F(f(x0, a), f(y_0, a)) → F(f(y_0, a), f(x0, f(y_0, a)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
POL(F(x1, x2)) = (1/4)x2
POL(f(x1, x2)) = (1/4)x2
POL(a) = 1/4
The value of delta used in the strict ordering is 3/256.
The following usable rules [FROCOS05] were oriented:
f(f(x, a), y) → f(y, f(x, y))
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(f(f(y_0, a), a), x1) → F(f(y_0, a), x1)
F(f(f(y_0, a), a), f(y_1, a)) → F(f(y_0, a), f(y_1, a))
The TRS R consists of the following rules:
f(f(x, a), y) → f(y, f(x, y))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- F(f(f(y_0, a), a), x1) → F(f(y_0, a), x1)
The graph contains the following edges 1 > 1, 2 >= 2
- F(f(f(y_0, a), a), f(y_1, a)) → F(f(y_0, a), f(y_1, a))
The graph contains the following edges 1 > 1, 2 >= 2
(10) TRUE