YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

p1: c#(x,c(y,z)) -> c#(+(x,y),z)
p2: c#(x,c(y,z)) -> +#(x,y)
p3: +#(|1|(),|9|()) -> c#(|1|(),|0|())
p4: +#(|2|(),|8|()) -> c#(|1|(),|0|())
p5: +#(|2|(),|9|()) -> c#(|1|(),|1|())
p6: +#(|3|(),|7|()) -> c#(|1|(),|0|())
p7: +#(|3|(),|8|()) -> c#(|1|(),|1|())
p8: +#(|3|(),|9|()) -> c#(|1|(),|2|())
p9: +#(|4|(),|6|()) -> c#(|1|(),|0|())
p10: +#(|4|(),|7|()) -> c#(|1|(),|1|())
p11: +#(|4|(),|8|()) -> c#(|1|(),|2|())
p12: +#(|4|(),|9|()) -> c#(|1|(),|3|())
p13: +#(|5|(),|5|()) -> c#(|1|(),|0|())
p14: +#(|5|(),|6|()) -> c#(|1|(),|1|())
p15: +#(|5|(),|7|()) -> c#(|1|(),|2|())
p16: +#(|5|(),|8|()) -> c#(|1|(),|3|())
p17: +#(|5|(),|9|()) -> c#(|1|(),|4|())
p18: +#(|6|(),|4|()) -> c#(|1|(),|0|())
p19: +#(|6|(),|5|()) -> c#(|1|(),|1|())
p20: +#(|6|(),|6|()) -> c#(|1|(),|2|())
p21: +#(|6|(),|7|()) -> c#(|1|(),|3|())
p22: +#(|6|(),|8|()) -> c#(|1|(),|4|())
p23: +#(|6|(),|9|()) -> c#(|1|(),|5|())
p24: +#(|7|(),|3|()) -> c#(|1|(),|0|())
p25: +#(|7|(),|4|()) -> c#(|1|(),|1|())
p26: +#(|7|(),|5|()) -> c#(|1|(),|2|())
p27: +#(|7|(),|6|()) -> c#(|1|(),|3|())
p28: +#(|7|(),|7|()) -> c#(|1|(),|4|())
p29: +#(|7|(),|8|()) -> c#(|1|(),|5|())
p30: +#(|7|(),|9|()) -> c#(|1|(),|6|())
p31: +#(|8|(),|2|()) -> c#(|1|(),|0|())
p32: +#(|8|(),|3|()) -> c#(|1|(),|1|())
p33: +#(|8|(),|4|()) -> c#(|1|(),|2|())
p34: +#(|8|(),|5|()) -> c#(|1|(),|3|())
p35: +#(|8|(),|6|()) -> c#(|1|(),|4|())
p36: +#(|8|(),|7|()) -> c#(|1|(),|5|())
p37: +#(|8|(),|8|()) -> c#(|1|(),|6|())
p38: +#(|8|(),|9|()) -> c#(|1|(),|7|())
p39: +#(|9|(),|1|()) -> c#(|1|(),|0|())
p40: +#(|9|(),|2|()) -> c#(|1|(),|1|())
p41: +#(|9|(),|3|()) -> c#(|1|(),|2|())
p42: +#(|9|(),|4|()) -> c#(|1|(),|3|())
p43: +#(|9|(),|5|()) -> c#(|1|(),|4|())
p44: +#(|9|(),|6|()) -> c#(|1|(),|5|())
p45: +#(|9|(),|7|()) -> c#(|1|(),|6|())
p46: +#(|9|(),|8|()) -> c#(|1|(),|7|())
p47: +#(|9|(),|9|()) -> c#(|1|(),|8|())
p48: +#(x,c(y,z)) -> c#(y,+(x,z))
p49: +#(x,c(y,z)) -> +#(x,z)
p50: +#(c(x,y),z) -> c#(x,+(y,z))
p51: +#(c(x,y),z) -> +#(y,z)
p52: *#(|2|(),|5|()) -> c#(|1|(),|0|())
p53: *#(|2|(),|6|()) -> c#(|1|(),|2|())
p54: *#(|2|(),|7|()) -> c#(|1|(),|4|())
p55: *#(|2|(),|8|()) -> c#(|1|(),|6|())
p56: *#(|2|(),|9|()) -> c#(|1|(),|8|())
p57: *#(|3|(),|4|()) -> c#(|1|(),|2|())
p58: *#(|3|(),|5|()) -> c#(|1|(),|5|())
p59: *#(|3|(),|6|()) -> c#(|1|(),|8|())
p60: *#(|3|(),|7|()) -> c#(|2|(),|1|())
p61: *#(|3|(),|8|()) -> c#(|2|(),|4|())
p62: *#(|3|(),|9|()) -> c#(|2|(),|7|())
p63: *#(|4|(),|3|()) -> c#(|1|(),|2|())
p64: *#(|4|(),|4|()) -> c#(|1|(),|6|())
p65: *#(|4|(),|5|()) -> c#(|2|(),|0|())
p66: *#(|4|(),|6|()) -> c#(|2|(),|4|())
p67: *#(|4|(),|7|()) -> c#(|2|(),|8|())
p68: *#(|4|(),|8|()) -> c#(|3|(),|2|())
p69: *#(|4|(),|9|()) -> c#(|3|(),|6|())
p70: *#(|5|(),|2|()) -> c#(|1|(),|0|())
p71: *#(|5|(),|3|()) -> c#(|1|(),|5|())
p72: *#(|5|(),|4|()) -> c#(|2|(),|0|())
p73: *#(|5|(),|5|()) -> c#(|2|(),|5|())
p74: *#(|5|(),|6|()) -> c#(|3|(),|0|())
p75: *#(|5|(),|7|()) -> c#(|3|(),|5|())
p76: *#(|5|(),|8|()) -> c#(|4|(),|0|())
p77: *#(|5|(),|9|()) -> c#(|4|(),|5|())
p78: *#(|6|(),|2|()) -> c#(|1|(),|2|())
p79: *#(|6|(),|3|()) -> c#(|1|(),|8|())
p80: *#(|6|(),|4|()) -> c#(|2|(),|4|())
p81: *#(|6|(),|5|()) -> c#(|3|(),|0|())
p82: *#(|6|(),|6|()) -> c#(|3|(),|6|())
p83: *#(|6|(),|7|()) -> c#(|4|(),|2|())
p84: *#(|6|(),|8|()) -> c#(|4|(),|8|())
p85: *#(|6|(),|9|()) -> c#(|5|(),|4|())
p86: *#(|7|(),|2|()) -> c#(|1|(),|4|())
p87: *#(|7|(),|3|()) -> c#(|2|(),|1|())
p88: *#(|7|(),|4|()) -> c#(|2|(),|8|())
p89: *#(|7|(),|5|()) -> c#(|3|(),|5|())
p90: *#(|7|(),|6|()) -> c#(|4|(),|2|())
p91: *#(|7|(),|7|()) -> c#(|4|(),|9|())
p92: *#(|7|(),|8|()) -> c#(|5|(),|6|())
p93: *#(|7|(),|9|()) -> c#(|6|(),|3|())
p94: *#(|8|(),|2|()) -> c#(|1|(),|8|())
p95: *#(|8|(),|3|()) -> c#(|2|(),|4|())
p96: *#(|8|(),|4|()) -> c#(|3|(),|2|())
p97: *#(|8|(),|5|()) -> c#(|4|(),|0|())
p98: *#(|8|(),|6|()) -> c#(|4|(),|8|())
p99: *#(|8|(),|7|()) -> c#(|5|(),|6|())
p100: *#(|8|(),|8|()) -> c#(|6|(),|4|())
p101: *#(|8|(),|9|()) -> c#(|7|(),|2|())
p102: *#(|9|(),|2|()) -> c#(|1|(),|8|())
p103: *#(|9|(),|3|()) -> c#(|2|(),|7|())
p104: *#(|9|(),|4|()) -> c#(|3|(),|6|())
p105: *#(|9|(),|5|()) -> c#(|4|(),|5|())
p106: *#(|9|(),|6|()) -> c#(|5|(),|4|())
p107: *#(|9|(),|7|()) -> c#(|6|(),|3|())
p108: *#(|9|(),|8|()) -> c#(|7|(),|2|())
p109: *#(|9|(),|9|()) -> c#(|8|(),|1|())
p110: *#(x,c(y,z)) -> c#(*(x,y),*(x,z))
p111: *#(x,c(y,z)) -> *#(x,y)
p112: *#(x,c(y,z)) -> *#(x,z)
p113: *#(c(x,y),z) -> c#(*(x,z),*(y,z))
p114: *#(c(x,y),z) -> *#(x,z)
p115: *#(c(x,y),z) -> *#(y,z)

and R consists of:

r1: c(|0|(),x) -> x
r2: c(x,c(y,z)) -> c(+(x,y),z)
r3: +(|0|(),|0|()) -> |0|()
r4: +(|0|(),|1|()) -> |1|()
r5: +(|0|(),|2|()) -> |2|()
r6: +(|0|(),|3|()) -> |3|()
r7: +(|0|(),|4|()) -> |4|()
r8: +(|0|(),|5|()) -> |5|()
r9: +(|0|(),|6|()) -> |6|()
r10: +(|0|(),|7|()) -> |7|()
r11: +(|0|(),|8|()) -> |8|()
r12: +(|0|(),|9|()) -> |9|()
r13: +(|1|(),|0|()) -> |1|()
r14: +(|1|(),|1|()) -> |2|()
r15: +(|1|(),|2|()) -> |3|()
r16: +(|1|(),|3|()) -> |4|()
r17: +(|1|(),|4|()) -> |5|()
r18: +(|1|(),|5|()) -> |6|()
r19: +(|1|(),|6|()) -> |7|()
r20: +(|1|(),|7|()) -> |8|()
r21: +(|1|(),|8|()) -> |9|()
r22: +(|1|(),|9|()) -> c(|1|(),|0|())
r23: +(|2|(),|0|()) -> |2|()
r24: +(|2|(),|1|()) -> |3|()
r25: +(|2|(),|2|()) -> |4|()
r26: +(|2|(),|3|()) -> |5|()
r27: +(|2|(),|4|()) -> |6|()
r28: +(|2|(),|5|()) -> |7|()
r29: +(|2|(),|6|()) -> |8|()
r30: +(|2|(),|7|()) -> |9|()
r31: +(|2|(),|8|()) -> c(|1|(),|0|())
r32: +(|2|(),|9|()) -> c(|1|(),|1|())
r33: +(|3|(),|0|()) -> |3|()
r34: +(|3|(),|1|()) -> |4|()
r35: +(|3|(),|2|()) -> |5|()
r36: +(|3|(),|3|()) -> |6|()
r37: +(|3|(),|4|()) -> |7|()
r38: +(|3|(),|5|()) -> |8|()
r39: +(|3|(),|6|()) -> |9|()
r40: +(|3|(),|7|()) -> c(|1|(),|0|())
r41: +(|3|(),|8|()) -> c(|1|(),|1|())
r42: +(|3|(),|9|()) -> c(|1|(),|2|())
r43: +(|4|(),|0|()) -> |4|()
r44: +(|4|(),|1|()) -> |5|()
r45: +(|4|(),|2|()) -> |6|()
r46: +(|4|(),|3|()) -> |7|()
r47: +(|4|(),|4|()) -> |8|()
r48: +(|4|(),|5|()) -> |9|()
r49: +(|4|(),|6|()) -> c(|1|(),|0|())
r50: +(|4|(),|7|()) -> c(|1|(),|1|())
r51: +(|4|(),|8|()) -> c(|1|(),|2|())
r52: +(|4|(),|9|()) -> c(|1|(),|3|())
r53: +(|5|(),|0|()) -> |5|()
r54: +(|5|(),|1|()) -> |6|()
r55: +(|5|(),|2|()) -> |7|()
r56: +(|5|(),|3|()) -> |8|()
r57: +(|5|(),|4|()) -> |9|()
r58: +(|5|(),|5|()) -> c(|1|(),|0|())
r59: +(|5|(),|6|()) -> c(|1|(),|1|())
r60: +(|5|(),|7|()) -> c(|1|(),|2|())
r61: +(|5|(),|8|()) -> c(|1|(),|3|())
r62: +(|5|(),|9|()) -> c(|1|(),|4|())
r63: +(|6|(),|0|()) -> |6|()
r64: +(|6|(),|1|()) -> |7|()
r65: +(|6|(),|2|()) -> |8|()
r66: +(|6|(),|3|()) -> |9|()
r67: +(|6|(),|4|()) -> c(|1|(),|0|())
r68: +(|6|(),|5|()) -> c(|1|(),|1|())
r69: +(|6|(),|6|()) -> c(|1|(),|2|())
r70: +(|6|(),|7|()) -> c(|1|(),|3|())
r71: +(|6|(),|8|()) -> c(|1|(),|4|())
r72: +(|6|(),|9|()) -> c(|1|(),|5|())
r73: +(|7|(),|0|()) -> |7|()
r74: +(|7|(),|1|()) -> |8|()
r75: +(|7|(),|2|()) -> |9|()
r76: +(|7|(),|3|()) -> c(|1|(),|0|())
r77: +(|7|(),|4|()) -> c(|1|(),|1|())
r78: +(|7|(),|5|()) -> c(|1|(),|2|())
r79: +(|7|(),|6|()) -> c(|1|(),|3|())
r80: +(|7|(),|7|()) -> c(|1|(),|4|())
r81: +(|7|(),|8|()) -> c(|1|(),|5|())
r82: +(|7|(),|9|()) -> c(|1|(),|6|())
r83: +(|8|(),|0|()) -> |8|()
r84: +(|8|(),|1|()) -> |9|()
r85: +(|8|(),|2|()) -> c(|1|(),|0|())
r86: +(|8|(),|3|()) -> c(|1|(),|1|())
r87: +(|8|(),|4|()) -> c(|1|(),|2|())
r88: +(|8|(),|5|()) -> c(|1|(),|3|())
r89: +(|8|(),|6|()) -> c(|1|(),|4|())
r90: +(|8|(),|7|()) -> c(|1|(),|5|())
r91: +(|8|(),|8|()) -> c(|1|(),|6|())
r92: +(|8|(),|9|()) -> c(|1|(),|7|())
r93: +(|9|(),|0|()) -> |9|()
r94: +(|9|(),|1|()) -> c(|1|(),|0|())
r95: +(|9|(),|2|()) -> c(|1|(),|1|())
r96: +(|9|(),|3|()) -> c(|1|(),|2|())
r97: +(|9|(),|4|()) -> c(|1|(),|3|())
r98: +(|9|(),|5|()) -> c(|1|(),|4|())
r99: +(|9|(),|6|()) -> c(|1|(),|5|())
r100: +(|9|(),|7|()) -> c(|1|(),|6|())
r101: +(|9|(),|8|()) -> c(|1|(),|7|())
r102: +(|9|(),|9|()) -> c(|1|(),|8|())
r103: +(x,c(y,z)) -> c(y,+(x,z))
r104: +(c(x,y),z) -> c(x,+(y,z))
r105: *(|0|(),|0|()) -> |0|()
r106: *(|0|(),|1|()) -> |0|()
r107: *(|0|(),|2|()) -> |0|()
r108: *(|0|(),|3|()) -> |0|()
r109: *(|0|(),|4|()) -> |0|()
r110: *(|0|(),|5|()) -> |0|()
r111: *(|0|(),|6|()) -> |0|()
r112: *(|0|(),|7|()) -> |0|()
r113: *(|0|(),|8|()) -> |0|()
r114: *(|0|(),|9|()) -> |0|()
r115: *(|1|(),|0|()) -> |0|()
r116: *(|1|(),|1|()) -> |1|()
r117: *(|1|(),|2|()) -> |2|()
r118: *(|1|(),|3|()) -> |3|()
r119: *(|1|(),|4|()) -> |4|()
r120: *(|1|(),|5|()) -> |5|()
r121: *(|1|(),|6|()) -> |6|()
r122: *(|1|(),|7|()) -> |7|()
r123: *(|1|(),|8|()) -> |8|()
r124: *(|1|(),|9|()) -> |9|()
r125: *(|2|(),|0|()) -> |0|()
r126: *(|2|(),|1|()) -> |2|()
r127: *(|2|(),|2|()) -> |4|()
r128: *(|2|(),|3|()) -> |6|()
r129: *(|2|(),|4|()) -> |8|()
r130: *(|2|(),|5|()) -> c(|1|(),|0|())
r131: *(|2|(),|6|()) -> c(|1|(),|2|())
r132: *(|2|(),|7|()) -> c(|1|(),|4|())
r133: *(|2|(),|8|()) -> c(|1|(),|6|())
r134: *(|2|(),|9|()) -> c(|1|(),|8|())
r135: *(|3|(),|0|()) -> |0|()
r136: *(|3|(),|1|()) -> |3|()
r137: *(|3|(),|2|()) -> |6|()
r138: *(|3|(),|3|()) -> |9|()
r139: *(|3|(),|4|()) -> c(|1|(),|2|())
r140: *(|3|(),|5|()) -> c(|1|(),|5|())
r141: *(|3|(),|6|()) -> c(|1|(),|8|())
r142: *(|3|(),|7|()) -> c(|2|(),|1|())
r143: *(|3|(),|8|()) -> c(|2|(),|4|())
r144: *(|3|(),|9|()) -> c(|2|(),|7|())
r145: *(|4|(),|0|()) -> |0|()
r146: *(|4|(),|1|()) -> |4|()
r147: *(|4|(),|2|()) -> |8|()
r148: *(|4|(),|3|()) -> c(|1|(),|2|())
r149: *(|4|(),|4|()) -> c(|1|(),|6|())
r150: *(|4|(),|5|()) -> c(|2|(),|0|())
r151: *(|4|(),|6|()) -> c(|2|(),|4|())
r152: *(|4|(),|7|()) -> c(|2|(),|8|())
r153: *(|4|(),|8|()) -> c(|3|(),|2|())
r154: *(|4|(),|9|()) -> c(|3|(),|6|())
r155: *(|5|(),|0|()) -> |0|()
r156: *(|5|(),|1|()) -> |5|()
r157: *(|5|(),|2|()) -> c(|1|(),|0|())
r158: *(|5|(),|3|()) -> c(|1|(),|5|())
r159: *(|5|(),|4|()) -> c(|2|(),|0|())
r160: *(|5|(),|5|()) -> c(|2|(),|5|())
r161: *(|5|(),|6|()) -> c(|3|(),|0|())
r162: *(|5|(),|7|()) -> c(|3|(),|5|())
r163: *(|5|(),|8|()) -> c(|4|(),|0|())
r164: *(|5|(),|9|()) -> c(|4|(),|5|())
r165: *(|6|(),|0|()) -> |0|()
r166: *(|6|(),|1|()) -> |6|()
r167: *(|6|(),|2|()) -> c(|1|(),|2|())
r168: *(|6|(),|3|()) -> c(|1|(),|8|())
r169: *(|6|(),|4|()) -> c(|2|(),|4|())
r170: *(|6|(),|5|()) -> c(|3|(),|0|())
r171: *(|6|(),|6|()) -> c(|3|(),|6|())
r172: *(|6|(),|7|()) -> c(|4|(),|2|())
r173: *(|6|(),|8|()) -> c(|4|(),|8|())
r174: *(|6|(),|9|()) -> c(|5|(),|4|())
r175: *(|7|(),|0|()) -> |0|()
r176: *(|7|(),|1|()) -> |7|()
r177: *(|7|(),|2|()) -> c(|1|(),|4|())
r178: *(|7|(),|3|()) -> c(|2|(),|1|())
r179: *(|7|(),|4|()) -> c(|2|(),|8|())
r180: *(|7|(),|5|()) -> c(|3|(),|5|())
r181: *(|7|(),|6|()) -> c(|4|(),|2|())
r182: *(|7|(),|7|()) -> c(|4|(),|9|())
r183: *(|7|(),|8|()) -> c(|5|(),|6|())
r184: *(|7|(),|9|()) -> c(|6|(),|3|())
r185: *(|8|(),|0|()) -> |0|()
r186: *(|8|(),|1|()) -> |8|()
r187: *(|8|(),|2|()) -> c(|1|(),|8|())
r188: *(|8|(),|3|()) -> c(|2|(),|4|())
r189: *(|8|(),|4|()) -> c(|3|(),|2|())
r190: *(|8|(),|5|()) -> c(|4|(),|0|())
r191: *(|8|(),|6|()) -> c(|4|(),|8|())
r192: *(|8|(),|7|()) -> c(|5|(),|6|())
r193: *(|8|(),|8|()) -> c(|6|(),|4|())
r194: *(|8|(),|9|()) -> c(|7|(),|2|())
r195: *(|9|(),|0|()) -> |0|()
r196: *(|9|(),|1|()) -> |9|()
r197: *(|9|(),|2|()) -> c(|1|(),|8|())
r198: *(|9|(),|3|()) -> c(|2|(),|7|())
r199: *(|9|(),|4|()) -> c(|3|(),|6|())
r200: *(|9|(),|5|()) -> c(|4|(),|5|())
r201: *(|9|(),|6|()) -> c(|5|(),|4|())
r202: *(|9|(),|7|()) -> c(|6|(),|3|())
r203: *(|9|(),|8|()) -> c(|7|(),|2|())
r204: *(|9|(),|9|()) -> c(|8|(),|1|())
r205: *(x,c(y,z)) -> c(*(x,y),*(x,z))
r206: *(c(x,y),z) -> c(*(x,z),*(y,z))

The estimated dependency graph contains the following SCCs:

  {p111, p112, p114, p115}
  {p1, p2, p48, p49, p50, p51}


-- Reduction pair.

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

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

and R consists of:

r1: c(|0|(),x) -> x
r2: c(x,c(y,z)) -> c(+(x,y),z)
r3: +(|0|(),|0|()) -> |0|()
r4: +(|0|(),|1|()) -> |1|()
r5: +(|0|(),|2|()) -> |2|()
r6: +(|0|(),|3|()) -> |3|()
r7: +(|0|(),|4|()) -> |4|()
r8: +(|0|(),|5|()) -> |5|()
r9: +(|0|(),|6|()) -> |6|()
r10: +(|0|(),|7|()) -> |7|()
r11: +(|0|(),|8|()) -> |8|()
r12: +(|0|(),|9|()) -> |9|()
r13: +(|1|(),|0|()) -> |1|()
r14: +(|1|(),|1|()) -> |2|()
r15: +(|1|(),|2|()) -> |3|()
r16: +(|1|(),|3|()) -> |4|()
r17: +(|1|(),|4|()) -> |5|()
r18: +(|1|(),|5|()) -> |6|()
r19: +(|1|(),|6|()) -> |7|()
r20: +(|1|(),|7|()) -> |8|()
r21: +(|1|(),|8|()) -> |9|()
r22: +(|1|(),|9|()) -> c(|1|(),|0|())
r23: +(|2|(),|0|()) -> |2|()
r24: +(|2|(),|1|()) -> |3|()
r25: +(|2|(),|2|()) -> |4|()
r26: +(|2|(),|3|()) -> |5|()
r27: +(|2|(),|4|()) -> |6|()
r28: +(|2|(),|5|()) -> |7|()
r29: +(|2|(),|6|()) -> |8|()
r30: +(|2|(),|7|()) -> |9|()
r31: +(|2|(),|8|()) -> c(|1|(),|0|())
r32: +(|2|(),|9|()) -> c(|1|(),|1|())
r33: +(|3|(),|0|()) -> |3|()
r34: +(|3|(),|1|()) -> |4|()
r35: +(|3|(),|2|()) -> |5|()
r36: +(|3|(),|3|()) -> |6|()
r37: +(|3|(),|4|()) -> |7|()
r38: +(|3|(),|5|()) -> |8|()
r39: +(|3|(),|6|()) -> |9|()
r40: +(|3|(),|7|()) -> c(|1|(),|0|())
r41: +(|3|(),|8|()) -> c(|1|(),|1|())
r42: +(|3|(),|9|()) -> c(|1|(),|2|())
r43: +(|4|(),|0|()) -> |4|()
r44: +(|4|(),|1|()) -> |5|()
r45: +(|4|(),|2|()) -> |6|()
r46: +(|4|(),|3|()) -> |7|()
r47: +(|4|(),|4|()) -> |8|()
r48: +(|4|(),|5|()) -> |9|()
r49: +(|4|(),|6|()) -> c(|1|(),|0|())
r50: +(|4|(),|7|()) -> c(|1|(),|1|())
r51: +(|4|(),|8|()) -> c(|1|(),|2|())
r52: +(|4|(),|9|()) -> c(|1|(),|3|())
r53: +(|5|(),|0|()) -> |5|()
r54: +(|5|(),|1|()) -> |6|()
r55: +(|5|(),|2|()) -> |7|()
r56: +(|5|(),|3|()) -> |8|()
r57: +(|5|(),|4|()) -> |9|()
r58: +(|5|(),|5|()) -> c(|1|(),|0|())
r59: +(|5|(),|6|()) -> c(|1|(),|1|())
r60: +(|5|(),|7|()) -> c(|1|(),|2|())
r61: +(|5|(),|8|()) -> c(|1|(),|3|())
r62: +(|5|(),|9|()) -> c(|1|(),|4|())
r63: +(|6|(),|0|()) -> |6|()
r64: +(|6|(),|1|()) -> |7|()
r65: +(|6|(),|2|()) -> |8|()
r66: +(|6|(),|3|()) -> |9|()
r67: +(|6|(),|4|()) -> c(|1|(),|0|())
r68: +(|6|(),|5|()) -> c(|1|(),|1|())
r69: +(|6|(),|6|()) -> c(|1|(),|2|())
r70: +(|6|(),|7|()) -> c(|1|(),|3|())
r71: +(|6|(),|8|()) -> c(|1|(),|4|())
r72: +(|6|(),|9|()) -> c(|1|(),|5|())
r73: +(|7|(),|0|()) -> |7|()
r74: +(|7|(),|1|()) -> |8|()
r75: +(|7|(),|2|()) -> |9|()
r76: +(|7|(),|3|()) -> c(|1|(),|0|())
r77: +(|7|(),|4|()) -> c(|1|(),|1|())
r78: +(|7|(),|5|()) -> c(|1|(),|2|())
r79: +(|7|(),|6|()) -> c(|1|(),|3|())
r80: +(|7|(),|7|()) -> c(|1|(),|4|())
r81: +(|7|(),|8|()) -> c(|1|(),|5|())
r82: +(|7|(),|9|()) -> c(|1|(),|6|())
r83: +(|8|(),|0|()) -> |8|()
r84: +(|8|(),|1|()) -> |9|()
r85: +(|8|(),|2|()) -> c(|1|(),|0|())
r86: +(|8|(),|3|()) -> c(|1|(),|1|())
r87: +(|8|(),|4|()) -> c(|1|(),|2|())
r88: +(|8|(),|5|()) -> c(|1|(),|3|())
r89: +(|8|(),|6|()) -> c(|1|(),|4|())
r90: +(|8|(),|7|()) -> c(|1|(),|5|())
r91: +(|8|(),|8|()) -> c(|1|(),|6|())
r92: +(|8|(),|9|()) -> c(|1|(),|7|())
r93: +(|9|(),|0|()) -> |9|()
r94: +(|9|(),|1|()) -> c(|1|(),|0|())
r95: +(|9|(),|2|()) -> c(|1|(),|1|())
r96: +(|9|(),|3|()) -> c(|1|(),|2|())
r97: +(|9|(),|4|()) -> c(|1|(),|3|())
r98: +(|9|(),|5|()) -> c(|1|(),|4|())
r99: +(|9|(),|6|()) -> c(|1|(),|5|())
r100: +(|9|(),|7|()) -> c(|1|(),|6|())
r101: +(|9|(),|8|()) -> c(|1|(),|7|())
r102: +(|9|(),|9|()) -> c(|1|(),|8|())
r103: +(x,c(y,z)) -> c(y,+(x,z))
r104: +(c(x,y),z) -> c(x,+(y,z))
r105: *(|0|(),|0|()) -> |0|()
r106: *(|0|(),|1|()) -> |0|()
r107: *(|0|(),|2|()) -> |0|()
r108: *(|0|(),|3|()) -> |0|()
r109: *(|0|(),|4|()) -> |0|()
r110: *(|0|(),|5|()) -> |0|()
r111: *(|0|(),|6|()) -> |0|()
r112: *(|0|(),|7|()) -> |0|()
r113: *(|0|(),|8|()) -> |0|()
r114: *(|0|(),|9|()) -> |0|()
r115: *(|1|(),|0|()) -> |0|()
r116: *(|1|(),|1|()) -> |1|()
r117: *(|1|(),|2|()) -> |2|()
r118: *(|1|(),|3|()) -> |3|()
r119: *(|1|(),|4|()) -> |4|()
r120: *(|1|(),|5|()) -> |5|()
r121: *(|1|(),|6|()) -> |6|()
r122: *(|1|(),|7|()) -> |7|()
r123: *(|1|(),|8|()) -> |8|()
r124: *(|1|(),|9|()) -> |9|()
r125: *(|2|(),|0|()) -> |0|()
r126: *(|2|(),|1|()) -> |2|()
r127: *(|2|(),|2|()) -> |4|()
r128: *(|2|(),|3|()) -> |6|()
r129: *(|2|(),|4|()) -> |8|()
r130: *(|2|(),|5|()) -> c(|1|(),|0|())
r131: *(|2|(),|6|()) -> c(|1|(),|2|())
r132: *(|2|(),|7|()) -> c(|1|(),|4|())
r133: *(|2|(),|8|()) -> c(|1|(),|6|())
r134: *(|2|(),|9|()) -> c(|1|(),|8|())
r135: *(|3|(),|0|()) -> |0|()
r136: *(|3|(),|1|()) -> |3|()
r137: *(|3|(),|2|()) -> |6|()
r138: *(|3|(),|3|()) -> |9|()
r139: *(|3|(),|4|()) -> c(|1|(),|2|())
r140: *(|3|(),|5|()) -> c(|1|(),|5|())
r141: *(|3|(),|6|()) -> c(|1|(),|8|())
r142: *(|3|(),|7|()) -> c(|2|(),|1|())
r143: *(|3|(),|8|()) -> c(|2|(),|4|())
r144: *(|3|(),|9|()) -> c(|2|(),|7|())
r145: *(|4|(),|0|()) -> |0|()
r146: *(|4|(),|1|()) -> |4|()
r147: *(|4|(),|2|()) -> |8|()
r148: *(|4|(),|3|()) -> c(|1|(),|2|())
r149: *(|4|(),|4|()) -> c(|1|(),|6|())
r150: *(|4|(),|5|()) -> c(|2|(),|0|())
r151: *(|4|(),|6|()) -> c(|2|(),|4|())
r152: *(|4|(),|7|()) -> c(|2|(),|8|())
r153: *(|4|(),|8|()) -> c(|3|(),|2|())
r154: *(|4|(),|9|()) -> c(|3|(),|6|())
r155: *(|5|(),|0|()) -> |0|()
r156: *(|5|(),|1|()) -> |5|()
r157: *(|5|(),|2|()) -> c(|1|(),|0|())
r158: *(|5|(),|3|()) -> c(|1|(),|5|())
r159: *(|5|(),|4|()) -> c(|2|(),|0|())
r160: *(|5|(),|5|()) -> c(|2|(),|5|())
r161: *(|5|(),|6|()) -> c(|3|(),|0|())
r162: *(|5|(),|7|()) -> c(|3|(),|5|())
r163: *(|5|(),|8|()) -> c(|4|(),|0|())
r164: *(|5|(),|9|()) -> c(|4|(),|5|())
r165: *(|6|(),|0|()) -> |0|()
r166: *(|6|(),|1|()) -> |6|()
r167: *(|6|(),|2|()) -> c(|1|(),|2|())
r168: *(|6|(),|3|()) -> c(|1|(),|8|())
r169: *(|6|(),|4|()) -> c(|2|(),|4|())
r170: *(|6|(),|5|()) -> c(|3|(),|0|())
r171: *(|6|(),|6|()) -> c(|3|(),|6|())
r172: *(|6|(),|7|()) -> c(|4|(),|2|())
r173: *(|6|(),|8|()) -> c(|4|(),|8|())
r174: *(|6|(),|9|()) -> c(|5|(),|4|())
r175: *(|7|(),|0|()) -> |0|()
r176: *(|7|(),|1|()) -> |7|()
r177: *(|7|(),|2|()) -> c(|1|(),|4|())
r178: *(|7|(),|3|()) -> c(|2|(),|1|())
r179: *(|7|(),|4|()) -> c(|2|(),|8|())
r180: *(|7|(),|5|()) -> c(|3|(),|5|())
r181: *(|7|(),|6|()) -> c(|4|(),|2|())
r182: *(|7|(),|7|()) -> c(|4|(),|9|())
r183: *(|7|(),|8|()) -> c(|5|(),|6|())
r184: *(|7|(),|9|()) -> c(|6|(),|3|())
r185: *(|8|(),|0|()) -> |0|()
r186: *(|8|(),|1|()) -> |8|()
r187: *(|8|(),|2|()) -> c(|1|(),|8|())
r188: *(|8|(),|3|()) -> c(|2|(),|4|())
r189: *(|8|(),|4|()) -> c(|3|(),|2|())
r190: *(|8|(),|5|()) -> c(|4|(),|0|())
r191: *(|8|(),|6|()) -> c(|4|(),|8|())
r192: *(|8|(),|7|()) -> c(|5|(),|6|())
r193: *(|8|(),|8|()) -> c(|6|(),|4|())
r194: *(|8|(),|9|()) -> c(|7|(),|2|())
r195: *(|9|(),|0|()) -> |0|()
r196: *(|9|(),|1|()) -> |9|()
r197: *(|9|(),|2|()) -> c(|1|(),|8|())
r198: *(|9|(),|3|()) -> c(|2|(),|7|())
r199: *(|9|(),|4|()) -> c(|3|(),|6|())
r200: *(|9|(),|5|()) -> c(|4|(),|5|())
r201: *(|9|(),|6|()) -> c(|5|(),|4|())
r202: *(|9|(),|7|()) -> c(|6|(),|3|())
r203: *(|9|(),|8|()) -> c(|7|(),|2|())
r204: *(|9|(),|9|()) -> c(|8|(),|1|())
r205: *(x,c(y,z)) -> c(*(x,y),*(x,z))
r206: *(c(x,y),z) -> c(*(x,z),*(y,z))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      *#_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + x2
      c_A(x1,x2) = ((1,0,0),(1,1,0),(1,1,1)) x1 + ((1,0,0),(0,0,0),(1,1,0)) x2 + (1,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: c#(x,c(y,z)) -> c#(+(x,y),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: +#(x,c(y,z)) -> +#(x,z)
p6: +#(x,c(y,z)) -> c#(y,+(x,z))

and R consists of:

r1: c(|0|(),x) -> x
r2: c(x,c(y,z)) -> c(+(x,y),z)
r3: +(|0|(),|0|()) -> |0|()
r4: +(|0|(),|1|()) -> |1|()
r5: +(|0|(),|2|()) -> |2|()
r6: +(|0|(),|3|()) -> |3|()
r7: +(|0|(),|4|()) -> |4|()
r8: +(|0|(),|5|()) -> |5|()
r9: +(|0|(),|6|()) -> |6|()
r10: +(|0|(),|7|()) -> |7|()
r11: +(|0|(),|8|()) -> |8|()
r12: +(|0|(),|9|()) -> |9|()
r13: +(|1|(),|0|()) -> |1|()
r14: +(|1|(),|1|()) -> |2|()
r15: +(|1|(),|2|()) -> |3|()
r16: +(|1|(),|3|()) -> |4|()
r17: +(|1|(),|4|()) -> |5|()
r18: +(|1|(),|5|()) -> |6|()
r19: +(|1|(),|6|()) -> |7|()
r20: +(|1|(),|7|()) -> |8|()
r21: +(|1|(),|8|()) -> |9|()
r22: +(|1|(),|9|()) -> c(|1|(),|0|())
r23: +(|2|(),|0|()) -> |2|()
r24: +(|2|(),|1|()) -> |3|()
r25: +(|2|(),|2|()) -> |4|()
r26: +(|2|(),|3|()) -> |5|()
r27: +(|2|(),|4|()) -> |6|()
r28: +(|2|(),|5|()) -> |7|()
r29: +(|2|(),|6|()) -> |8|()
r30: +(|2|(),|7|()) -> |9|()
r31: +(|2|(),|8|()) -> c(|1|(),|0|())
r32: +(|2|(),|9|()) -> c(|1|(),|1|())
r33: +(|3|(),|0|()) -> |3|()
r34: +(|3|(),|1|()) -> |4|()
r35: +(|3|(),|2|()) -> |5|()
r36: +(|3|(),|3|()) -> |6|()
r37: +(|3|(),|4|()) -> |7|()
r38: +(|3|(),|5|()) -> |8|()
r39: +(|3|(),|6|()) -> |9|()
r40: +(|3|(),|7|()) -> c(|1|(),|0|())
r41: +(|3|(),|8|()) -> c(|1|(),|1|())
r42: +(|3|(),|9|()) -> c(|1|(),|2|())
r43: +(|4|(),|0|()) -> |4|()
r44: +(|4|(),|1|()) -> |5|()
r45: +(|4|(),|2|()) -> |6|()
r46: +(|4|(),|3|()) -> |7|()
r47: +(|4|(),|4|()) -> |8|()
r48: +(|4|(),|5|()) -> |9|()
r49: +(|4|(),|6|()) -> c(|1|(),|0|())
r50: +(|4|(),|7|()) -> c(|1|(),|1|())
r51: +(|4|(),|8|()) -> c(|1|(),|2|())
r52: +(|4|(),|9|()) -> c(|1|(),|3|())
r53: +(|5|(),|0|()) -> |5|()
r54: +(|5|(),|1|()) -> |6|()
r55: +(|5|(),|2|()) -> |7|()
r56: +(|5|(),|3|()) -> |8|()
r57: +(|5|(),|4|()) -> |9|()
r58: +(|5|(),|5|()) -> c(|1|(),|0|())
r59: +(|5|(),|6|()) -> c(|1|(),|1|())
r60: +(|5|(),|7|()) -> c(|1|(),|2|())
r61: +(|5|(),|8|()) -> c(|1|(),|3|())
r62: +(|5|(),|9|()) -> c(|1|(),|4|())
r63: +(|6|(),|0|()) -> |6|()
r64: +(|6|(),|1|()) -> |7|()
r65: +(|6|(),|2|()) -> |8|()
r66: +(|6|(),|3|()) -> |9|()
r67: +(|6|(),|4|()) -> c(|1|(),|0|())
r68: +(|6|(),|5|()) -> c(|1|(),|1|())
r69: +(|6|(),|6|()) -> c(|1|(),|2|())
r70: +(|6|(),|7|()) -> c(|1|(),|3|())
r71: +(|6|(),|8|()) -> c(|1|(),|4|())
r72: +(|6|(),|9|()) -> c(|1|(),|5|())
r73: +(|7|(),|0|()) -> |7|()
r74: +(|7|(),|1|()) -> |8|()
r75: +(|7|(),|2|()) -> |9|()
r76: +(|7|(),|3|()) -> c(|1|(),|0|())
r77: +(|7|(),|4|()) -> c(|1|(),|1|())
r78: +(|7|(),|5|()) -> c(|1|(),|2|())
r79: +(|7|(),|6|()) -> c(|1|(),|3|())
r80: +(|7|(),|7|()) -> c(|1|(),|4|())
r81: +(|7|(),|8|()) -> c(|1|(),|5|())
r82: +(|7|(),|9|()) -> c(|1|(),|6|())
r83: +(|8|(),|0|()) -> |8|()
r84: +(|8|(),|1|()) -> |9|()
r85: +(|8|(),|2|()) -> c(|1|(),|0|())
r86: +(|8|(),|3|()) -> c(|1|(),|1|())
r87: +(|8|(),|4|()) -> c(|1|(),|2|())
r88: +(|8|(),|5|()) -> c(|1|(),|3|())
r89: +(|8|(),|6|()) -> c(|1|(),|4|())
r90: +(|8|(),|7|()) -> c(|1|(),|5|())
r91: +(|8|(),|8|()) -> c(|1|(),|6|())
r92: +(|8|(),|9|()) -> c(|1|(),|7|())
r93: +(|9|(),|0|()) -> |9|()
r94: +(|9|(),|1|()) -> c(|1|(),|0|())
r95: +(|9|(),|2|()) -> c(|1|(),|1|())
r96: +(|9|(),|3|()) -> c(|1|(),|2|())
r97: +(|9|(),|4|()) -> c(|1|(),|3|())
r98: +(|9|(),|5|()) -> c(|1|(),|4|())
r99: +(|9|(),|6|()) -> c(|1|(),|5|())
r100: +(|9|(),|7|()) -> c(|1|(),|6|())
r101: +(|9|(),|8|()) -> c(|1|(),|7|())
r102: +(|9|(),|9|()) -> c(|1|(),|8|())
r103: +(x,c(y,z)) -> c(y,+(x,z))
r104: +(c(x,y),z) -> c(x,+(y,z))
r105: *(|0|(),|0|()) -> |0|()
r106: *(|0|(),|1|()) -> |0|()
r107: *(|0|(),|2|()) -> |0|()
r108: *(|0|(),|3|()) -> |0|()
r109: *(|0|(),|4|()) -> |0|()
r110: *(|0|(),|5|()) -> |0|()
r111: *(|0|(),|6|()) -> |0|()
r112: *(|0|(),|7|()) -> |0|()
r113: *(|0|(),|8|()) -> |0|()
r114: *(|0|(),|9|()) -> |0|()
r115: *(|1|(),|0|()) -> |0|()
r116: *(|1|(),|1|()) -> |1|()
r117: *(|1|(),|2|()) -> |2|()
r118: *(|1|(),|3|()) -> |3|()
r119: *(|1|(),|4|()) -> |4|()
r120: *(|1|(),|5|()) -> |5|()
r121: *(|1|(),|6|()) -> |6|()
r122: *(|1|(),|7|()) -> |7|()
r123: *(|1|(),|8|()) -> |8|()
r124: *(|1|(),|9|()) -> |9|()
r125: *(|2|(),|0|()) -> |0|()
r126: *(|2|(),|1|()) -> |2|()
r127: *(|2|(),|2|()) -> |4|()
r128: *(|2|(),|3|()) -> |6|()
r129: *(|2|(),|4|()) -> |8|()
r130: *(|2|(),|5|()) -> c(|1|(),|0|())
r131: *(|2|(),|6|()) -> c(|1|(),|2|())
r132: *(|2|(),|7|()) -> c(|1|(),|4|())
r133: *(|2|(),|8|()) -> c(|1|(),|6|())
r134: *(|2|(),|9|()) -> c(|1|(),|8|())
r135: *(|3|(),|0|()) -> |0|()
r136: *(|3|(),|1|()) -> |3|()
r137: *(|3|(),|2|()) -> |6|()
r138: *(|3|(),|3|()) -> |9|()
r139: *(|3|(),|4|()) -> c(|1|(),|2|())
r140: *(|3|(),|5|()) -> c(|1|(),|5|())
r141: *(|3|(),|6|()) -> c(|1|(),|8|())
r142: *(|3|(),|7|()) -> c(|2|(),|1|())
r143: *(|3|(),|8|()) -> c(|2|(),|4|())
r144: *(|3|(),|9|()) -> c(|2|(),|7|())
r145: *(|4|(),|0|()) -> |0|()
r146: *(|4|(),|1|()) -> |4|()
r147: *(|4|(),|2|()) -> |8|()
r148: *(|4|(),|3|()) -> c(|1|(),|2|())
r149: *(|4|(),|4|()) -> c(|1|(),|6|())
r150: *(|4|(),|5|()) -> c(|2|(),|0|())
r151: *(|4|(),|6|()) -> c(|2|(),|4|())
r152: *(|4|(),|7|()) -> c(|2|(),|8|())
r153: *(|4|(),|8|()) -> c(|3|(),|2|())
r154: *(|4|(),|9|()) -> c(|3|(),|6|())
r155: *(|5|(),|0|()) -> |0|()
r156: *(|5|(),|1|()) -> |5|()
r157: *(|5|(),|2|()) -> c(|1|(),|0|())
r158: *(|5|(),|3|()) -> c(|1|(),|5|())
r159: *(|5|(),|4|()) -> c(|2|(),|0|())
r160: *(|5|(),|5|()) -> c(|2|(),|5|())
r161: *(|5|(),|6|()) -> c(|3|(),|0|())
r162: *(|5|(),|7|()) -> c(|3|(),|5|())
r163: *(|5|(),|8|()) -> c(|4|(),|0|())
r164: *(|5|(),|9|()) -> c(|4|(),|5|())
r165: *(|6|(),|0|()) -> |0|()
r166: *(|6|(),|1|()) -> |6|()
r167: *(|6|(),|2|()) -> c(|1|(),|2|())
r168: *(|6|(),|3|()) -> c(|1|(),|8|())
r169: *(|6|(),|4|()) -> c(|2|(),|4|())
r170: *(|6|(),|5|()) -> c(|3|(),|0|())
r171: *(|6|(),|6|()) -> c(|3|(),|6|())
r172: *(|6|(),|7|()) -> c(|4|(),|2|())
r173: *(|6|(),|8|()) -> c(|4|(),|8|())
r174: *(|6|(),|9|()) -> c(|5|(),|4|())
r175: *(|7|(),|0|()) -> |0|()
r176: *(|7|(),|1|()) -> |7|()
r177: *(|7|(),|2|()) -> c(|1|(),|4|())
r178: *(|7|(),|3|()) -> c(|2|(),|1|())
r179: *(|7|(),|4|()) -> c(|2|(),|8|())
r180: *(|7|(),|5|()) -> c(|3|(),|5|())
r181: *(|7|(),|6|()) -> c(|4|(),|2|())
r182: *(|7|(),|7|()) -> c(|4|(),|9|())
r183: *(|7|(),|8|()) -> c(|5|(),|6|())
r184: *(|7|(),|9|()) -> c(|6|(),|3|())
r185: *(|8|(),|0|()) -> |0|()
r186: *(|8|(),|1|()) -> |8|()
r187: *(|8|(),|2|()) -> c(|1|(),|8|())
r188: *(|8|(),|3|()) -> c(|2|(),|4|())
r189: *(|8|(),|4|()) -> c(|3|(),|2|())
r190: *(|8|(),|5|()) -> c(|4|(),|0|())
r191: *(|8|(),|6|()) -> c(|4|(),|8|())
r192: *(|8|(),|7|()) -> c(|5|(),|6|())
r193: *(|8|(),|8|()) -> c(|6|(),|4|())
r194: *(|8|(),|9|()) -> c(|7|(),|2|())
r195: *(|9|(),|0|()) -> |0|()
r196: *(|9|(),|1|()) -> |9|()
r197: *(|9|(),|2|()) -> c(|1|(),|8|())
r198: *(|9|(),|3|()) -> c(|2|(),|7|())
r199: *(|9|(),|4|()) -> c(|3|(),|6|())
r200: *(|9|(),|5|()) -> c(|4|(),|5|())
r201: *(|9|(),|6|()) -> c(|5|(),|4|())
r202: *(|9|(),|7|()) -> c(|6|(),|3|())
r203: *(|9|(),|8|()) -> c(|7|(),|2|())
r204: *(|9|(),|9|()) -> c(|8|(),|1|())
r205: *(x,c(y,z)) -> c(*(x,y),*(x,z))
r206: *(c(x,y),z) -> c(*(x,z),*(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:

  matrix interpretations:
  
    carrier: N^3
    order: lexicographic order
    interpretations:
      c#_A(x1,x2) = ((1,0,0),(1,1,0),(0,1,1)) x1 + ((1,0,0),(0,1,0),(1,0,1)) x2
      c_A(x1,x2) = ((1,0,0),(1,1,0),(1,0,1)) x1 + ((1,0,0),(0,0,0),(1,0,0)) x2 + (73,759,0)
      +_A(x1,x2) = ((1,0,0),(0,1,0),(1,1,1)) x1 + ((1,0,0),(1,1,0),(0,0,0)) x2 + (72,3,71)
      +#_A(x1,x2) = ((1,0,0),(0,0,0),(0,1,0)) x1 + x2 + (0,0,144)
      |0|_A() = (73,1049,0)
      |1|_A() = (35,1,1592)
      |2|_A() = (29,141,1458)
      |3|_A() = (27,143,0)
      |4|_A() = (129,1,0)
      |5|_A() = (123,271,0)
      |6|_A() = (33,399,1194)
      |7|_A() = (83,437,202)
      |8|_A() = (133,623,1698)
      |9|_A() = (127,663,794)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

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