R

     ↳Dependency Pair Analysis

+'(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)) -> 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)

   R

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

       →DP Problem 8

         ↳Remaining Obligation(s)

       →DP Problem 9

         ↳Remaining Obligation(s)

• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pair:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pair:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pair:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  

   R

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

       →DP Problem 6

         ↳Remaining Obligation(s)

       →DP Problem 7

         ↳Remaining Obligation(s)

       →DP Problem 8

         ↳Remaining Obligation(s)

       →DP Problem 9

         ↳Remaining Obligation(s)

• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pair:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pair:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pair:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))

  
  
  
• Dependency Pairs:
  

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

  
  Rules:
  

  
  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)))