(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f(a, b, x) → f(x, x, x)
The relative TRS consists of the following S rules:
f(x, y, z) → f(y, x, z)
f(x, y, z) → f(x, z, y)
f(x, y, z) → f(z, y, x)
(1) RootLabelingProof (EQUIVALENT transformation)
We used plain root labeling [ROOTLAB] with the following heuristic:
LabelAll: All function symbols get labeled
(2) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f_{a,b,f_3}(a, b, x) → f_{f_3,f_3,f_3}(x, x, x)
f_{a,b,a}(a, b, x) → f_{a,a,a}(x, x, x)
f_{a,b,b}(a, b, x) → f_{b,b,b}(x, x, x)
The relative TRS consists of the following S rules:
f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,f_3}(y, x, z)
f_{f_3,f_3,a}(x, y, z) → f_{f_3,f_3,a}(y, x, z)
f_{f_3,f_3,b}(x, y, z) → f_{f_3,f_3,b}(y, x, z)
f_{f_3,a,f_3}(x, y, z) → f_{a,f_3,f_3}(y, x, z)
f_{f_3,a,a}(x, y, z) → f_{a,f_3,a}(y, x, z)
f_{f_3,a,b}(x, y, z) → f_{a,f_3,b}(y, x, z)
f_{f_3,b,f_3}(x, y, z) → f_{b,f_3,f_3}(y, x, z)
f_{f_3,b,a}(x, y, z) → f_{b,f_3,a}(y, x, z)
f_{f_3,b,b}(x, y, z) → f_{b,f_3,b}(y, x, z)
f_{a,f_3,f_3}(x, y, z) → f_{f_3,a,f_3}(y, x, z)
f_{a,f_3,a}(x, y, z) → f_{f_3,a,a}(y, x, z)
f_{a,f_3,b}(x, y, z) → f_{f_3,a,b}(y, x, z)
f_{a,a,f_3}(x, y, z) → f_{a,a,f_3}(y, x, z)
f_{a,a,a}(x, y, z) → f_{a,a,a}(y, x, z)
f_{a,a,b}(x, y, z) → f_{a,a,b}(y, x, z)
f_{a,b,f_3}(x, y, z) → f_{b,a,f_3}(y, x, z)
f_{a,b,a}(x, y, z) → f_{b,a,a}(y, x, z)
f_{a,b,b}(x, y, z) → f_{b,a,b}(y, x, z)
f_{b,f_3,f_3}(x, y, z) → f_{f_3,b,f_3}(y, x, z)
f_{b,f_3,a}(x, y, z) → f_{f_3,b,a}(y, x, z)
f_{b,f_3,b}(x, y, z) → f_{f_3,b,b}(y, x, z)
f_{b,a,f_3}(x, y, z) → f_{a,b,f_3}(y, x, z)
f_{b,a,a}(x, y, z) → f_{a,b,a}(y, x, z)
f_{b,a,b}(x, y, z) → f_{a,b,b}(y, x, z)
f_{b,b,f_3}(x, y, z) → f_{b,b,f_3}(y, x, z)
f_{b,b,a}(x, y, z) → f_{b,b,a}(y, x, z)
f_{b,b,b}(x, y, z) → f_{b,b,b}(y, x, z)
f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,f_3}(x, z, y)
f_{f_3,f_3,a}(x, y, z) → f_{f_3,a,f_3}(x, z, y)
f_{f_3,f_3,b}(x, y, z) → f_{f_3,b,f_3}(x, z, y)
f_{f_3,a,f_3}(x, y, z) → f_{f_3,f_3,a}(x, z, y)
f_{f_3,a,a}(x, y, z) → f_{f_3,a,a}(x, z, y)
f_{f_3,a,b}(x, y, z) → f_{f_3,b,a}(x, z, y)
f_{f_3,b,f_3}(x, y, z) → f_{f_3,f_3,b}(x, z, y)
f_{f_3,b,a}(x, y, z) → f_{f_3,a,b}(x, z, y)
f_{f_3,b,b}(x, y, z) → f_{f_3,b,b}(x, z, y)
f_{a,f_3,f_3}(x, y, z) → f_{a,f_3,f_3}(x, z, y)
f_{a,f_3,a}(x, y, z) → f_{a,a,f_3}(x, z, y)
f_{a,f_3,b}(x, y, z) → f_{a,b,f_3}(x, z, y)
f_{a,a,f_3}(x, y, z) → f_{a,f_3,a}(x, z, y)
f_{a,a,a}(x, y, z) → f_{a,a,a}(x, z, y)
f_{a,a,b}(x, y, z) → f_{a,b,a}(x, z, y)
f_{a,b,f_3}(x, y, z) → f_{a,f_3,b}(x, z, y)
f_{a,b,a}(x, y, z) → f_{a,a,b}(x, z, y)
f_{a,b,b}(x, y, z) → f_{a,b,b}(x, z, y)
f_{b,f_3,f_3}(x, y, z) → f_{b,f_3,f_3}(x, z, y)
f_{b,f_3,a}(x, y, z) → f_{b,a,f_3}(x, z, y)
f_{b,f_3,b}(x, y, z) → f_{b,b,f_3}(x, z, y)
f_{b,a,f_3}(x, y, z) → f_{b,f_3,a}(x, z, y)
f_{b,a,a}(x, y, z) → f_{b,a,a}(x, z, y)
f_{b,a,b}(x, y, z) → f_{b,b,a}(x, z, y)
f_{b,b,f_3}(x, y, z) → f_{b,f_3,b}(x, z, y)
f_{b,b,a}(x, y, z) → f_{b,a,b}(x, z, y)
f_{b,b,b}(x, y, z) → f_{b,b,b}(x, z, y)
f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,f_3}(z, y, x)
f_{f_3,f_3,a}(x, y, z) → f_{a,f_3,f_3}(z, y, x)
f_{f_3,f_3,b}(x, y, z) → f_{b,f_3,f_3}(z, y, x)
f_{f_3,a,f_3}(x, y, z) → f_{f_3,a,f_3}(z, y, x)
f_{f_3,a,a}(x, y, z) → f_{a,a,f_3}(z, y, x)
f_{f_3,a,b}(x, y, z) → f_{b,a,f_3}(z, y, x)
f_{f_3,b,f_3}(x, y, z) → f_{f_3,b,f_3}(z, y, x)
f_{f_3,b,a}(x, y, z) → f_{a,b,f_3}(z, y, x)
f_{f_3,b,b}(x, y, z) → f_{b,b,f_3}(z, y, x)
f_{a,f_3,f_3}(x, y, z) → f_{f_3,f_3,a}(z, y, x)
f_{a,f_3,a}(x, y, z) → f_{a,f_3,a}(z, y, x)
f_{a,f_3,b}(x, y, z) → f_{b,f_3,a}(z, y, x)
f_{a,a,f_3}(x, y, z) → f_{f_3,a,a}(z, y, x)
f_{a,a,a}(x, y, z) → f_{a,a,a}(z, y, x)
f_{a,a,b}(x, y, z) → f_{b,a,a}(z, y, x)
f_{a,b,f_3}(x, y, z) → f_{f_3,b,a}(z, y, x)
f_{a,b,a}(x, y, z) → f_{a,b,a}(z, y, x)
f_{a,b,b}(x, y, z) → f_{b,b,a}(z, y, x)
f_{b,f_3,f_3}(x, y, z) → f_{f_3,f_3,b}(z, y, x)
f_{b,f_3,a}(x, y, z) → f_{a,f_3,b}(z, y, x)
f_{b,f_3,b}(x, y, z) → f_{b,f_3,b}(z, y, x)
f_{b,a,f_3}(x, y, z) → f_{f_3,a,b}(z, y, x)
f_{b,a,a}(x, y, z) → f_{a,a,b}(z, y, x)
f_{b,a,b}(x, y, z) → f_{b,a,b}(z, y, x)
f_{b,b,f_3}(x, y, z) → f_{f_3,b,b}(z, y, x)
f_{b,b,a}(x, y, z) → f_{a,b,b}(z, y, x)
f_{b,b,b}(x, y, z) → f_{b,b,b}(z, y, x)
(3) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Recursive path order with status [RPO].
Quasi-Precedence:
[f{a,b,f3}3, f{f3,a,b}3, f{a,f3,b}3, f{f3,b,a}3, f{b,f3,a}3, f{b,a,f3}3] > f{f3,f3,f3}3
a > f{f3,f3,f3}3
b > f{f3,f3,f3}3
[f{a,b,a}3, f{a,a,b}3, f{b,a,a}3] > f{a,a,a}3
[f{a,b,b}3, f{b,a,b}3, f{b,b,a}3] > f{b,b,b}3
[f{f3,f3,a}3, f{f3,a,f3}3, f{a,f3,f3}3]
[f{f3,f3,b}3, f{f3,b,f3}3, f{b,f3,f3}3]
[f{f3,a,a}3, f{a,f3,a}3, f{a,a,f3}3]
[f{f3,b,b}3, f{b,f3,b}3, f{b,b,f3}3]
Status:
f{a,b,f3}3: multiset
a: multiset
b: multiset
f{f3,f3,f3}3: multiset
f{a,b,a}3: multiset
f{a,a,a}3: multiset
f{a,b,b}3: multiset
f{b,b,b}3: multiset
f{f3,f3,a}3: multiset
f{f3,f3,b}3: multiset
f{f3,a,f3}3: multiset
f{a,f3,f3}3: multiset
f{f3,a,a}3: multiset
f{a,f3,a}3: multiset
f{f3,a,b}3: multiset
f{a,f3,b}3: multiset
f{f3,b,f3}3: multiset
f{b,f3,f3}3: multiset
f{f3,b,a}3: multiset
f{b,f3,a}3: multiset
f{f3,b,b}3: multiset
f{b,f3,b}3: multiset
f{a,a,f3}3: multiset
f{a,a,b}3: multiset
f{b,a,f3}3: multiset
f{b,a,a}3: multiset
f{b,a,b}3: multiset
f{b,b,f3}3: multiset
f{b,b,a}3: multiset
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
f_{a,b,f_3}(a, b, x) → f_{f_3,f_3,f_3}(x, x, x)
f_{a,b,a}(a, b, x) → f_{a,a,a}(x, x, x)
f_{a,b,b}(a, b, x) → f_{b,b,b}(x, x, x)
Rules from S:
none
(4) Obligation:
Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:
f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,f_3}(y, x, z)
f_{f_3,f_3,a}(x, y, z) → f_{f_3,f_3,a}(y, x, z)
f_{f_3,f_3,b}(x, y, z) → f_{f_3,f_3,b}(y, x, z)
f_{f_3,a,f_3}(x, y, z) → f_{a,f_3,f_3}(y, x, z)
f_{f_3,a,a}(x, y, z) → f_{a,f_3,a}(y, x, z)
f_{f_3,a,b}(x, y, z) → f_{a,f_3,b}(y, x, z)
f_{f_3,b,f_3}(x, y, z) → f_{b,f_3,f_3}(y, x, z)
f_{f_3,b,a}(x, y, z) → f_{b,f_3,a}(y, x, z)
f_{f_3,b,b}(x, y, z) → f_{b,f_3,b}(y, x, z)
f_{a,f_3,f_3}(x, y, z) → f_{f_3,a,f_3}(y, x, z)
f_{a,f_3,a}(x, y, z) → f_{f_3,a,a}(y, x, z)
f_{a,f_3,b}(x, y, z) → f_{f_3,a,b}(y, x, z)
f_{a,a,f_3}(x, y, z) → f_{a,a,f_3}(y, x, z)
f_{a,a,a}(x, y, z) → f_{a,a,a}(y, x, z)
f_{a,a,b}(x, y, z) → f_{a,a,b}(y, x, z)
f_{a,b,f_3}(x, y, z) → f_{b,a,f_3}(y, x, z)
f_{a,b,a}(x, y, z) → f_{b,a,a}(y, x, z)
f_{a,b,b}(x, y, z) → f_{b,a,b}(y, x, z)
f_{b,f_3,f_3}(x, y, z) → f_{f_3,b,f_3}(y, x, z)
f_{b,f_3,a}(x, y, z) → f_{f_3,b,a}(y, x, z)
f_{b,f_3,b}(x, y, z) → f_{f_3,b,b}(y, x, z)
f_{b,a,f_3}(x, y, z) → f_{a,b,f_3}(y, x, z)
f_{b,a,a}(x, y, z) → f_{a,b,a}(y, x, z)
f_{b,a,b}(x, y, z) → f_{a,b,b}(y, x, z)
f_{b,b,f_3}(x, y, z) → f_{b,b,f_3}(y, x, z)
f_{b,b,a}(x, y, z) → f_{b,b,a}(y, x, z)
f_{b,b,b}(x, y, z) → f_{b,b,b}(y, x, z)
f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,f_3}(x, z, y)
f_{f_3,f_3,a}(x, y, z) → f_{f_3,a,f_3}(x, z, y)
f_{f_3,f_3,b}(x, y, z) → f_{f_3,b,f_3}(x, z, y)
f_{f_3,a,f_3}(x, y, z) → f_{f_3,f_3,a}(x, z, y)
f_{f_3,a,a}(x, y, z) → f_{f_3,a,a}(x, z, y)
f_{f_3,a,b}(x, y, z) → f_{f_3,b,a}(x, z, y)
f_{f_3,b,f_3}(x, y, z) → f_{f_3,f_3,b}(x, z, y)
f_{f_3,b,a}(x, y, z) → f_{f_3,a,b}(x, z, y)
f_{f_3,b,b}(x, y, z) → f_{f_3,b,b}(x, z, y)
f_{a,f_3,f_3}(x, y, z) → f_{a,f_3,f_3}(x, z, y)
f_{a,f_3,a}(x, y, z) → f_{a,a,f_3}(x, z, y)
f_{a,f_3,b}(x, y, z) → f_{a,b,f_3}(x, z, y)
f_{a,a,f_3}(x, y, z) → f_{a,f_3,a}(x, z, y)
f_{a,a,a}(x, y, z) → f_{a,a,a}(x, z, y)
f_{a,a,b}(x, y, z) → f_{a,b,a}(x, z, y)
f_{a,b,f_3}(x, y, z) → f_{a,f_3,b}(x, z, y)
f_{a,b,a}(x, y, z) → f_{a,a,b}(x, z, y)
f_{a,b,b}(x, y, z) → f_{a,b,b}(x, z, y)
f_{b,f_3,f_3}(x, y, z) → f_{b,f_3,f_3}(x, z, y)
f_{b,f_3,a}(x, y, z) → f_{b,a,f_3}(x, z, y)
f_{b,f_3,b}(x, y, z) → f_{b,b,f_3}(x, z, y)
f_{b,a,f_3}(x, y, z) → f_{b,f_3,a}(x, z, y)
f_{b,a,a}(x, y, z) → f_{b,a,a}(x, z, y)
f_{b,a,b}(x, y, z) → f_{b,b,a}(x, z, y)
f_{b,b,f_3}(x, y, z) → f_{b,f_3,b}(x, z, y)
f_{b,b,a}(x, y, z) → f_{b,a,b}(x, z, y)
f_{b,b,b}(x, y, z) → f_{b,b,b}(x, z, y)
f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,f_3}(z, y, x)
f_{f_3,f_3,a}(x, y, z) → f_{a,f_3,f_3}(z, y, x)
f_{f_3,f_3,b}(x, y, z) → f_{b,f_3,f_3}(z, y, x)
f_{f_3,a,f_3}(x, y, z) → f_{f_3,a,f_3}(z, y, x)
f_{f_3,a,a}(x, y, z) → f_{a,a,f_3}(z, y, x)
f_{f_3,a,b}(x, y, z) → f_{b,a,f_3}(z, y, x)
f_{f_3,b,f_3}(x, y, z) → f_{f_3,b,f_3}(z, y, x)
f_{f_3,b,a}(x, y, z) → f_{a,b,f_3}(z, y, x)
f_{f_3,b,b}(x, y, z) → f_{b,b,f_3}(z, y, x)
f_{a,f_3,f_3}(x, y, z) → f_{f_3,f_3,a}(z, y, x)
f_{a,f_3,a}(x, y, z) → f_{a,f_3,a}(z, y, x)
f_{a,f_3,b}(x, y, z) → f_{b,f_3,a}(z, y, x)
f_{a,a,f_3}(x, y, z) → f_{f_3,a,a}(z, y, x)
f_{a,a,a}(x, y, z) → f_{a,a,a}(z, y, x)
f_{a,a,b}(x, y, z) → f_{b,a,a}(z, y, x)
f_{a,b,f_3}(x, y, z) → f_{f_3,b,a}(z, y, x)
f_{a,b,a}(x, y, z) → f_{a,b,a}(z, y, x)
f_{a,b,b}(x, y, z) → f_{b,b,a}(z, y, x)
f_{b,f_3,f_3}(x, y, z) → f_{f_3,f_3,b}(z, y, x)
f_{b,f_3,a}(x, y, z) → f_{a,f_3,b}(z, y, x)
f_{b,f_3,b}(x, y, z) → f_{b,f_3,b}(z, y, x)
f_{b,a,f_3}(x, y, z) → f_{f_3,a,b}(z, y, x)
f_{b,a,a}(x, y, z) → f_{a,a,b}(z, y, x)
f_{b,a,b}(x, y, z) → f_{b,a,b}(z, y, x)
f_{b,b,f_3}(x, y, z) → f_{f_3,b,b}(z, y, x)
f_{b,b,a}(x, y, z) → f_{a,b,b}(z, y, x)
f_{b,b,b}(x, y, z) → f_{b,b,b}(z, y, x)
(5) RIsEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(6) YES