MAYBE
MAYBE
TRS:
 {
             0(#()) -> #(),
          +(x, #()) -> x,
      +(x, +(y, z)) -> +(+(x, y), z),
          +(#(), 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, #()) -> 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(true()) -> false(),
       not(false()) -> true(),
     and(x, true()) -> x,
    and(x, false()) -> false(),
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
         ge(x, #()) -> true(),
      ge(#(), 0(x)) -> ge(#(), x),
      ge(#(), 1(x)) -> false(),
     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),
          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))
  )
 }
 DUP: We consider a duplicating system.
  Trs:
   {
               0(#()) -> #(),
            +(x, #()) -> x,
        +(x, +(y, z)) -> +(+(x, y), z),
            +(#(), 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, #()) -> 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(true()) -> false(),
         not(false()) -> true(),
       and(x, true()) -> x,
      and(x, false()) -> false(),
     if(true(), x, y) -> x,
    if(false(), x, y) -> y,
           ge(x, #()) -> true(),
        ge(#(), 0(x)) -> ge(#(), x),
        ge(#(), 1(x)) -> false(),
       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),
            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))
    )
   }
  Fail