Termination proof

1: switching to dependency pairs

+#( 0( x ) , 0( y ) )	→	0#( +( x , y ) )
+#( 0( x ) , 0( y ) )	→	+#( x , y )
+#( 0( x ) , 1( y ) )	→	+#( x , y )
+#( 1( x ) , 0( y ) )	→	+#( x , y )
+#( 1( x ) , 1( y ) )	→	0#( +( +( x , y ) , 1( # ) ) )
+#( 1( x ) , 1( y ) )	→	+#( +( x , y ) , 1( # ) )
+#( 1( x ) , 1( y ) )	→	+#( x , y )
+#( x , +( y , z ) )	→	+#( +( x , y ) , z )
+#( x , +( y , z ) )	→	+#( x , y )
-#( 0( x ) , 0( y ) )	→	0#( -( x , y ) )
-#( 0( x ) , 0( y ) )	→	-#( x , y )
-#( 0( x ) , 1( y ) )	→	-#( -( x , y ) , 1( # ) )
-#( 0( x ) , 1( y ) )	→	-#( x , y )
-#( 1( x ) , 0( y ) )	→	-#( x , y )
-#( 1( x ) , 1( y ) )	→	0#( -( x , y ) )
-#( 1( x ) , 1( y ) )	→	-#( x , y )
ge#( 0( x ) , 0( y ) )	→	ge#( x , y )
ge#( 0( x ) , 1( y ) )	→	not#( ge( y , x ) )
ge#( 0( x ) , 1( y ) )	→	ge#( y , x )
ge#( 1( x ) , 0( y ) )	→	ge#( x , y )
ge#( 1( x ) , 1( y ) )	→	ge#( x , y )
ge#( # , 0( x ) )	→	ge#( # , x )
min#( n( x , y , z ) )	→	min#( y )
max#( n( x , y , z ) )	→	max#( z )
bs#( n( x , y , z ) )	→	and#( and( ge( x , max( y ) ) , ge( min( z ) , x ) ) , and( bs( y ) , bs( z ) ) )
bs#( n( x , y , z ) )	→	and#( ge( x , max( y ) ) , ge( min( z ) , x ) )
bs#( n( x , y , z ) )	→	ge#( x , max( y ) )
bs#( n( x , y , z ) )	→	max#( y )
bs#( n( x , y , z ) )	→	ge#( min( z ) , x )
bs#( n( x , y , z ) )	→	min#( z )
bs#( n( x , y , z ) )	→	and#( bs( y ) , bs( z ) )
bs#( n( x , y , z ) )	→	bs#( y )
bs#( n( x , y , z ) )	→	bs#( z )
size#( n( x , y , z ) )	→	+#( +( size( x ) , size( y ) ) , 1( # ) )
size#( n( x , y , z ) )	→	+#( size( x ) , size( y ) )
size#( n( x , y , z ) )	→	size#( x )
size#( n( x , y , z ) )	→	size#( y )
wb#( n( x , y , z ) )	→	and#( if( ge( size( y ) , size( z ) ) , ge( 1( # ) , -( size( y ) , size( z ) ) ) , ge( 1( # ) , -( size( z ) , size( y ) ) ) ) , and( wb( y ) , wb( z ) ) )
wb#( n( x , y , z ) )	→	if#( ge( size( y ) , size( z ) ) , ge( 1( # ) , -( size( y ) , size( z ) ) ) , ge( 1( # ) , -( size( z ) , size( y ) ) ) )
wb#( n( x , y , z ) )	→	ge#( size( y ) , size( z ) )
wb#( n( x , y , z ) )	→	size#( y )
wb#( n( x , y , z ) )	→	size#( z )
wb#( n( x , y , z ) )	→	ge#( 1( # ) , -( size( y ) , size( z ) ) )
wb#( n( x , y , z ) )	→	-#( size( y ) , size( z ) )
wb#( n( x , y , z ) )	→	size#( y )
wb#( n( x , y , z ) )	→	size#( z )
wb#( n( x , y , z ) )	→	ge#( 1( # ) , -( size( z ) , size( y ) ) )
wb#( n( x , y , z ) )	→	-#( size( z ) , size( y ) )
wb#( n( x , y , z ) )	→	size#( z )
wb#( n( x , y , z ) )	→	size#( y )
wb#( n( x , y , z ) )	→	and#( wb( y ) , wb( z ) )
wb#( n( x , y , z ) )	→	wb#( y )
wb#( n( x , y , z ) )	→	wb#( z )

1.1: dependency graph processor

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

• The 1st component contains the pair(s)

  wb#( n( x , y , z ) )	→	wb#( z )
  wb#( n( x , y , z ) )	→	wb#( y )

  1.1.1: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	x1 + 2 x2 + x3
  [#]	=	0
  [wb (x1) ]	=	2 x1 + 2
  [n (x1, x2, x3) ]	=	3 x1 + 3 x2 + 2 x3 + 3
  [size (x1) ]	=	x1
  [1 (x1) ]	=	2
  [wb# (x1) ]	=	2 x1
  [ge (x1, x2) ]	=	1
  [max (x1) ]	=	x1
  [true]	=	1
  [and (x1, x2) ]	=	2 x1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + x2
  [- (x1, x2) ]	=	x1 + 2 x2
  [l (x1) ]	=	x1 + 2
  [min (x1) ]	=	3 x1
  [0 (x1) ]	=	0
  [bs (x1) ]	=	3 x1
  [not (x1) ]	=	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.

• The 2nd component contains the pair(s)

  size#( n( x , y , z ) )	→	size#( y )
  size#( n( x , y , z ) )	→	size#( x )

  1.1.2: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	x1 + 2 x2
  [#]	=	0
  [wb (x1) ]	=	1
  [n (x1, x2, x3) ]	=	3 x1 + 2 x2 + 2 x3 + 3
  [size (x1) ]	=	2 x1 + 2
  [1 (x1) ]	=	2
  [ge (x1, x2) ]	=	0
  [max (x1) ]	=	x1
  [true]	=	0
  [and (x1, x2) ]	=	2 x1
  [size# (x1) ]	=	2 x1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + x2
  [- (x1, x2) ]	=	2 x1
  [l (x1) ]	=	x1 + 3
  [min (x1) ]	=	3 x1
  [0 (x1) ]	=	2
  [bs (x1) ]	=	3 x1 + 3
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.2.1: P is empty

  All dependency pairs have been removed.

• The 3rd component contains the pair(s)

  +#( 0( x ) , 1( y ) )	→	+#( x , y )
  +#( 0( x ) , 0( y ) )	→	+#( x , y )
  +#( 1( x ) , 0( y ) )	→	+#( x , y )
  +#( 1( x ) , 1( y ) )	→	+#( +( x , y ) , 1( # ) )
  +#( 1( x ) , 1( y ) )	→	+#( x , y )
  +#( x , +( y , z ) )	→	+#( +( x , y ) , z )
  +#( x , +( y , z ) )	→	+#( x , y )

  1.1.3: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	2 x1 + 2 x2
  [#]	=	0
  [wb (x1) ]	=	0
  [n (x1, x2, x3) ]	=	x1 + x2 + 2 x3 + 3
  [size (x1) ]	=	2 x1 + 2
  [1 (x1) ]	=	x1 + 1
  [+# (x1, x2) ]	=	2 x1
  [ge (x1, x2) ]	=	0
  [max (x1) ]	=	2 x1
  [true]	=	0
  [and (x1, x2) ]	=	2 x1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + x2
  [- (x1, x2) ]	=	x1
  [l (x1) ]	=	x1 + 3
  [min (x1) ]	=	2 x1
  [0 (x1) ]	=	x1 + 1
  [bs (x1) ]	=	0
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

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

  1.1.3.1: dependency graph processor

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

  • The 1st component contains the pair(s)

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

    1.1.3.1.1: reduction pair processor

    Using the following reduction pair

    Linear polynomial interpretation over the naturals

    [val (x1) ]	=	x1
    [if (x1, x2, x3) ]	=	x1 + x2
    [#]	=	0
    [wb (x1) ]	=	2 x1 + 1
    [n (x1, x2, x3) ]	=	2 x1 + 2 x2 + 2 x3 + 1
    [size (x1) ]	=	3 x1
    [1 (x1) ]	=	0
    [+# (x1, x2) ]	=	x1
    [ge (x1, x2) ]	=	0
    [max (x1) ]	=	x1
    [true]	=	0
    [and (x1, x2) ]	=	x1
    [false]	=	0
    [+ (x1, x2) ]	=	x1 + 2 x2 + 1
    [- (x1, x2) ]	=	x1 + 1
    [l (x1) ]	=	x1
    [min (x1) ]	=	x1
    [0 (x1) ]	=	1
    [bs (x1) ]	=	1
    [not (x1) ]	=	0
    [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

    one remains with the following pair(s).

    none

    1.1.3.1.1.1: P is empty

    All dependency pairs have been removed.

  • The 2nd component contains the pair(s)

    +#( 1( x ) , 1( y ) )

    →

    +#( +( x , y ) , 1( # ) )

    1.1.3.1.2: reduction pair processor

    Using the following reduction pair

    Linear polynomial interpretation over the naturals

    [val (x1) ]	=	x1
    [if (x1, x2, x3) ]	=	2 x1 + 2 x2
    [#]	=	0
    [wb (x1) ]	=	1
    [n (x1, x2, x3) ]	=	2 x1 + 2 x2 + 2 x3 + 3
    [size (x1) ]	=	2 x1
    [1 (x1) ]	=	x1 + 2
    [+# (x1, x2) ]	=	x1 + 2 x2
    [ge (x1, x2) ]	=	0
    [max (x1) ]	=	x1
    [true]	=	0
    [and (x1, x2) ]	=	2 x1
    [false]	=	0
    [+ (x1, x2) ]	=	x1 + 2 x2
    [- (x1, x2) ]	=	x1
    [l (x1) ]	=	x1 + 1
    [min (x1) ]	=	3 x1
    [0 (x1) ]	=	x1 + 2
    [bs (x1) ]	=	3
    [not (x1) ]	=	0
    [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

    one remains with the following pair(s).

    none

    1.1.3.1.2.1: P is empty

    All dependency pairs have been removed.

• The 4th component contains the pair(s)

  -#( 0( x ) , 1( y ) )	→	-#( -( x , y ) , 1( # ) )
  -#( 0( x ) , 1( y ) )	→	-#( x , y )
  -#( 0( x ) , 0( y ) )	→	-#( x , y )
  -#( 1( x ) , 0( y ) )	→	-#( x , y )
  -#( 1( x ) , 1( y ) )	→	-#( x , y )

  1.1.4: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	2 x1 + 2 x2
  [#]	=	0
  [wb (x1) ]	=	2
  [n (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3 + 2
  [size (x1) ]	=	2 x1 + 1
  [1 (x1) ]	=	x1 + 2
  [-# (x1, x2) ]	=	2 x1
  [ge (x1, x2) ]	=	0
  [max (x1) ]	=	x1
  [true]	=	0
  [and (x1, x2) ]	=	2 x1 + 1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + x2
  [- (x1, x2) ]	=	x1
  [l (x1) ]	=	x1 + 2
  [min (x1) ]	=	3 x1
  [0 (x1) ]	=	x1 + 2
  [bs (x1) ]	=	2 x1
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.4.1: P is empty

  All dependency pairs have been removed.

• The 5th component contains the pair(s)

  bs#( n( x , y , z ) )	→	bs#( z )
  bs#( n( x , y , z ) )	→	bs#( y )

  1.1.5: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	x1 + 2 x2 + x3
  [#]	=	0
  [wb (x1) ]	=	2 x1 + 2
  [n (x1, x2, x3) ]	=	3 x1 + 3 x2 + 2 x3 + 3
  [size (x1) ]	=	x1
  [1 (x1) ]	=	2
  [bs# (x1) ]	=	2 x1
  [ge (x1, x2) ]	=	1
  [max (x1) ]	=	x1
  [true]	=	1
  [and (x1, x2) ]	=	2 x1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + x2
  [- (x1, x2) ]	=	x1 + 2 x2
  [l (x1) ]	=	x1 + 2
  [min (x1) ]	=	3 x1
  [0 (x1) ]	=	0
  [bs (x1) ]	=	3 x1
  [not (x1) ]	=	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.5.1: P is empty

  All dependency pairs have been removed.

• The 6th component contains the pair(s)

  ge#( 0( x ) , 1( y ) )	→	ge#( y , x )
  ge#( 0( x ) , 0( y ) )	→	ge#( x , y )
  ge#( 1( x ) , 0( y ) )	→	ge#( x , y )
  ge#( 1( x ) , 1( y ) )	→	ge#( x , y )

  1.1.6: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	2 x1 + 2 x2
  [#]	=	0
  [wb (x1) ]	=	1
  [n (x1, x2, x3) ]	=	x1 + 2 x2 + 2 x3 + 3
  [size (x1) ]	=	2 x1 + 1
  [1 (x1) ]	=	x1 + 1
  [ge (x1, x2) ]	=	0
  [max (x1) ]	=	x1
  [true]	=	0
  [and (x1, x2) ]	=	2 x1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + 2 x2
  [- (x1, x2) ]	=	x1
  [l (x1) ]	=	x1
  [min (x1) ]	=	3 x1
  [0 (x1) ]	=	x1 + 1
  [ge# (x1, x2) ]	=	3 x1 + 3 x2
  [bs (x1) ]	=	3
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.6.1: P is empty

  All dependency pairs have been removed.

• The 7th component contains the pair(s)

  ge#( # , 0( x ) )

  →

  ge#( # , x )

  1.1.7: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	2 x1 + 2 x2
  [#]	=	0
  [wb (x1) ]	=	0
  [n (x1, x2, x3) ]	=	3 x1 + 2 x2 + 2 x3 + 2
  [size (x1) ]	=	2 x1
  [1 (x1) ]	=	x1 + 1
  [ge (x1, x2) ]	=	0
  [max (x1) ]	=	3 x1
  [true]	=	0
  [and (x1, x2) ]	=	2 x1 + x2
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + 2 x2
  [- (x1, x2) ]	=	x1
  [l (x1) ]	=	x1 + 1
  [min (x1) ]	=	2 x1
  [0 (x1) ]	=	x1 + 1
  [ge# (x1, x2) ]	=	2 x1
  [bs (x1) ]	=	x1
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.7.1: P is empty

  All dependency pairs have been removed.

• The 8th component contains the pair(s)

  min#( n( x , y , z ) )

  →

  min#( y )

  1.1.8: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	2 x1 + x2
  [#]	=	0
  [wb (x1) ]	=	2 x1 + 2
  [n (x1, x2, x3) ]	=	2 x1 + 2 x2 + 2 x3 + 3
  [size (x1) ]	=	x1
  [1 (x1) ]	=	x1 + 1
  [ge (x1, x2) ]	=	x1
  [min# (x1) ]	=	3 x1
  [max (x1) ]	=	3 x1 + 1
  [true]	=	0
  [and (x1, x2) ]	=	x1 + 1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + x2
  [- (x1, x2) ]	=	x1
  [l (x1) ]	=	x1 + 3
  [min (x1) ]	=	2 x1
  [0 (x1) ]	=	x1 + 1
  [bs (x1) ]	=	2 x1 + 2
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.8.1: P is empty

  All dependency pairs have been removed.

• The 9th component contains the pair(s)

  max#( n( x , y , z ) )

  →

  max#( z )

  1.1.9: reduction pair processor

  Using the following reduction pair

  Linear polynomial interpretation over the naturals

  [val (x1) ]	=	x1
  [if (x1, x2, x3) ]	=	2 x1 + 2 x2
  [#]	=	0
  [wb (x1) ]	=	0
  [n (x1, x2, x3) ]	=	x1 + x2 + 3 x3 + 1
  [size (x1) ]	=	0
  [1 (x1) ]	=	0
  [ge (x1, x2) ]	=	0
  [max (x1) ]	=	3 x1
  [true]	=	0
  [and (x1, x2) ]	=	2 x1
  [false]	=	0
  [+ (x1, x2) ]	=	x1 + 2 x2
  [- (x1, x2) ]	=	2 x1
  [l (x1) ]	=	x1
  [min (x1) ]	=	x1
  [0 (x1) ]	=	0
  [max# (x1) ]	=	2 x1
  [bs (x1) ]	=	0
  [not (x1) ]	=	0
  [f(x1, ..., xn)]	=	x1 + ... + xn + 1	for all other symbols f of arity n

  one remains with the following pair(s).

  none

  1.1.9.1: P is empty

  All dependency pairs have been removed.