Termination proof

1: switching to dependency pairs

+#( 1 , 9 )	→	c#( 1 , 0 )
+#( 2 , 8 )	→	c#( 1 , 0 )
+#( 2 , 9 )	→	c#( 1 , 1 )
+#( 3 , 7 )	→	c#( 1 , 0 )
+#( 3 , 8 )	→	c#( 1 , 1 )
+#( 3 , 9 )	→	c#( 1 , 2 )
+#( 4 , 6 )	→	c#( 1 , 0 )
+#( 4 , 7 )	→	c#( 1 , 1 )
+#( 4 , 8 )	→	c#( 1 , 2 )
+#( 4 , 9 )	→	c#( 1 , 3 )
+#( 5 , 5 )	→	c#( 1 , 0 )
+#( 5 , 6 )	→	c#( 1 , 1 )
+#( 5 , 7 )	→	c#( 1 , 2 )
+#( 5 , 8 )	→	c#( 1 , 3 )
+#( 5 , 9 )	→	c#( 1 , 4 )
+#( 6 , 4 )	→	c#( 1 , 0 )
+#( 6 , 5 )	→	c#( 1 , 1 )
+#( 6 , 6 )	→	c#( 1 , 2 )
+#( 6 , 7 )	→	c#( 1 , 3 )
+#( 6 , 8 )	→	c#( 1 , 4 )
+#( 6 , 9 )	→	c#( 1 , 5 )
+#( 7 , 3 )	→	c#( 1 , 0 )
+#( 7 , 4 )	→	c#( 1 , 1 )
+#( 7 , 5 )	→	c#( 1 , 2 )
+#( 7 , 6 )	→	c#( 1 , 3 )
+#( 7 , 7 )	→	c#( 1 , 4 )
+#( 7 , 8 )	→	c#( 1 , 5 )
+#( 7 , 9 )	→	c#( 1 , 6 )
+#( 8 , 2 )	→	c#( 1 , 0 )
+#( 8 , 3 )	→	c#( 1 , 1 )
+#( 8 , 4 )	→	c#( 1 , 2 )
+#( 8 , 5 )	→	c#( 1 , 3 )
+#( 8 , 6 )	→	c#( 1 , 4 )
+#( 8 , 7 )	→	c#( 1 , 5 )
+#( 8 , 8 )	→	c#( 1 , 6 )
+#( 8 , 9 )	→	c#( 1 , 7 )
+#( 9 , 1 )	→	c#( 1 , 0 )
+#( 9 , 2 )	→	c#( 1 , 1 )
+#( 9 , 3 )	→	c#( 1 , 2 )
+#( 9 , 4 )	→	c#( 1 , 3 )
+#( 9 , 5 )	→	c#( 1 , 4 )
+#( 9 , 6 )	→	c#( 1 , 5 )
+#( 9 , 7 )	→	c#( 1 , 6 )
+#( 9 , 8 )	→	c#( 1 , 7 )
+#( 9 , 9 )	→	c#( 1 , 8 )
+#( x , c( y , z ) )	→	c#( y , +( x , z ) )
+#( x , c( y , z ) )	→	+#( x , z )
+#( c( x , y ) , z )	→	c#( x , +( y , z ) )
+#( c( x , y ) , z )	→	+#( y , z )
c#( x , c( y , z ) )	→	c#( +( x , y ) , z )
c#( x , c( y , z ) )	→	+#( x , y )

1.1: dependency graph processor

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

• The 1st component contains the pair(s)

  +#( x , c( y , z ) )	→	c#( y , +( x , z ) )
  c#( x , c( y , z ) )	→	c#( +( x , y ) , z )
  c#( x , c( y , z ) )	→	+#( x , y )
  +#( x , c( y , z ) )	→	+#( x , z )
  +#( c( x , y ) , z )	→	c#( x , +( y , z ) )
  +#( c( x , y ) , z )	→	+#( y , z )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [c# (x1, x2) ]	=	x1 + x2
  [2]	=	1
  [6]	=	2
  [0]	=	0
  [+# (x1, x2) ]	=	x1 + x2
  [7]	=	2
  [9]	=	2
  [5]	=	1
  [c (x1, x2) ]	=	x1 + x2 + 1
  [+ (x1, x2) ]	=	x1 + x2
  [8]	=	2
  [1]	=	1
  [3]	=	1
  [4]	=	1
  [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.1: P is empty

  All dependency pairs have been removed.