YES

We show the termination of the TRS R:

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

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: +#(|0|(x),|0|(y)) -> |0|#(+(x,y))
p2: +#(|0|(x),|0|(y)) -> +#(x,y)
p3: +#(|0|(x),|1|(y)) -> +#(x,y)
p4: +#(|1|(x),|0|(y)) -> +#(x,y)
p5: +#(|1|(x),|1|(y)) -> |0|#(+(+(x,y),|1|(|#|())))
p6: +#(|1|(x),|1|(y)) -> +#(+(x,y),|1|(|#|()))
p7: +#(|1|(x),|1|(y)) -> +#(x,y)
p8: +#(x,+(y,z)) -> +#(+(x,y),z)
p9: +#(x,+(y,z)) -> +#(x,y)
p10: -#(|0|(x),|0|(y)) -> |0|#(-(x,y))
p11: -#(|0|(x),|0|(y)) -> -#(x,y)
p12: -#(|0|(x),|1|(y)) -> -#(-(x,y),|1|(|#|()))
p13: -#(|0|(x),|1|(y)) -> -#(x,y)
p14: -#(|1|(x),|0|(y)) -> -#(x,y)
p15: -#(|1|(x),|1|(y)) -> |0|#(-(x,y))
p16: -#(|1|(x),|1|(y)) -> -#(x,y)
p17: ge#(|0|(x),|0|(y)) -> ge#(x,y)
p18: ge#(|0|(x),|1|(y)) -> not#(ge(y,x))
p19: ge#(|0|(x),|1|(y)) -> ge#(y,x)
p20: ge#(|1|(x),|0|(y)) -> ge#(x,y)
p21: ge#(|1|(x),|1|(y)) -> ge#(x,y)
p22: ge#(|#|(),|0|(x)) -> ge#(|#|(),x)
p23: min#(n(x,y,z)) -> min#(y)
p24: max#(n(x,y,z)) -> max#(z)
p25: bs#(n(x,y,z)) -> and#(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
p26: bs#(n(x,y,z)) -> and#(ge(x,max(y)),ge(min(z),x))
p27: bs#(n(x,y,z)) -> ge#(x,max(y))
p28: bs#(n(x,y,z)) -> max#(y)
p29: bs#(n(x,y,z)) -> ge#(min(z),x)
p30: bs#(n(x,y,z)) -> min#(z)
p31: bs#(n(x,y,z)) -> and#(bs(y),bs(z))
p32: bs#(n(x,y,z)) -> bs#(y)
p33: bs#(n(x,y,z)) -> bs#(z)
p34: size#(n(x,y,z)) -> +#(+(size(x),size(y)),|1|(|#|()))
p35: size#(n(x,y,z)) -> +#(size(x),size(y))
p36: size#(n(x,y,z)) -> size#(x)
p37: size#(n(x,y,z)) -> size#(y)
p38: 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)))
p39: wb#(n(x,y,z)) -> if#(ge(size(y),size(z)),ge(|1|(|#|()),-(size(y),size(z))),ge(|1|(|#|()),-(size(z),size(y))))
p40: wb#(n(x,y,z)) -> ge#(size(y),size(z))
p41: wb#(n(x,y,z)) -> size#(y)
p42: wb#(n(x,y,z)) -> size#(z)
p43: wb#(n(x,y,z)) -> ge#(|1|(|#|()),-(size(y),size(z)))
p44: wb#(n(x,y,z)) -> -#(size(y),size(z))
p45: wb#(n(x,y,z)) -> ge#(|1|(|#|()),-(size(z),size(y)))
p46: wb#(n(x,y,z)) -> -#(size(z),size(y))
p47: wb#(n(x,y,z)) -> and#(wb(y),wb(z))
p48: wb#(n(x,y,z)) -> wb#(y)
p49: wb#(n(x,y,z)) -> wb#(z)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The estimated dependency graph contains the following SCCs:

  {p48, p49}
  {p36, p37}
  {p2, p3, p4, p6, p7, p8, p9}
  {p11, p12, p13, p14, p16}
  {p32, p33}
  {p17, p19, p20, p21}
  {p22}
  {p23}
  {p24}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: wb#(n(x,y,z)) -> wb#(z)
p2: wb#(n(x,y,z)) -> wb#(y)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      wb#_A(x1) = ((1,0),(1,1)) x1
      n_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: size#(n(x,y,z)) -> size#(y)
p2: size#(n(x,y,z)) -> size#(x)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      size#_A(x1) = ((1,0),(1,1)) x1
      n_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: +#(|0|(x),|0|(y)) -> +#(x,y)
p2: +#(x,+(y,z)) -> +#(x,y)
p3: +#(x,+(y,z)) -> +#(+(x,y),z)
p4: +#(|1|(x),|1|(y)) -> +#(x,y)
p5: +#(|1|(x),|1|(y)) -> +#(+(x,y),|1|(|#|()))
p6: +#(|0|(x),|1|(y)) -> +#(x,y)
p7: +#(|1|(x),|0|(y)) -> +#(x,y)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      +#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2
      |0|_A(x1) = x1 + (1,2)
      +_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,1)) x2 + (1,1)
      |1|_A(x1) = x1 + (4,8)
      |#|_A() = (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: -#(|0|(x),|0|(y)) -> -#(x,y)
p2: -#(|1|(x),|1|(y)) -> -#(x,y)
p3: -#(|1|(x),|0|(y)) -> -#(x,y)
p4: -#(|0|(x),|1|(y)) -> -#(x,y)
p5: -#(|0|(x),|1|(y)) -> -#(-(x,y),|1|(|#|()))

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  r1, r9, r10, r11, r12, r13, r14

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      -#_A(x1,x2) = ((1,0),(1,1)) x1 + x2
      |0|_A(x1) = x1 + (7,11)
      |1|_A(x1) = ((1,0),(1,1)) x1 + (4,1)
      -_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,18)
      |#|_A() = (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: bs#(n(x,y,z)) -> bs#(z)
p2: bs#(n(x,y,z)) -> bs#(y)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      bs#_A(x1) = ((1,0),(1,1)) x1
      n_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (1,1)

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: ge#(|0|(x),|0|(y)) -> ge#(x,y)
p2: ge#(|1|(x),|1|(y)) -> ge#(x,y)
p3: ge#(|1|(x),|0|(y)) -> ge#(x,y)
p4: ge#(|0|(x),|1|(y)) -> ge#(y,x)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      ge#_A(x1,x2) = x1 + x2
      |0|_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      |1|_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: ge#(|#|(),|0|(x)) -> ge#(|#|(),x)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      ge#_A(x1,x2) = x2
      |#|_A() = (0,0)
      |0|_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: min#(n(x,y,z)) -> min#(y)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      min#_A(x1) = x1
      n_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((1,0),(1,1)) x2 + ((0,0),(1,0)) x3 + (1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: max#(n(x,y,z)) -> max#(z)

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(x,+(y,z)) -> +(+(x,y),z)
r9: -(x,|#|()) -> x
r10: -(|#|(),x) -> |#|()
r11: -(|0|(x),|0|(y)) -> |0|(-(x,y))
r12: -(|0|(x),|1|(y)) -> |1|(-(-(x,y),|1|(|#|())))
r13: -(|1|(x),|0|(y)) -> |1|(-(x,y))
r14: -(|1|(x),|1|(y)) -> |0|(-(x,y))
r15: not(false()) -> true()
r16: not(true()) -> false()
r17: and(x,true()) -> x
r18: and(x,false()) -> false()
r19: if(true(),x,y) -> x
r20: if(false(),x,y) -> y
r21: ge(|0|(x),|0|(y)) -> ge(x,y)
r22: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r23: ge(|1|(x),|0|(y)) -> ge(x,y)
r24: ge(|1|(x),|1|(y)) -> ge(x,y)
r25: ge(x,|#|()) -> true()
r26: ge(|#|(),|1|(x)) -> false()
r27: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r28: val(l(x)) -> x
r29: val(n(x,y,z)) -> x
r30: min(l(x)) -> x
r31: min(n(x,y,z)) -> min(y)
r32: max(l(x)) -> x
r33: max(n(x,y,z)) -> max(z)
r34: bs(l(x)) -> true()
r35: bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))
r36: size(l(x)) -> |1|(|#|())
r37: size(n(x,y,z)) -> +(+(size(x),size(y)),|1|(|#|()))
r38: wb(l(x)) -> true()
r39: 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)))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      max#_A(x1) = x1
      n_A(x1,x2,x3) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + ((1,0),(1,1)) x3 + (1,1)

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.