Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

minus#( x , s( y ) ) pred#( minus( x , y ) )
minus#( x , s( y ) ) minus#( x , y )
quot#( s( x ) , s( y ) ) quot#( minus( x , y ) , s( y ) )
quot#( s( x ) , s( y ) ) minus#( x , y )

1.1: dependency graph processor

The dependency pairs are split into 2 component(s).