(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f(x, 0) → s(x)
g(x) → h(x, gen)
h(0, x) → f(x, x)
a → b
The relative TRS consists of the following S rules:
gen → s(gen)
(1) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Combined order from the following AFS and order.
f(
x1,
x2) =
f(
x1,
x2)
0 =
0
s(
x1) =
x1
g(
x1) =
g(
x1)
h(
x1,
x2) =
h(
x1,
x2)
gen =
gen
a =
a
b =
b
Recursive path order with status [RPO].
Quasi-Precedence:
g1 > h2 > [f2, 0]
g1 > gen > [f2, 0]
a > b > [f2, 0]
Status:
f2: multiset
0: multiset
g1: multiset
h2: [2,1]
gen: multiset
a: multiset
b: multiset
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
f(x, 0) → s(x)
g(x) → h(x, gen)
h(0, x) → f(x, x)
a → b
Rules from S:
none
(2) Obligation:
Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:
gen → s(gen)
(3) RIsEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(4) YES