Term Rewriting System R:

   [x, y, z]
   0(#) -> #
   +(x, #) -> x
   +(#, x) -> x
   +(0(x), 0(y)) -> 0(+(x, y))
   +(0(x), 1(y)) -> 1(+(x, y))
   +(1(x), 0(y)) -> 1(+(x, y))
   +(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
   +(x, +(y, z)) -> +(+(x, y), z)
   -(x, #) -> x
   -(#, x) -> #
   -(0(x), 0(y)) -> 0(-(x, y))
   -(0(x), 1(y)) -> 1(-(-(x, y), 1(#)))
   -(1(x), 0(y)) -> 1(-(x, y))
   -(1(x), 1(y)) -> 0(-(x, y))
   not(false) -> true
   not(true) -> false
   and(x, true) -> x
   and(x, false) -> false
   if(true, x, y) -> x
   if(false, x, y) -> y
   ge(0(x), 0(y)) -> ge(x, y)
   ge(0(x), 1(y)) -> not(ge(y, x))
   ge(1(x), 0(y)) -> ge(x, y)
   ge(1(x), 1(y)) -> ge(x, y)
   ge(x, #) -> true
   ge(#, 1(x)) -> false
   ge(#, 0(x)) -> ge(#, x)
   val(l(x)) -> x
   val(n(x, y, z)) -> x
   min(l(x)) -> x
   min(n(x, y, z)) -> min(y)
   max(l(x)) -> x
   max(n(x, y, z)) -> max(z)
   bs(l(x)) -> true
   bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
   size(l(x)) -> 1(#)
   size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#))
   wb(l(x)) -> true
   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)))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   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), 1(y)) -> GE(x, y)
   GE(#, 0(x)) -> GE(#, x)
   GE(1(x), 0(y)) -> GE(x, y)
   +'(x, +(y, z)) -> +'(+(x, y), z)
   +'(x, +(y, z)) -> +'(x, y)
   +'(0(x), 1(y)) -> +'(x, y)
   +'(1(x), 0(y)) -> +'(x, y)
   +'(0(x), 0(y)) -> 0'(+(x, y))
   +'(0(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)
   -'(0(x), 1(y)) -> -'(-(x, y), 1(#))
   -'(0(x), 1(y)) -> -'(x, y)
   -'(0(x), 0(y)) -> 0'(-(x, y))
   -'(0(x), 0(y)) -> -'(x, y)
   -'(1(x), 1(y)) -> 0'(-(x, y))
   -'(1(x), 1(y)) -> -'(x, y)
   -'(1(x), 0(y)) -> -'(x, y)
   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)
   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)
   MIN(n(x, y, z)) -> MIN(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)) -> GE(1(#), -(size(z), size(y)))
   WB(n(x, y, z)) -> -'(size(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)

Furthermore, R contains nine SCCs.


SCC1:

GE(#, 0(x)) -> GE(#, x)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(GE(x_1, x_2)) = 1 + x_1 + x_2
POL(0(x_1)) = 1 + x_1
POL(#) = 1

The following Dependency Pairs can be deleted:

   GE(#, 0(x)) -> GE(#, x)



 This transformation is resulting in no new subcycles.


SCC2:

GE(1(x), 0(y)) -> GE(x, y)
GE(1(x), 1(y)) -> GE(x, y)
GE(0(x), 1(y)) -> GE(y, x)
GE(0(x), 0(y)) -> GE(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(1(x_1)) = 1 + x_1
POL(GE(x_1, x_2)) = 1 + x_1 + x_2
POL(0(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   GE(1(x), 0(y)) -> GE(x, y)
   GE(1(x), 1(y)) -> GE(x, y)
   GE(0(x), 1(y)) -> GE(y, x)
   GE(0(x), 0(y)) -> GE(x, y)



 This transformation is resulting in no new subcycles.


SCC3:

+'(1(x), 1(y)) -> +'(x, y)
+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(0(x), 0(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(x, +(y, z)) -> +'(x, y)
+'(x, +(y, z)) -> +'(+(x, y), z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(1(x_1)) = x_1
POL(+'(x_1, x_2)) = 1 + x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0(x_1)) = x_1
POL(#) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   ge(0(x), 0(y)) -> ge(x, y)
   ge(0(x), 1(y)) -> not(ge(y, x))
   ge(1(x), 1(y)) -> ge(x, y)
   ge(x, #) -> true
   ge(#, 0(x)) -> ge(#, x)
   ge(1(x), 0(y)) -> ge(x, y)
   ge(#, 1(x)) -> false
   val(l(x)) -> x
   val(n(x, y, z)) -> x
   not(true) -> false
   not(false) -> true
   -(0(x), 1(y)) -> 1(-(-(x, y), 1(#)))
   -(0(x), 0(y)) -> 0(-(x, y))
   -(1(x), 1(y)) -> 0(-(x, y))
   -(1(x), 0(y)) -> 1(-(x, y))
   -(x, #) -> x
   -(#, x) -> #
   and(x, false) -> false
   and(x, true) -> x
   size(l(x)) -> 1(#)
   size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#))
   max(n(x, y, z)) -> max(z)
   max(l(x)) -> x
   bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
   bs(l(x)) -> true
   min(l(x)) -> x
   min(n(x, y, z)) -> min(y)
   if(false, x, y) -> y
   if(true, x, y) -> x
   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(l(x)) -> true


 This transformation is resulting in one new subcycle:


SCC3.MRR1:

+'(1(x), 1(y)) -> +'(+(x, y), 1(#))
+'(0(x), 0(y)) -> +'(x, y)
+'(1(x), 0(y)) -> +'(x, y)
+'(0(x), 1(y)) -> +'(x, y)
+'(x, +(y, z)) -> +'(x, y)
+'(x, +(y, z)) -> +'(+(x, y), z)
+'(1(x), 1(y)) -> +'(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(1(x_1)) = 1 + x_1
POL(+'(x_1, x_2)) = 1 + x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0(x_1)) = x_1
POL(#) = 0

The following Dependency Pairs can be deleted:

   +'(1(x), 1(y)) -> +'(+(x, y), 1(#))
   +'(1(x), 0(y)) -> +'(x, y)
   +'(0(x), 1(y)) -> +'(x, y)
   +'(1(x), 1(y)) -> +'(x, y)

The following rules of R can be deleted: 

   +(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))


 This transformation is resulting in one new subcycle:


SCC3.MRR1.MRR1:

+'(x, +(y, z)) -> +'(x, y)
+'(x, +(y, z)) -> +'(+(x, y), z)
+'(0(x), 0(y)) -> +'(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(1(x_1)) = x_1
POL(+'(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0(x_1)) = 1 + x_1
POL(#) = 0

The following Dependency Pairs can be deleted:

   +'(0(x), 0(y)) -> +'(x, y)

The following rules of R can be deleted: 

   +(0(x), 1(y)) -> 1(+(x, y))
   +(1(x), 0(y)) -> 1(+(x, y))
   +(0(x), 0(y)) -> 0(+(x, y))
   0(#) -> #
   +(x, #) -> x
   +(#, x) -> x


 This transformation is resulting in one new subcycle:


SCC3.MRR1.MRR1.MRR1:

+'(x, +(y, z)) -> +'(+(x, y), z)
+'(x, +(y, z)) -> +'(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(+'(x_1, x_2)) = 1 + x_1 + x_2
POL(+(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   +'(x, +(y, z)) -> +'(x, y)

No rules of R can be deleted.


 This transformation is resulting in one new subcycle:


SCC3.MRR1.MRR1.MRR1.MRR1:

+'(x, +(y, z)) -> +'(+(x, y), z)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(+(x_1, x_2)) = 1 + x_2
POL(+'(x_1, x_2)) = x_2

 resulting in no subcycles.


SCC4:

-'(1(x), 0(y)) -> -'(x, y)
-'(1(x), 1(y)) -> -'(x, y)
-'(0(x), 0(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(-(x, y), 1(#))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(1(x_1)) = x_1
POL(-(x_1, x_2)) = x_1 + x_2
POL(-'(x_1, x_2)) = 1 + x_1 + x_2
POL(0(x_1)) = x_1
POL(#) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   ge(0(x), 0(y)) -> ge(x, y)
   ge(0(x), 1(y)) -> not(ge(y, x))
   ge(1(x), 1(y)) -> ge(x, y)
   ge(x, #) -> true
   ge(#, 0(x)) -> ge(#, x)
   ge(1(x), 0(y)) -> ge(x, y)
   ge(#, 1(x)) -> false
   val(l(x)) -> x
   val(n(x, y, z)) -> x
   +(x, +(y, z)) -> +(+(x, y), z)
   +(0(x), 1(y)) -> 1(+(x, y))
   +(1(x), 0(y)) -> 1(+(x, y))
   +(0(x), 0(y)) -> 0(+(x, y))
   +(1(x), 1(y)) -> 0(+(+(x, y), 1(#)))
   +(x, #) -> x
   +(#, x) -> x
   not(true) -> false
   not(false) -> true
   and(x, false) -> false
   and(x, true) -> x
   size(l(x)) -> 1(#)
   size(n(x, y, z)) -> +(+(size(x), size(y)), 1(#))
   max(n(x, y, z)) -> max(z)
   max(l(x)) -> x
   bs(n(x, y, z)) -> and(and(ge(x, max(y)), ge(min(z), x)), and(bs(y), bs(z)))
   bs(l(x)) -> true
   min(l(x)) -> x
   min(n(x, y, z)) -> min(y)
   if(false, x, y) -> y
   if(true, x, y) -> x
   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(l(x)) -> true


 This transformation is resulting in one new subcycle:


SCC4.MRR1:

-'(1(x), 1(y)) -> -'(x, y)
-'(0(x), 0(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(x, y)
-'(0(x), 1(y)) -> -'(-(x, y), 1(#))
-'(1(x), 0(y)) -> -'(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(1(x_1)) = 1 + x_1
POL(-(x_1, x_2)) = x_1 + x_2
POL(-'(x_1, x_2)) = 1 + x_1 + x_2
POL(0(x_1)) = 1 + x_1
POL(#) = 0

The following Dependency Pairs can be deleted:

   -'(1(x), 1(y)) -> -'(x, y)
   -'(0(x), 0(y)) -> -'(x, y)
   -'(0(x), 1(y)) -> -'(x, y)
   -'(0(x), 1(y)) -> -'(-(x, y), 1(#))
   -'(1(x), 0(y)) -> -'(x, y)



 This transformation is resulting in no new subcycles.


SCC5:

MAX(n(x, y, z)) -> MAX(z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(MAX(x_1)) = 1 + x_1
POL(n(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

   MAX(n(x, y, z)) -> MAX(z)



 This transformation is resulting in no new subcycles.


SCC6:

MIN(n(x, y, z)) -> MIN(y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(MIN(x_1)) = 1 + x_1
POL(n(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

   MIN(n(x, y, z)) -> MIN(y)



 This transformation is resulting in no new subcycles.


SCC7:

BS(n(x, y, z)) -> BS(z)
BS(n(x, y, z)) -> BS(y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(BS(x_1)) = 1 + x_1
POL(n(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

   BS(n(x, y, z)) -> BS(z)
   BS(n(x, y, z)) -> BS(y)



 This transformation is resulting in no new subcycles.


SCC8:

SIZE(n(x, y, z)) -> SIZE(y)
SIZE(n(x, y, z)) -> SIZE(x)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(SIZE(x_1)) = 1 + x_1
POL(n(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

   SIZE(n(x, y, z)) -> SIZE(y)
   SIZE(n(x, y, z)) -> SIZE(x)



 This transformation is resulting in no new subcycles.


SCC9:

WB(n(x, y, z)) -> WB(z)
WB(n(x, y, z)) -> WB(y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(WB(x_1)) = 1 + x_1
POL(n(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

   WB(n(x, y, z)) -> WB(z)
   WB(n(x, y, z)) -> WB(y)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 3.795 seconds.