Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

app#( app( apply , f ) , x ) → app#( f , x )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals

[app (x₁, x₂) ] = 2 x₁ + 2

[app# (x₁, x₂) ] = 3 x₁

[apply] = 0

[f(x₁, ..., x_n)] = x₁ + ... + 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.

[app (x₁, x₂) ]	=	2 x₁ + 2
[app# (x₁, x₂) ]	=	3 x₁
[apply]	=	0
[f(x₁, ..., x_n)]	=	x₁ + ... + x_n + 1	for all other symbols f of arity n