Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
a#
(
b
(
x
) )
→
a#
(
x
)
1.1: reduction pair processor
Using the following reduction pair
Linear polynomial interpretation over the naturals
[
a
(
x
1
) ]
=
2
x
1
[
b
(
x
1
) ]
=
x
1
+ 1
[
a#
(
x
1
) ]
=
x
1
[f(
x
1
, ...,
x
n
)]
=
x
1
+ ... +
x
n
+ 1
for all other symbols f of arity n
one remains with the following pair(s).
none
1.1.1: P is empty
All dependency pairs have been removed.