Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

not#( or( x , y ) ) → not#( not( not( x ) ) )
not#( or( x , y ) ) → not#( not( x ) )
not#( or( x , y ) ) → not#( x )
not#( or( x , y ) ) → not#( not( not( y ) ) )
not#( or( x , y ) ) → not#( not( y ) )
not#( or( x , y ) ) → not#( y )
not#( and( x , y ) ) → not#( not( not( x ) ) )
not#( and( x , y ) ) → not#( not( x ) )
not#( and( x , y ) ) → not#( x )
not#( and( x , y ) ) → not#( not( not( y ) ) )
not#( and( x , y ) ) → not#( not( y ) )
not#( and( x , y ) ) → not#( y )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[and (x1, x2) ] = x1 + x2 + 1
[or (x1, x2) ] = x1 + x2 + 1
[not# (x1) ] = x1
[not (x1) ] = x1
[f(x1, ..., xn)] = x1 + ... + xn + 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.