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(true()) -> false()
  not(false()) -> true()
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eq(|#|(),|#|()) -> true()
  eq(|#|(),|1|(y)) -> false()
  eq(|1|(x),|#|()) -> false()
  eq(|#|(),|0|(y)) -> eq(|#|(),y)
  eq(|0|(x),|#|()) -> eq(x,|#|())
  eq(|1|(x),|1|(y)) -> eq(x,y)
  eq(|0|(x),|1|(y)) -> false()
  eq(|1|(x),|0|(y)) -> false()
  eq(|0|(x),|0|(y)) -> eq(x,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(|#|(),|0|(x)) -> ge(|#|(),x)
  ge(|#|(),|1|(x)) -> false()
  log(x) -> -(|log'|(x),|1|(|#|()))
  |log'|(|#|()) -> |#|()
  |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
  |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
  *(|#|(),x) -> |#|()
  *(|0|(x),y) -> |0|(*(x,y))
  *(|1|(x),y) -> +(|0|(*(x,y)),y)
  *(*(x,y),z) -> *(x,*(y,z))
  *(x,+(y,z)) -> +(*(x,y),*(x,z))
  app(nil(),l) -> l
  app(cons(x,l1),l2) -> cons(x,app(l1,l2))
  sum(nil()) -> |0|(|#|())
  sum(cons(x,l)) -> +(x,sum(l))
  sum(app(l1,l2)) -> +(sum(l1),sum(l2))
  prod(nil()) -> |1|(|#|())
  prod(cons(x,l)) -> *(x,prod(l))
  prod(app(l1,l2)) -> *(prod(l1),prod(l2))
  mem(x,nil()) -> false()
  mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
  inter(x,nil()) -> nil()
  inter(nil(),x) -> nil()
  inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
  inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
  inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
  inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
  ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
  ifinter(false(),x,l1,l2) -> inter(l1,l2)


-- 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) -> +#(y,z)
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: eq#(|#|(),|0|(y)) -> eq#(|#|(),y)
p18: eq#(|0|(x),|#|()) -> eq#(x,|#|())
p19: eq#(|1|(x),|1|(y)) -> eq#(x,y)
p20: eq#(|0|(x),|0|(y)) -> eq#(x,y)
p21: ge#(|0|(x),|0|(y)) -> ge#(x,y)
p22: ge#(|0|(x),|1|(y)) -> not#(ge(y,x))
p23: ge#(|0|(x),|1|(y)) -> ge#(y,x)
p24: ge#(|1|(x),|0|(y)) -> ge#(x,y)
p25: ge#(|1|(x),|1|(y)) -> ge#(x,y)
p26: ge#(|#|(),|0|(x)) -> ge#(|#|(),x)
p27: log#(x) -> -#(|log'|(x),|1|(|#|()))
p28: log#(x) -> |log'|#(x)
p29: |log'|#(|1|(x)) -> +#(|log'|(x),|1|(|#|()))
p30: |log'|#(|1|(x)) -> |log'|#(x)
p31: |log'|#(|0|(x)) -> if#(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
p32: |log'|#(|0|(x)) -> ge#(x,|1|(|#|()))
p33: |log'|#(|0|(x)) -> +#(|log'|(x),|1|(|#|()))
p34: |log'|#(|0|(x)) -> |log'|#(x)
p35: *#(|0|(x),y) -> |0|#(*(x,y))
p36: *#(|0|(x),y) -> *#(x,y)
p37: *#(|1|(x),y) -> +#(|0|(*(x,y)),y)
p38: *#(|1|(x),y) -> |0|#(*(x,y))
p39: *#(|1|(x),y) -> *#(x,y)
p40: *#(*(x,y),z) -> *#(x,*(y,z))
p41: *#(*(x,y),z) -> *#(y,z)
p42: *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
p43: *#(x,+(y,z)) -> *#(x,y)
p44: *#(x,+(y,z)) -> *#(x,z)
p45: app#(cons(x,l1),l2) -> app#(l1,l2)
p46: sum#(nil()) -> |0|#(|#|())
p47: sum#(cons(x,l)) -> +#(x,sum(l))
p48: sum#(cons(x,l)) -> sum#(l)
p49: sum#(app(l1,l2)) -> +#(sum(l1),sum(l2))
p50: sum#(app(l1,l2)) -> sum#(l1)
p51: sum#(app(l1,l2)) -> sum#(l2)
p52: prod#(cons(x,l)) -> *#(x,prod(l))
p53: prod#(cons(x,l)) -> prod#(l)
p54: prod#(app(l1,l2)) -> *#(prod(l1),prod(l2))
p55: prod#(app(l1,l2)) -> prod#(l1)
p56: prod#(app(l1,l2)) -> prod#(l2)
p57: mem#(x,cons(y,l)) -> if#(eq(x,y),true(),mem(x,l))
p58: mem#(x,cons(y,l)) -> eq#(x,y)
p59: mem#(x,cons(y,l)) -> mem#(x,l)
p60: inter#(app(l1,l2),l3) -> app#(inter(l1,l3),inter(l2,l3))
p61: inter#(app(l1,l2),l3) -> inter#(l1,l3)
p62: inter#(app(l1,l2),l3) -> inter#(l2,l3)
p63: inter#(l1,app(l2,l3)) -> app#(inter(l1,l2),inter(l1,l3))
p64: inter#(l1,app(l2,l3)) -> inter#(l1,l2)
p65: inter#(l1,app(l2,l3)) -> inter#(l1,l3)
p66: inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
p67: inter#(cons(x,l1),l2) -> mem#(x,l2)
p68: inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
p69: inter#(l1,cons(x,l2)) -> mem#(x,l1)
p70: ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
p71: ifinter#(false(),x,l1,l2) -> inter#(l1,l2)

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The estimated dependency graph contains the following SCCs:

  {p48, p50, p51}
  {p53, p55, p56}
  {p36, p39, p40, p41, p43, p44}
  {p30, p34}
  {p2, p3, p4, p6, p7, p8, p9}
  {p11, p12, p13, p14, p16}
  {p61, p62, p64, p65, p66, p68, p70, p71}
  {p59}
  {p19, p20}
  {p17}
  {p18}
  {p21, p23, p24, p25}
  {p26}
  {p45}


-- Reduction pair.

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

p1: sum#(app(l1,l2)) -> sum#(l2)
p2: sum#(app(l1,l2)) -> sum#(l1)
p3: sum#(cons(x,l)) -> sum#(l)

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r49

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:
          sum#_A(x1) = x1
          app_A(x1,x2) = x1 + x2 + 15
          cons_A(x1,x2) = x1 + x2 + 14
          prod_A(x1) = x1 + 3
          nil_A() = 13
          |1|_A(x1) = x1 + 9
          |#|_A() = 3
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          sum#_A(x1) = max{0, x1 - 5}
          app_A(x1,x2) = max{5, x1 + 1, x2 + 1}
          cons_A(x1,x2) = max{6, x1 - 36, x2 + 4}
          prod_A(x1) = max{14, x1 - 21}
          nil_A = 12
          |1|_A(x1) = max{0, x1 - 21}
          |#|_A = 19
          sum#!_A(x1) = 0
          app!_A(x1,x2) = max{0, x1 - 7, x2 - 12}
          cons!_A(x1,x2) = max{46, x1 - 42, x2 - 52}
          prod!_A(x1) = max{0, x1 - 53}
          nil!_A = 26
          |1|!_A(x1) = 17
          |#|!_A = 19
  
    partial status:
  
      pi(sum#) = [1]
      pi(app) = [1, 2]
      pi(cons) = [2]
      pi(prod) = []
      pi(nil) = []
      pi(|1|) = []
      pi(|#|) = []

The following rules are removed:

  p1, p2, p3

Then no dependency pair remains.

-- Reduction pair.

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

p1: prod#(app(l1,l2)) -> prod#(l2)
p2: prod#(app(l1,l2)) -> prod#(l1)
p3: prod#(cons(x,l)) -> prod#(l)

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r16, r32

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:
          prod#_A(x1) = x1
          app_A(x1,x2) = x1 + x2 + 13
          cons_A(x1,x2) = x1 + x2 + 12
          not_A(x1) = x1 + 10
          false_A() = 10
          true_A() = 1
          ge_A(x1,x2) = x1 + 3
          |#|_A() = 8
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          prod#_A(x1) = max{0, x1 - 3}
          app_A(x1,x2) = max{3, x1 + 2, x2 + 1}
          cons_A(x1,x2) = max{4, x1 - 13, x2 + 1}
          not_A(x1) = max{283, x1 - 285}
          false_A = 284
          true_A = 1
          ge_A(x1,x2) = max{282, x1 - 222, x2 - 15}
          |#|_A = 14
          prod#!_A(x1) = 300
          app!_A(x1,x2) = max{299, x1 - 623, x2 - 621}
          cons!_A(x1,x2) = max{296, x1 - 1218, x2 - 1222}
          not!_A(x1) = max{281, x1 - 1559}
          false!_A = 17
          true!_A = 1
          ge!_A(x1,x2) = max{87, x2 - 1278}
          |#|!_A = 14
  
    partial status:
  
      pi(prod#) = [1]
      pi(app) = [1, 2]
      pi(cons) = [1, 2]
      pi(not) = []
      pi(false) = []
      pi(true) = []
      pi(ge) = []
      pi(|#|) = []

The following rules are removed:

  p1, p2, p3

Then no dependency pair remains.

-- Reduction pair.

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

p1: *#(x,+(y,z)) -> *#(x,z)
p2: *#(x,+(y,z)) -> *#(x,y)
p3: *#(*(x,y),z) -> *#(y,z)
p4: *#(*(x,y),z) -> *#(x,*(y,z))
p5: *#(|1|(x),y) -> *#(x,y)
p6: *#(|0|(x),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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r1, r2, r3, r9, r36, r39, r46

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 + 3
          +_A(x1,x2) = x1 + x2 + 2
          *_A(x1,x2) = x1 + x2 + 17
          |1|_A(x1) = x1 + 5
          |0|_A(x1) = x1 + 16
          |#|_A() = 4
          -_A(x1,x2) = 10
          |log'|_A(x1) = x1 + 12
          sum_A(x1) = x1 + 28
          nil_A() = 1
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          *#_A(x1,x2) = max{0, x1 - 238}
          +_A(x1,x2) = max{726, x1 + 482, x2 + 482}
          *_A(x1,x2) = max{483, x1 + 238, x2 + 238}
          |1|_A(x1) = max{487, x1 + 485}
          |0|_A(x1) = max{300, x1 + 87}
          |#|_A = 24
          -_A(x1,x2) = max{298, x1 + 161}
          |log'|_A(x1) = 699
          sum_A(x1) = max{326, x1 - 483}
          nil_A = 211
          *#!_A(x1,x2) = 0
          +!_A(x1,x2) = 243
          *!_A(x1,x2) = max{6, x1 - 245, x2 - 729}
          |1|!_A(x1) = max{7, x1 - 321}
          |0|!_A(x1) = 7
          |#|!_A = 377
          -!_A(x1,x2) = max{188, x1 - 299, x2 - 111}
          |log'|!_A(x1) = max{9, x1 - 479}
          sum!_A(x1) = max{378, x1 - 243}
          nil!_A = 462
  
    partial status:
  
      pi(*#) = [1]
      pi(+) = []
      pi(*) = []
      pi(|1|) = [1]
      pi(|0|) = []
      pi(|#|) = []
      pi(-) = []
      pi(|log'|) = []
      pi(sum) = []
      pi(nil) = []

The following rules are removed:

  p3, p4, p5, p6



-- SCC decomposition.

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

p1: *#(x,+(y,z)) -> *#(x,z)
p2: *#(x,+(y,z)) -> *#(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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: *#(x,+(y,z)) -> *#(x,z)
p2: *#(x,+(y,z)) -> *#(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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9, r16, r19, r32, r36, r39

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) = 1
          +_A(x1,x2) = 10
          -_A(x1,x2) = x2 + 12
          |#|_A() = 11
          not_A(x1) = x1 + 9
          false_A() = 1
          true_A() = 2
          eq_A(x1,x2) = x1 + x2 + 51
          ge_A(x1,x2) = x1 + 3
          |log'|_A(x1) = 12
          *_A(x1,x2) = x1 + x2 + 38
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          *#_A(x1,x2) = max{0, x2 - 16}
          +_A(x1,x2) = max{165, x1 + 15, x2}
          -_A(x1,x2) = 129
          |#|_A = 0
          not_A(x1) = max{384, x1 - 386}
          false_A = 385
          true_A = 1
          eq_A(x1,x2) = max{x1 + 182, x2 + 182}
          ge_A(x1,x2) = max{x1 + 182, x2 + 365}
          |log'|_A(x1) = max{0, x1 - 142}
          *_A(x1,x2) = max{131, x2 - 181}
          *#!_A(x1,x2) = x2 + 142
          +!_A(x1,x2) = max{x1 + 142, x2 + 181}
          -!_A(x1,x2) = 270
          |#|!_A = 270
          not!_A(x1) = max{270, x1 - 386}
          false!_A = 0
          true!_A = 269
          eq!_A(x1,x2) = 269
          ge!_A(x1,x2) = max{0, x1 - 224}
          |log'|!_A(x1) = max{114, x1 - 19}
          *!_A(x1,x2) = max{313, x1 - 133, x2 - 166}
  
    partial status:
  
      pi(*#) = []
      pi(+) = []
      pi(-) = [2]
      pi(|#|) = []
      pi(not) = [1]
      pi(false) = []
      pi(true) = []
      pi(eq) = []
      pi(ge) = [1]
      pi(|log'|) = []
      pi(*) = [1]

The following rules are removed:

  p2



-- SCC decomposition.

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

p1: *#(x,+(y,z)) -> *#(x,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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: *#(x,+(y,z)) -> *#(x,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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9

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
          +_A(x1,x2) = x2 + 10
          -_A(x1,x2) = x1 + 2
          |#|_A() = 4
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          *#_A(x1,x2) = max{0, x2 - 4}
          +_A(x1,x2) = max{19, x1 - 100, x2 + 3}
          -_A(x1,x2) = max{192, x2 - 92}
          |#|_A = 60
          *#!_A(x1,x2) = max{1, x1 - 1, x2 - 1}
          +!_A(x1,x2) = max{0, x2 - 21}
          -!_A(x1,x2) = max{25, x2 - 1}
          |#|!_A = 3
  
    partial status:
  
      pi(*#) = [2]
      pi(+) = []
      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: |log'|#(|0|(x)) -> |log'|#(x)
p2: |log'|#(|1|(x)) -> |log'|#(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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r15, r16, r32, r34

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:
          |log'|#_A(x1) = x1
          |0|_A(x1) = x1 + 8
          |1|_A(x1) = x1 + 13
          not_A(x1) = x1 + 9
          true_A() = 1
          false_A() = 2
          ge_A(x1,x2) = x1 + 2
          |#|_A() = 3
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          |log'|#_A(x1) = 0
          |0|_A(x1) = max{0, x1 - 25}
          |1|_A(x1) = 15
          not_A(x1) = max{26, x1 - 21}
          true_A = 1
          false_A = 1
          ge_A(x1,x2) = x1 + 25
          |#|_A = 25
          |log'|#!_A(x1) = 28
          |0|!_A(x1) = 70
          |1|!_A(x1) = max{71, x1 + 27}
          not!_A(x1) = max{78, x1 - 21}
          true!_A = 71
          false!_A = 77
          ge!_A(x1,x2) = max{76, x1 - 26}
          |#|!_A = 73
  
    partial status:
  
      pi(|log'|#) = [1]
      pi(|0|) = []
      pi(|1|) = [1]
      pi(not) = [1]
      pi(true) = []
      pi(false) = []
      pi(ge) = [1]
      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: +#(|0|(x),|0|(y)) -> +#(x,y)
p2: +#(+(x,y),z) -> +#(y,z)
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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

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:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          +#_A(x1,x2) = x1 + x2 + 22
          |0|_A(x1) = x1 + 6
          +_A(x1,x2) = x1 + x2 + 5
          |1|_A(x1) = x1 + 21
          |#|_A() = 9
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          +#_A(x1,x2) = max{0, x1 - 108, x2 - 108}
          |0|_A(x1) = max{13, x1}
          +_A(x1,x2) = max{107, x1, x2}
          |1|_A(x1) = max{4, x1}
          |#|_A = 17
          +#!_A(x1,x2) = 0
          |0|!_A(x1) = max{7, x1}
          +!_A(x1,x2) = 106
          |1|!_A(x1) = 0
          |#|!_A = 34
  
    partial status:
  
      pi(+#) = [1, 2]
      pi(|0|) = [1]
      pi(+) = [1]
      pi(|1|) = [1]
      pi(|#|) = []

The following rules are removed:

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

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

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) = x1 + x2 + 16
          |0|_A(x1) = x1 + 15
          |1|_A(x1) = x1 + 15
          -_A(x1,x2) = x1
          |#|_A() = 3
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          -#_A(x1,x2) = max{0, x1 - 29, x2 - 57}
          |0|_A(x1) = x1 + 27
          |1|_A(x1) = x1 + 27
          -_A(x1,x2) = max{x1, x2 - 84}
          |#|_A = 29
          -#!_A(x1,x2) = max{113, x2 + 86}
          |0|!_A(x1) = max{94, x1 + 85}
          |1|!_A(x1) = 92
          -!_A(x1,x2) = max{94, x1 + 62, x2 - 26}
          |#|!_A = 90
  
    partial status:
  
      pi(-#) = [1]
      pi(|0|) = []
      pi(|1|) = [1]
      pi(-) = [1]
      pi(|#|) = []

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: ifinter#(false(),x,l1,l2) -> inter#(l1,l2)
p2: inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
p3: ifinter#(true(),x,l1,l2) -> inter#(l1,l2)
p4: inter#(cons(x,l1),l2) -> ifinter#(mem(x,l2),x,l1,l2)
p5: inter#(l1,app(l2,l3)) -> inter#(l1,l3)
p6: inter#(l1,app(l2,l3)) -> inter#(l1,l2)
p7: inter#(app(l1,l2),l3) -> inter#(l2,l3)
p8: inter#(app(l1,l2),l3) -> inter#(l1,l3)

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r32, r33, r34, r52, r53

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:
          ifinter#_A(x1,x2,x3,x4) = x3 + x4 + 36
          false_A() = 4
          inter#_A(x1,x2) = x1 + x2 + 2
          cons_A(x1,x2) = x1 + x2 + 35
          mem_A(x1,x2) = x1 + x2 + 36
          true_A() = 3
          app_A(x1,x2) = x1 + x2 + 47
          -_A(x1,x2) = 7
          |#|_A() = 6
          not_A(x1) = x1 + 2
          if_A(x1,x2,x3) = x2 + x3 + 31
          eq_A(x1,x2) = 5
          |1|_A(x1) = 19
          |0|_A(x1) = x1 + 11
          ge_A(x1,x2) = 5
          nil_A() = 20
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          ifinter#_A(x1,x2,x3,x4) = max{0, x1 - 2, x2 - 316, x3 - 12, x4 - 16}
          false_A = 0
          inter#_A(x1,x2) = max{0, x1 - 16, x2 - 16}
          cons_A(x1,x2) = max{14, x1 - 300, x2 + 4}
          mem_A(x1,x2) = max{1, x1 - 612, x2 - 305}
          true_A = 0
          app_A(x1,x2) = max{13, x1 + 1, x2 + 4}
          -_A(x1,x2) = max{24, x1 + 5}
          |#|_A = 23
          not_A(x1) = max{78, x1 - 78}
          if_A(x1,x2,x3) = max{x1 - 78, x2 + 1, x3}
          eq_A(x1,x2) = max{0, x1 - 565, x2 - 563}
          |1|_A(x1) = x1 + 25
          |0|_A(x1) = max{54, x1 + 48}
          ge_A(x1,x2) = max{77, x1 - 176, x2 - 49}
          nil_A = 13
          ifinter#!_A(x1,x2,x3,x4) = max{24, x1 - 319, x2 - 318, x3 - 12, x4 - 1}
          false!_A = 1
          inter#!_A(x1,x2) = max{23, x1 - 17, x2 - 15}
          cons!_A(x1,x2) = max{0, x1 - 56}
          mem!_A(x1,x2) = max{0, x1 - 622, x2 - 320}
          true!_A = 0
          app!_A(x1,x2) = max{22, x1 - 322, x2 - 321}
          -!_A(x1,x2) = max{0, x1 - 25}
          |#|!_A = 11
          not!_A(x1) = max{2, x1 - 80}
          if!_A(x1,x2,x3) = max{20, x1 - 57, x3 - 10}
          eq!_A(x1,x2) = max{10, x1 - 623, x2 - 55}
          |1|!_A(x1) = 0
          |0|!_A(x1) = max{0, x1 - 4}
          ge!_A(x1,x2) = max{3, x1 - 178, x2 - 44}
          nil!_A = 20
  
    partial status:
  
      pi(ifinter#) = []
      pi(false) = []
      pi(inter#) = [1, 2]
      pi(cons) = [2]
      pi(mem) = [1, 2]
      pi(true) = []
      pi(app) = [1, 2]
      pi(-) = []
      pi(|#|) = []
      pi(not) = [1]
      pi(if) = []
      pi(eq) = []
      pi(|1|) = []
      pi(|0|) = []
      pi(ge) = []
      pi(nil) = []

The following rules are removed:

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

Then no dependency pair remains.

-- Reduction pair.

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

p1: mem#(x,cons(y,l)) -> mem#(x,l)

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9, r36, r39, r52

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:
          mem#_A(x1,x2) = x2
          cons_A(x1,x2) = x1 + x2 + 12
          -_A(x1,x2) = 7
          |#|_A() = 0
          |log'|_A(x1) = x1 + 1
          *_A(x1,x2) = x1 + x2 + 10
          mem_A(x1,x2) = x1 + 3
          nil_A() = 15
          false_A() = 2
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          mem#_A(x1,x2) = max{0, x2 - 6}
          cons_A(x1,x2) = max{x1 - 95, x2 + 5}
          -_A(x1,x2) = max{4, x1 - 137, x2 - 163}
          |#|_A = 0
          |log'|_A(x1) = max{0, x1 - 23}
          *_A(x1,x2) = max{1, x1 - 23, x2 - 23}
          mem_A(x1,x2) = max{5, x1 - 20, x2 - 13}
          nil_A = 2
          false_A = 2
          mem#!_A(x1,x2) = max{108, x1 - 1, x2 - 6}
          cons!_A(x1,x2) = max{107, x1 - 150, x2 - 56}
          -!_A(x1,x2) = max{10, x1 - 6, x2 - 72}
          |#|!_A = 67
          |log'|!_A(x1) = max{10, x1 - 52}
          *!_A(x1,x2) = max{106, x1 - 182, x2 - 86}
          mem!_A(x1,x2) = max{108, x1 - 149, x2 - 55}
          nil!_A = 104
          false!_A = 103
  
    partial status:
  
      pi(mem#) = []
      pi(cons) = [2]
      pi(-) = []
      pi(|#|) = []
      pi(|log'|) = []
      pi(*) = []
      pi(mem) = []
      pi(nil) = []
      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: eq#(|0|(x),|0|(y)) -> eq#(x,y)
p2: eq#(|1|(x),|1|(y)) -> eq#(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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9, 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:
          eq#_A(x1,x2) = x1 + x2 + 19
          |0|_A(x1) = x1 + 9
          |1|_A(x1) = x1 + 18
          -_A(x1,x2) = 8
          |#|_A() = 6
          |log'|_A(x1) = 8
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          eq#_A(x1,x2) = 0
          |0|_A(x1) = x1 + 54
          |1|_A(x1) = max{2, x1 - 62}
          -_A(x1,x2) = max{281, x1 - 220, x2 - 55}
          |#|_A = 14
          |log'|_A(x1) = max{62, x1 - 61}
          eq#!_A(x1,x2) = max{x1 + 61, x2 - 1}
          |0|!_A(x1) = max{19, x1 - 16}
          |1|!_A(x1) = 0
          -!_A(x1,x2) = 20
          |#|!_A = 20
          |log'|!_A(x1) = max{18, x1 - 55}
  
    partial status:
  
      pi(eq#) = [2]
      pi(|0|) = [1]
      pi(|1|) = []
      pi(-) = []
      pi(|#|) = []
      pi(|log'|) = []

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: eq#(|#|(),|0|(y)) -> eq#(|#|(),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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9, r39

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:
          eq#_A(x1,x2) = x2
          |#|_A() = 3
          |0|_A(x1) = x1 + 8
          -_A(x1,x2) = 9
          *_A(x1,x2) = x1 + x2 + 19
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          eq#_A(x1,x2) = max{0, x2 - 17}
          |#|_A = 21
          |0|_A(x1) = max{19, x1 + 16}
          -_A(x1,x2) = max{210, x2 - 403}
          *_A(x1,x2) = max{28, x1 - 246, x2 - 245}
          eq#!_A(x1,x2) = max{1, x1 - 22}
          |#|!_A = 266
          |0|!_A(x1) = 3
          -!_A(x1,x2) = max{266, x1 + 233}
          *!_A(x1,x2) = max{277, x1 + 244, x2 + 2}
  
    partial status:
  
      pi(eq#) = [2]
      pi(|#|) = []
      pi(|0|) = [1]
      pi(-) = []
      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: eq#(|0|(x),|#|()) -> eq#(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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9, r36, r39, r49

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:
          eq#_A(x1,x2) = x1
          |0|_A(x1) = x1 + 55
          |#|_A() = 14
          -_A(x1,x2) = x1 + x2 + 14
          |log'|_A(x1) = 27
          *_A(x1,x2) = x1 + x2 + 3
          prod_A(x1) = x1 + 1
          nil_A() = 70
          |1|_A(x1) = x1 + 7
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          eq#_A(x1,x2) = max{0, x1 - 8}
          |0|_A(x1) = x1 + 7
          |#|_A = 0
          -_A(x1,x2) = max{58, x1 - 58, x2}
          |log'|_A(x1) = max{0, x1 - 48}
          *_A(x1,x2) = max{1, x1 - 58, x2 - 58}
          prod_A(x1) = max{0, x1 - 102}
          nil_A = 16
          |1|_A(x1) = 0
          eq#!_A(x1,x2) = max{62, x1 - 8}
          |0|!_A(x1) = 47
          |#|!_A = 61
          -!_A(x1,x2) = max{1, x2 - 1}
          |log'|!_A(x1) = max{63, x1 + 60}
          *!_A(x1,x2) = max{48, x1 - 3, x2 - 5}
          prod!_A(x1) = max{6, x1 - 107}
          nil!_A = 1
          |1|!_A(x1) = 5
  
    partial status:
  
      pi(eq#) = [1]
      pi(|0|) = [1]
      pi(|#|) = []
      pi(-) = []
      pi(|log'|) = []
      pi(*) = [1]
      pi(prod) = []
      pi(nil) = []
      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: 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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r1, r46

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 + 7
          |0|_A(x1) = x1 + 6
          |1|_A(x1) = x1 + 8
          |#|_A() = 0
          sum_A(x1) = x1 + 5
          nil_A() = 9
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          ge#_A(x1,x2) = max{0, x1 - 22, x2 - 22}
          |0|_A(x1) = max{11, x1}
          |1|_A(x1) = x1 + 21
          |#|_A = 93
          sum_A(x1) = max{421, x1 - 422}
          nil_A = 33
          ge#!_A(x1,x2) = max{310, x2 + 289}
          |0|!_A(x1) = max{290, x1 + 288}
          |1|!_A(x1) = x1 + 189
          |#|!_A = 287
          sum!_A(x1) = max{688, x1 - 132}
          nil!_A = 382
  
    partial status:
  
      pi(ge#) = [1, 2]
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|#|) = []
      pi(sum) = [1]
      pi(nil) = []

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  r9

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
          |#|_A() = 7
          |0|_A(x1) = x1 + 38
          -_A(x1,x2) = x2 + 10
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          ge#_A(x1,x2) = max{0, x2 - 1}
          |#|_A = 9
          |0|_A(x1) = max{8, x1}
          -_A(x1,x2) = max{105, x1 - 104, x2 - 100}
          ge#!_A(x1,x2) = max{8, x1 - 2}
          |#|!_A = 6
          |0|!_A(x1) = 6
          -!_A(x1,x2) = max{7, x1 - 213, x2 - 1}
  
    partial status:
  
      pi(ge#) = [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: app#(cons(x,l1),l2) -> app#(l1,l2)

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) -> |#|()
r10: -(x,|#|()) -> 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(true()) -> false()
r16: not(false()) -> true()
r17: if(true(),x,y) -> x
r18: if(false(),x,y) -> y
r19: eq(|#|(),|#|()) -> true()
r20: eq(|#|(),|1|(y)) -> false()
r21: eq(|1|(x),|#|()) -> false()
r22: eq(|#|(),|0|(y)) -> eq(|#|(),y)
r23: eq(|0|(x),|#|()) -> eq(x,|#|())
r24: eq(|1|(x),|1|(y)) -> eq(x,y)
r25: eq(|0|(x),|1|(y)) -> false()
r26: eq(|1|(x),|0|(y)) -> false()
r27: eq(|0|(x),|0|(y)) -> eq(x,y)
r28: ge(|0|(x),|0|(y)) -> ge(x,y)
r29: ge(|0|(x),|1|(y)) -> not(ge(y,x))
r30: ge(|1|(x),|0|(y)) -> ge(x,y)
r31: ge(|1|(x),|1|(y)) -> ge(x,y)
r32: ge(x,|#|()) -> true()
r33: ge(|#|(),|0|(x)) -> ge(|#|(),x)
r34: ge(|#|(),|1|(x)) -> false()
r35: log(x) -> -(|log'|(x),|1|(|#|()))
r36: |log'|(|#|()) -> |#|()
r37: |log'|(|1|(x)) -> +(|log'|(x),|1|(|#|()))
r38: |log'|(|0|(x)) -> if(ge(x,|1|(|#|())),+(|log'|(x),|1|(|#|())),|#|())
r39: *(|#|(),x) -> |#|()
r40: *(|0|(x),y) -> |0|(*(x,y))
r41: *(|1|(x),y) -> +(|0|(*(x,y)),y)
r42: *(*(x,y),z) -> *(x,*(y,z))
r43: *(x,+(y,z)) -> +(*(x,y),*(x,z))
r44: app(nil(),l) -> l
r45: app(cons(x,l1),l2) -> cons(x,app(l1,l2))
r46: sum(nil()) -> |0|(|#|())
r47: sum(cons(x,l)) -> +(x,sum(l))
r48: sum(app(l1,l2)) -> +(sum(l1),sum(l2))
r49: prod(nil()) -> |1|(|#|())
r50: prod(cons(x,l)) -> *(x,prod(l))
r51: prod(app(l1,l2)) -> *(prod(l1),prod(l2))
r52: mem(x,nil()) -> false()
r53: mem(x,cons(y,l)) -> if(eq(x,y),true(),mem(x,l))
r54: inter(x,nil()) -> nil()
r55: inter(nil(),x) -> nil()
r56: inter(app(l1,l2),l3) -> app(inter(l1,l3),inter(l2,l3))
r57: inter(l1,app(l2,l3)) -> app(inter(l1,l2),inter(l1,l3))
r58: inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
r59: inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
r60: ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
r61: ifinter(false(),x,l1,l2) -> inter(l1,l2)

The set of usable rules consists of

  (no rules)

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:
          app#_A(x1,x2) = x1
          cons_A(x1,x2) = x1 + x2 + 29
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        max/plus interpretation on natural numbers:
        
          app#_A(x1,x2) = max{0, x1 - 2}
          cons_A(x1,x2) = max{3, x1 - 199, x2 + 1}
          app#!_A(x1,x2) = max{1, x2 - 1}
          cons!_A(x1,x2) = max{0, x1 - 6, x2 - 328}
  
    partial status:
  
      pi(app#) = []
      pi(cons) = [2]

The following rules are removed:

  p1

Then no dependency pair remains.