YES
We show the termination of the TRS R:

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


-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  r54

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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              sum#_A(x1) = 0
              app_A(x1,x2) = 5
              cons_A(x1,x2) = x1 + x2 + 6
              inter_A(x1,x2) = x1 + x2 + 1
              nil_A() = 20
              sum#!_A(x1) = 12
              app!_A(x1,x2) = x1 + 13
              cons!_A(x1,x2) = 11
              inter!_A(x1,x2) = x2
              nil!_A() = 5
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            sum#_A(x1) = x1
            app_A(x1,x2) = max{406, x1 + 3, x2 + 101}
            cons_A(x1,x2) = max{x1 - 4, x2 + 407}
            inter_A(x1,x2) = max{204, x1 - 712, x2 - 101}
            nil_A = 0
            sum#!_A(x1) = max{6, x1 - 202}
            app!_A(x1,x2) = max{8, x1 - 100, x2 - 102}
            cons!_A(x1,x2) = max{5, x1 + 2}
            inter!_A(x1,x2) = max{0, x1 - 407}
            nil!_A = 5
        
  
    partial status:
  
      pi(sum#) = []
      pi(app) = [1]
      pi(cons) = [1]
      pi(inter) = []
      pi(nil) = []

The following rules are removed:

  p1, p2, p3

Then no dependency pair remains.

-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  (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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              prod#_A(x1) = x1
              app_A(x1,x2) = x1 + x2 + 18
              cons_A(x1,x2) = x1 + x2 + 1
              prod#!_A(x1) = x1 + 2
              app!_A(x1,x2) = x1 + 1
              cons!_A(x1,x2) = x1 + 3
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            prod#_A(x1) = 0
            app_A(x1,x2) = max{297, x1 - 296}
            cons_A(x1,x2) = max{4, x1 - 296, x2 - 296}
            prod#!_A(x1) = max{302, x1 - 298}
            app!_A(x1,x2) = max{301, x1 + 297, x2 + 7}
            cons!_A(x1,x2) = 0
        
  
    partial status:
  
      pi(prod#) = []
      pi(app) = [1]
      pi(cons) = [1]

The following rules are removed:

  p1, p2, p3

Then no dependency pair remains.

-- Reduction pair.

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

p1: *#(x,+(y,z)) -> *#(x,z)
p2: *#(x,+(y,z)) -> *#(x,y)
p3: *#(*(x,y),z) -> *#(y,z)
p4: *#(*(x,y),z) -> *#(x,*(y,z))
p5: *#(|1|(x),y) -> *#(x,y)
p6: *#(|0|(x),y) -> *#(x,y)

and R consists of:

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

The set of usable rules consists of

  r2, r3, r39

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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              *#_A(x1,x2) = x1
              +_A(x1,x2) = x1 + x2 + 15
              *_A(x1,x2) = x1 + x2 + 20
              |1|_A(x1) = x1 + 14
              |0|_A(x1) = x1 + 19
              |#|_A() = 16
              *#!_A(x1,x2) = x1
              +!_A(x1,x2) = x1 + 1
              *!_A(x1,x2) = x2 + 31
              |1|!_A(x1) = x1 + 17
              |0|!_A(x1) = x1 + 12
              |#|!_A() = 30
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            *#_A(x1,x2) = 0
            +_A(x1,x2) = max{259, x1 + 17, x2 + 17}
            *_A(x1,x2) = max{260, x2 + 17}
            |1|_A(x1) = max{239, x1 + 17}
            |0|_A(x1) = max{64, x1 + 17}
            |#|_A = 221
            *#!_A(x1,x2) = x1 + 709
            +!_A(x1,x2) = max{707, x1 - 278}
            *!_A(x1,x2) = max{74, x1 + 10}
            |1|!_A(x1) = max{707, x1 + 267}
            |0|!_A(x1) = max{75, x1 + 9}
            |#|!_A = 174
        
  
    partial status:
  
      pi(*#) = []
      pi(+) = [1, 2]
      pi(*) = [2]
      pi(|1|) = []
      pi(|0|) = []
      pi(|#|) = []

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

  r19, 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              *#_A(x1,x2) = x2
              +_A(x1,x2) = x1 + x2 + 7
              eq_A(x1,x2) = 3
              |#|_A() = 2
              true_A() = 3
              *_A(x1,x2) = x1
              *#!_A(x1,x2) = x2 + 1
              +!_A(x1,x2) = x1
              eq!_A(x1,x2) = 7
              |#|!_A() = 6
              true!_A() = 4
              *!_A(x1,x2) = x1 + 5
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            *#_A(x1,x2) = 0
            +_A(x1,x2) = max{476, x1 - 512, x2 - 512}
            eq_A(x1,x2) = max{2, x1 - 319, x2 - 319}
            |#|_A = 0
            true_A = 2
            *_A(x1,x2) = max{394, x1 - 512}
            *#!_A(x1,x2) = max{503, x1 - 1}
            +!_A(x1,x2) = max{502, x1 - 34, x2 - 124}
            eq!_A(x1,x2) = max{506, x2 - 1}
            |#|!_A = 28
            true!_A = 1
            *!_A(x1,x2) = max{421, x1 + 104, x2 + 27}
        
  
    partial status:
  
      pi(*#) = []
      pi(+) = []
      pi(eq) = []
      pi(|#|) = []
      pi(true) = []
      pi(*) = [1]

The following rules are removed:

  p1, p2

Then no dependency pair remains.

-- Reduction pair.

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

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

  r9

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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              |log'|#_A(x1) = 0
              |0|_A(x1) = 13
              |1|_A(x1) = 7
              -_A(x1,x2) = 6
              |#|_A() = 2
              |log'|#!_A(x1) = 9
              |0|!_A(x1) = x1 + 9
              |1|!_A(x1) = x1 + 5
              -!_A(x1,x2) = x2 + 3
              |#|!_A() = 2
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            |log'|#_A(x1) = x1
            |0|_A(x1) = max{141, x1}
            |1|_A(x1) = x1 + 26
            -_A(x1,x2) = max{44, x2 - 71}
            |#|_A = 26
            |log'|#!_A(x1) = x1 + 17
            |0|!_A(x1) = x1 + 8
            |1|!_A(x1) = max{51, x1 + 18}
            -!_A(x1,x2) = max{204, x1 + 63, x2 - 62}
            |#|!_A = 47
        
  
    partial status:
  
      pi(|log'|#) = []
      pi(|0|) = []
      pi(|1|) = [1]
      pi(-) = [1]
      pi(|#|) = []

The following rules are removed:

  p2



-- SCC decomposition.

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

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

  {p1}


-- Reduction pair.

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

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

  (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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              |log'|#_A(x1) = 0
              |0|_A(x1) = 14
              |log'|#!_A(x1) = 35
              |0|!_A(x1) = 34
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            |log'|#_A(x1) = 0
            |0|_A(x1) = 1056
            |log'|#!_A(x1) = 619
            |0|!_A(x1) = max{618, x1 - 2}
        
  
    partial status:
  
      pi(|log'|#) = [1]
      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: +#(|0|(x),|0|(y)) -> +#(x,y)
p2: +#(+(x,y),z) -> +#(y,z)
p3: +#(+(x,y),z) -> +#(x,+(y,z))
p4: +#(|1|(x),|1|(y)) -> +#(x,y)
p5: +#(|1|(x),|1|(y)) -> +#(+(x,y),|1|(|#|()))
p6: +#(|0|(x),|1|(y)) -> +#(x,y)
p7: +#(|1|(x),|0|(y)) -> +#(x,y)

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              +#_A(x1,x2) = 0
              |0|_A(x1) = x1 + 4
              +_A(x1,x2) = x1 + x2 + 3
              |1|_A(x1) = x1 + 10
              |#|_A() = 3
              +#!_A(x1,x2) = x1 + x2
              |0|!_A(x1) = 17
              +!_A(x1,x2) = 16
              |1|!_A(x1) = 19
              |#|!_A() = 7
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = 0
            |0|_A(x1) = 1229
            +_A(x1,x2) = max{1121, x1 + 216, x2}
            |1|_A(x1) = 1119
            |#|_A = 1225
            +#!_A(x1,x2) = 4133
            |0|!_A(x1) = 1
            +!_A(x1,x2) = max{438, x1 + 432, x2 + 2}
            |1|!_A(x1) = 4132
            |#|!_A = 1333
        
  
    partial status:
  
      pi(+#) = []
      pi(|0|) = []
      pi(+) = [1, 2]
      pi(|1|) = []
      pi(|#|) = []

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

  r2, r5, r6, r12, r19, 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              +#_A(x1,x2) = x1
              +_A(x1,x2) = x1 + x2
              |#|_A() = 2
              |0|_A(x1) = 10
              |1|_A(x1) = 13
              -_A(x1,x2) = x2 + 1
              eq_A(x1,x2) = 3
              true_A() = 3
              *_A(x1,x2) = 9
              +#!_A(x1,x2) = x1 + 23
              +!_A(x1,x2) = 22
              |#|!_A() = 21
              |0|!_A(x1) = 25
              |1|!_A(x1) = 23
              -!_A(x1,x2) = x1 + x2
              eq!_A(x1,x2) = 24
              true!_A() = 19
              *!_A(x1,x2) = x1 + 17
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            +#_A(x1,x2) = max{0, x1 - 618}
            +_A(x1,x2) = max{x1 + 27, x2 + 617}
            |#|_A = 244
            |0|_A(x1) = 265
            |1|_A(x1) = 619
            -_A(x1,x2) = max{834, x1 - 645}
            eq_A(x1,x2) = max{204, x1 - 620}
            true_A = 189
            *_A(x1,x2) = max{x1 - 266, x2 + 617}
            +#!_A(x1,x2) = max{25, x1 - 1}
            +!_A(x1,x2) = max{1258, x1 - 620, x2 + 24}
            |#|!_A = 18
            |0|!_A(x1) = max{532, x1 + 23}
            |1|!_A(x1) = 0
            -!_A(x1,x2) = 0
            eq!_A(x1,x2) = max{562, x2 - 264}
            true!_A = 21
            *!_A(x1,x2) = x1 + 267
        
  
    partial status:
  
      pi(+#) = []
      pi(+) = [1]
      pi(|#|) = []
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = [1, 2]
      pi(eq) = [1]
      pi(true) = []
      pi(*) = [1]

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

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

p1: -#(|0|(x),|0|(y)) -> -#(x,y)
p2: -#(|1|(x),|1|(y)) -> -#(x,y)
p3: -#(|1|(x),|0|(y)) -> -#(x,y)
p4: -#(|0|(x),|1|(y)) -> -#(x,y)
p5: -#(|0|(x),|1|(y)) -> -#(-(x,y),|1|(|#|()))

and R consists of:

r1: |0|(|#|()) -> |#|()
r2: +(x,|#|()) -> x
r3: +(|#|(),x) -> x
r4: +(|0|(x),|0|(y)) -> |0|(+(x,y))
r5: +(|0|(x),|1|(y)) -> |1|(+(x,y))
r6: +(|1|(x),|0|(y)) -> |1|(+(x,y))
r7: +(|1|(x),|1|(y)) -> |0|(+(+(x,y),|1|(|#|())))
r8: +(+(x,y),z) -> +(x,+(y,z))
r9: -(|#|(),x) -> |#|()
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, 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              -#_A(x1,x2) = 0
              |0|_A(x1) = 16
              |1|_A(x1) = 4
              -_A(x1,x2) = x1 + x2 + 8
              |#|_A() = 3
              *_A(x1,x2) = 3
              -#!_A(x1,x2) = 3
              |0|!_A(x1) = x1 + 9
              |1|!_A(x1) = 7
              -!_A(x1,x2) = x1 + 2
              |#|!_A() = 4
              *!_A(x1,x2) = x1
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{0, x2 - 99}
            |0|_A(x1) = max{158, x1}
            |1|_A(x1) = max{98, x1 + 5}
            -_A(x1,x2) = max{158, x2 + 67}
            |#|_A = 82
            *_A(x1,x2) = 158
            -#!_A(x1,x2) = max{1, x2 - 6}
            |0|!_A(x1) = 80
            |1|!_A(x1) = max{78, x1 + 11}
            -!_A(x1,x2) = max{x1 + 171, x2 + 72}
            |#|!_A = 165
            *!_A(x1,x2) = max{x1 + 82, x2 + 82}
        
  
    partial status:
  
      pi(-#) = []
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(-) = [1]
      pi(|#|) = []
      pi(*) = [1, 2]

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

  r1

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      trivial reduction triple (T x T, T x T, Φ)
  
    base order 2:
  
      lexicographic combination of reduction triples:
      
        1. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              -#_A(x1,x2) = x2
              |0|_A(x1) = x1 + 4
              |1|_A(x1) = 4
              |#|_A() = 8
              -#!_A(x1,x2) = 5
              |0|!_A(x1) = 11
              |1|!_A(x1) = x1 + 4
              |#|!_A() = 2
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = 0
            |0|_A(x1) = 46
            |1|_A(x1) = 5
            |#|_A = 5
            -#!_A(x1,x2) = max{40, x1 - 6, x2 - 46}
            |0|!_A(x1) = x1 + 4
            |1|!_A(x1) = x1 + 2
            |#|!_A = 7
        
  
    partial status:
  
      pi(-#) = [2]
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|#|) = []

The following rules are removed:

  p1, p2

Then no dependency pair remains.

-- Reduction pair.

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

p1: -#(|0|(x),|1|(y)) -> -#(-(x,y),|1|(|#|()))

and R consists of:

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

The set of usable rules consists of

  r1, r9, r10, r11, r12, r13, r14

Take the reduction pair:

  generalized weighted path order (>=MG, >G)
  
    base order 1:
  
      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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              -#_A(x1,x2) = x1 + x2
              |0|_A(x1) = x1 + 24
              |1|_A(x1) = x1 + 13
              -_A(x1,x2) = x1 + x2 + 1
              |#|_A() = 10
              -#!_A(x1,x2) = x1 + x2
              |0|!_A(x1) = 25
              |1|!_A(x1) = 27
              -!_A(x1,x2) = 38
              |#|!_A() = 22
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            -#_A(x1,x2) = max{0, x1 - 231, x2 - 286}
            |0|_A(x1) = max{229, x1 + 170}
            |1|_A(x1) = max{229, x1 + 170}
            -_A(x1,x2) = max{59, x1}
            |#|_A = 115
            -#!_A(x1,x2) = max{148, x1 + 93, x2 - 13}
            |0|!_A(x1) = max{217, x1 + 149}
            |1|!_A(x1) = 0
            -!_A(x1,x2) = max{x1 + 91, x2 - 226}
            |#|!_A = 321
        
  
    partial status:
  
      pi(-#) = [2]
      pi(|0|) = []
      pi(|1|) = []
      pi(-) = [1, 2]
      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

  r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              ifinter#_A(x1,x2,x3,x4) = x3 + x4
              false_A() = 3
              inter#_A(x1,x2) = x1 + x2
              cons_A(x1,x2) = x1 + x2 + 15
              mem_A(x1,x2) = x1 + x2 + 1
              true_A() = 3
              app_A(x1,x2) = x1 + x2 + 1
              if_A(x1,x2,x3) = x2 + x3
              eq_A(x1,x2) = 3
              |#|_A() = 3
              |1|_A(x1) = 4
              |0|_A(x1) = x1 + 1
              nil_A() = 2
              ifinter#!_A(x1,x2,x3,x4) = x3 + x4 + 1
              false!_A() = 5
              inter#!_A(x1,x2) = x1 + x2
              cons!_A(x1,x2) = x1 + x2 + 2
              mem!_A(x1,x2) = 14
              true!_A() = 4
              app!_A(x1,x2) = 11
              if!_A(x1,x2,x3) = 3
              eq!_A(x1,x2) = 13
              |#|!_A() = 6
              |1|!_A(x1) = 8
              |0|!_A(x1) = 13
              nil!_A() = 9
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ifinter#_A(x1,x2,x3,x4) = max{8, x3 - 1, x4 - 897}
            false_A = 186
            inter#_A(x1,x2) = max{8, x1 - 897, x2 - 897}
            cons_A(x1,x2) = x2 + 904
            mem_A(x1,x2) = max{x1 + 186, x2 + 187}
            true_A = 186
            app_A(x1,x2) = max{901, x1 + 899, x2 + 900}
            if_A(x1,x2,x3) = max{1091, x1 - 862, x2 + 11, x3}
            eq_A(x1,x2) = 728
            |#|_A = 374
            |1|_A(x1) = 557
            |0|_A(x1) = x1 + 441
            nil_A = 550
            ifinter#!_A(x1,x2,x3,x4) = max{0, x1 - 188, x2 - 1, x4 - 1}
            false!_A = 548
            inter#!_A(x1,x2) = max{892, x2 - 9}
            cons!_A(x1,x2) = x1 + 1813
            mem!_A(x1,x2) = max{7, x2 - 1}
            true!_A = 391
            app!_A(x1,x2) = max{915, x1 + 907, x2 - 1809}
            if!_A(x1,x2,x3) = max{1814, x1 - 729, x2 + 13, x3 - 188}
            eq!_A(x1,x2) = 0
            |#|!_A = 8
            |1|!_A(x1) = x1 + 833
            |0|!_A(x1) = max{0, x1 - 728}
            nil!_A = 9
        
  
    partial status:
  
      pi(ifinter#) = []
      pi(false) = []
      pi(inter#) = []
      pi(cons) = []
      pi(mem) = []
      pi(true) = []
      pi(app) = []
      pi(if) = [2, 3]
      pi(eq) = []
      pi(|#|) = []
      pi(|1|) = []
      pi(|0|) = [1]
      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

  (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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              mem#_A(x1,x2) = x2
              cons_A(x1,x2) = x2 + 76
              mem#!_A(x1,x2) = x2 + 85
              cons!_A(x1,x2) = 84
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            mem#_A(x1,x2) = 0
            cons_A(x1,x2) = max{2, x1 - 23, x2 - 23}
            mem#!_A(x1,x2) = x1 + 2
            cons!_A(x1,x2) = 0
        
  
    partial status:
  
      pi(mem#) = [2]
      pi(cons) = [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

  r36, 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              eq#_A(x1,x2) = x1 + x2
              |0|_A(x1) = x1 + 9
              |1|_A(x1) = x1 + 11
              |log'|_A(x1) = x1
              |#|_A() = 13
              inter_A(x1,x2) = 8
              nil_A() = 7
              eq#!_A(x1,x2) = 21
              |0|!_A(x1) = 22
              |1|!_A(x1) = x1 + 10
              |log'|!_A(x1) = x1 + 10
              |#|!_A() = 8
              inter!_A(x1,x2) = x2 + 18
              nil!_A() = 17
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = 0
            |0|_A(x1) = 710
            |1|_A(x1) = x1 + 2168
            |log'|_A(x1) = x1 + 1407
            |#|_A = 10
            inter_A(x1,x2) = max{634, x1 + 126, x2 - 636}
            nil_A = 127
            eq#!_A(x1,x2) = max{3, x2 - 4347}
            |0|!_A(x1) = max{4, x1 + 2}
            |1|!_A(x1) = max{7, x1 - 688}
            |log'|!_A(x1) = max{3, x1 - 704}
            |#|!_A = 757
            inter!_A(x1,x2) = 0
            nil!_A = 6
        
  
    partial status:
  
      pi(eq#) = [2]
      pi(|0|) = [1]
      pi(|1|) = [1]
      pi(|log'|) = []
      pi(|#|) = []
      pi(inter) = []
      pi(nil) = []

The following rules are removed:

  p1



-- SCC decomposition.

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

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

  {p1}


-- Reduction pair.

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

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

  (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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              eq#_A(x1,x2) = 0
              |1|_A(x1) = 11
              eq#!_A(x1,x2) = 0
              |1|!_A(x1) = 13
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = 0
            |1|_A(x1) = max{235, x1 - 950}
            eq#!_A(x1,x2) = max{x1 + 1162, x2 + 1162}
            |1|!_A(x1) = max{210, x1 - 115}
        
  
    partial status:
  
      pi(eq#) = [1]
      pi(|1|) = [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|(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

  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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              eq#_A(x1,x2) = 0
              |#|_A() = 3
              |0|_A(x1) = 9
              inter_A(x1,x2) = x1 + x2 + 1
              nil_A() = 1
              eq#!_A(x1,x2) = 6
              |#|!_A() = 5
              |0|!_A(x1) = 10
              inter!_A(x1,x2) = 3
              nil!_A() = 2
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = 0
            |#|_A = 9
            |0|_A(x1) = x1 + 49
            inter_A(x1,x2) = max{101, x1 - 102, x2 - 102}
            nil_A = 0
            eq#!_A(x1,x2) = x1 + 34
            |#|!_A = 42
            |0|!_A(x1) = max{78, x1 + 34}
            inter!_A(x1,x2) = 37
            nil!_A = 5
        
  
    partial status:
  
      pi(eq#) = [2]
      pi(|#|) = []
      pi(|0|) = [1]
      pi(inter) = []
      pi(nil) = []

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

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

p1: 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              eq#_A(x1,x2) = 0
              |0|_A(x1) = x1 + 14
              |#|_A() = 5
              eq#!_A(x1,x2) = 5
              |0|!_A(x1) = 22
              |#|!_A() = 6
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            eq#_A(x1,x2) = x1
            |0|_A(x1) = x1 + 55
            |#|_A = 18
            eq#!_A(x1,x2) = 3
            |0|!_A(x1) = max{39, x1 - 65}
            |#|!_A = 4
        
  
    partial status:
  
      pi(eq#) = [1, 2]
      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

  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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              ge#_A(x1,x2) = x1 + x2
              |0|_A(x1) = x1 + 15
              |1|_A(x1) = x1 + 17
              inter_A(x1,x2) = x1 + 1
              nil_A() = 1
              ge#!_A(x1,x2) = x1 + x2
              |0|!_A(x1) = 31
              |1|!_A(x1) = 31
              inter!_A(x1,x2) = 33
              nil!_A() = 32
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = 0
            |0|_A(x1) = max{16, x1 - 12}
            |1|_A(x1) = max{54, x1 + 9}
            inter_A(x1,x2) = max{158, x1 - 151, x2 - 304}
            nil_A = 2
            ge#!_A(x1,x2) = x2 + 25
            |0|!_A(x1) = x1 + 65
            |1|!_A(x1) = max{426, x1 + 11}
            inter!_A(x1,x2) = x1 + 150
            nil!_A = 427
        
  
    partial status:
  
      pi(ge#) = []
      pi(|0|) = []
      pi(|1|) = [1]
      pi(inter) = []
      pi(nil) = []

The following rules are removed:

  p1, p2, p3, p4

Then no dependency pair remains.

-- Reduction pair.

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

p1: ge#(|#|(),|0|(x)) -> ge#(|#|(),x)

and R consists of:

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

The set of usable rules consists of

  (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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              ge#_A(x1,x2) = 0
              |#|_A() = 3
              |0|_A(x1) = 58
              ge#!_A(x1,x2) = 19
              |#|!_A() = 39
              |0|!_A(x1) = x1 + 20
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            ge#_A(x1,x2) = 0
            |#|_A = 213
            |0|_A(x1) = 221
            ge#!_A(x1,x2) = max{1, x1 - 413}
            |#|!_A = 0
            |0|!_A(x1) = max{9, x1 - 199}
        
  
    partial status:
  
      pi(ge#) = [2]
      pi(|#|) = []
      pi(|0|) = [1]

The following rules are removed:

  p1

Then no dependency pair remains.

-- Reduction pair.

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

p1: 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!):
        
          matrix interpretation with standard point-wise order:
          
            carrier: N^1
            order: standard order
            interpretations:
              app#_A(x1,x2) = x1
              cons_A(x1,x2) = x1 + x2 + 1
              prod_A(x1) = x1 + 1
              nil_A() = 0
              |1|_A(x1) = 0
              |#|_A() = 15
              app#!_A(x1,x2) = x1
              cons!_A(x1,x2) = 3
              prod!_A(x1) = 51
              nil!_A() = 34
              |1|!_A(x1) = x1 + 18
              |#|!_A() = 16
        
        2. marked-algebra reduction triple (>=A, >=A!, >A!):
        
          max/plus interpretation on natural numbers:
          
            app#_A(x1,x2) = 0
            cons_A(x1,x2) = max{2, x1 - 6, x2 - 6}
            prod_A(x1) = max{99, x1 - 7}
            nil_A = 5
            |1|_A(x1) = 7
            |#|_A = 16
            app#!_A(x1,x2) = max{x1 + 102, x2 + 2}
            cons!_A(x1,x2) = 0
            prod!_A(x1) = 102
            nil!_A = 99
            |1|!_A(x1) = max{0, x1 - 53}
            |#|!_A = 98
        
  
    partial status:
  
      pi(app#) = []
      pi(cons) = [1]
      pi(prod) = []
      pi(nil) = []
      pi(|1|) = []
      pi(|#|) = []

The following rules are removed:

  p1

Then no dependency pair remains.