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

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          sum#_A(x1) = x1 + 2
          app_A(x1,x2) = max{x1 + 1, x2 + 2}
          cons_A(x1,x2) = max{x1 + 2, x2 + 2}
    
      precedence:
      
        sum# = app = cons
      
      partial status:
    
        pi(sum#) = []
        pi(app) = [1, 2]
        pi(cons) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          sum#_A(x1) = 4
          app_A(x1,x2) = max{x1 + 1, x2 + 3}
          cons_A(x1,x2) = max{3, x2 + 1}
    
      precedence:
      
        sum# > app = cons
      
      partial status:
    
        pi(sum#) = []
        pi(app) = [2]
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1, p2, p3

We remove them from the problem.  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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          prod#_A(x1) = x1 + 2
          app_A(x1,x2) = max{x1 + 1, x2 + 2}
          cons_A(x1,x2) = max{x1 + 2, x2 + 2}
    
      precedence:
      
        prod# = app = cons
      
      partial status:
    
        pi(prod#) = []
        pi(app) = [1, 2]
        pi(cons) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          prod#_A(x1) = 4
          app_A(x1,x2) = max{x1 + 1, x2 + 3}
          cons_A(x1,x2) = max{3, x2 + 1}
    
      precedence:
      
        prod# > app = cons
      
      partial status:
    
        pi(prod#) = []
        pi(app) = [2]
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1, p2, p3

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r39, r40, r41, r42, r43

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          *#_A(x1,x2) = x1 + 5
          +_A(x1,x2) = max{8, x1, x2}
          *_A(x1,x2) = max{x1 + 6, x2}
          |1|_A(x1) = max{2, x1}
          |0|_A(x1) = max{3, x1}
          |#|_A = 1
    
      precedence:
      
        *# > * > + = |1| = |0| = |#|
      
      partial status:
    
        pi(*#) = []
        pi(+) = [1, 2]
        pi(*) = [1, 2]
        pi(|1|) = []
        pi(|0|) = []
        pi(|#|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          *#_A(x1,x2) = 0
          +_A(x1,x2) = max{9, x2}
          *_A(x1,x2) = x1 + 9
          |1|_A(x1) = 9
          |0|_A(x1) = 8
          |#|_A = 13
    
      precedence:
      
        + = * > *# = |#| > |1| = |0|
      
      partial status:
    
        pi(*#) = []
        pi(+) = []
        pi(*) = []
        pi(|1|) = []
        pi(|0|) = []
        pi(|#|) = []
    

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- 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)
p3: *#(*(x,y),z) -> *#(y,z)
p4: *#(|1|(x),y) -> *#(x,y)
p5: *#(|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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5}


-- Reduction pair.

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

p1: *#(x,+(y,z)) -> *#(x,z)
p2: *#(|0|(x),y) -> *#(x,y)
p3: *#(|1|(x),y) -> *#(x,y)
p4: *#(*(x,y),z) -> *#(y,z)
p5: *#(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

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          *#_A(x1,x2) = max{3, x1 + 1, x2 + 1}
          +_A(x1,x2) = max{x1, x2}
          |0|_A(x1) = max{1, x1}
          |1|_A(x1) = max{2, x1 + 1}
          *_A(x1,x2) = max{2, x2}
    
      precedence:
      
        *# = + = |0| = |1| = *
      
      partial status:
    
        pi(*#) = [1, 2]
        pi(+) = [1, 2]
        pi(|0|) = [1]
        pi(|1|) = [1]
        pi(*) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          *#_A(x1,x2) = max{x1 + 1, x2 + 1}
          +_A(x1,x2) = max{x1, x2}
          |0|_A(x1) = x1
          |1|_A(x1) = x1
          *_A(x1,x2) = x2
    
      precedence:
      
        *# = + = |0| = |1| = *
      
      partial status:
    
        pi(*#) = [1, 2]
        pi(+) = [1, 2]
        pi(|0|) = [1]
        pi(|1|) = [1]
        pi(*) = [2]
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5

We remove them from the problem.  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

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          |log'|#_A(x1) = max{6, x1 + 4}
          |0|_A(x1) = max{4, x1 + 3}
          |1|_A(x1) = max{2, x1 + 1}
    
      precedence:
      
        |log'|# = |0| = |1|
      
      partial status:
    
        pi(|log'|#) = [1]
        pi(|0|) = [1]
        pi(|1|) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          |log'|#_A(x1) = x1 + 1
          |0|_A(x1) = x1
          |1|_A(x1) = x1
    
      precedence:
      
        |log'|# = |0| = |1|
      
      partial status:
    
        pi(|log'|#) = [1]
        pi(|0|) = [1]
        pi(|1|) = [1]
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            +#_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,1),(1,1)) x2 + (6,18)
            |0|_A(x1) = ((1,0),(1,1)) x1 + (1,2)
            +_A(x1,x2) = x1 + x2 + (2,3)
            |1|_A(x1) = ((1,0),(1,1)) x1 + (5,17)
            |#|_A() = (1,1)
    
      precedence:
      
        +# = + > |0| > |1| = |#|
      
      partial status:
    
        pi(+#) = [1]
        pi(|0|) = [1]
        pi(+) = [1, 2]
        pi(|1|) = [1]
        pi(|#|) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            +#_A(x1,x2) = x1
            |0|_A(x1) = x1 + (2,1)
            +_A(x1,x2) = x1
            |1|_A(x1) = x1 + (2,1)
            |#|_A() = (1,1)
    
      precedence:
      
        + = |1| = |#| > |0| > +#
      
      partial status:
    
        pi(+#) = [1]
        pi(|0|) = [1]
        pi(+) = [1]
        pi(|1|) = [1]
        pi(|#|) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.

-- SCC decomposition.

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

p1: +#(|1|(x),|1|(y)) -> +#(+(x,y),|1|(|#|()))
p2: +#(|0|(x),|1|(y)) -> +#(x,y)
p3: +#(|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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3}


-- Reduction pair.

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

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

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            +#_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,1),(0,1)) x2 + (3,0)
            |1|_A(x1) = ((1,0),(1,1)) x1 + (2,3)
            +_A(x1,x2) = x1 + x2 + (0,1)
            |#|_A() = (0,0)
            |0|_A(x1) = ((1,0),(1,1)) x1 + (1,0)
    
      precedence:
      
        + > +# = |1| = |#| = |0|
      
      partial status:
    
        pi(+#) = [2]
        pi(|1|) = []
        pi(+) = [1, 2]
        pi(|#|) = []
        pi(|0|) = [1]
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            +#_A(x1,x2) = (1,1)
            |1|_A(x1) = (5,3)
            +_A(x1,x2) = ((1,1),(0,0)) x2 + (4,4)
            |#|_A() = (2,2)
            |0|_A(x1) = (3,2)
    
      precedence:
      
        +# = |1| = + = |0| > |#|
      
      partial status:
    
        pi(+#) = []
        pi(|1|) = []
        pi(+) = []
        pi(|#|) = []
        pi(|0|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: +#(|0|(x),|1|(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 estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          +#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          |0|_A(x1) = max{1, x1}
          |1|_A(x1) = max{1, x1}
    
      precedence:
      
        +# = |0| = |1|
      
      partial status:
    
        pi(+#) = [1, 2]
        pi(|0|) = [1]
        pi(|1|) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          +#_A(x1,x2) = max{x1 + 1, x2 - 1}
          |0|_A(x1) = x1
          |1|_A(x1) = x1
    
      precedence:
      
        +# = |0| = |1|
      
      partial status:
    
        pi(+#) = [1]
        pi(|0|) = [1]
        pi(|1|) = [1]
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          -#_A(x1,x2) = max{x1 + 4, x2 + 2}
          |0|_A(x1) = max{4, x1 + 3}
          |1|_A(x1) = max{4, x1 + 3}
          -_A(x1,x2) = x1
          |#|_A = 0
    
      precedence:
      
        -# = - > |0| = |1| = |#|
      
      partial status:
    
        pi(-#) = [1, 2]
        pi(|0|) = [1]
        pi(|1|) = [1]
        pi(-) = [1]
        pi(|#|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          -#_A(x1,x2) = max{0, x1 - 25, x2 - 31}
          |0|_A(x1) = max{48, x1 + 37}
          |1|_A(x1) = max{42, x1 + 35}
          -_A(x1,x2) = 26
          |#|_A = 1
    
      precedence:
      
        |0| > -# = |1| = - = |#|
      
      partial status:
    
        pi(-#) = []
        pi(|0|) = [1]
        pi(|1|) = []
        pi(-) = []
        pi(|#|) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5

We remove them from the problem.  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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          ifinter#_A(x1,x2,x3,x4) = max{x2 + 4, x3 + 13, x4 + 1}
          false_A = 45
          inter#_A(x1,x2) = max{13, x1 + 12, x2 + 1}
          cons_A(x1,x2) = max{x1 + 4, x2 + 13}
          mem_A(x1,x2) = x2 + 18
          true_A = 0
          app_A(x1,x2) = max{x1 + 1, x2 + 1}
          if_A(x1,x2,x3) = max{x2 + 31, x3 + 8}
          eq_A(x1,x2) = max{x1 + 20, x2 + 23}
          |#|_A = 44
          |1|_A(x1) = x1 + 46
          |0|_A(x1) = max{67, x1 + 23}
          nil_A = 46
    
      precedence:
      
        |#| > cons > ifinter# = inter# = mem = true > app = |0| > if = eq = |1| = nil > false
      
      partial status:
    
        pi(ifinter#) = [3, 4]
        pi(false) = []
        pi(inter#) = [1]
        pi(cons) = [1, 2]
        pi(mem) = [2]
        pi(true) = []
        pi(app) = [1, 2]
        pi(if) = [3]
        pi(eq) = [2]
        pi(|#|) = []
        pi(|1|) = []
        pi(|0|) = [1]
        pi(nil) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          ifinter#_A(x1,x2,x3,x4) = 0
          false_A = 8
          inter#_A(x1,x2) = max{1, x1 - 11}
          cons_A(x1,x2) = max{x1 + 9, x2 + 9}
          mem_A(x1,x2) = max{2, x2 - 3}
          true_A = 8
          app_A(x1,x2) = max{13, x1, x2 + 10}
          if_A(x1,x2,x3) = max{3, x3}
          eq_A(x1,x2) = max{7, x2}
          |#|_A = 0
          |1|_A(x1) = 7
          |0|_A(x1) = x1 + 1
          nil_A = 7
    
      precedence:
      
        false > inter# > ifinter# = cons = mem > true > app = if = eq = |#| = |1| = |0| = nil
      
      partial status:
    
        pi(ifinter#) = []
        pi(false) = []
        pi(inter#) = []
        pi(cons) = [1, 2]
        pi(mem) = []
        pi(true) = []
        pi(app) = [2]
        pi(if) = [3]
        pi(eq) = [2]
        pi(|#|) = []
        pi(|1|) = []
        pi(|0|) = [1]
        pi(nil) = []
    

The next rules are strictly ordered:

  p1, p3, p4, p7, p8

We remove them from the problem.

-- SCC decomposition.

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

p1: inter#(l1,cons(x,l2)) -> ifinter#(mem(x,l1),x,l2,l1)
p2: inter#(l1,app(l2,l3)) -> inter#(l1,l3)
p3: inter#(l1,app(l2,l3)) -> 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:

  {p2, p3}


-- Reduction pair.

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

p1: inter#(l1,app(l2,l3)) -> inter#(l1,l3)
p2: inter#(l1,app(l2,l3)) -> 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 set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          inter#_A(x1,x2) = x2 + 1
          app_A(x1,x2) = max{x1 + 1, x2 + 1}
    
      precedence:
      
        inter# = app
      
      partial status:
    
        pi(inter#) = []
        pi(app) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          inter#_A(x1,x2) = 0
          app_A(x1,x2) = x2
    
      precedence:
      
        inter# > app
      
      partial status:
    
        pi(inter#) = []
        pi(app) = [2]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

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

  {p1}


-- Reduction pair.

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

p1: inter#(l1,app(l2,l3)) -> 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 set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          inter#_A(x1,x2) = max{0, x2 - 2}
          app_A(x1,x2) = max{x1 + 1, x2 + 3}
    
      precedence:
      
        inter# = app
      
      partial status:
    
        pi(inter#) = []
        pi(app) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          inter#_A(x1,x2) = 0
          app_A(x1,x2) = max{x1 + 1, x2}
    
      precedence:
      
        inter# = app
      
      partial status:
    
        pi(inter#) = []
        pi(app) = [2]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mem#_A(x1,x2) = max{0, x2 - 2}
          cons_A(x1,x2) = max{3, x1, x2 + 1}
    
      precedence:
      
        mem# = cons
      
      partial status:
    
        pi(mem#) = []
        pi(cons) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mem#_A(x1,x2) = 0
          cons_A(x1,x2) = x2
    
      precedence:
      
        mem# = cons
      
      partial status:
    
        pi(mem#) = []
        pi(cons) = [2]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  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

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{2, x1 + 1, x2 + 1}
          |0|_A(x1) = max{1, x1}
          |1|_A(x1) = max{1, x1}
    
      precedence:
      
        eq# = |0| = |1|
      
      partial status:
    
        pi(eq#) = [1, 2]
        pi(|0|) = [1]
        pi(|1|) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{0, x1 - 4, x2 - 2}
          |0|_A(x1) = max{5, x1 + 3}
          |1|_A(x1) = max{5, x1 + 1}
    
      precedence:
      
        eq# = |0| = |1|
      
      partial status:
    
        pi(eq#) = []
        pi(|0|) = [1]
        pi(|1|) = [1]
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: eq#(|#|(),|0|(y)) -> eq#(|#|(),y)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{x1 + 5, x2 + 4}
          |#|_A = 1
          |0|_A(x1) = x1 + 2
    
      precedence:
      
        eq# = |#| = |0|
      
      partial status:
    
        pi(eq#) = [1, 2]
        pi(|#|) = []
        pi(|0|) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{5, x1 + 4, x2 + 3}
          |#|_A = 1
          |0|_A(x1) = x1 + 2
    
      precedence:
      
        eq# = |#| = |0|
      
      partial status:
    
        pi(eq#) = []
        pi(|#|) = []
        pi(|0|) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{x1 + 4, x2 + 5}
          |0|_A(x1) = x1 + 2
          |#|_A = 1
    
      precedence:
      
        eq# = |0| = |#|
      
      partial status:
    
        pi(eq#) = [1, 2]
        pi(|0|) = [1]
        pi(|#|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          eq#_A(x1,x2) = max{5, x1 + 3, x2 + 4}
          |0|_A(x1) = x1 + 2
          |#|_A = 1
    
      precedence:
      
        eq# = |0| = |#|
      
      partial status:
    
        pi(eq#) = [1]
        pi(|0|) = [1]
        pi(|#|) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  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

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          ge#_A(x1,x2) = max{x1 + 1, x2 - 2}
          |0|_A(x1) = max{3, x1 + 1}
          |1|_A(x1) = max{5, x1 + 4}
    
      precedence:
      
        ge# = |0| = |1|
      
      partial status:
    
        pi(ge#) = [1]
        pi(|0|) = [1]
        pi(|1|) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          ge#_A(x1,x2) = 0
          |0|_A(x1) = max{3, x1}
          |1|_A(x1) = max{3, x1}
    
      precedence:
      
        ge# = |0| = |1|
      
      partial status:
    
        pi(ge#) = []
        pi(|0|) = [1]
        pi(|1|) = [1]
    

The next rules are strictly ordered:

  p1, p2, p3, p4

We remove them from the problem.  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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          ge#_A(x1,x2) = max{x1 + 5, x2 + 4}
          |#|_A = 1
          |0|_A(x1) = x1 + 2
    
      precedence:
      
        ge# = |#| = |0|
      
      partial status:
    
        pi(ge#) = [1, 2]
        pi(|#|) = []
        pi(|0|) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          ge#_A(x1,x2) = max{5, x1 + 4, x2 + 3}
          |#|_A = 1
          |0|_A(x1) = x1 + 2
    
      precedence:
      
        ge# = |#| = |0|
      
      partial status:
    
        pi(ge#) = []
        pi(|#|) = []
        pi(|0|) = [1]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

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

p1: app#(cons(x,l1),l2) -> app#(l1,l2)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          app#_A(x1,x2) = x1 + 1
          cons_A(x1,x2) = max{x1, x2 + 1}
    
      precedence:
      
        app# = cons
      
      partial status:
    
        pi(app#) = [1]
        pi(cons) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          app#_A(x1,x2) = max{0, x1 - 1}
          cons_A(x1,x2) = max{x1, x2}
    
      precedence:
      
        app# = cons
      
      partial status:
    
        pi(app#) = []
        pi(cons) = [1, 2]
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.