Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
f#
(
f
(
x
) )
→
f#
(
x
)
1.1: reduction pair processor
Using the following reduction pair
Linear polynomial interpretation over the naturals
[
f
(
x
1
) ]
=
2
x
1
+ 2
[
f#
(
x
1
) ]
=
3
x
1
[
g
(
x
1
) ]
=
x
1
+ 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.