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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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 + 1
              |#|_A() = 2
              wb#!_A(x1) = x1 + 6
              n!_A(x1,x2,x3) = x2 + x3 + 5
              |0|!_A(x1) = 9
              |#|!_A() = 2
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            wb#_A(x1) = 0
            n_A(x1,x2,x3) = max{3, x1 - 741, x2 - 745, x3 + 1}
            |0|_A(x1) = max{70, x1 - 143}
            |#|_A = 0
            wb#!_A(x1) = x1 + 744
            n!_A(x1,x2,x3) = max{0, x2 - 138}
            |0|!_A(x1) = x1 + 179
            |#|!_A = 0
        
  
    partial status:
  
      pi(wb#) = []
      pi(n) = [1]
      pi(|0|) = []
      pi(|#|) = []

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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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
              size#!_A(x1) = x1 + 7
              n!_A(x1,x2,x3) = x2 + x3 + 6
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            size#_A(x1) = 0
            n_A(x1,x2,x3) = max{6, x1 - 529, x3 - 1189}
            size#!_A(x1) = x1 + 1191
            n!_A(x1,x2,x3) = max{x1 - 837, x2 + 13, x3 + 63}
        
  
    partial status:
  
      pi(size#) = []
      pi(n) = [1, 3]

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

  r3

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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 + 8
              +_A(x1,x2) = x1 + x2 + 8
              |1|_A(x1) = x1 + 15
              |#|_A() = 0
              +#!_A(x1,x2) = x2
              |0|!_A(x1) = 42
              +!_A(x1,x2) = x1 + x2 + 16
              |1|!_A(x1) = 40
              |#|!_A() = 45
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = 0
            |0|_A(x1) = 3438
            +_A(x1,x2) = x2 + 2158
            |1|_A(x1) = x1 + 1279
            |#|_A = 780
            +#!_A(x1,x2) = max{1276, x2 - 783}
            |0|!_A(x1) = 1377
            +!_A(x1,x2) = max{2157, x2 - 1}
            |1|!_A(x1) = 1376
            |#|!_A = 1277
        
  
    partial status:
  
      pi(+#) = []
      pi(|0|) = []
      pi(+) = [1, 2]
      pi(|1|) = []
      pi(|#|) = []

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              +#_A(x1,x2) = x2
              |1|_A(x1) = x1 + 3
              +_A(x1,x2) = x1 + x2 + 1
              |#|_A() = 0
              |0|_A(x1) = x1
              -_A(x1,x2) = x2
              +#!_A(x1,x2) = x1 + x2
              |1|!_A(x1) = 5
              +!_A(x1,x2) = x2 + 8
              |#|!_A() = 3
              |0|!_A(x1) = 7
              -!_A(x1,x2) = 6
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = max{0, x2 - 4}
            |1|_A(x1) = max{1, x1 - 2}
            +_A(x1,x2) = max{1352, x1, x2}
            |#|_A = 5
            |0|_A(x1) = max{1348, x1 - 2}
            -_A(x1,x2) = max{x1 - 6, x2 + 678}
            +#!_A(x1,x2) = x2 + 12
            |1|!_A(x1) = x1 + 8
            +!_A(x1,x2) = x1 + 11
            |#|!_A = 699
            |0|!_A(x1) = 14
            -!_A(x1,x2) = max{x1 - 661, x2 + 681}
        
  
    partial status:
  
      pi(+#) = []
      pi(|1|) = []
      pi(+) = [1, 2]
      pi(|#|) = []
      pi(|0|) = []
      pi(-) = [2]

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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
              and_A(x1,x2) = x2 + 1
              false_A() = 7
              -#!_A(x1,x2) = x1 + x2
              |0|!_A(x1) = 6
              |1|!_A(x1) = 7
              -!_A(x1,x2) = 8
              |#|!_A() = 3
              and!_A(x1,x2) = 10
              false!_A() = 0
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{0, x1 - 62, x2 - 65}
            |0|_A(x1) = x1 + 60
            |1|_A(x1) = x1 + 60
            -_A(x1,x2) = max{x1, x2 - 64}
            |#|_A = 4
            and_A(x1,x2) = max{61, x1 - 62, x2 - 110}
            false_A = 0
            -#!_A(x1,x2) = max{44, x1 - 59}
            |0|!_A(x1) = max{73, x1 + 43}
            |1|!_A(x1) = 47
            -!_A(x1,x2) = max{45, x2 - 12}
            |#|!_A = 46
            and!_A(x1,x2) = max{3, x1 - 12, x2 - 12}
            false!_A = 339
        
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = [1, 2]
      pi(|#|) = []
      pi(and) = []
      pi(false) = []

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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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
              bs#!_A(x1) = x1
              n!_A(x1,x2,x3) = 4
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            bs#_A(x1) = x1
            n_A(x1,x2,x3) = max{x1 + 4, x2 + 4, x3 + 4}
            bs#!_A(x1) = max{2, x1 - 1}
            n!_A(x1,x2,x3) = max{x1 + 51, x3 + 98}
        
  
    partial status:
  
      pi(bs#) = []
      pi(n) = []

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

  r1

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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 + 1
              |1|_A(x1) = x1 + 1
              |#|_A() = 8
              ge#!_A(x1,x2) = x1 + x2 + 9
              |0|!_A(x1) = 7
              |1|!_A(x1) = 8
              |#|!_A() = 2
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = 0
            |0|_A(x1) = x1 + 53
            |1|_A(x1) = max{89, x1 - 73}
            |#|_A = 19
            ge#!_A(x1,x2) = 0
            |0|!_A(x1) = max{154, x1 + 136}
            |1|!_A(x1) = x1 + 171
            |#|!_A = 65
        
  
    partial status:
  
      pi(ge#) = []
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|#|) = []

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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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) = 0
              |#|_A() = 12
              |0|_A(x1) = 12
              ge#!_A(x1,x2) = 6
              |#|!_A() = 7
              |0|!_A(x1) = 5
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = x2
            |#|_A = 388
            |0|_A(x1) = x1 + 1333
            ge#!_A(x1,x2) = max{380, x1 - 389, x2 - 1}
            |#|!_A = 1722
            |0|!_A(x1) = x1 + 1333
        
  
    partial status:
  
      pi(ge#) = []
      pi(|#|) = []
      pi(|0|) = []

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

  r18

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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
              and_A(x1,x2) = x2 + 1
              false_A() = 4
              min#!_A(x1) = x1
              n!_A(x1,x2,x3) = x1 + 7
              and!_A(x1,x2) = x1 + x2 + 4
              false!_A() = 0
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            min#_A(x1) = 0
            n_A(x1,x2,x3) = max{18, x1 + 12, x3 - 190}
            and_A(x1,x2) = max{124, x1 - 30, x2 - 240}
            false_A = 44
            min#!_A(x1) = max{1, x1 - 13}
            n!_A(x1,x2,x3) = max{0, x3 - 691}
            and!_A(x1,x2) = max{0, x1 - 9, x2 - 45}
            false!_A = 0
        
  
    partial status:
  
      pi(min#) = [1]
      pi(n) = [1, 2, 3]
      pi(and) = [1, 2]
      pi(false) = []

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

  r18

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. 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
              and_A(x1,x2) = x2 + 1
              false_A() = 19
              max#!_A(x1) = x1 + 22
              n!_A(x1,x2,x3) = x1 + 21
              and!_A(x1,x2) = x1 + x2
              false!_A() = 18
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            max#_A(x1) = x1
            n_A(x1,x2,x3) = max{x1 + 505, x3 + 640}
            and_A(x1,x2) = max{1, x1 - 84, x2 - 2}
            false_A = 0
            max#!_A(x1) = 2278
            n!_A(x1,x2,x3) = max{x1 + 2277, x2 + 2, x3 + 401}
            and!_A(x1,x2) = max{3405, x1 + 3000, x2 + 3403}
            false!_A = 3404
        
  
    partial status:
  
      pi(max#) = []
      pi(n) = []
      pi(and) = [1]
      pi(false) = []

The following rules are removed:

  p1

Then no dependency pair remains.