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

  r54, r55

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 + 24
          cons_A(x1,x2) = x2 + 2
          inter_A(x1,x2) = x1 + x2 + 25
          nil_A() = 26
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            sum#_A(x1) = x1
            app_A(x1,x2) = x1 + x2 + 8
            cons_A(x1,x2) = x1 + x2 + 5
            inter_A(x1,x2) = x1 + x2 + 10
            nil_A() = 2
            sum#!_A(x1) = x1
            app!_A(x1,x2) = x1 + 36
            cons!_A(x1,x2) = x2 + 35
            inter!_A(x1,x2) = x1 + x2 + 37
            nil!_A() = 36
  
    partial status:
  
      pi(sum#) = [1]
      pi(app) = [1, 2]
      pi(cons) = [2]
      pi(inter) = []
      pi(nil) = []

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

  r54, r55

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 + 2
          cons_A(x1,x2) = x2 + 4
          inter_A(x1,x2) = x1 + x2 + 4
          nil_A() = 44
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            prod#_A(x1) = x1
            app_A(x1,x2) = x1 + x2 + 1
            cons_A(x1,x2) = x1 + x2 + 4
            inter_A(x1,x2) = x1 + x2 + 2
            nil_A() = 1
            prod#!_A(x1) = x1
            app!_A(x1,x2) = x1 + x2 + 20
            cons!_A(x1,x2) = x2 + 22
            inter!_A(x1,x2) = x1 + x2 + 22
            nil!_A() = 22
  
    partial status:
  
      pi(prod#) = [1]
      pi(app) = [1, 2]
      pi(cons) = [2]
      pi(inter) = []
      pi(nil) = []

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

  r2, r3, r39, r55

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 + 1
          +_A(x1,x2) = x1 + x2 + 13
          *_A(x1,x2) = x1 + x2 + 12
          |1|_A(x1) = x1 + 37
          |0|_A(x1) = x1 + 11
          |#|_A() = 2
          inter_A(x1,x2) = x1 + x2 + 76
          nil_A() = 9
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            *#_A(x1,x2) = 0
            +_A(x1,x2) = x1 + x2 + 2
            *_A(x1,x2) = x1 + x2 + 4
            |1|_A(x1) = 9
            |0|_A(x1) = 21
            |#|_A() = 21
            inter_A(x1,x2) = x1 + 6
            nil_A() = 7
            *#!_A(x1,x2) = 7
            +!_A(x1,x2) = 28
            *!_A(x1,x2) = x1 + x2 + 31
            |1|!_A(x1) = 8
            |0|!_A(x1) = 27
            |#|!_A() = 3
            inter!_A(x1,x2) = x1 + x2 + 30
            nil!_A() = 28
  
    partial status:
  
      pi(*#) = []
      pi(+) = []
      pi(*) = [2]
      pi(|1|) = []
      pi(|0|) = []
      pi(|#|) = []
      pi(inter) = [2]
      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

  r2, r5, r6, r55

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) = x1 + 6
          |#|_A() = 10
          |0|_A(x1) = 7
          |1|_A(x1) = 11
          inter_A(x1,x2) = x1 + x2 + 9
          nil_A() = 8
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            *#_A(x1,x2) = x2
            +_A(x1,x2) = x1 + x2 + 1
            |#|_A() = 33
            |0|_A(x1) = 32
            |1|_A(x1) = 15
            inter_A(x1,x2) = x1 + 1
            nil_A() = 8
            *#!_A(x1,x2) = x2 + 5
            +!_A(x1,x2) = x2 + 6
            |#|!_A() = 19
            |0|!_A(x1) = 5
            |1|!_A(x1) = 18
            inter!_A(x1,x2) = x1 + x2 + 6
            nil!_A() = 20
  
    partial status:
  
      pi(*#) = []
      pi(+) = [1]
      pi(|#|) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(inter) = [2]
      pi(nil) = []

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

  r54, r55

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 + 65
          |1|_A(x1) = x1 + 33
          inter_A(x1,x2) = x1 + x2 + 138
          nil_A() = 1
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            |log'|#_A(x1) = x1
            |0|_A(x1) = x1 + 19
            |1|_A(x1) = x1 + 18
            inter_A(x1,x2) = x1 + x2 + 2
            nil_A() = 12
            |log'|#!_A(x1) = x1
            |0|!_A(x1) = 12
            |1|!_A(x1) = x1 + 12
            inter!_A(x1,x2) = x1 + x2 + 6
            nil!_A() = 13
  
    partial status:
  
      pi(|log'|#) = []
      pi(|0|) = []
      pi(|1|) = [1]
      pi(inter) = [1, 2]
      pi(nil) = []

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      matrix interpretation with standard point-wise order:
      
        carrier: N^1
        order: standard order
        interpretations:
          +#_A(x1,x2) = x1 + x2 + 1
          |0|_A(x1) = x1 + 17
          +_A(x1,x2) = x1 + x2 + 2
          |1|_A(x1) = x1 + 23
          |#|_A() = 3
          inter_A(x1,x2) = x1 + x2 + 3
          nil_A() = 19
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            +#_A(x1,x2) = 0
            |0|_A(x1) = 6
            +_A(x1,x2) = x1 + x2 + 3
            |1|_A(x1) = 4
            |#|_A() = 6
            inter_A(x1,x2) = x1 + 1
            nil_A() = 2
            +#!_A(x1,x2) = x1 + 8
            |0|!_A(x1) = 6
            +!_A(x1,x2) = x1 + 7
            |1|!_A(x1) = 0
            |#|!_A() = 4
            inter!_A(x1,x2) = x1 + x2 + 6
            nil!_A() = 7
  
    partial status:
  
      pi(+#) = [1]
      pi(|0|) = []
      pi(+) = []
      pi(|1|) = [1]
      pi(|#|) = []
      pi(inter) = [2]
      pi(nil) = []

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

  r9, r39, r49, r55

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) = 12
          |0|_A(x1) = 13
          |1|_A(x1) = x1 + 15
          -_A(x1,x2) = 14
          |#|_A() = 2
          *_A(x1,x2) = x1 + x2 + 20
          prod_A(x1) = x1 + 20
          nil_A() = 18
          inter_A(x1,x2) = x1 + x2 + 62
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            -#_A(x1,x2) = x2
            |0|_A(x1) = x1 + 2
            |1|_A(x1) = x1 + 1
            -_A(x1,x2) = x2 + 1
            |#|_A() = 0
            *_A(x1,x2) = 7
            prod_A(x1) = x1 + 1
            nil_A() = 8
            inter_A(x1,x2) = x1 + 7
            -#!_A(x1,x2) = x2
            |0|!_A(x1) = x1 + 13
            |1|!_A(x1) = 3
            -!_A(x1,x2) = 2
            |#|!_A() = 15
            *!_A(x1,x2) = x2 + 20
            prod!_A(x1) = x1 + 17
            nil!_A() = 14
            inter!_A(x1,x2) = x1 + x2 + 19
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = []
      pi(|#|) = []
      pi(*) = [1]
      pi(prod) = []
      pi(nil) = []
      pi(inter) = [2]

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) -> |#|()
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: -#(|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, r54, r55

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
          |0|_A(x1) = x1 + 4
          |1|_A(x1) = x1 + 4
          -_A(x1,x2) = x1
          |#|_A() = 6
          inter_A(x1,x2) = x1 + x2 + 10
          nil_A() = 11
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            -#_A(x1,x2) = 0
            |0|_A(x1) = x1 + 1
            |1|_A(x1) = x1 + 1
            -_A(x1,x2) = x1
            |#|_A() = 21
            inter_A(x1,x2) = x1 + 2
            nil_A() = 0
            -#!_A(x1,x2) = x1 + 4
            |0|!_A(x1) = 2
            |1|!_A(x1) = 6
            -!_A(x1,x2) = 7
            |#|!_A() = 4
            inter!_A(x1,x2) = x1 + x2 + 7
            nil!_A() = 1
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = [1]
      pi(|#|) = []
      pi(inter) = [1, 2]
      pi(nil) = []

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

  r54, r55

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 + 8
          false_A() = 4
          inter#_A(x1,x2) = x1 + x2 + 2
          cons_A(x1,x2) = x1 + x2 + 7
          mem_A(x1,x2) = x1 + x2 + 8
          true_A() = 3
          app_A(x1,x2) = x1 + x2 + 22
          inter_A(x1,x2) = x1 + x2 + 23
          nil_A() = 6
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            ifinter#_A(x1,x2,x3,x4) = x3 + x4
            false_A() = 3
            inter#_A(x1,x2) = x1 + x2
            cons_A(x1,x2) = x2 + 10
            mem_A(x1,x2) = 1
            true_A() = 3
            app_A(x1,x2) = x1 + x2 + 10
            inter_A(x1,x2) = x1 + x2 + 71
            nil_A() = 1
            ifinter#!_A(x1,x2,x3,x4) = x2 + x3 + x4 + 42
            false!_A() = 44
            inter#!_A(x1,x2) = 43
            cons!_A(x1,x2) = x1 + 86
            mem!_A(x1,x2) = x2 + 156
            true!_A() = 85
            app!_A(x1,x2) = x1 + 87
            inter!_A(x1,x2) = x1 + x2 + 147
            nil!_A() = 87
  
    partial status:
  
      pi(ifinter#) = [3, 4]
      pi(false) = []
      pi(inter#) = []
      pi(cons) = []
      pi(mem) = []
      pi(true) = []
      pi(app) = []
      pi(inter) = [2]
      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

  r19, r54, r55

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 + 39
          eq_A(x1,x2) = x1 + 21
          |#|_A() = 3
          true_A() = 1
          inter_A(x1,x2) = x1 + x2 + 41
          nil_A() = 34
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        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 + 1
            eq_A(x1,x2) = 3
            |#|_A() = 4
            true_A() = 3
            inter_A(x1,x2) = x1 + x2 + 1
            nil_A() = 1
            mem#!_A(x1,x2) = x2 + 28
            cons!_A(x1,x2) = x1 + x2 + 27
            eq!_A(x1,x2) = x1 + x2 + 5
            |#|!_A() = 17
            true!_A() = 0
            inter!_A(x1,x2) = x1 + x2 + 30
            nil!_A() = 18
  
    partial status:
  
      pi(mem#) = []
      pi(cons) = [1, 2]
      pi(eq) = [1]
      pi(|#|) = []
      pi(true) = []
      pi(inter) = [1, 2]
      pi(nil) = []

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

  r2, r55

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 + 31
          |0|_A(x1) = x1 + 30
          |1|_A(x1) = x1 + 15
          +_A(x1,x2) = x1 + 8
          |#|_A() = 5
          inter_A(x1,x2) = x1 + 37
          nil_A() = 36
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            eq#_A(x1,x2) = x1 + x2
            |0|_A(x1) = x1 + 41
            |1|_A(x1) = x1 + 40
            +_A(x1,x2) = x1 + x2 + 26
            |#|_A() = 13
            inter_A(x1,x2) = x1 + 1
            nil_A() = 2
            eq#!_A(x1,x2) = x1 + x2 + 6
            |0|!_A(x1) = x1 + 5
            |1|!_A(x1) = 4
            +!_A(x1,x2) = x1 + x2 + 19
            |#|!_A() = 3
            inter!_A(x1,x2) = x1 + x2 + 20
            nil!_A() = 20
  
    partial status:
  
      pi(eq#) = [1]
      pi(|0|) = []
      pi(|1|) = []
      pi(+) = []
      pi(|#|) = []
      pi(inter) = [1]
      pi(nil) = []

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

  r1, r45, r55

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 + 13
          |#|_A() = 1
          |0|_A(x1) = x1 + 12
          app_A(x1,x2) = x1 + x2 + 13
          cons_A(x1,x2) = x1 + 14
          inter_A(x1,x2) = x1 + x2 + 16
          nil_A() = 6
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            eq#_A(x1,x2) = x2
            |#|_A() = 72
            |0|_A(x1) = x1 + 20
            app_A(x1,x2) = x1 + x2 + 4
            cons_A(x1,x2) = x1 + 1
            inter_A(x1,x2) = x1 + 3
            nil_A() = 6
            eq#!_A(x1,x2) = x2 + 70
            |#|!_A() = 71
            |0|!_A(x1) = 46
            app!_A(x1,x2) = x1 + x2 + 90
            cons!_A(x1,x2) = 49
            inter!_A(x1,x2) = x1 + x2 + 91
            nil!_A() = 71
  
    partial status:
  
      pi(eq#) = []
      pi(|#|) = []
      pi(|0|) = []
      pi(app) = [1, 2]
      pi(cons) = [1]
      pi(inter) = [2]
      pi(nil) = []

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

  r55

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 + 8
          |0|_A(x1) = x1 + 10
          |#|_A() = 3
          inter_A(x1,x2) = x1 + x2 + 3
          nil_A() = 14
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            eq#_A(x1,x2) = x1
            |0|_A(x1) = x1 + 11
            |#|_A() = 15
            inter_A(x1,x2) = x1 + 4
            nil_A() = 10
            eq#!_A(x1,x2) = 17
            |0|!_A(x1) = 24
            |#|!_A() = 16
            inter!_A(x1,x2) = x1 + x2 + 25
            nil!_A() = 15
  
    partial status:
  
      pi(eq#) = [1, 2]
      pi(|0|) = [1]
      pi(|#|) = []
      pi(inter) = []
      pi(nil) = []

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

  r54, r55

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
          |0|_A(x1) = x1 + 19
          |1|_A(x1) = x1 + 26
          inter_A(x1,x2) = x1 + x2 + 46
          nil_A() = 21
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            ge#_A(x1,x2) = x1 + x2
            |0|_A(x1) = x1 + 15
            |1|_A(x1) = x1 + 6
            inter_A(x1,x2) = x1 + x2 + 15
            nil_A() = 28
            ge#!_A(x1,x2) = x1 + x2 + 8
            |0|!_A(x1) = x1 + 7
            |1|!_A(x1) = 28
            inter!_A(x1,x2) = x1 + x2 + 30
            nil!_A() = 32
  
    partial status:
  
      pi(ge#) = [2]
      pi(|0|) = []
      pi(|1|) = []
      pi(inter) = []
      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

  r55

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 + 8
          |#|_A() = 7
          |0|_A(x1) = x1 + 18
          inter_A(x1,x2) = x1 + x2 + 27
          nil_A() = 24
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        matrix interpretation with standard point-wise order:
        
          carrier: N^1
          order: standard order
          interpretations:
            ge#_A(x1,x2) = x2
            |#|_A() = 7
            |0|_A(x1) = x1 + 24
            inter_A(x1,x2) = x1 + 1
            nil_A() = 2
            ge#!_A(x1,x2) = x2
            |#|!_A() = 14
            |0|!_A(x1) = x1 + 13
            inter!_A(x1,x2) = x1 + x2 + 25
            nil!_A() = 25
  
    partial status:
  
      pi(ge#) = []
      pi(|#|) = []
      pi(|0|) = []
      pi(inter) = [2]
      pi(nil) = []

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

  r16, r32, r54, r55

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 + 8
          not_A(x1) = x1 + 5
          false_A() = 10
          true_A() = 6
          ge_A(x1,x2) = x2 + 12
          |#|_A() = 11
          inter_A(x1,x2) = x1 + x2 + 11
          nil_A() = 43
  
    base order 2:
  
      marked-algebra reduction triple (>=A, >=A!, >A!):
      
        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 + 1
            not_A(x1) = 3
            false_A() = 4
            true_A() = 2
            ge_A(x1,x2) = 2
            |#|_A() = 12
            inter_A(x1,x2) = x1 + x2 + 1
            nil_A() = 1
            app#!_A(x1,x2) = x1
            cons!_A(x1,x2) = x1 + x2 + 24
            not!_A(x1) = 11
            false!_A() = 7
            true!_A() = 11
            ge!_A(x1,x2) = 11
            |#|!_A() = 9
            inter!_A(x1,x2) = x1 + x2 + 22
            nil!_A() = 22
  
    partial status:
  
      pi(app#) = []
      pi(cons) = [1]
      pi(not) = [1]
      pi(false) = []
      pi(true) = []
      pi(ge) = [2]
      pi(|#|) = []
      pi(inter) = []
      pi(nil) = []

The following rules are removed:

  p1

Then no dependency pair remains.