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

  r1, r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        wb#_A(x1) = 91
        n_A(x1,x2,x3) = max{x1 + 90, x2 - 192}
        |0|_A(x1) = x1 + 39
        |#|_A = 8
        val_A(x1) = x1 + 199
        l_A(x1) = max{41, x1 - 198}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            wb#_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            |0|_A(x1) = x1 + 2
            |#|_A() = 2
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            wb#!_A(x1) = x1 + 5
            n!_A(x1,x2,x3) = x2 + x3 + 4
            |0|!_A(x1) = x1 + 1
            |#|!_A() = 3
            val!_A(x1) = x1
            l!_A(x1) = 4
  
    partial status:
  
      pi(wb#) = []
      pi(n) = [1]
      pi(|0|) = [1]
      pi(|#|) = []
      pi(val) = [1]
      pi(l) = []

The following rules are removed:

  p1, p2

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

  r1, r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        size#_A(x1) = 15
        n_A(x1,x2,x3) = max{x1 + 14, x2 - 628, x3 - 65}
        |0|_A(x1) = max{1754, x1 + 149}
        |#|_A = 11
        val_A(x1) = x1 + 2
        l_A(x1) = max{12, x1 - 1}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            size#_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            |0|_A(x1) = x1 + 2
            |#|_A() = 2
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            size#!_A(x1) = x1 + 7
            n!_A(x1,x2,x3) = x2 + x3 + 6
            |0|!_A(x1) = x1 + 7
            |#|!_A() = 2
            val!_A(x1) = x1
            l!_A(x1) = 4
  
    partial status:
  
      pi(size#) = []
      pi(n) = [1]
      pi(|0|) = []
      pi(|#|) = []
      pi(val) = [1]
      pi(l) = []

The following rules are removed:

  p1, p2

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, r10, r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        +#_A(x1,x2) = max{220, x2 + 110}
        |0|_A(x1) = max{220, x1 + 132}
        +_A(x1,x2) = max{220, x1 + 111, x2 + 132}
        |1|_A(x1) = max{219, x1 + 132}
        |#|_A = 2
        -_A(x1,x2) = max{218, x1 - 887, x2 - 872}
        val_A(x1) = x1 + 361
        l_A(x1) = x1 + 3
        n_A(x1,x2,x3) = max{8, x1 - 360, x2 + 4, x3 - 322}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            +#_A(x1,x2) = 0
            |0|_A(x1) = x1 + 5
            +_A(x1,x2) = 4
            |1|_A(x1) = x1 + 2
            |#|_A() = 0
            -_A(x1,x2) = x2
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            +#!_A(x1,x2) = x2 + 5
            |0|!_A(x1) = 12
            +!_A(x1,x2) = x2 + 8
            |1|!_A(x1) = 11
            |#|!_A() = 6
            -!_A(x1,x2) = 10
            val!_A(x1) = x1
            l!_A(x1) = 7
            n!_A(x1,x2,x3) = 3
  
    partial status:
  
      pi(+#) = []
      pi(|0|) = [1]
      pi(+) = [1, 2]
      pi(|1|) = [1]
      pi(|#|) = []
      pi(-) = []
      pi(val) = [1]
      pi(l) = []
      pi(n) = []

The following rules are removed:

  p1, p2, p3, p4, p6, p7



-- SCC decomposition.

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

p1: +#(|1|(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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: +#(|1|(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, r2, r3, r4, r5, r6, r7, r8, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        +#_A(x1,x2) = 1
        |1|_A(x1) = 14
        +_A(x1,x2) = max{x1, x2 + 13}
        |#|_A = 13
        |0|_A(x1) = 13
        val_A(x1) = x1 + 155
        n_A(x1,x2,x3) = max{15, x1 - 154, x2 - 50, x3 - 3}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            +#_A(x1,x2) = 0
            |1|_A(x1) = x1 + 4
            +_A(x1,x2) = x1 + x2 + 1
            |#|_A() = 1
            |0|_A(x1) = x1 + 2
            val_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            +#!_A(x1,x2) = x1 + x2
            |1|!_A(x1) = 9
            +!_A(x1,x2) = x2 + 13
            |#|!_A() = 12
            |0|!_A(x1) = 14
            val!_A(x1) = x1
            n!_A(x1,x2,x3) = 10
  
    partial status:
  
      pi(+#) = []
      pi(|1|) = []
      pi(+) = [1, 2]
      pi(|#|) = []
      pi(|0|) = []
      pi(val) = [1]
      pi(n) = []

The following rules are removed:

  p1

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, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        -#_A(x1,x2) = max{1, x1 - 61, x2 - 103}
        |0|_A(x1) = max{63, x1 + 19}
        |1|_A(x1) = max{63, x1 + 19}
        -_A(x1,x2) = max{20, x1, x2 - 83}
        |#|_A = 81
        val_A(x1) = x1 + 299
        n_A(x1,x2,x3) = max{3, x1 - 297}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            -#_A(x1,x2) = x1 + x2
            |0|_A(x1) = x1 + 4
            |1|_A(x1) = x1 + 2
            -_A(x1,x2) = x1 + x2 + 1
            |#|_A() = 1
            val_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            -#!_A(x1,x2) = x1
            |0|!_A(x1) = 5
            |1|!_A(x1) = 5
            -!_A(x1,x2) = 9
            |#|!_A() = 5
            val!_A(x1) = x1
            n!_A(x1,x2,x3) = x3 + 4
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = [1]
      pi(|1|) = []
      pi(-) = [1]
      pi(|#|) = []
      pi(val) = [1]
      pi(n) = []

The following rules are removed:

  p1, p2, p3, p4, p5

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

  r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        bs#_A(x1) = max{77, x1 + 75}
        n_A(x1,x2,x3) = max{76, x1 + 67, x2 + 65, x3 + 74}
        val_A(x1) = x1 + 118
        l_A(x1) = max{30, x1 - 117}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            bs#_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            bs#!_A(x1) = x1 + 8
            n!_A(x1,x2,x3) = x1 + x2 + x3 + 7
            val!_A(x1) = x1
            l!_A(x1) = 1
  
    partial status:
  
      pi(bs#) = []
      pi(n) = [3]
      pi(val) = []
      pi(l) = []

The following rules are removed:

  p1, p2

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

  r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        ge#_A(x1,x2) = 392
        |0|_A(x1) = 0
        |1|_A(x1) = max{391, x1}
        val_A(x1) = x1
        l_A(x1) = x1 + 151
        n_A(x1,x2,x3) = max{458, x1 + 456, x2 + 456, x3 + 414}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            ge#_A(x1,x2) = x1 + x2
            |0|_A(x1) = x1 + 2
            |1|_A(x1) = x1 + 1
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            ge#!_A(x1,x2) = x1 + x2 + 8
            |0|!_A(x1) = 6
            |1|!_A(x1) = 7
            val!_A(x1) = x1
            l!_A(x1) = 7
            n!_A(x1,x2,x3) = x2 + 4
  
    partial status:
  
      pi(ge#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(val) = [1]
      pi(l) = [1]
      pi(n) = [3]

The following rules are removed:

  p1, p2, p3, p4

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

  r1, r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        ge#_A(x1,x2) = max{2, x1 - 1, x2 + 1}
        |#|_A = 4
        |0|_A(x1) = max{223, x1 + 26}
        val_A(x1) = x1 + 532
        l_A(x1) = max{29, x1 - 531}
        n_A(x1,x2,x3) = max{x1 + 286, x3 + 320}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            ge#_A(x1,x2) = x2
            |#|_A() = 3
            |0|_A(x1) = x1 + 15
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            ge#!_A(x1,x2) = 0
            |#|!_A() = 12
            |0|!_A(x1) = 14
            val!_A(x1) = x1
            l!_A(x1) = 13
            n!_A(x1,x2,x3) = x2 + x3 + 11
  
    partial status:
  
      pi(ge#) = [2]
      pi(|#|) = []
      pi(|0|) = [1]
      pi(val) = [1]
      pi(l) = []
      pi(n) = [3]

The following rules are removed:

  p1

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

  r1, r28, r29

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        min#_A(x1) = 1
        n_A(x1,x2,x3) = max{0, x1 - 197, x2 - 87, x3 - 231}
        |0|_A(x1) = x1 + 45
        |#|_A = 50
        val_A(x1) = x1 + 231
        l_A(x1) = max{51, x1 - 230}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            min#_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            |0|_A(x1) = x1 + 2
            |#|_A() = 6
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            min#!_A(x1) = x1 + 2
            n!_A(x1,x2,x3) = x3 + 1
            |0|!_A(x1) = 4
            |#|!_A() = 7
            val!_A(x1) = x1
            l!_A(x1) = 8
  
    partial status:
  
      pi(min#) = []
      pi(n) = []
      pi(|0|) = [1]
      pi(|#|) = []
      pi(val) = [1]
      pi(l) = []

The following rules are removed:

  p1

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

  r28

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      max/plus interpretation on natural numbers:
      
        max#_A(x1) = 559
        n_A(x1,x2,x3) = max{x2 + 558, x3 - 560}
        val_A(x1) = x1 + 2
        l_A(x1) = max{2527, x1 - 1}
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            max#_A(x1) = x1
            n_A(x1,x2,x3) = x1 + x2 + x3 + 1
            val_A(x1) = x1
            l_A(x1) = x1 + 1
            max#!_A(x1) = x1 + 9
            n!_A(x1,x2,x3) = 8
            val!_A(x1) = x1
            l!_A(x1) = 3
  
    partial status:
  
      pi(max#) = []
      pi(n) = []
      pi(val) = [1]
      pi(l) = []

The following rules are removed:

  p1

Then no dependency pair remains.