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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      +#_A(x1,x2) = x1 + x2
      c_A(x1,x2) = x1 + x2 + 1
      c#_A(x1,x2) = x1 + x2
      +_A(x1,x2) = x1 + x2 + 1
      |0|_A() = 1
      |1|_A() = 1
      |2|_A() = 3
      |3|_A() = 2
      |4|_A() = 1
      |5|_A() = 3
      |6|_A() = 2
      |7|_A() = 1
      |8|_A() = 3
      |9|_A() = 5

The next rules are strictly ordered:

  p2, p3, p6
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r13, r14, r16, r17, r20, r21, r22, r23, r24, r25, r26, r27, r29, r30, r31, r32, r33, r34, r35, r36, r38, r39, r40, r41, r43, r44, r47, r50, r51, r52, r53, r54, r56, r57, r59, r60, r61, r62, r63, r65, r66, r69, r70, r71, r74, r80, r81, r83, r84, r86, r87, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r103

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: c(x,c(y,z)) -> c(+(x,y),z)
r2: +(|1|(),|1|()) -> |2|()
r3: +(|1|(),|4|()) -> |5|()
r4: +(|1|(),|7|()) -> |8|()
r5: +(|1|(),|8|()) -> |9|()
r6: +(|2|(),|7|()) -> |9|()
r7: +(|3|(),|6|()) -> |9|()
r8: +(|4|(),|1|()) -> |5|()
r9: +(|4|(),|4|()) -> |8|()
r10: +(|4|(),|5|()) -> |9|()
r11: +(|4|(),|7|()) -> c(|1|(),|1|())
r12: +(|4|(),|8|()) -> c(|1|(),|2|())
r13: +(|5|(),|4|()) -> |9|()
r14: +(|5|(),|7|()) -> c(|1|(),|2|())
r15: +(|6|(),|3|()) -> |9|()
r16: +(|6|(),|6|()) -> c(|1|(),|2|())
r17: +(|6|(),|7|()) -> c(|1|(),|3|())
r18: +(|7|(),|1|()) -> |8|()
r19: +(|7|(),|2|()) -> |9|()
r20: +(|7|(),|4|()) -> c(|1|(),|1|())
r21: +(|7|(),|5|()) -> c(|1|(),|2|())
r22: +(|7|(),|6|()) -> c(|1|(),|3|())
r23: +(|7|(),|7|()) -> c(|1|(),|4|())
r24: +(|7|(),|8|()) -> c(|1|(),|5|())
r25: +(|8|(),|1|()) -> |9|()
r26: +(|8|(),|4|()) -> c(|1|(),|2|())
r27: +(|8|(),|7|()) -> c(|1|(),|5|())
r28: +(x,c(y,z)) -> c(y,+(x,z))
r29: +(c(x,y),z) -> c(x,+(y,z))

The estimated dependency graph contains the following SCCs:

  {p3}


-- 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: c(x,c(y,z)) -> c(+(x,y),z)
r2: +(|1|(),|1|()) -> |2|()
r3: +(|1|(),|4|()) -> |5|()
r4: +(|1|(),|7|()) -> |8|()
r5: +(|1|(),|8|()) -> |9|()
r6: +(|2|(),|7|()) -> |9|()
r7: +(|3|(),|6|()) -> |9|()
r8: +(|4|(),|1|()) -> |5|()
r9: +(|4|(),|4|()) -> |8|()
r10: +(|4|(),|5|()) -> |9|()
r11: +(|4|(),|7|()) -> c(|1|(),|1|())
r12: +(|4|(),|8|()) -> c(|1|(),|2|())
r13: +(|5|(),|4|()) -> |9|()
r14: +(|5|(),|7|()) -> c(|1|(),|2|())
r15: +(|6|(),|3|()) -> |9|()
r16: +(|6|(),|6|()) -> c(|1|(),|2|())
r17: +(|6|(),|7|()) -> c(|1|(),|3|())
r18: +(|7|(),|1|()) -> |8|()
r19: +(|7|(),|2|()) -> |9|()
r20: +(|7|(),|4|()) -> c(|1|(),|1|())
r21: +(|7|(),|5|()) -> c(|1|(),|2|())
r22: +(|7|(),|6|()) -> c(|1|(),|3|())
r23: +(|7|(),|7|()) -> c(|1|(),|4|())
r24: +(|7|(),|8|()) -> c(|1|(),|5|())
r25: +(|8|(),|1|()) -> |9|()
r26: +(|8|(),|4|()) -> c(|1|(),|2|())
r27: +(|8|(),|7|()) -> c(|1|(),|5|())
r28: +(x,c(y,z)) -> c(y,+(x,z))
r29: +(c(x,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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      c#_A(x1,x2) = x2
      c_A(x1,x2) = x1 + x2 + 1
      +_A(x1,x2) = x1 + x2 + 1
      |1|_A() = 0
      |2|_A() = 0
      |4|_A() = 0
      |5|_A() = 0
      |7|_A() = 0
      |8|_A() = 0
      |9|_A() = 0
      |3|_A() = 0
      |6|_A() = 0

The next rules are strictly ordered:

  p1

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