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

  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!):
        
          max/plus interpretation on natural numbers:
          
            wb#_A(x1) = max{0, x1 - 16}
            n_A(x1,x2,x3) = max{x1 + 8, x2 + 15, x3 + 15}
            -_A(x1,x2) = max{1016, x1 - 12, x2 - 12}
            |#|_A = 10
            wb#!_A(x1) = max{1, x1}
            n!_A(x1,x2,x3) = max{142, x2, x3 + 89}
            -!_A(x1,x2) = max{98, x2 - 1001}
            |#|!_A = 2
        
        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) = 0
              n_A(x1,x2,x3) = x1 + x2 + 4
              -_A(x1,x2) = x2 + 5
              |#|_A() = 5
              wb#!_A(x1) = x1
              n!_A(x1,x2,x3) = x1 + x2 + 16
              -!_A(x1,x2) = x1
              |#|!_A() = 10
        
  
    partial status:
  
      pi(wb#) = [1]
      pi(n) = [2, 3]
      pi(-) = []
      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!):
        
          max/plus interpretation on natural numbers:
          
            size#_A(x1) = max{0, x1 - 247}
            n_A(x1,x2,x3) = max{x1 + 246, x2, x3}
            size#!_A(x1) = max{204, x1 - 3}
            n!_A(x1,x2,x3) = max{1677, x1 + 207, x2 + 7, x3 + 203}
        
        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
              size#!_A(x1) = x1 + 14
              n!_A(x1,x2,x3) = x1 + x2 + x3 + 14
        
  
    partial status:
  
      pi(size#) = []
      pi(n) = [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

  r1, r2, r3, 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!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = 0
            |0|_A(x1) = max{230, x1 + 68}
            +_A(x1,x2) = max{302, x1 + 152, x2 + 151}
            |1|_A(x1) = max{218, x1 + 95}
            |#|_A = 57
            -_A(x1,x2) = max{564, x1 - 57}
            +#!_A(x1,x2) = max{65, x2 - 153}
            |0|!_A(x1) = max{706, x1 + 640}
            +!_A(x1,x2) = x2 + 711
            |1|!_A(x1) = 10
            |#|!_A = 240
            -!_A(x1,x2) = max{x1 - 218, x2 + 639}
        
        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 + 1
              +_A(x1,x2) = x1 + x2 + 2
              |1|_A(x1) = x1 + 2
              |#|_A() = 0
              -_A(x1,x2) = 0
              +#!_A(x1,x2) = x2 + 7
              |0|!_A(x1) = 5
              +!_A(x1,x2) = 1
              |1|!_A(x1) = 8
              |#|!_A() = 0
              -!_A(x1,x2) = x2 + 6
        
  
    partial status:
  
      pi(+#) = []
      pi(|0|) = [1]
      pi(+) = [1, 2]
      pi(|1|) = []
      pi(|#|) = []
      pi(-) = [2]

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

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!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = 0
            |1|_A(x1) = max{108, x1 - 4}
            +_A(x1,x2) = max{137, x1, x2 + 34}
            |#|_A = 40
            |0|_A(x1) = max{40, x1 - 4}
            +#!_A(x1,x2) = 3
            |1|!_A(x1) = 46
            +!_A(x1,x2) = max{45, x2 + 5}
            |#|!_A = 2
            |0|!_A(x1) = 111
        
        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
              |1|_A(x1) = x1 + 4
              +_A(x1,x2) = x1 + x2 + 1
              |#|_A() = 2
              |0|_A(x1) = x1 + 1
              +#!_A(x1,x2) = x1 + x2
              |1|!_A(x1) = 6
              +!_A(x1,x2) = 9
              |#|!_A() = 4
              |0|!_A(x1) = 7
        
  
    partial status:
  
      pi(+#) = []
      pi(|1|) = []
      pi(+) = [1, 2]
      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: -#(|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

  r10, r15

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!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{0, x2 - 6}
            |0|_A(x1) = max{50, x1}
            |1|_A(x1) = max{4, x1}
            -_A(x1,x2) = max{50, x1, x2}
            |#|_A = 5
            not_A(x1) = max{69, x1 - 71}
            false_A = 70
            true_A = 69
            -#!_A(x1,x2) = max{0, x2 - 6}
            |0|!_A(x1) = 0
            |1|!_A(x1) = 2
            -!_A(x1,x2) = max{228, x1 + 1}
            |#|!_A = 216
            not!_A(x1) = max{275, x1 + 132}
            false!_A = 204
            true!_A = 203
        
        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) = x2
              |0|_A(x1) = x1 + 5
              |1|_A(x1) = x1 + 1
              -_A(x1,x2) = 1
              |#|_A() = 0
              not_A(x1) = 8
              false_A() = 9
              true_A() = 8
              -#!_A(x1,x2) = x2 + 2
              |0|!_A(x1) = 8
              |1|!_A(x1) = 6
              -!_A(x1,x2) = x2 + 4
              |#|!_A() = 2
              not!_A(x1) = 9
              false!_A() = 1
              true!_A() = 0
        
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = [1, 2]
      pi(|#|) = []
      pi(not) = []
      pi(false) = []
      pi(true) = []

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:
  
      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!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{x1, x2 - 312}
            |0|_A(x1) = max{213, x1 + 189}
            |1|_A(x1) = max{213, x1 + 189}
            -_A(x1,x2) = x1
            |#|_A = 122
            -#!_A(x1,x2) = max{1, x1 - 64, x2 - 187}
            |0|!_A(x1) = max{58, x1 + 32}
            |1|!_A(x1) = max{0, x1 - 63}
            -!_A(x1,x2) = max{0, x1 - 155}
            |#|!_A = 0
        
        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
              |0|_A(x1) = x1 + 2
              |1|_A(x1) = x1 + 2
              -_A(x1,x2) = x1
              |#|_A() = 4
              -#!_A(x1,x2) = x1 + 6
              |0|!_A(x1) = 4
              |1|!_A(x1) = 5
              -!_A(x1,x2) = 4
              |#|!_A() = 3
        
  
    partial status:
  
      pi(-#) = [1]
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(-) = [1]
      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

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!):
        
          max/plus interpretation on natural numbers:
          
            bs#_A(x1) = max{0, x1 - 129}
            n_A(x1,x2,x3) = max{x1, x2 + 4, x3 + 128}
            |0|_A(x1) = max{115, x1 + 113}
            |#|_A = 83
            bs#!_A(x1) = x1 + 2017
            n!_A(x1,x2,x3) = max{2015, x2 + 15, x3 + 20}
            |0|!_A(x1) = 919
            |#|!_A = 918
        
        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
              |0|_A(x1) = x1 + 7
              |#|_A() = 5
              bs#!_A(x1) = x1 + 8
              n!_A(x1,x2,x3) = x1 + x3 + 7
              |0|!_A(x1) = x1 + 9
              |#|!_A() = 4
        
  
    partial status:
  
      pi(bs#) = [1]
      pi(n) = [2, 3]
      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: 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, 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!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = max{0, x1 - 293, x2 - 293}
            |0|_A(x1) = x1 + 292
            |1|_A(x1) = max{218, x1 + 130}
            |#|_A = 1
            and_A(x1,x2) = max{1166, x1 + 62, x2 + 57}
            false_A = 1167
            ge#!_A(x1,x2) = 0
            |0|!_A(x1) = max{956, x1 + 163}
            |1|!_A(x1) = x1 + 837
            |#|!_A = 155
            and!_A(x1,x2) = max{x1 + 201, x2 + 241}
            false!_A = 154
        
        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 + 1
              |1|_A(x1) = x1 + 5
              |#|_A() = 2
              and_A(x1,x2) = x2
              false_A() = 9
              ge#!_A(x1,x2) = x1 + x2 + 13
              |0|!_A(x1) = 16
              |1|!_A(x1) = 14
              |#|!_A() = 1
              and!_A(x1,x2) = x1 + 8
              false!_A() = 12
        
  
    partial status:
  
      pi(ge#) = []
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|#|) = []
      pi(and) = []
      pi(false) = []

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!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = max{0, x2 - 18}
            |#|_A = 3
            |0|_A(x1) = x1 + 17
            ge#!_A(x1,x2) = max{12, x1 - 2, x2 - 1}
            |#|!_A = 198
            |0|!_A(x1) = 202
        
        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) = 0
              |#|_A() = 15
              |0|_A(x1) = 14
              ge#!_A(x1,x2) = x2 + 6
              |#|!_A() = 1
              |0|!_A(x1) = 5
        
  
    partial status:
  
      pi(ge#) = [2]
      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

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!):
        
          max/plus interpretation on natural numbers:
          
            min#_A(x1) = 0
            n_A(x1,x2,x3) = max{182, x1 - 1286, x3 - 1286}
            |0|_A(x1) = max{72, x1 + 14}
            |#|_A = 48
            min#!_A(x1) = 1
            n!_A(x1,x2,x3) = max{7, x1 - 1701, x2 - 1093, x3 - 416}
            |0|!_A(x1) = x1 + 9
            |#|!_A = 58
        
        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 + 8
              |#|_A() = 2
              min#!_A(x1) = x1
              n!_A(x1,x2,x3) = x1 + x3 + 12
              |0|!_A(x1) = 8
              |#|!_A() = 0
        
  
    partial status:
  
      pi(min#) = []
      pi(n) = [3]
      pi(|0|) = [1]
      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: max#(n(x,y,z)) -> max#(z)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  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!):
        
          max/plus interpretation on natural numbers:
          
            max#_A(x1) = max{0, x1 - 209}
            n_A(x1,x2,x3) = max{x1 + 7, x3 + 208}
            max#!_A(x1) = max{1, x1 - 209}
            n!_A(x1,x2,x3) = max{x1 - 1, x2}
        
        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 + x3 + 1
              max#!_A(x1) = x1
              n!_A(x1,x2,x3) = x1 + x2 + x3 + 8
        
  
    partial status:
  
      pi(max#) = [1]
      pi(n) = [2, 3]

The following rules are removed:

  p1

Then no dependency pair remains.