YES

We show the termination of the TRS R:

  +(|0|(),|0|()) -> |0|()
  +(|0|(),|1|()) -> |1|()
  +(|0|(),|2|()) -> |2|()
  +(|0|(),|3|()) -> |3|()
  +(|0|(),|4|()) -> |4|()
  +(|0|(),|5|()) -> |5|()
  +(|0|(),|6|()) -> |6|()
  +(|0|(),|7|()) -> |7|()
  +(|0|(),|8|()) -> |8|()
  +(|0|(),|9|()) -> |9|()
  +(|1|(),|0|()) -> |1|()
  +(|1|(),|1|()) -> |2|()
  +(|1|(),|2|()) -> |3|()
  +(|1|(),|3|()) -> |4|()
  +(|1|(),|4|()) -> |5|()
  +(|1|(),|5|()) -> |6|()
  +(|1|(),|6|()) -> |7|()
  +(|1|(),|7|()) -> |8|()
  +(|1|(),|8|()) -> |9|()
  +(|1|(),|9|()) -> c(|1|(),|0|())
  +(|2|(),|0|()) -> |2|()
  +(|2|(),|1|()) -> |3|()
  +(|2|(),|2|()) -> |4|()
  +(|2|(),|3|()) -> |5|()
  +(|2|(),|4|()) -> |6|()
  +(|2|(),|5|()) -> |7|()
  +(|2|(),|6|()) -> |8|()
  +(|2|(),|7|()) -> |9|()
  +(|2|(),|8|()) -> c(|1|(),|0|())
  +(|2|(),|9|()) -> c(|1|(),|1|())
  +(|3|(),|0|()) -> |3|()
  +(|3|(),|1|()) -> |4|()
  +(|3|(),|2|()) -> |5|()
  +(|3|(),|3|()) -> |6|()
  +(|3|(),|4|()) -> |7|()
  +(|3|(),|5|()) -> |8|()
  +(|3|(),|6|()) -> |9|()
  +(|3|(),|7|()) -> c(|1|(),|0|())
  +(|3|(),|8|()) -> c(|1|(),|1|())
  +(|3|(),|9|()) -> c(|1|(),|2|())
  +(|4|(),|0|()) -> |4|()
  +(|4|(),|1|()) -> |5|()
  +(|4|(),|2|()) -> |6|()
  +(|4|(),|3|()) -> |7|()
  +(|4|(),|4|()) -> |8|()
  +(|4|(),|5|()) -> |9|()
  +(|4|(),|6|()) -> c(|1|(),|0|())
  +(|4|(),|7|()) -> c(|1|(),|1|())
  +(|4|(),|8|()) -> c(|1|(),|2|())
  +(|4|(),|9|()) -> c(|1|(),|3|())
  +(|5|(),|0|()) -> |5|()
  +(|5|(),|1|()) -> |6|()
  +(|5|(),|2|()) -> |7|()
  +(|5|(),|3|()) -> |8|()
  +(|5|(),|4|()) -> |9|()
  +(|5|(),|5|()) -> c(|1|(),|0|())
  +(|5|(),|6|()) -> c(|1|(),|1|())
  +(|5|(),|7|()) -> c(|1|(),|2|())
  +(|5|(),|8|()) -> c(|1|(),|3|())
  +(|5|(),|9|()) -> c(|1|(),|4|())
  +(|6|(),|0|()) -> |6|()
  +(|6|(),|1|()) -> |7|()
  +(|6|(),|2|()) -> |8|()
  +(|6|(),|3|()) -> |9|()
  +(|6|(),|4|()) -> c(|1|(),|0|())
  +(|6|(),|5|()) -> c(|1|(),|1|())
  +(|6|(),|6|()) -> c(|1|(),|2|())
  +(|6|(),|7|()) -> c(|1|(),|3|())
  +(|6|(),|8|()) -> c(|1|(),|4|())
  +(|6|(),|9|()) -> c(|1|(),|5|())
  +(|7|(),|0|()) -> |7|()
  +(|7|(),|1|()) -> |8|()
  +(|7|(),|2|()) -> |9|()
  +(|7|(),|3|()) -> c(|1|(),|0|())
  +(|7|(),|4|()) -> c(|1|(),|1|())
  +(|7|(),|5|()) -> c(|1|(),|2|())
  +(|7|(),|6|()) -> c(|1|(),|3|())
  +(|7|(),|7|()) -> c(|1|(),|4|())
  +(|7|(),|8|()) -> c(|1|(),|5|())
  +(|7|(),|9|()) -> c(|1|(),|6|())
  +(|8|(),|0|()) -> |8|()
  +(|8|(),|1|()) -> |9|()
  +(|8|(),|2|()) -> c(|1|(),|0|())
  +(|8|(),|3|()) -> c(|1|(),|1|())
  +(|8|(),|4|()) -> c(|1|(),|2|())
  +(|8|(),|5|()) -> c(|1|(),|3|())
  +(|8|(),|6|()) -> c(|1|(),|4|())
  +(|8|(),|7|()) -> c(|1|(),|5|())
  +(|8|(),|8|()) -> c(|1|(),|6|())
  +(|8|(),|9|()) -> c(|1|(),|7|())
  +(|9|(),|0|()) -> |9|()
  +(|9|(),|1|()) -> c(|1|(),|0|())
  +(|9|(),|2|()) -> c(|1|(),|1|())
  +(|9|(),|3|()) -> c(|1|(),|2|())
  +(|9|(),|4|()) -> c(|1|(),|3|())
  +(|9|(),|5|()) -> c(|1|(),|4|())
  +(|9|(),|6|()) -> c(|1|(),|5|())
  +(|9|(),|7|()) -> c(|1|(),|6|())
  +(|9|(),|8|()) -> c(|1|(),|7|())
  +(|9|(),|9|()) -> c(|1|(),|8|())
  +(x,c(y,z)) -> c(y,+(x,z))
  +(c(x,y),z) -> c(x,+(y,z))
  c(|0|(),x) -> x
  c(x,c(y,z)) -> c(+(x,y),z)

-- SCC decomposition.

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

p1: +#(|1|(),|9|()) -> c#(|1|(),|0|())
p2: +#(|2|(),|8|()) -> c#(|1|(),|0|())
p3: +#(|2|(),|9|()) -> c#(|1|(),|1|())
p4: +#(|3|(),|7|()) -> c#(|1|(),|0|())
p5: +#(|3|(),|8|()) -> c#(|1|(),|1|())
p6: +#(|3|(),|9|()) -> c#(|1|(),|2|())
p7: +#(|4|(),|6|()) -> c#(|1|(),|0|())
p8: +#(|4|(),|7|()) -> c#(|1|(),|1|())
p9: +#(|4|(),|8|()) -> c#(|1|(),|2|())
p10: +#(|4|(),|9|()) -> c#(|1|(),|3|())
p11: +#(|5|(),|5|()) -> c#(|1|(),|0|())
p12: +#(|5|(),|6|()) -> c#(|1|(),|1|())
p13: +#(|5|(),|7|()) -> c#(|1|(),|2|())
p14: +#(|5|(),|8|()) -> c#(|1|(),|3|())
p15: +#(|5|(),|9|()) -> c#(|1|(),|4|())
p16: +#(|6|(),|4|()) -> c#(|1|(),|0|())
p17: +#(|6|(),|5|()) -> c#(|1|(),|1|())
p18: +#(|6|(),|6|()) -> c#(|1|(),|2|())
p19: +#(|6|(),|7|()) -> c#(|1|(),|3|())
p20: +#(|6|(),|8|()) -> c#(|1|(),|4|())
p21: +#(|6|(),|9|()) -> c#(|1|(),|5|())
p22: +#(|7|(),|3|()) -> c#(|1|(),|0|())
p23: +#(|7|(),|4|()) -> c#(|1|(),|1|())
p24: +#(|7|(),|5|()) -> c#(|1|(),|2|())
p25: +#(|7|(),|6|()) -> c#(|1|(),|3|())
p26: +#(|7|(),|7|()) -> c#(|1|(),|4|())
p27: +#(|7|(),|8|()) -> c#(|1|(),|5|())
p28: +#(|7|(),|9|()) -> c#(|1|(),|6|())
p29: +#(|8|(),|2|()) -> c#(|1|(),|0|())
p30: +#(|8|(),|3|()) -> c#(|1|(),|1|())
p31: +#(|8|(),|4|()) -> c#(|1|(),|2|())
p32: +#(|8|(),|5|()) -> c#(|1|(),|3|())
p33: +#(|8|(),|6|()) -> c#(|1|(),|4|())
p34: +#(|8|(),|7|()) -> c#(|1|(),|5|())
p35: +#(|8|(),|8|()) -> c#(|1|(),|6|())
p36: +#(|8|(),|9|()) -> c#(|1|(),|7|())
p37: +#(|9|(),|1|()) -> c#(|1|(),|0|())
p38: +#(|9|(),|2|()) -> c#(|1|(),|1|())
p39: +#(|9|(),|3|()) -> c#(|1|(),|2|())
p40: +#(|9|(),|4|()) -> c#(|1|(),|3|())
p41: +#(|9|(),|5|()) -> c#(|1|(),|4|())
p42: +#(|9|(),|6|()) -> c#(|1|(),|5|())
p43: +#(|9|(),|7|()) -> c#(|1|(),|6|())
p44: +#(|9|(),|8|()) -> c#(|1|(),|7|())
p45: +#(|9|(),|9|()) -> c#(|1|(),|8|())
p46: +#(x,c(y,z)) -> c#(y,+(x,z))
p47: +#(x,c(y,z)) -> +#(x,z)
p48: +#(c(x,y),z) -> c#(x,+(y,z))
p49: +#(c(x,y),z) -> +#(y,z)
p50: c#(x,c(y,z)) -> c#(+(x,y),z)
p51: c#(x,c(y,z)) -> +#(x,y)

and R consists of:

r1: +(|0|(),|0|()) -> |0|()
r2: +(|0|(),|1|()) -> |1|()
r3: +(|0|(),|2|()) -> |2|()
r4: +(|0|(),|3|()) -> |3|()
r5: +(|0|(),|4|()) -> |4|()
r6: +(|0|(),|5|()) -> |5|()
r7: +(|0|(),|6|()) -> |6|()
r8: +(|0|(),|7|()) -> |7|()
r9: +(|0|(),|8|()) -> |8|()
r10: +(|0|(),|9|()) -> |9|()
r11: +(|1|(),|0|()) -> |1|()
r12: +(|1|(),|1|()) -> |2|()
r13: +(|1|(),|2|()) -> |3|()
r14: +(|1|(),|3|()) -> |4|()
r15: +(|1|(),|4|()) -> |5|()
r16: +(|1|(),|5|()) -> |6|()
r17: +(|1|(),|6|()) -> |7|()
r18: +(|1|(),|7|()) -> |8|()
r19: +(|1|(),|8|()) -> |9|()
r20: +(|1|(),|9|()) -> c(|1|(),|0|())
r21: +(|2|(),|0|()) -> |2|()
r22: +(|2|(),|1|()) -> |3|()
r23: +(|2|(),|2|()) -> |4|()
r24: +(|2|(),|3|()) -> |5|()
r25: +(|2|(),|4|()) -> |6|()
r26: +(|2|(),|5|()) -> |7|()
r27: +(|2|(),|6|()) -> |8|()
r28: +(|2|(),|7|()) -> |9|()
r29: +(|2|(),|8|()) -> c(|1|(),|0|())
r30: +(|2|(),|9|()) -> c(|1|(),|1|())
r31: +(|3|(),|0|()) -> |3|()
r32: +(|3|(),|1|()) -> |4|()
r33: +(|3|(),|2|()) -> |5|()
r34: +(|3|(),|3|()) -> |6|()
r35: +(|3|(),|4|()) -> |7|()
r36: +(|3|(),|5|()) -> |8|()
r37: +(|3|(),|6|()) -> |9|()
r38: +(|3|(),|7|()) -> c(|1|(),|0|())
r39: +(|3|(),|8|()) -> c(|1|(),|1|())
r40: +(|3|(),|9|()) -> c(|1|(),|2|())
r41: +(|4|(),|0|()) -> |4|()
r42: +(|4|(),|1|()) -> |5|()
r43: +(|4|(),|2|()) -> |6|()
r44: +(|4|(),|3|()) -> |7|()
r45: +(|4|(),|4|()) -> |8|()
r46: +(|4|(),|5|()) -> |9|()
r47: +(|4|(),|6|()) -> c(|1|(),|0|())
r48: +(|4|(),|7|()) -> c(|1|(),|1|())
r49: +(|4|(),|8|()) -> c(|1|(),|2|())
r50: +(|4|(),|9|()) -> c(|1|(),|3|())
r51: +(|5|(),|0|()) -> |5|()
r52: +(|5|(),|1|()) -> |6|()
r53: +(|5|(),|2|()) -> |7|()
r54: +(|5|(),|3|()) -> |8|()
r55: +(|5|(),|4|()) -> |9|()
r56: +(|5|(),|5|()) -> c(|1|(),|0|())
r57: +(|5|(),|6|()) -> c(|1|(),|1|())
r58: +(|5|(),|7|()) -> c(|1|(),|2|())
r59: +(|5|(),|8|()) -> c(|1|(),|3|())
r60: +(|5|(),|9|()) -> c(|1|(),|4|())
r61: +(|6|(),|0|()) -> |6|()
r62: +(|6|(),|1|()) -> |7|()
r63: +(|6|(),|2|()) -> |8|()
r64: +(|6|(),|3|()) -> |9|()
r65: +(|6|(),|4|()) -> c(|1|(),|0|())
r66: +(|6|(),|5|()) -> c(|1|(),|1|())
r67: +(|6|(),|6|()) -> c(|1|(),|2|())
r68: +(|6|(),|7|()) -> c(|1|(),|3|())
r69: +(|6|(),|8|()) -> c(|1|(),|4|())
r70: +(|6|(),|9|()) -> c(|1|(),|5|())
r71: +(|7|(),|0|()) -> |7|()
r72: +(|7|(),|1|()) -> |8|()
r73: +(|7|(),|2|()) -> |9|()
r74: +(|7|(),|3|()) -> c(|1|(),|0|())
r75: +(|7|(),|4|()) -> c(|1|(),|1|())
r76: +(|7|(),|5|()) -> c(|1|(),|2|())
r77: +(|7|(),|6|()) -> c(|1|(),|3|())
r78: +(|7|(),|7|()) -> c(|1|(),|4|())
r79: +(|7|(),|8|()) -> c(|1|(),|5|())
r80: +(|7|(),|9|()) -> c(|1|(),|6|())
r81: +(|8|(),|0|()) -> |8|()
r82: +(|8|(),|1|()) -> |9|()
r83: +(|8|(),|2|()) -> c(|1|(),|0|())
r84: +(|8|(),|3|()) -> c(|1|(),|1|())
r85: +(|8|(),|4|()) -> c(|1|(),|2|())
r86: +(|8|(),|5|()) -> c(|1|(),|3|())
r87: +(|8|(),|6|()) -> c(|1|(),|4|())
r88: +(|8|(),|7|()) -> c(|1|(),|5|())
r89: +(|8|(),|8|()) -> c(|1|(),|6|())
r90: +(|8|(),|9|()) -> c(|1|(),|7|())
r91: +(|9|(),|0|()) -> |9|()
r92: +(|9|(),|1|()) -> c(|1|(),|0|())
r93: +(|9|(),|2|()) -> c(|1|(),|1|())
r94: +(|9|(),|3|()) -> c(|1|(),|2|())
r95: +(|9|(),|4|()) -> c(|1|(),|3|())
r96: +(|9|(),|5|()) -> c(|1|(),|4|())
r97: +(|9|(),|6|()) -> c(|1|(),|5|())
r98: +(|9|(),|7|()) -> c(|1|(),|6|())
r99: +(|9|(),|8|()) -> c(|1|(),|7|())
r100: +(|9|(),|9|()) -> c(|1|(),|8|())
r101: +(x,c(y,z)) -> c(y,+(x,z))
r102: +(c(x,y),z) -> c(x,+(y,z))
r103: c(|0|(),x) -> x
r104: c(x,c(y,z)) -> c(+(x,y),z)

The estimated dependency graph contains the following SCCs:

  {p46, p47, p48, p49, p50, p51}


-- Reduction pair.

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

p1: +#(x,c(y,z)) -> c#(y,+(x,z))
p2: c#(x,c(y,z)) -> +#(x,y)
p3: +#(c(x,y),z) -> +#(y,z)
p4: +#(c(x,y),z) -> c#(x,+(y,z))
p5: c#(x,c(y,z)) -> c#(+(x,y),z)
p6: +#(x,c(y,z)) -> +#(x,z)

and R consists of:

r1: +(|0|(),|0|()) -> |0|()
r2: +(|0|(),|1|()) -> |1|()
r3: +(|0|(),|2|()) -> |2|()
r4: +(|0|(),|3|()) -> |3|()
r5: +(|0|(),|4|()) -> |4|()
r6: +(|0|(),|5|()) -> |5|()
r7: +(|0|(),|6|()) -> |6|()
r8: +(|0|(),|7|()) -> |7|()
r9: +(|0|(),|8|()) -> |8|()
r10: +(|0|(),|9|()) -> |9|()
r11: +(|1|(),|0|()) -> |1|()
r12: +(|1|(),|1|()) -> |2|()
r13: +(|1|(),|2|()) -> |3|()
r14: +(|1|(),|3|()) -> |4|()
r15: +(|1|(),|4|()) -> |5|()
r16: +(|1|(),|5|()) -> |6|()
r17: +(|1|(),|6|()) -> |7|()
r18: +(|1|(),|7|()) -> |8|()
r19: +(|1|(),|8|()) -> |9|()
r20: +(|1|(),|9|()) -> c(|1|(),|0|())
r21: +(|2|(),|0|()) -> |2|()
r22: +(|2|(),|1|()) -> |3|()
r23: +(|2|(),|2|()) -> |4|()
r24: +(|2|(),|3|()) -> |5|()
r25: +(|2|(),|4|()) -> |6|()
r26: +(|2|(),|5|()) -> |7|()
r27: +(|2|(),|6|()) -> |8|()
r28: +(|2|(),|7|()) -> |9|()
r29: +(|2|(),|8|()) -> c(|1|(),|0|())
r30: +(|2|(),|9|()) -> c(|1|(),|1|())
r31: +(|3|(),|0|()) -> |3|()
r32: +(|3|(),|1|()) -> |4|()
r33: +(|3|(),|2|()) -> |5|()
r34: +(|3|(),|3|()) -> |6|()
r35: +(|3|(),|4|()) -> |7|()
r36: +(|3|(),|5|()) -> |8|()
r37: +(|3|(),|6|()) -> |9|()
r38: +(|3|(),|7|()) -> c(|1|(),|0|())
r39: +(|3|(),|8|()) -> c(|1|(),|1|())
r40: +(|3|(),|9|()) -> c(|1|(),|2|())
r41: +(|4|(),|0|()) -> |4|()
r42: +(|4|(),|1|()) -> |5|()
r43: +(|4|(),|2|()) -> |6|()
r44: +(|4|(),|3|()) -> |7|()
r45: +(|4|(),|4|()) -> |8|()
r46: +(|4|(),|5|()) -> |9|()
r47: +(|4|(),|6|()) -> c(|1|(),|0|())
r48: +(|4|(),|7|()) -> c(|1|(),|1|())
r49: +(|4|(),|8|()) -> c(|1|(),|2|())
r50: +(|4|(),|9|()) -> c(|1|(),|3|())
r51: +(|5|(),|0|()) -> |5|()
r52: +(|5|(),|1|()) -> |6|()
r53: +(|5|(),|2|()) -> |7|()
r54: +(|5|(),|3|()) -> |8|()
r55: +(|5|(),|4|()) -> |9|()
r56: +(|5|(),|5|()) -> c(|1|(),|0|())
r57: +(|5|(),|6|()) -> c(|1|(),|1|())
r58: +(|5|(),|7|()) -> c(|1|(),|2|())
r59: +(|5|(),|8|()) -> c(|1|(),|3|())
r60: +(|5|(),|9|()) -> c(|1|(),|4|())
r61: +(|6|(),|0|()) -> |6|()
r62: +(|6|(),|1|()) -> |7|()
r63: +(|6|(),|2|()) -> |8|()
r64: +(|6|(),|3|()) -> |9|()
r65: +(|6|(),|4|()) -> c(|1|(),|0|())
r66: +(|6|(),|5|()) -> c(|1|(),|1|())
r67: +(|6|(),|6|()) -> c(|1|(),|2|())
r68: +(|6|(),|7|()) -> c(|1|(),|3|())
r69: +(|6|(),|8|()) -> c(|1|(),|4|())
r70: +(|6|(),|9|()) -> c(|1|(),|5|())
r71: +(|7|(),|0|()) -> |7|()
r72: +(|7|(),|1|()) -> |8|()
r73: +(|7|(),|2|()) -> |9|()
r74: +(|7|(),|3|()) -> c(|1|(),|0|())
r75: +(|7|(),|4|()) -> c(|1|(),|1|())
r76: +(|7|(),|5|()) -> c(|1|(),|2|())
r77: +(|7|(),|6|()) -> c(|1|(),|3|())
r78: +(|7|(),|7|()) -> c(|1|(),|4|())
r79: +(|7|(),|8|()) -> c(|1|(),|5|())
r80: +(|7|(),|9|()) -> c(|1|(),|6|())
r81: +(|8|(),|0|()) -> |8|()
r82: +(|8|(),|1|()) -> |9|()
r83: +(|8|(),|2|()) -> c(|1|(),|0|())
r84: +(|8|(),|3|()) -> c(|1|(),|1|())
r85: +(|8|(),|4|()) -> c(|1|(),|2|())
r86: +(|8|(),|5|()) -> c(|1|(),|3|())
r87: +(|8|(),|6|()) -> c(|1|(),|4|())
r88: +(|8|(),|7|()) -> c(|1|(),|5|())
r89: +(|8|(),|8|()) -> c(|1|(),|6|())
r90: +(|8|(),|9|()) -> c(|1|(),|7|())
r91: +(|9|(),|0|()) -> |9|()
r92: +(|9|(),|1|()) -> c(|1|(),|0|())
r93: +(|9|(),|2|()) -> c(|1|(),|1|())
r94: +(|9|(),|3|()) -> c(|1|(),|2|())
r95: +(|9|(),|4|()) -> c(|1|(),|3|())
r96: +(|9|(),|5|()) -> c(|1|(),|4|())
r97: +(|9|(),|6|()) -> c(|1|(),|5|())
r98: +(|9|(),|7|()) -> c(|1|(),|6|())
r99: +(|9|(),|8|()) -> c(|1|(),|7|())
r100: +(|9|(),|9|()) -> c(|1|(),|8|())
r101: +(x,c(y,z)) -> c(y,+(x,z))
r102: +(c(x,y),z) -> c(x,+(y,z))
r103: c(|0|(),x) -> x
r104: c(x,c(y,z)) -> c(+(x,y),z)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104

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,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,3)
            c_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (130,2)
            c#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,0)
            +_A(x1,x2) = x1 + x2 + (126,3)
            |0|_A() = (62,27)
            |1|_A() = (2,52)
            |2|_A() = (1,29)
            |3|_A() = (125,18)
            |4|_A() = (127,15)
            |5|_A() = (61,24)
            |6|_A() = (187,27)
            |7|_A() = (124,36)
            |8|_A() = (123,33)
            |9|_A() = (126,30)
    
      precedence:
      
        |0| > +# = |3| > + = |2| = |5| = |7| = |9| > |4| = |8| > |1| > c > c# = |6|
      
      partial status:
    
        pi(+#) = [1]
        pi(c) = [2]
        pi(c#) = [1, 2]
        pi(+) = [1]
        pi(|0|) = []
        pi(|1|) = []
        pi(|2|) = []
        pi(|3|) = []
        pi(|4|) = []
        pi(|5|) = []
        pi(|6|) = []
        pi(|7|) = []
        pi(|8|) = []
        pi(|9|) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            +#_A(x1,x2) = (0,0)
            c_A(x1,x2) = (2,0)
            c#_A(x1,x2) = ((1,1),(1,1)) x1 + (1,1)
            +_A(x1,x2) = ((1,0),(0,0)) x1
            |0|_A() = (0,0)
            |1|_A() = (2,0)
            |2|_A() = (5,0)
            |3|_A() = (5,0)
            |4|_A() = (4,0)
            |5|_A() = (0,0)
            |6|_A() = (3,0)
            |7|_A() = (1,0)
            |8|_A() = (0,0)
            |9|_A() = (3,0)
    
      precedence:
      
        |2| = |3| = |5| = |7| = |8| > |0| = |1| > |9| > +# = c = c# = + = |4| = |6|
      
      partial status:
    
        pi(+#) = []
        pi(c) = []
        pi(c#) = [1]
        pi(+) = []
        pi(|0|) = []
        pi(|1|) = []
        pi(|2|) = []
        pi(|3|) = []
        pi(|4|) = []
        pi(|5|) = []
        pi(|6|) = []
        pi(|7|) = []
        pi(|8|) = []
        pi(|9|) = []
    

The next rules are strictly ordered:

  p1, p4

We remove them from the problem.

-- SCC decomposition.

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

p1: c#(x,c(y,z)) -> +#(x,y)
p2: +#(c(x,y),z) -> +#(y,z)
p3: c#(x,c(y,z)) -> c#(+(x,y),z)
p4: +#(x,c(y,z)) -> +#(x,z)

and R consists of:

r1: +(|0|(),|0|()) -> |0|()
r2: +(|0|(),|1|()) -> |1|()
r3: +(|0|(),|2|()) -> |2|()
r4: +(|0|(),|3|()) -> |3|()
r5: +(|0|(),|4|()) -> |4|()
r6: +(|0|(),|5|()) -> |5|()
r7: +(|0|(),|6|()) -> |6|()
r8: +(|0|(),|7|()) -> |7|()
r9: +(|0|(),|8|()) -> |8|()
r10: +(|0|(),|9|()) -> |9|()
r11: +(|1|(),|0|()) -> |1|()
r12: +(|1|(),|1|()) -> |2|()
r13: +(|1|(),|2|()) -> |3|()
r14: +(|1|(),|3|()) -> |4|()
r15: +(|1|(),|4|()) -> |5|()
r16: +(|1|(),|5|()) -> |6|()
r17: +(|1|(),|6|()) -> |7|()
r18: +(|1|(),|7|()) -> |8|()
r19: +(|1|(),|8|()) -> |9|()
r20: +(|1|(),|9|()) -> c(|1|(),|0|())
r21: +(|2|(),|0|()) -> |2|()
r22: +(|2|(),|1|()) -> |3|()
r23: +(|2|(),|2|()) -> |4|()
r24: +(|2|(),|3|()) -> |5|()
r25: +(|2|(),|4|()) -> |6|()
r26: +(|2|(),|5|()) -> |7|()
r27: +(|2|(),|6|()) -> |8|()
r28: +(|2|(),|7|()) -> |9|()
r29: +(|2|(),|8|()) -> c(|1|(),|0|())
r30: +(|2|(),|9|()) -> c(|1|(),|1|())
r31: +(|3|(),|0|()) -> |3|()
r32: +(|3|(),|1|()) -> |4|()
r33: +(|3|(),|2|()) -> |5|()
r34: +(|3|(),|3|()) -> |6|()
r35: +(|3|(),|4|()) -> |7|()
r36: +(|3|(),|5|()) -> |8|()
r37: +(|3|(),|6|()) -> |9|()
r38: +(|3|(),|7|()) -> c(|1|(),|0|())
r39: +(|3|(),|8|()) -> c(|1|(),|1|())
r40: +(|3|(),|9|()) -> c(|1|(),|2|())
r41: +(|4|(),|0|()) -> |4|()
r42: +(|4|(),|1|()) -> |5|()
r43: +(|4|(),|2|()) -> |6|()
r44: +(|4|(),|3|()) -> |7|()
r45: +(|4|(),|4|()) -> |8|()
r46: +(|4|(),|5|()) -> |9|()
r47: +(|4|(),|6|()) -> c(|1|(),|0|())
r48: +(|4|(),|7|()) -> c(|1|(),|1|())
r49: +(|4|(),|8|()) -> c(|1|(),|2|())
r50: +(|4|(),|9|()) -> c(|1|(),|3|())
r51: +(|5|(),|0|()) -> |5|()
r52: +(|5|(),|1|()) -> |6|()
r53: +(|5|(),|2|()) -> |7|()
r54: +(|5|(),|3|()) -> |8|()
r55: +(|5|(),|4|()) -> |9|()
r56: +(|5|(),|5|()) -> c(|1|(),|0|())
r57: +(|5|(),|6|()) -> c(|1|(),|1|())
r58: +(|5|(),|7|()) -> c(|1|(),|2|())
r59: +(|5|(),|8|()) -> c(|1|(),|3|())
r60: +(|5|(),|9|()) -> c(|1|(),|4|())
r61: +(|6|(),|0|()) -> |6|()
r62: +(|6|(),|1|()) -> |7|()
r63: +(|6|(),|2|()) -> |8|()
r64: +(|6|(),|3|()) -> |9|()
r65: +(|6|(),|4|()) -> c(|1|(),|0|())
r66: +(|6|(),|5|()) -> c(|1|(),|1|())
r67: +(|6|(),|6|()) -> c(|1|(),|2|())
r68: +(|6|(),|7|()) -> c(|1|(),|3|())
r69: +(|6|(),|8|()) -> c(|1|(),|4|())
r70: +(|6|(),|9|()) -> c(|1|(),|5|())
r71: +(|7|(),|0|()) -> |7|()
r72: +(|7|(),|1|()) -> |8|()
r73: +(|7|(),|2|()) -> |9|()
r74: +(|7|(),|3|()) -> c(|1|(),|0|())
r75: +(|7|(),|4|()) -> c(|1|(),|1|())
r76: +(|7|(),|5|()) -> c(|1|(),|2|())
r77: +(|7|(),|6|()) -> c(|1|(),|3|())
r78: +(|7|(),|7|()) -> c(|1|(),|4|())
r79: +(|7|(),|8|()) -> c(|1|(),|5|())
r80: +(|7|(),|9|()) -> c(|1|(),|6|())
r81: +(|8|(),|0|()) -> |8|()
r82: +(|8|(),|1|()) -> |9|()
r83: +(|8|(),|2|()) -> c(|1|(),|0|())
r84: +(|8|(),|3|()) -> c(|1|(),|1|())
r85: +(|8|(),|4|()) -> c(|1|(),|2|())
r86: +(|8|(),|5|()) -> c(|1|(),|3|())
r87: +(|8|(),|6|()) -> c(|1|(),|4|())
r88: +(|8|(),|7|()) -> c(|1|(),|5|())
r89: +(|8|(),|8|()) -> c(|1|(),|6|())
r90: +(|8|(),|9|()) -> c(|1|(),|7|())
r91: +(|9|(),|0|()) -> |9|()
r92: +(|9|(),|1|()) -> c(|1|(),|0|())
r93: +(|9|(),|2|()) -> c(|1|(),|1|())
r94: +(|9|(),|3|()) -> c(|1|(),|2|())
r95: +(|9|(),|4|()) -> c(|1|(),|3|())
r96: +(|9|(),|5|()) -> c(|1|(),|4|())
r97: +(|9|(),|6|()) -> c(|1|(),|5|())
r98: +(|9|(),|7|()) -> c(|1|(),|6|())
r99: +(|9|(),|8|()) -> c(|1|(),|7|())
r100: +(|9|(),|9|()) -> c(|1|(),|8|())
r101: +(x,c(y,z)) -> c(y,+(x,z))
r102: +(c(x,y),z) -> c(x,+(y,z))
r103: c(|0|(),x) -> x
r104: c(x,c(y,z)) -> c(+(x,y),z)

The estimated dependency graph contains the following SCCs:

  {p3}
  {p2, p4}


-- Reduction pair.

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

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

and R consists of:

r1: +(|0|(),|0|()) -> |0|()
r2: +(|0|(),|1|()) -> |1|()
r3: +(|0|(),|2|()) -> |2|()
r4: +(|0|(),|3|()) -> |3|()
r5: +(|0|(),|4|()) -> |4|()
r6: +(|0|(),|5|()) -> |5|()
r7: +(|0|(),|6|()) -> |6|()
r8: +(|0|(),|7|()) -> |7|()
r9: +(|0|(),|8|()) -> |8|()
r10: +(|0|(),|9|()) -> |9|()
r11: +(|1|(),|0|()) -> |1|()
r12: +(|1|(),|1|()) -> |2|()
r13: +(|1|(),|2|()) -> |3|()
r14: +(|1|(),|3|()) -> |4|()
r15: +(|1|(),|4|()) -> |5|()
r16: +(|1|(),|5|()) -> |6|()
r17: +(|1|(),|6|()) -> |7|()
r18: +(|1|(),|7|()) -> |8|()
r19: +(|1|(),|8|()) -> |9|()
r20: +(|1|(),|9|()) -> c(|1|(),|0|())
r21: +(|2|(),|0|()) -> |2|()
r22: +(|2|(),|1|()) -> |3|()
r23: +(|2|(),|2|()) -> |4|()
r24: +(|2|(),|3|()) -> |5|()
r25: +(|2|(),|4|()) -> |6|()
r26: +(|2|(),|5|()) -> |7|()
r27: +(|2|(),|6|()) -> |8|()
r28: +(|2|(),|7|()) -> |9|()
r29: +(|2|(),|8|()) -> c(|1|(),|0|())
r30: +(|2|(),|9|()) -> c(|1|(),|1|())
r31: +(|3|(),|0|()) -> |3|()
r32: +(|3|(),|1|()) -> |4|()
r33: +(|3|(),|2|()) -> |5|()
r34: +(|3|(),|3|()) -> |6|()
r35: +(|3|(),|4|()) -> |7|()
r36: +(|3|(),|5|()) -> |8|()
r37: +(|3|(),|6|()) -> |9|()
r38: +(|3|(),|7|()) -> c(|1|(),|0|())
r39: +(|3|(),|8|()) -> c(|1|(),|1|())
r40: +(|3|(),|9|()) -> c(|1|(),|2|())
r41: +(|4|(),|0|()) -> |4|()
r42: +(|4|(),|1|()) -> |5|()
r43: +(|4|(),|2|()) -> |6|()
r44: +(|4|(),|3|()) -> |7|()
r45: +(|4|(),|4|()) -> |8|()
r46: +(|4|(),|5|()) -> |9|()
r47: +(|4|(),|6|()) -> c(|1|(),|0|())
r48: +(|4|(),|7|()) -> c(|1|(),|1|())
r49: +(|4|(),|8|()) -> c(|1|(),|2|())
r50: +(|4|(),|9|()) -> c(|1|(),|3|())
r51: +(|5|(),|0|()) -> |5|()
r52: +(|5|(),|1|()) -> |6|()
r53: +(|5|(),|2|()) -> |7|()
r54: +(|5|(),|3|()) -> |8|()
r55: +(|5|(),|4|()) -> |9|()
r56: +(|5|(),|5|()) -> c(|1|(),|0|())
r57: +(|5|(),|6|()) -> c(|1|(),|1|())
r58: +(|5|(),|7|()) -> c(|1|(),|2|())
r59: +(|5|(),|8|()) -> c(|1|(),|3|())
r60: +(|5|(),|9|()) -> c(|1|(),|4|())
r61: +(|6|(),|0|()) -> |6|()
r62: +(|6|(),|1|()) -> |7|()
r63: +(|6|(),|2|()) -> |8|()
r64: +(|6|(),|3|()) -> |9|()
r65: +(|6|(),|4|()) -> c(|1|(),|0|())
r66: +(|6|(),|5|()) -> c(|1|(),|1|())
r67: +(|6|(),|6|()) -> c(|1|(),|2|())
r68: +(|6|(),|7|()) -> c(|1|(),|3|())
r69: +(|6|(),|8|()) -> c(|1|(),|4|())
r70: +(|6|(),|9|()) -> c(|1|(),|5|())
r71: +(|7|(),|0|()) -> |7|()
r72: +(|7|(),|1|()) -> |8|()
r73: +(|7|(),|2|()) -> |9|()
r74: +(|7|(),|3|()) -> c(|1|(),|0|())
r75: +(|7|(),|4|()) -> c(|1|(),|1|())
r76: +(|7|(),|5|()) -> c(|1|(),|2|())
r77: +(|7|(),|6|()) -> c(|1|(),|3|())
r78: +(|7|(),|7|()) -> c(|1|(),|4|())
r79: +(|7|(),|8|()) -> c(|1|(),|5|())
r80: +(|7|(),|9|()) -> c(|1|(),|6|())
r81: +(|8|(),|0|()) -> |8|()
r82: +(|8|(),|1|()) -> |9|()
r83: +(|8|(),|2|()) -> c(|1|(),|0|())
r84: +(|8|(),|3|()) -> c(|1|(),|1|())
r85: +(|8|(),|4|()) -> c(|1|(),|2|())
r86: +(|8|(),|5|()) -> c(|1|(),|3|())
r87: +(|8|(),|6|()) -> c(|1|(),|4|())
r88: +(|8|(),|7|()) -> c(|1|(),|5|())
r89: +(|8|(),|8|()) -> c(|1|(),|6|())
r90: +(|8|(),|9|()) -> c(|1|(),|7|())
r91: +(|9|(),|0|()) -> |9|()
r92: +(|9|(),|1|()) -> c(|1|(),|0|())
r93: +(|9|(),|2|()) -> c(|1|(),|1|())
r94: +(|9|(),|3|()) -> c(|1|(),|2|())
r95: +(|9|(),|4|()) -> c(|1|(),|3|())
r96: +(|9|(),|5|()) -> c(|1|(),|4|())
r97: +(|9|(),|6|()) -> c(|1|(),|5|())
r98: +(|9|(),|7|()) -> c(|1|(),|6|())
r99: +(|9|(),|8|()) -> c(|1|(),|7|())
r100: +(|9|(),|9|()) -> c(|1|(),|8|())
r101: +(x,c(y,z)) -> c(y,+(x,z))
r102: +(c(x,y),z) -> c(x,+(y,z))
r103: c(|0|(),x) -> x
r104: c(x,c(y,z)) -> c(+(x,y),z)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          c#_A(x1,x2) = x2 + 1
          c_A(x1,x2) = max{x1, x2}
          +_A(x1,x2) = max{x1, x2}
          |0|_A = 1
          |1|_A = 1
          |2|_A = 1
          |3|_A = 1
          |4|_A = 1
          |5|_A = 1
          |6|_A = 1
          |7|_A = 1
          |8|_A = 1
          |9|_A = 1
    
      precedence:
      
        c# = + = |2| = |7| = |8| = |9| > |6| > c = |0| = |1| = |3| = |4| = |5|
      
      partial status:
    
        pi(c#) = [2]
        pi(c) = [2]
        pi(+) = [1, 2]
        pi(|0|) = []
        pi(|1|) = []
        pi(|2|) = []
        pi(|3|) = []
        pi(|4|) = []
        pi(|5|) = []
        pi(|6|) = []
        pi(|7|) = []
        pi(|8|) = []
        pi(|9|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          c#_A(x1,x2) = x2 + 26
          c_A(x1,x2) = max{24, x2}
          +_A(x1,x2) = x1 + 24
          |0|_A = 36
          |1|_A = 54
          |2|_A = 1
          |3|_A = 18
          |4|_A = 23
          |5|_A = 12
          |6|_A = 22
          |7|_A = 0
          |8|_A = 45
          |9|_A = 21
    
      precedence:
      
        c = + = |0| = |1| = |2| = |3| = |4| = |5| = |6| = |7| = |8| > c# = |9|
      
      partial status:
    
        pi(c#) = [2]
        pi(c) = []
        pi(+) = []
        pi(|0|) = []
        pi(|1|) = []
        pi(|2|) = []
        pi(|3|) = []
        pi(|4|) = []
        pi(|5|) = []
        pi(|6|) = []
        pi(|7|) = []
        pi(|8|) = []
        pi(|9|) = []
    

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: +#(c(x,y),z) -> +#(y,z)
p2: +#(x,c(y,z)) -> +#(x,z)

and R consists of:

r1: +(|0|(),|0|()) -> |0|()
r2: +(|0|(),|1|()) -> |1|()
r3: +(|0|(),|2|()) -> |2|()
r4: +(|0|(),|3|()) -> |3|()
r5: +(|0|(),|4|()) -> |4|()
r6: +(|0|(),|5|()) -> |5|()
r7: +(|0|(),|6|()) -> |6|()
r8: +(|0|(),|7|()) -> |7|()
r9: +(|0|(),|8|()) -> |8|()
r10: +(|0|(),|9|()) -> |9|()
r11: +(|1|(),|0|()) -> |1|()
r12: +(|1|(),|1|()) -> |2|()
r13: +(|1|(),|2|()) -> |3|()
r14: +(|1|(),|3|()) -> |4|()
r15: +(|1|(),|4|()) -> |5|()
r16: +(|1|(),|5|()) -> |6|()
r17: +(|1|(),|6|()) -> |7|()
r18: +(|1|(),|7|()) -> |8|()
r19: +(|1|(),|8|()) -> |9|()
r20: +(|1|(),|9|()) -> c(|1|(),|0|())
r21: +(|2|(),|0|()) -> |2|()
r22: +(|2|(),|1|()) -> |3|()
r23: +(|2|(),|2|()) -> |4|()
r24: +(|2|(),|3|()) -> |5|()
r25: +(|2|(),|4|()) -> |6|()
r26: +(|2|(),|5|()) -> |7|()
r27: +(|2|(),|6|()) -> |8|()
r28: +(|2|(),|7|()) -> |9|()
r29: +(|2|(),|8|()) -> c(|1|(),|0|())
r30: +(|2|(),|9|()) -> c(|1|(),|1|())
r31: +(|3|(),|0|()) -> |3|()
r32: +(|3|(),|1|()) -> |4|()
r33: +(|3|(),|2|()) -> |5|()
r34: +(|3|(),|3|()) -> |6|()
r35: +(|3|(),|4|()) -> |7|()
r36: +(|3|(),|5|()) -> |8|()
r37: +(|3|(),|6|()) -> |9|()
r38: +(|3|(),|7|()) -> c(|1|(),|0|())
r39: +(|3|(),|8|()) -> c(|1|(),|1|())
r40: +(|3|(),|9|()) -> c(|1|(),|2|())
r41: +(|4|(),|0|()) -> |4|()
r42: +(|4|(),|1|()) -> |5|()
r43: +(|4|(),|2|()) -> |6|()
r44: +(|4|(),|3|()) -> |7|()
r45: +(|4|(),|4|()) -> |8|()
r46: +(|4|(),|5|()) -> |9|()
r47: +(|4|(),|6|()) -> c(|1|(),|0|())
r48: +(|4|(),|7|()) -> c(|1|(),|1|())
r49: +(|4|(),|8|()) -> c(|1|(),|2|())
r50: +(|4|(),|9|()) -> c(|1|(),|3|())
r51: +(|5|(),|0|()) -> |5|()
r52: +(|5|(),|1|()) -> |6|()
r53: +(|5|(),|2|()) -> |7|()
r54: +(|5|(),|3|()) -> |8|()
r55: +(|5|(),|4|()) -> |9|()
r56: +(|5|(),|5|()) -> c(|1|(),|0|())
r57: +(|5|(),|6|()) -> c(|1|(),|1|())
r58: +(|5|(),|7|()) -> c(|1|(),|2|())
r59: +(|5|(),|8|()) -> c(|1|(),|3|())
r60: +(|5|(),|9|()) -> c(|1|(),|4|())
r61: +(|6|(),|0|()) -> |6|()
r62: +(|6|(),|1|()) -> |7|()
r63: +(|6|(),|2|()) -> |8|()
r64: +(|6|(),|3|()) -> |9|()
r65: +(|6|(),|4|()) -> c(|1|(),|0|())
r66: +(|6|(),|5|()) -> c(|1|(),|1|())
r67: +(|6|(),|6|()) -> c(|1|(),|2|())
r68: +(|6|(),|7|()) -> c(|1|(),|3|())
r69: +(|6|(),|8|()) -> c(|1|(),|4|())
r70: +(|6|(),|9|()) -> c(|1|(),|5|())
r71: +(|7|(),|0|()) -> |7|()
r72: +(|7|(),|1|()) -> |8|()
r73: +(|7|(),|2|()) -> |9|()
r74: +(|7|(),|3|()) -> c(|1|(),|0|())
r75: +(|7|(),|4|()) -> c(|1|(),|1|())
r76: +(|7|(),|5|()) -> c(|1|(),|2|())
r77: +(|7|(),|6|()) -> c(|1|(),|3|())
r78: +(|7|(),|7|()) -> c(|1|(),|4|())
r79: +(|7|(),|8|()) -> c(|1|(),|5|())
r80: +(|7|(),|9|()) -> c(|1|(),|6|())
r81: +(|8|(),|0|()) -> |8|()
r82: +(|8|(),|1|()) -> |9|()
r83: +(|8|(),|2|()) -> c(|1|(),|0|())
r84: +(|8|(),|3|()) -> c(|1|(),|1|())
r85: +(|8|(),|4|()) -> c(|1|(),|2|())
r86: +(|8|(),|5|()) -> c(|1|(),|3|())
r87: +(|8|(),|6|()) -> c(|1|(),|4|())
r88: +(|8|(),|7|()) -> c(|1|(),|5|())
r89: +(|8|(),|8|()) -> c(|1|(),|6|())
r90: +(|8|(),|9|()) -> c(|1|(),|7|())
r91: +(|9|(),|0|()) -> |9|()
r92: +(|9|(),|1|()) -> c(|1|(),|0|())
r93: +(|9|(),|2|()) -> c(|1|(),|1|())
r94: +(|9|(),|3|()) -> c(|1|(),|2|())
r95: +(|9|(),|4|()) -> c(|1|(),|3|())
r96: +(|9|(),|5|()) -> c(|1|(),|4|())
r97: +(|9|(),|6|()) -> c(|1|(),|5|())
r98: +(|9|(),|7|()) -> c(|1|(),|6|())
r99: +(|9|(),|8|()) -> c(|1|(),|7|())
r100: +(|9|(),|9|()) -> c(|1|(),|8|())
r101: +(x,c(y,z)) -> c(y,+(x,z))
r102: +(c(x,y),z) -> c(x,+(y,z))
r103: c(|0|(),x) -> x
r104: c(x,c(y,z)) -> c(+(x,y),z)

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{x1 + 1, x2 + 1}
          c_A(x1,x2) = x2
    
      precedence:
      
        +# = c
      
      partial status:
    
        pi(+#) = [1, 2]
        pi(c) = [2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          +#_A(x1,x2) = max{0, x1 - 2}
          c_A(x1,x2) = max{3, x2 + 1}
    
      precedence:
      
        +# = c
      
      partial status:
    
        pi(+#) = []
        pi(c) = [2]
    

The next rules are strictly ordered:

  p1, p2

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