(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
l(m(x)) → m(l(x))
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
The relative TRS consists of the following S rules:
f(x, y) → f(x, r(y))
b → l(b)
(1) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
| POL(f(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
l(m(x)) → m(l(x))
Rules from S:
none
(2) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
m(r(x)) → r(m(x))
f(m(x), y) → f(x, m(y))
The relative TRS consists of the following S rules:
f(x, y) → f(x, r(y))
b → l(b)
(3) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Combined order from the following AFS and order.
m(
x1) =
m(
x1)
r(
x1) =
x1
f(
x1,
x2) =
f(
x1,
x2)
b =
b
l(
x1) =
x1
Recursive path order with status [RPO].
Quasi-Precedence:
f2 > m1
b > m1
Status:
m1: multiset
f2: [1,2]
b: multiset
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
f(m(x), y) → f(x, m(y))
Rules from S:
none
(4) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
m(r(x)) → r(m(x))
The relative TRS consists of the following S rules:
f(x, y) → f(x, r(y))
b → l(b)
(5) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
| POL(f(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
m(r(x)) → r(m(x))
Rules from S:
none
(6) Obligation:
Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:
f(x, y) → f(x, r(y))
b → l(b)
(7) RIsEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(8) YES