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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          wb#_A(x1) = x1 + 8
          n_A(x1,x2,x3) = x1 + x2 + x3 + 9
          |0|_A(x1) = 13
          |#|_A() = 3
          -_A(x1,x2) = x1 + 7
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          wb#_A(x1) = max{0, x1 - 13}
          n_A(x1,x2,x3) = max{x1 + 1378, x2, x3 + 12}
          |0|_A(x1) = x1 + 20
          |#|_A = 15
          -_A(x1,x2) = max{429, x1 - 897, x2 - 1079}
          wb#!_A(x1) = 0
          n!_A(x1,x2,x3) = max{0, x1 - 3110, x3 - 1728}
          |0|!_A(x1) = max{2184, x1 + 1754}
          |#|!_A = 0
          -!_A(x1,x2) = max{1809, x1 - 1470, x2 - 1474}
  
    partial status:
  
      pi(wb#) = [1]
      pi(n) = [2, 3]
      pi(|0|) = []
      pi(|#|) = []
      pi(-) = [1]

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

  r10, r18

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          size#_A(x1) = x1 + 4
          n_A(x1,x2,x3) = x1 + x2 + 5
          -_A(x1,x2) = 4
          |#|_A() = 3
          and_A(x1,x2) = 4
          false_A() = 1
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          size#_A(x1) = max{0, x1 - 729}
          n_A(x1,x2,x3) = max{x1 + 728, x2 + 34, x3 + 32}
          -_A(x1,x2) = max{185, x1 - 463, x2 - 463}
          |#|_A = 3
          and_A(x1,x2) = max{29, x1 - 131, x2 - 127}
          false_A = 2
          size#!_A(x1) = max{701, x1 + 668}
          n!_A(x1,x2,x3) = max{701, x1 + 669, x2 - 145, x3 - 151}
          -!_A(x1,x2) = max{0, x1 - 762, x2 - 117}
          |#|!_A = 4
          and!_A(x1,x2) = max{700, x1 - 25, x2 - 43}
          false!_A = 700
  
    partial status:
  
      pi(size#) = []
      pi(n) = [2]
      pi(-) = []
      pi(|#|) = []
      pi(and) = []
      pi(false) = []

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          +#_A(x1,x2) = x2 + 8
          |0|_A(x1) = x1 + 9
          +_A(x1,x2) = x1 + x2
          |1|_A(x1) = x1 + 18
          |#|_A() = 0
          -_A(x1,x2) = 8
          not_A(x1) = 4
          true_A() = 3
          false_A() = 2
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          +#_A(x1,x2) = 0
          |0|_A(x1) = max{142, x1 - 107}
          +_A(x1,x2) = max{107, x1}
          |1|_A(x1) = max{107, x1}
          |#|_A = 0
          -_A(x1,x2) = max{141, x1 - 143, x2 - 678}
          not_A(x1) = max{142, x1 - 113}
          true_A = 143
          false_A = 47
          +#!_A(x1,x2) = 502
          |0|!_A(x1) = x1 + 428
          +!_A(x1,x2) = max{501, x1 + 394, x2 - 103}
          |1|!_A(x1) = 431
          |#|!_A = 429
          -!_A(x1,x2) = max{430, x1 + 143, x2 - 143}
          not!_A(x1) = max{432, x1 - 144}
          true!_A = 431
          false!_A = 430
  
    partial status:
  
      pi(+#) = []
      pi(|0|) = [1]
      pi(+) = []
      pi(|1|) = []
      pi(|#|) = []
      pi(-) = []
      pi(not) = []
      pi(true) = []
      pi(false) = []

The following rules are removed:

  p1, p4, p6, p7



-- SCC decomposition.

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

p1: +#(x,+(y,z)) -> +#(x,y)
p2: +#(x,+(y,z)) -> +#(+(x,y),z)
p3: +#(|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, p2}
  {p3}


-- Reduction pair.

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

p1: +#(x,+(y,z)) -> +#(x,y)
p2: +#(x,+(y,z)) -> +#(+(x,y),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

  r1, r2, r3

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          +#_A(x1,x2) = x2 + 10
          +_A(x1,x2) = x1 + x2 + 9
          |0|_A(x1) = x1 + 23
          |#|_A() = 5
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          +#_A(x1,x2) = max{0, x2 - 21}
          +_A(x1,x2) = max{x1, x2 + 20}
          |0|_A(x1) = max{30, x1 - 133}
          |#|_A = 22
          +#!_A(x1,x2) = max{1, x2 - 1}
          +!_A(x1,x2) = max{47, x2 - 21}
          |0|!_A(x1) = 0
          |#|!_A = 6
  
    partial status:
  
      pi(+#) = [2]
      pi(+) = [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: +#(|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:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          +#_A(x1,x2) = x1 + x2
          |1|_A(x1) = x1 + 9
          +_A(x1,x2) = x1 + x2
          |#|_A() = 2
          |0|_A(x1) = x1 + 5
          -_A(x1,x2) = x1 + 5
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          +#_A(x1,x2) = 0
          |1|_A(x1) = max{23, x1 - 5}
          +_A(x1,x2) = max{29, x1, x2 + 14}
          |#|_A = 26
          |0|_A(x1) = max{30, x1 - 5}
          -_A(x1,x2) = max{x1 + 3, x2 - 17}
          +#!_A(x1,x2) = max{x1 + 585, x2 + 620}
          |1|!_A(x1) = 645
          +!_A(x1,x2) = max{644, x1 - 28, x2 + 614}
          |#|!_A = 678
          |0|!_A(x1) = max{682, x1 - 677}
          -!_A(x1,x2) = x1 + 651
  
    partial status:
  
      pi(+#) = [1]
      pi(|1|) = []
      pi(+) = [2]
      pi(|#|) = []
      pi(|0|) = []
      pi(-) = [1]

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, r15, r16, r26, r36

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          -#_A(x1,x2) = x2 + 1
          |0|_A(x1) = x1 + 57
          |1|_A(x1) = x1 + 2
          -_A(x1,x2) = x1 + x2 + 28
          |#|_A() = 0
          not_A(x1) = 5
          false_A() = 3
          true_A() = 4
          ge_A(x1,x2) = 6
          size_A(x1) = x1 + 8
          l_A(x1) = x1 + 5
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          -#_A(x1,x2) = max{0, x2 - 908}
          |0|_A(x1) = x1 + 907
          |1|_A(x1) = max{134, x1 + 3}
          -_A(x1,x2) = x1
          |#|_A = 2
          not_A(x1) = max{760, x1 - 48}
          false_A = 40
          true_A = 47
          ge_A(x1,x2) = max{46, x1 - 148, x2 - 137}
          size_A(x1) = max{192, x1 - 202}
          l_A(x1) = max{186, x1 + 1}
          -#!_A(x1,x2) = 916
          |0|!_A(x1) = max{10, x1 - 896}
          |1|!_A(x1) = max{916, x1 - 183}
          -!_A(x1,x2) = max{916, x1 + 8, x2 - 58}
          |#|!_A = 9
          not!_A(x1) = max{919, x1 - 228}
          false!_A = 917
          true!_A = 918
          ge!_A(x1,x2) = max{723, x2 - 184}
          size!_A(x1) = 917
          l!_A(x1) = max{919, x1 + 917}
  
    partial status:
  
      pi(-#) = [2]
      pi(|0|) = [1]
      pi(|1|) = []
      pi(-) = [2]
      pi(|#|) = []
      pi(not) = []
      pi(false) = []
      pi(true) = []
      pi(ge) = []
      pi(size) = []
      pi(l) = [1]

The following rules are removed:

  p1, p2, p3, p4



-- SCC decomposition.

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

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

  {p1}


-- Reduction pair.

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

p1: -#(|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:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          -#_A(x1,x2) = 5
          |0|_A(x1) = 7
          |1|_A(x1) = 6
          -_A(x1,x2) = x1 + 8
          |#|_A() = 2
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          -#_A(x1,x2) = max{0, x1 - 158, x2 - 134}
          |0|_A(x1) = max{133, x1 + 2}
          |1|_A(x1) = max{133, x1 + 2}
          -_A(x1,x2) = max{27, x1, x2 - 136}
          |#|_A = 121
          -#!_A(x1,x2) = max{11, x1 - 108, x2 - 240}
          |0|!_A(x1) = max{10, x1 - 700}
          |1|!_A(x1) = max{1, x1 - 243}
          -!_A(x1,x2) = max{4, x2 - 242}
          |#|!_A = 3
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = []
      pi(|#|) = []

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

  r1, r16, r26

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          bs#_A(x1) = 1
          n_A(x1,x2,x3) = x2 + 9
          |0|_A(x1) = 13
          |#|_A() = 6
          not_A(x1) = 3
          true_A() = 2
          false_A() = 1
          ge_A(x1,x2) = 12
          |1|_A(x1) = 4
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          bs#_A(x1) = max{0, x1 - 1092}
          n_A(x1,x2,x3) = max{x1 + 1094, x2 + 1091, x3 + 181}
          |0|_A(x1) = x1 + 187
          |#|_A = 0
          not_A(x1) = max{1105, x1 - 1189}
          true_A = 1106
          false_A = 2
          ge_A(x1,x2) = max{x1 + 917, x2 - 459}
          |1|_A(x1) = max{371, x1 + 187}
          bs#!_A(x1) = max{1, x1 - 1089}
          n!_A(x1,x2,x3) = max{1286, x1 - 1086, x2 - 1088, x3 - 853}
          |0|!_A(x1) = max{1288, x1}
          |#|!_A = 4
          not!_A(x1) = max{1289, x1 - 1279}
          true!_A = 2
          false!_A = 1
          ge!_A(x1,x2) = max{1285, x1 - 1458, x2 - 867}
          |1|!_A(x1) = max{0, x1 - 367}
  
    partial status:
  
      pi(bs#) = []
      pi(n) = [2]
      pi(|0|) = []
      pi(|#|) = []
      pi(not) = []
      pi(true) = []
      pi(false) = []
      pi(ge) = []
      pi(|1|) = []

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:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          ge#_A(x1,x2) = x1 + x2 + 9
          |0|_A(x1) = x1 + 8
          |1|_A(x1) = x1
          |#|_A() = 3
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          ge#_A(x1,x2) = max{0, x1 - 1250, x2 - 1250}
          |0|_A(x1) = x1 + 1249
          |1|_A(x1) = x1 + 1244
          |#|_A = 80
          ge#!_A(x1,x2) = max{6, x1 - 2500, x2 - 1250}
          |0|!_A(x1) = max{5, x1 - 77}
          |1|!_A(x1) = max{4, x1 - 81}
          |#|!_A = 2
  
    partial status:
  
      pi(ge#) = [1, 2]
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|#|) = []

The following rules are removed:

  p1, p3, p4



-- SCC decomposition.

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

p1: ge#(|1|(x),|1|(y)) -> ge#(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 estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: ge#(|1|(x),|1|(y)) -> ge#(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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          ge#_A(x1,x2) = x1 + x2 + 6
          |1|_A(x1) = x1 + 5
          |0|_A(x1) = 12
          |#|_A() = 0
          -_A(x1,x2) = 6
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          ge#_A(x1,x2) = max{0, x1 - 1, x2 - 1}
          |1|_A(x1) = max{251, x1}
          |0|_A(x1) = max{124, x1 - 396}
          |#|_A = 36
          -_A(x1,x2) = max{86, x1 - 562, x2 - 993}
          ge#!_A(x1,x2) = 5
          |1|!_A(x1) = max{5, x1 - 73}
          |0|!_A(x1) = 14
          |#|!_A = 1
          -!_A(x1,x2) = max{11, x1 - 7466, x2 - 7379}
  
    partial status:
  
      pi(ge#) = []
      pi(|1|) = [1]
      pi(|0|) = []
      pi(|#|) = []
      pi(-) = []

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          ge#_A(x1,x2) = x2 + 7
          |#|_A() = 6
          |0|_A(x1) = x1 + 19
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          ge#_A(x1,x2) = 0
          |#|_A = 8
          |0|_A(x1) = 109
          ge#!_A(x1,x2) = max{220, x1 - 10, x2 - 110}
          |#|!_A = 179
          |0|!_A(x1) = max{220, x1 + 8}
  
    partial status:
  
      pi(ge#) = []
      pi(|#|) = []
      pi(|0|) = [1]

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, r10, r16, r26, r36

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          min#_A(x1) = x1
          n_A(x1,x2,x3) = x2 + 13
          |0|_A(x1) = x1 + 15
          |#|_A() = 3
          -_A(x1,x2) = 4
          not_A(x1) = 3
          true_A() = 2
          false_A() = 1
          ge_A(x1,x2) = 8
          |1|_A(x1) = 5
          size_A(x1) = 6
          l_A(x1) = x1 + 6
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          min#_A(x1) = 0
          n_A(x1,x2,x3) = max{0, x1 - 107, x2 - 107, x3 - 107}
          |0|_A(x1) = max{24, x1 - 48}
          |#|_A = 20
          -_A(x1,x2) = max{22, x1 - 48, x2 - 48}
          not_A(x1) = max{86, x1 - 88}
          true_A = 87
          false_A = 77
          ge_A(x1,x2) = max{85, x1 - 28, x2 - 78}
          |1|_A(x1) = max{0, x1 - 48}
          size_A(x1) = x1
          l_A(x1) = max{0, x1 - 29}
          min#!_A(x1) = 4
          n!_A(x1,x2,x3) = max{x1 - 4, x3 + 4}
          |0|!_A(x1) = 79
          |#|!_A = 45
          -!_A(x1,x2) = max{45, x1 - 25, x2 - 46}
          not!_A(x1) = max{80, x1 - 88}
          true!_A = 2
          false!_A = 1
          ge!_A(x1,x2) = max{58, x1 + 38}
          |1|!_A(x1) = max{55, x1 + 24}
          size!_A(x1) = max{56, x1 - 227}
          l!_A(x1) = max{56, x1 + 1}
  
    partial status:
  
      pi(min#) = []
      pi(n) = [2]
      pi(|0|) = [1]
      pi(|#|) = []
      pi(-) = []
      pi(not) = []
      pi(true) = []
      pi(false) = []
      pi(ge) = []
      pi(|1|) = []
      pi(size) = []
      pi(l) = [1]

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

  r36

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          max#_A(x1) = x1
          n_A(x1,x2,x3) = x2 + x3 + 15
          size_A(x1) = x1 + 14
          l_A(x1) = x1 + 8
          |1|_A(x1) = 6
          |#|_A() = 7
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          max#_A(x1) = 0
          n_A(x1,x2,x3) = max{x1 + 23, x2 - 88, x3 - 88}
          size_A(x1) = max{35, x1 - 68}
          l_A(x1) = max{0, x1 - 88}
          |1|_A(x1) = max{15, x1 - 27}
          |#|_A = 5
          max#!_A(x1) = max{176, x1 + 2}
          n!_A(x1,x2,x3) = max{175, x1 - 236, x2 - 260}
          size!_A(x1) = max{176, x1 - 17}
          l!_A(x1) = max{175, x1 + 40}
          |1|!_A(x1) = x1 + 151
          |#|!_A = 174
  
    partial status:
  
      pi(max#) = []
      pi(n) = [2]
      pi(size) = []
      pi(l) = [1]
      pi(|1|) = []
      pi(|#|) = []

The following rules are removed:

  p1

Then no dependency pair remains.