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

  r36

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            sum#_A(x1) = 0
            app_A(x1,x2) = max{6, x2 - 59}
            cons_A(x1,x2) = max{8, x1 - 4}
            |log'|_A(x1) = max{507, x1 - 790}
            |#|_A = 27
            sum#!_A(x1) = 1
            app!_A(x1,x2) = x1 + 4
            cons!_A(x1,x2) = max{149, x1 + 14, x2 + 58}
            |log'|!_A(x1) = x1 + 275
            |#|!_A = 146
        
        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) = 0
              app_A(x1,x2) = x1 + x2 + 1
              cons_A(x1,x2) = x1 + x2 + 1
              |log'|_A(x1) = x1 + 1
              |#|_A() = 10
              sum#!_A(x1) = x1 + 45
              app!_A(x1,x2) = 44
              cons!_A(x1,x2) = x1 + x2 + 46
              |log'|!_A(x1) = x1 + 22
              |#|!_A() = 33
        
  
    partial status:
  
      pi(sum#) = [1]
      pi(app) = [1, 2]
      pi(cons) = [2]
      pi(|log'|) = [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

  r15, r39

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            prod#_A(x1) = 0
            app_A(x1,x2) = 6
            cons_A(x1,x2) = x1 + 5
            not_A(x1) = 407
            true_A = 0
            false_A = 407
            *_A(x1,x2) = max{x1 + 107, x2 + 5}
            |#|_A = 407
            prod#!_A(x1) = 395
            app!_A(x1,x2) = x2 + 2
            cons!_A(x1,x2) = max{394, x2 + 5}
            not!_A(x1) = 7
            true!_A = 4
            false!_A = 7
            *!_A(x1,x2) = max{401, x1 - 4}
            |#|!_A = 392
        
        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) = 0
              app_A(x1,x2) = 20
              cons_A(x1,x2) = x1 + x2 + 8
              not_A(x1) = 2
              true_A() = 3
              false_A() = 2
              *_A(x1,x2) = x1 + 20
              |#|_A() = 2
              prod#!_A(x1) = 44
              app!_A(x1,x2) = 67
              cons!_A(x1,x2) = x2 + 43
              not!_A(x1) = 12
              true!_A() = 8
              false!_A() = 10
              *!_A(x1,x2) = x2 + 30
              |#|!_A() = 29
        
  
    partial status:
  
      pi(prod#) = [1]
      pi(app) = [1, 2]
      pi(cons) = [2]
      pi(not) = []
      pi(true) = []
      pi(false) = []
      pi(*) = [1]
      pi(|#|) = []

The following rules are removed:

  p2, p3



-- SCC decomposition.

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

p1: prod#(app(l1,l2)) -> prod#(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:

  {p1}


-- Reduction pair.

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

p1: prod#(app(l1,l2)) -> prod#(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:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            prod#_A(x1) = 0
            app_A(x1,x2) = max{x1 + 193, x2 - 1}
            prod#!_A(x1) = x1 + 1
            app!_A(x1,x2) = max{188, x1 + 186, x2 + 1}
        
        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) = 0
              app_A(x1,x2) = 1
              prod#!_A(x1) = 0
              app!_A(x1,x2) = 25
        
  
    partial status:
  
      pi(prod#) = [1]
      pi(app) = [1, 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: *#(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, r54, r55

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            *#_A(x1,x2) = max{0, x1 - 38}
            +_A(x1,x2) = max{51, x1 + 31, x2 + 31}
            *_A(x1,x2) = max{37, x1 + 31, x2 + 31}
            |1|_A(x1) = max{32, x1 + 30}
            |0|_A(x1) = max{22, x1 + 13}
            |#|_A = 0
            inter_A(x1,x2) = x1 + 351
            nil_A = 178
            *#!_A(x1,x2) = max{7, x1 - 14}
            +!_A(x1,x2) = max{0, x1 - 51, x2 - 283}
            *!_A(x1,x2) = max{6, x1 - 21}
            |1|!_A(x1) = 0
            |0|!_A(x1) = 0
            |#|!_A = 5
            inter!_A(x1,x2) = max{75, x1 - 173, x2 + 5}
            nil!_A = 4
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              *#_A(x1,x2) = x1
              +_A(x1,x2) = x1 + x2 + 4
              *_A(x1,x2) = x1 + x2 + 5
              |1|_A(x1) = x1 + 2
              |0|_A(x1) = x1 + 18
              |#|_A() = 15
              inter_A(x1,x2) = x1 + x2 + 1
              nil_A() = 5
              *#!_A(x1,x2) = x1 + 36
              +!_A(x1,x2) = x1 + 22
              *!_A(x1,x2) = x1 + 26
              |1|!_A(x1) = 25
              |0|!_A(x1) = 35
              |#|!_A() = 32
              inter!_A(x1,x2) = 14
              nil!_A() = 24
        
  
    partial status:
  
      pi(*#) = []
      pi(+) = [1, 2]
      pi(*) = [1, 2]
      pi(|1|) = []
      pi(|0|) = []
      pi(|#|) = []
      pi(inter) = []
      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, r3

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            *#_A(x1,x2) = max{0, x2 - 2}
            +_A(x1,x2) = max{44, x1, x2 + 1}
            |#|_A = 53
            *#!_A(x1,x2) = x1 + 299
            +!_A(x1,x2) = max{297, x1 - 43, x2 - 4}
            |#|!_A = 0
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              *#_A(x1,x2) = x2
              +_A(x1,x2) = x1 + x2 + 34
              |#|_A() = 57
              *#!_A(x1,x2) = x2
              +!_A(x1,x2) = x2 + 14
              |#|!_A() = 8
        
  
    partial status:
  
      pi(*#) = [2]
      pi(+) = [1, 2]
      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: |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

  r36, r39

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            |log'|#_A(x1) = 0
            |0|_A(x1) = max{151, x1}
            |1|_A(x1) = 156
            |log'|_A(x1) = max{160, x1 + 7}
            |#|_A = 156
            *_A(x1,x2) = max{x1 + 9, x2 + 150}
            |log'|#!_A(x1) = 140
            |0|!_A(x1) = x1 + 11
            |1|!_A(x1) = 139
            |log'|!_A(x1) = max{0, x1 - 157}
            |#|!_A = 129
            *!_A(x1,x2) = max{9, x2 - 8}
        
        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 + 13
              |1|_A(x1) = x1 + 1
              |log'|_A(x1) = 3
              |#|_A() = 3
              *_A(x1,x2) = x2 + 5
              |log'|#!_A(x1) = x1
              |0|!_A(x1) = 15
              |1|!_A(x1) = x1 + 8
              |log'|!_A(x1) = 12
              |#|!_A() = 2
              *!_A(x1,x2) = x1
        
  
    partial status:
  
      pi(|log'|#) = [1]
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|log'|) = [1]
      pi(|#|) = []
      pi(*) = [1, 2]

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = 0
            |0|_A(x1) = max{7, x1}
            +_A(x1,x2) = max{9, x1, x2}
            |1|_A(x1) = max{18, x1}
            |#|_A = 18
            |log'|_A(x1) = x1 + 18
            inter_A(x1,x2) = x1 + 52
            nil_A = 8
            +#!_A(x1,x2) = max{8, x1 + 1, x2 + 1}
            |0|!_A(x1) = 11
            +!_A(x1,x2) = max{10, x1 - 6}
            |1|!_A(x1) = 19
            |#|!_A = 9
            |log'|!_A(x1) = 19
            inter!_A(x1,x2) = 21
            nil!_A = 20
        
        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 + 9
              +_A(x1,x2) = x1 + x2 + 2
              |1|_A(x1) = x1 + 17
              |#|_A() = 6
              |log'|_A(x1) = x1 + 1
              inter_A(x1,x2) = x2 + 2
              nil_A() = 0
              +#!_A(x1,x2) = x1 + x2
              |0|!_A(x1) = 64
              +!_A(x1,x2) = 65
              |1|!_A(x1) = 34
              |#|!_A() = 49
              |log'|!_A(x1) = 34
              inter!_A(x1,x2) = x1 + 49
              nil!_A() = 64
        
  
    partial status:
  
      pi(+#) = []
      pi(|0|) = []
      pi(+) = [1, 2]
      pi(|1|) = []
      pi(|#|) = []
      pi(|log'|) = [1]
      pi(inter) = [1]
      pi(nil) = []

The following rules are removed:

  p1, p2, p4, p5, p6, p7



-- SCC decomposition.

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

p1: +#(+(x,y),z) -> +#(x,+(y,z))

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(+(x,y),z) -> +(x,+(y,z))
r9: -(|#|(),x) -> |#|()
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,+(y,z))

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(+(x,y),z) -> +(x,+(y,z))
r9: -(|#|(),x) -> |#|()
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, r3, r54

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = max{0, x1 - 18}
            +_A(x1,x2) = max{17, x1, x2}
            |0|_A(x1) = max{7, x1}
            |#|_A = 33
            inter_A(x1,x2) = max{705, x2 - 242}
            nil_A = 1
            +#!_A(x1,x2) = max{573, x1 + 1}
            +!_A(x1,x2) = max{579, x1 + 563, x2 + 572}
            |0|!_A(x1) = 574
            |#|!_A = 1139
            inter!_A(x1,x2) = max{1137, x2 + 188}
            nil!_A = 572
        
        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) = x2 + 9
              |0|_A(x1) = 11
              |#|_A() = 3
              inter_A(x1,x2) = x2 + 1
              nil_A() = 2
              +#!_A(x1,x2) = x1 + 7
              +!_A(x1,x2) = x2 + 6
              |0|!_A(x1) = 7
              |#|!_A() = 3
              inter!_A(x1,x2) = x1 + x2 + 12
              nil!_A() = 12
        
  
    partial status:
  
      pi(+#) = [1]
      pi(+) = [1, 2]
      pi(|0|) = [1]
      pi(|#|) = []
      pi(inter) = [1]
      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: -#(|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

  r36, r39, r49

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{0, x2 - 147}
            |0|_A(x1) = max{17, x1 + 2}
            |1|_A(x1) = x1 + 146
            -_A(x1,x2) = max{43, x1 - 44, x2 - 110}
            |#|_A = 0
            |log'|_A(x1) = max{28, x1 - 598}
            *_A(x1,x2) = max{144, x2 + 114}
            prod_A(x1) = 147
            nil_A = 135
            -#!_A(x1,x2) = max{127, x2 - 18}
            |0|!_A(x1) = 131
            |1|!_A(x1) = max{126, x1 + 89}
            -!_A(x1,x2) = max{52, x2 - 58}
            |#|!_A = 54
            |log'|!_A(x1) = 131
            *!_A(x1,x2) = 0
            prod!_A(x1) = x1 + 148
            nil!_A = 132
        
        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) = 27
              |1|_A(x1) = 0
              -_A(x1,x2) = x2 + 31
              |#|_A() = 17
              |log'|_A(x1) = 17
              *_A(x1,x2) = 17
              prod_A(x1) = x1 + 15
              nil_A() = 21
              -#!_A(x1,x2) = 29
              |0|!_A(x1) = x1 + 30
              |1|!_A(x1) = 28
              -!_A(x1,x2) = x1
              |#|!_A() = 16
              |log'|!_A(x1) = 24
              *!_A(x1,x2) = x2 + 15
              prod!_A(x1) = x1 + 28
              nil!_A() = 48
        
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(-) = []
      pi(|#|) = []
      pi(|log'|) = [1]
      pi(*) = [1]
      pi(prod) = []
      pi(nil) = []

The following rules are removed:

  p2, p4



-- SCC decomposition.

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

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


-- Reduction pair.

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

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

  r54, r55

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{0, x1 - 43, x2 - 43}
            |0|_A(x1) = x1 + 42
            |1|_A(x1) = x1 + 11
            inter_A(x1,x2) = max{574, x2 - 250}
            nil_A = 128
            -#!_A(x1,x2) = max{37, x1 - 5}
            |0|!_A(x1) = max{39, x1 - 56}
            |1|!_A(x1) = max{39, x1 - 4}
            inter!_A(x1,x2) = max{x1 + 248, x2 + 631}
            nil!_A = 247
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              -#_A(x1,x2) = x1 + x2
              |0|_A(x1) = x1 + 3
              |1|_A(x1) = x1 + 11
              inter_A(x1,x2) = x2 + 1
              nil_A() = 0
              -#!_A(x1,x2) = 5
              |0|!_A(x1) = 4
              |1|!_A(x1) = 9
              inter!_A(x1,x2) = x2 + 16
              nil!_A() = 17
        
  
    partial status:
  
      pi(-#) = [2]
      pi(|0|) = [1]
      pi(|1|) = [1]
      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: -#(|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, r19, r21, r23, r26, r39

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{x1 + 1, x2 - 259}
            |0|_A(x1) = max{259, x1 + 29}
            |1|_A(x1) = max{259, x1 + 29}
            -_A(x1,x2) = max{1, x1}
            |#|_A = 34
            eq_A(x1,x2) = max{0, x1 - 28, x2 - 260}
            true_A = 2
            false_A = 7
            *_A(x1,x2) = max{64, x1 - 68}
            -#!_A(x1,x2) = max{257, x1 - 2}
            |0|!_A(x1) = 377
            |1|!_A(x1) = 377
            -!_A(x1,x2) = max{378, x2 + 350}
            |#|!_A = 330
            eq!_A(x1,x2) = max{439, x1 - 260, x2 + 70}
            true!_A = 439
            false!_A = 10
            *!_A(x1,x2) = max{x1 + 69, x2 + 377}
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              -#_A(x1,x2) = x1 + x2
              |0|_A(x1) = x1 + 15
              |1|_A(x1) = x1 + 15
              -_A(x1,x2) = x1
              |#|_A() = 8
              eq_A(x1,x2) = 3
              true_A() = 3
              false_A() = 3
              *_A(x1,x2) = 11
              -#!_A(x1,x2) = x1 + 24
              |0|!_A(x1) = 24
              |1|!_A(x1) = 24
              -!_A(x1,x2) = x1 + 23
              |#|!_A() = 30
              eq!_A(x1,x2) = 31
              true!_A() = 29
              false!_A() = 28
              *!_A(x1,x2) = 25
        
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = [1, 2]
      pi(|#|) = []
      pi(eq) = [2]
      pi(true) = []
      pi(false) = []
      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: 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

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

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ifinter#_A(x1,x2,x3,x4) = max{1, x1 - 173, x2 - 4, x3 - 142, x4 - 142}
            false_A = 172
            inter#_A(x1,x2) = max{1, x1 - 142, x2 - 142}
            cons_A(x1,x2) = max{141, x1 + 138, x2 + 140}
            mem_A(x1,x2) = max{174, x1 + 167, x2 - 141}
            true_A = 172
            app_A(x1,x2) = max{678, x1 + 140, x2 + 136}
            not_A(x1) = max{1051, x1 - 1051}
            if_A(x1,x2,x3) = max{174, x1 - 1051, x2, x3}
            eq_A(x1,x2) = 1048
            |#|_A = 1569
            |1|_A(x1) = max{180, x1 + 177}
            |0|_A(x1) = max{175, x1 - 1048}
            ge_A(x1,x2) = max{1050, x1 - 2615, x2 - 1570}
            nil_A = 142
            ifinter#!_A(x1,x2,x3,x4) = max{x1 - 168, x3 + 138, x4 - 1}
            false!_A = 0
            inter#!_A(x1,x2) = max{x1 + 7, x2 - 1}
            cons!_A(x1,x2) = max{x1 + 409, x2 + 137}
            mem!_A(x1,x2) = max{x1 + 1048, x2 + 137}
            true!_A = 273
            app!_A(x1,x2) = max{x1 + 533, x2 + 272}
            not!_A(x1) = 2098
            if!_A(x1,x2,x3) = max{279, x1 - 1049, x2 - 524}
            eq!_A(x1,x2) = 274
            |#|!_A = 531
            |1|!_A(x1) = max{2097, x1 + 527}
            |0|!_A(x1) = 0
            ge!_A(x1,x2) = 0
            nil!_A = 2098
        
        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) = 0
              false_A() = 1
              inter#_A(x1,x2) = 0
              cons_A(x1,x2) = x2 + 3
              mem_A(x1,x2) = 1
              true_A() = 0
              app_A(x1,x2) = x1 + x2 + 1
              not_A(x1) = 26
              if_A(x1,x2,x3) = x2 + x3
              eq_A(x1,x2) = x1 + 1
              |#|_A() = 15
              |1|_A(x1) = x1 + 33
              |0|_A(x1) = x1 + 96
              ge_A(x1,x2) = 25
              nil_A() = 109
              ifinter#!_A(x1,x2,x3,x4) = x1 + x3 + x4 + 5
              false!_A() = 3
              inter#!_A(x1,x2) = x1 + x2 + 4
              cons!_A(x1,x2) = 7
              mem!_A(x1,x2) = x1 + x2 + 10
              true!_A() = 14
              app!_A(x1,x2) = 98
              not!_A(x1) = 49
              if!_A(x1,x2,x3) = x1 + x3 + 10
              eq!_A(x1,x2) = x2 + 32
              |#|!_A() = 97
              |1|!_A(x1) = x1 + 99
              |0|!_A(x1) = 48
              ge!_A(x1,x2) = x2
              nil!_A() = 98
        
  
    partial status:
  
      pi(ifinter#) = []
      pi(false) = []
      pi(inter#) = []
      pi(cons) = [2]
      pi(mem) = [2]
      pi(true) = []
      pi(app) = [1, 2]
      pi(not) = [1]
      pi(if) = [2, 3]
      pi(eq) = []
      pi(|#|) = []
      pi(|1|) = [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

  r49, r54

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            mem#_A(x1,x2) = 0
            cons_A(x1,x2) = max{185, x1 - 327, x2 - 164}
            prod_A(x1) = x1 + 335
            nil_A = 184
            |1|_A(x1) = max{38, x1 - 342}
            |#|_A = 32
            inter_A(x1,x2) = max{183, x1 - 331, x2 + 17}
            mem#!_A(x1,x2) = x2 + 329
            cons!_A(x1,x2) = max{346, x1 - 2, x2 + 330}
            prod!_A(x1) = max{665, x1 + 333}
            nil!_A = 343
            |1|!_A(x1) = 310
            |#|!_A = 1
            inter!_A(x1,x2) = x2 + 344
        
        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
              prod_A(x1) = x1 + 1
              nil_A() = 31
              |1|_A(x1) = 18
              |#|_A() = 14
              inter_A(x1,x2) = x1 + x2 + 1
              mem#!_A(x1,x2) = 0
              cons!_A(x1,x2) = x1 + 18
              prod!_A(x1) = x1 + 19
              nil!_A() = 51
              |1|!_A(x1) = x1 + 16
              |#|!_A() = 15
              inter!_A(x1,x2) = x1 + 11
        
  
    partial status:
  
      pi(mem#) = [2]
      pi(cons) = [1, 2]
      pi(prod) = []
      pi(nil) = []
      pi(|1|) = []
      pi(|#|) = []
      pi(inter) = [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: 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

  r54, r55

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = max{0, x1 - 14, x2 - 14}
            |0|_A(x1) = max{14, x1}
            |1|_A(x1) = max{291, x1 + 13}
            inter_A(x1,x2) = max{722, x2 - 292}
            nil_A = 11
            eq#!_A(x1,x2) = max{669, x1 + 378}
            |0|!_A(x1) = x1 + 378
            |1|!_A(x1) = x1 + 542
            inter!_A(x1,x2) = 715
            nil!_A = 714
        
        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 + 2
              |1|_A(x1) = x1 + 2
              inter_A(x1,x2) = x1 + x2 + 1
              nil_A() = 1
              eq#!_A(x1,x2) = x2 + 3
              |0|!_A(x1) = 14
              |1|!_A(x1) = x1 + 4
              inter!_A(x1,x2) = x1 + 16
              nil!_A() = 15
        
  
    partial status:
  
      pi(eq#) = []
      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: 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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = max{0, x2 - 1}
            |#|_A = 114
            |0|_A(x1) = max{107, x1}
            eq#!_A(x1,x2) = max{0, x1 - 115}
            |#|!_A = 5
            |0|!_A(x1) = max{423, x1 + 49}
        
        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() = 30
              |0|_A(x1) = x1 + 35
              eq#!_A(x1,x2) = 0
              |#|!_A() = 1
              |0|!_A(x1) = x1 + 20
        
  
    partial status:
  
      pi(eq#) = [2]
      pi(|#|) = []
      pi(|0|) = [1]

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

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

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

  (no rules)

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = max{0, x1 - 11}
            |0|_A(x1) = max{80, x1 + 10}
            |#|_A = 0
            eq#!_A(x1,x2) = max{357, x1 - 81, x2 - 72}
            |0|!_A(x1) = max{356, x1 + 180}
            |#|!_A = 289
        
        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 + 17
              |#|_A() = 11
              eq#!_A(x1,x2) = 30
              |0|!_A(x1) = x1 + 21
              |#|!_A() = 29
        
  
    partial status:
  
      pi(eq#) = [1]
      pi(|0|) = [1]
      pi(|#|) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

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

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

  r55

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = max{0, x1 - 120, x2 - 239}
            |0|_A(x1) = x1 + 89
            |1|_A(x1) = x1 + 119
            inter_A(x1,x2) = max{x1 + 76, x2 + 76}
            nil_A = 2
            ge#!_A(x1,x2) = max{31, x1 - 1, x2 - 1}
            |0|!_A(x1) = x1 + 452
            |1|!_A(x1) = 7
            inter!_A(x1,x2) = 2
            nil!_A = 3
        
        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 + 12
              |1|_A(x1) = x1 + 11
              inter_A(x1,x2) = x1 + x2 + 1
              nil_A() = 0
              ge#!_A(x1,x2) = x2 + 7
              |0|!_A(x1) = 22
              |1|!_A(x1) = 8
              inter!_A(x1,x2) = x1 + 1
              nil!_A() = 2
        
  
    partial status:
  
      pi(ge#) = []
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(inter) = [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, r54, r55

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = max{0, x2 - 1}
            |#|_A = 80
            |0|_A(x1) = x1 + 162
            -_A(x1,x2) = max{165, x2 - 205}
            inter_A(x1,x2) = max{62, x1 - 296, x2 - 296}
            nil_A = 0
            ge#!_A(x1,x2) = max{69, x1 - 81}
            |#|!_A = 70
            |0|!_A(x1) = max{156, x1 - 212}
            -!_A(x1,x2) = max{76, x1 - 46, x2 - 5}
            inter!_A(x1,x2) = 72
            nil!_A = 71
        
        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() = 3
              |0|_A(x1) = x1 + 7
              -_A(x1,x2) = x2 + 8
              inter_A(x1,x2) = x1 + x2 + 1
              nil_A() = 16
              ge#!_A(x1,x2) = x2 + 15
              |#|!_A() = 14
              |0|!_A(x1) = x1 + 6
              -!_A(x1,x2) = 13
              inter!_A(x1,x2) = 4
              nil!_A() = 15
        
  
    partial status:
  
      pi(ge#) = []
      pi(|#|) = []
      pi(|0|) = [1]
      pi(-) = [1, 2]
      pi(inter) = [1]
      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

  r49

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            app#_A(x1,x2) = max{0, x1 - 3}
            cons_A(x1,x2) = max{x1, x2 + 2}
            prod_A(x1) = max{442, x1 - 349}
            nil_A = 451
            |1|_A(x1) = max{23, x1 - 174}
            |#|_A = 13
            app#!_A(x1,x2) = max{x1 - 1, x2 + 447}
            cons!_A(x1,x2) = 445
            prod!_A(x1) = 442
            nil!_A = 447
            |1|!_A(x1) = max{440, x1 + 426}
            |#|!_A = 441
        
        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 + 5
              prod_A(x1) = x1 + 1
              nil_A() = 96
              |1|_A(x1) = 58
              |#|_A() = 12
              app#!_A(x1,x2) = x1 + 29
              cons!_A(x1,x2) = x2 + 28
              prod!_A(x1) = 12
              nil!_A() = 116
              |1|!_A(x1) = x1 + 101
              |#|!_A() = 11
        
  
    partial status:
  
      pi(app#) = [1]
      pi(cons) = [2]
      pi(prod) = [1]
      pi(nil) = []
      pi(|1|) = [1]
      pi(|#|) = []

The following rules are removed:

  p1

Then no dependency pair remains.