Consider the TRS R consisting of the rewrite rules

1: c(0,x) -> x
2: c(x,c(y,z)) -> c(x + y,z)
3: 0 + 0 -> 0
4: 0 + 1 -> 1
5: 0 + 2 -> 2
6: 0 + 3 -> 3
7: 0 + 4 -> 4
8: 0 + 5 -> 5
9: 0 + 6 -> 6
10: 0 + 7 -> 7
11: 0 + 8 -> 8
12: 0 + 9 -> 9
13: 1 + 0 -> 1
14: 1 + 1 -> 2
15: 1 + 2 -> 3
16: 1 + 3 -> 4
17: 1 + 4 -> 5
18: 1 + 5 -> 6
19: 1 + 6 -> 7
20: 1 + 7 -> 8
21: 1 + 8 -> 9
22: 1 + 9 -> c(1,0)
23: 2 + 0 -> 2
24: 2 + 1 -> 3
25: 2 + 2 -> 4
26: 2 + 3 -> 5
27: 2 + 4 -> 6
28: 2 + 5 -> 7
29: 2 + 6 -> 8
30: 2 + 7 -> 9
31: 2 + 8 -> c(1,0)
32: 2 + 9 -> c(1,1)
33: 3 + 0 -> 3
34: 3 + 1 -> 4
35: 3 + 2 -> 5
36: 3 + 3 -> 6
37: 3 + 4 -> 7
38: 3 + 5 -> 8
39: 3 + 6 -> 9
40: 3 + 7 -> c(1,0)
41: 3 + 8 -> c(1,1)
42: 3 + 9 -> c(1,2)
43: 4 + 0 -> 4
44: 4 + 1 -> 5
45: 4 + 2 -> 6
46: 4 + 3 -> 7
47: 4 + 4 -> 8
48: 4 + 5 -> 9
49: 4 + 6 -> c(1,0)
50: 4 + 7 -> c(1,1)
51: 4 + 8 -> c(1,2)
52: 4 + 9 -> c(1,3)
53: 5 + 0 -> 5
54: 5 + 1 -> 6
55: 5 + 2 -> 7
56: 5 + 3 -> 8
57: 5 + 4 -> 9
58: 5 + 5 -> c(1,0)
59: 5 + 6 -> c(1,1)
60: 5 + 7 -> c(1,2)
61: 5 + 8 -> c(1,3)
62: 5 + 9 -> c(1,4)
63: 6 + 0 -> 6
64: 6 + 1 -> 7
65: 6 + 2 -> 8
66: 6 + 3 -> 9
67: 6 + 4 -> c(1,0)
68: 6 + 5 -> c(1,1)
69: 6 + 6 -> c(1,2)
70: 6 + 7 -> c(1,3)
71: 6 + 8 -> c(1,4)
72: 6 + 9 -> c(1,5)
73: 7 + 0 -> 7
74: 7 + 1 -> 8
75: 7 + 2 -> 9
76: 7 + 3 -> c(1,0)
77: 7 + 4 -> c(1,1)
78: 7 + 5 -> c(1,2)
79: 7 + 6 -> c(1,3)
80: 7 + 7 -> c(1,4)
81: 7 + 8 -> c(1,5)
82: 7 + 9 -> c(1,6)
83: 8 + 0 -> 8
84: 8 + 1 -> 9
85: 8 + 2 -> c(1,0)
86: 8 + 3 -> c(1,1)
87: 8 + 4 -> c(1,2)
88: 8 + 5 -> c(1,3)
89: 8 + 6 -> c(1,4)
90: 8 + 7 -> c(1,5)
91: 8 + 8 -> c(1,6)
92: 8 + 9 -> c(1,7)
93: 9 + 0 -> 9
94: 9 + 1 -> c(1,0)
95: 9 + 2 -> c(1,1)
96: 9 + 3 -> c(1,2)
97: 9 + 4 -> c(1,3)
98: 9 + 5 -> c(1,4)
99: 9 + 6 -> c(1,5)
100: 9 + 7 -> c(1,6)
101: 9 + 8 -> c(1,7)
102: 9 + 9 -> c(1,8)
103: x + c(y,z) -> c(y,x + z)
104: c(x,y) + z -> c(x,y + z)
105: 0 * 0 -> 0
106: 0 * 1 -> 0
107: 0 * 2 -> 0
108: 0 * 3 -> 0
109: 0 * 4 -> 0
110: 0 * 5 -> 0
111: 0 * 6 -> 0
112: 0 * 7 -> 0
113: 0 * 8 -> 0
114: 0 * 9 -> 0
115: 1 * 0 -> 0
116: 1 * 1 -> 1
117: 1 * 2 -> 2
118: 1 * 3 -> 3
119: 1 * 4 -> 4
120: 1 * 5 -> 5
121: 1 * 6 -> 6
122: 1 * 7 -> 7
123: 1 * 8 -> 8
124: 1 * 9 -> 9
125: 2 * 0 -> 0
126: 2 * 1 -> 2
127: 2 * 2 -> 4
128: 2 * 3 -> 6
129: 2 * 4 -> 8
130: 2 * 5 -> c(1,0)
131: 2 * 6 -> c(1,2)
132: 2 * 7 -> c(1,4)
133: 2 * 8 -> c(1,6)
134: 2 * 9 -> c(1,8)
135: 3 * 0 -> 0
136: 3 * 1 -> 3
137: 3 * 2 -> 6
138: 3 * 3 -> 9
139: 3 * 4 -> c(1,2)
140: 3 * 5 -> c(1,5)
141: 3 * 6 -> c(1,8)
142: 3 * 7 -> c(2,1)
143: 3 * 8 -> c(2,4)
144: 3 * 9 -> c(2,7)
145: 4 * 0 -> 0
146: 4 * 1 -> 4
147: 4 * 2 -> 8
148: 4 * 3 -> c(1,2)
149: 4 * 4 -> c(1,6)
150: 4 * 5 -> c(2,0)
151: 4 * 6 -> c(2,4)
152: 4 * 7 -> c(2,8)
153: 4 * 8 -> c(3,2)
154: 4 * 9 -> c(3,6)
155: 5 * 0 -> 0
156: 5 * 1 -> 5
157: 5 * 2 -> c(1,0)
158: 5 * 3 -> c(1,5)
159: 5 * 4 -> c(2,0)
160: 5 * 5 -> c(2,5)
161: 5 * 6 -> c(3,0)
162: 5 * 7 -> c(3,5)
163: 5 * 8 -> c(4,0)
164: 5 * 9 -> c(4,5)
165: 6 * 0 -> 0
166: 6 * 1 -> 6
167: 6 * 2 -> c(1,2)
168: 6 * 3 -> c(1,8)
169: 6 * 4 -> c(2,4)
170: 6 * 5 -> c(3,0)
171: 6 * 6 -> c(3,6)
172: 6 * 7 -> c(4,2)
173: 6 * 8 -> c(4,8)
174: 6 * 9 -> c(5,4)
175: 7 * 0 -> 0
176: 7 * 1 -> 7
177: 7 * 2 -> c(1,4)
178: 7 * 3 -> c(2,1)
179: 7 * 4 -> c(2,8)
180: 7 * 5 -> c(3,5)
181: 7 * 6 -> c(4,2)
182: 7 * 7 -> c(4,9)
183: 7 * 8 -> c(5,6)
184: 7 * 9 -> c(6,3)
185: 8 * 0 -> 0
186: 8 * 1 -> 8
187: 8 * 2 -> c(1,8)
188: 8 * 3 -> c(2,4)
189: 8 * 4 -> c(3,2)
190: 8 * 5 -> c(4,0)
191: 8 * 6 -> c(4,8)
192: 8 * 7 -> c(5,6)
193: 8 * 8 -> c(6,4)
194: 8 * 9 -> c(7,2)
195: 9 * 0 -> 0
196: 9 * 1 -> 9
197: 9 * 2 -> c(1,8)
198: 9 * 3 -> c(2,7)
199: 9 * 4 -> c(3,6)
200: 9 * 5 -> c(4,5)
201: 9 * 6 -> c(5,4)
202: 9 * 7 -> c(6,3)
203: 9 * 8 -> c(7,2)
204: 9 * 9 -> c(8,1)
205: x * c(y,z) -> c(x * y,x * z)
206: c(x,y) * z -> c(x * z,y * z)

There are 115 dependency pairs:

207: C(x,c(y,z)) -> C(x + y,z)
208: C(x,c(y,z)) -> x +# y
209: 1 +# 9 -> C(1,0)
210: 2 +# 8 -> C(1,0)
211: 2 +# 9 -> C(1,1)
212: 3 +# 7 -> C(1,0)
213: 3 +# 8 -> C(1,1)
214: 3 +# 9 -> C(1,2)
215: 4 +# 6 -> C(1,0)
216: 4 +# 7 -> C(1,1)
217: 4 +# 8 -> C(1,2)
218: 4 +# 9 -> C(1,3)
219: 5 +# 5 -> C(1,0)
220: 5 +# 6 -> C(1,1)
221: 5 +# 7 -> C(1,2)
222: 5 +# 8 -> C(1,3)
223: 5 +# 9 -> C(1,4)
224: 6 +# 4 -> C(1,0)
225: 6 +# 5 -> C(1,1)
226: 6 +# 6 -> C(1,2)
227: 6 +# 7 -> C(1,3)
228: 6 +# 8 -> C(1,4)
229: 6 +# 9 -> C(1,5)
230: 7 +# 3 -> C(1,0)
231: 7 +# 4 -> C(1,1)
232: 7 +# 5 -> C(1,2)
233: 7 +# 6 -> C(1,3)
234: 7 +# 7 -> C(1,4)
235: 7 +# 8 -> C(1,5)
236: 7 +# 9 -> C(1,6)
237: 8 +# 2 -> C(1,0)
238: 8 +# 3 -> C(1,1)
239: 8 +# 4 -> C(1,2)
240: 8 +# 5 -> C(1,3)
241: 8 +# 6 -> C(1,4)
242: 8 +# 7 -> C(1,5)
243: 8 +# 8 -> C(1,6)
244: 8 +# 9 -> C(1,7)
245: 9 +# 1 -> C(1,0)
246: 9 +# 2 -> C(1,1)
247: 9 +# 3 -> C(1,2)
248: 9 +# 4 -> C(1,3)
249: 9 +# 5 -> C(1,4)
250: 9 +# 6 -> C(1,5)
251: 9 +# 7 -> C(1,6)
252: 9 +# 8 -> C(1,7)
253: 9 +# 9 -> C(1,8)
254: x +# c(y,z) -> C(y,x + z)
255: x +# c(y,z) -> x +# z
256: c(x,y) +# z -> C(x,y + z)
257: c(x,y) +# z -> y +# z
258: 2 *# 5 -> C(1,0)
259: 2 *# 6 -> C(1,2)
260: 2 *# 7 -> C(1,4)
261: 2 *# 8 -> C(1,6)
262: 2 *# 9 -> C(1,8)
263: 3 *# 4 -> C(1,2)
264: 3 *# 5 -> C(1,5)
265: 3 *# 6 -> C(1,8)
266: 3 *# 7 -> C(2,1)
267: 3 *# 8 -> C(2,4)
268: 3 *# 9 -> C(2,7)
269: 4 *# 3 -> C(1,2)
270: 4 *# 4 -> C(1,6)
271: 4 *# 5 -> C(2,0)
272: 4 *# 6 -> C(2,4)
273: 4 *# 7 -> C(2,8)
274: 4 *# 8 -> C(3,2)
275: 4 *# 9 -> C(3,6)
276: 5 *# 2 -> C(1,0)
277: 5 *# 3 -> C(1,5)
278: 5 *# 4 -> C(2,0)
279: 5 *# 5 -> C(2,5)
280: 5 *# 6 -> C(3,0)
281: 5 *# 7 -> C(3,5)
282: 5 *# 8 -> C(4,0)
283: 5 *# 9 -> C(4,5)
284: 6 *# 2 -> C(1,2)
285: 6 *# 3 -> C(1,8)
286: 6 *# 4 -> C(2,4)
287: 6 *# 5 -> C(3,0)
288: 6 *# 6 -> C(3,6)
289: 6 *# 7 -> C(4,2)
290: 6 *# 8 -> C(4,8)
291: 6 *# 9 -> C(5,4)
292: 7 *# 2 -> C(1,4)
293: 7 *# 3 -> C(2,1)
294: 7 *# 4 -> C(2,8)
295: 7 *# 5 -> C(3,5)
296: 7 *# 6 -> C(4,2)
297: 7 *# 7 -> C(4,9)
298: 7 *# 8 -> C(5,6)
299: 7 *# 9 -> C(6,3)
300: 8 *# 2 -> C(1,8)
301: 8 *# 3 -> C(2,4)
302: 8 *# 4 -> C(3,2)
303: 8 *# 5 -> C(4,0)
304: 8 *# 6 -> C(4,8)
305: 8 *# 7 -> C(5,6)
306: 8 *# 8 -> C(6,4)
307: 8 *# 9 -> C(7,2)
308: 9 *# 2 -> C(1,8)
309: 9 *# 3 -> C(2,7)
310: 9 *# 4 -> C(3,6)
311: 9 *# 5 -> C(4,5)
312: 9 *# 6 -> C(5,4)
313: 9 *# 7 -> C(6,3)
314: 9 *# 8 -> C(7,2)
315: 9 *# 9 -> C(8,1)
316: x *# c(y,z) -> C(x * y,x * z)
317: x *# c(y,z) -> x *# y
318: x *# c(y,z) -> x *# z
319: c(x,y) *# z -> C(x * z,y * z)
320: c(x,y) *# z -> x *# z
321: c(x,y) *# z -> y *# z

The approximated dependency graph contains 2 SCCs:
{207,208,254-257}
and {317,318,320,321}.

- Consider the SCC {207,208,254-257}.
The usable rules are {1-104}.
By taking the polynomial interpretation
[0] = [1] = [2] = [3] = [4] = [5] = [6] = [7] = [8] = [9] = 1
and [+](x,y) = [+#](x,y) = [c](x,y) = [C](x,y) = x + y + 1,
the rules in {2,22,31,32,40-42,49-52,58-62,67-72,76-82,85-92,94-104,207,254,256}
are weakly decreasing and
the rules in {1,3-21,23-30,33-39,43-48,53-57,63-66,73-75,83,84,93,208,255,257}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {207}.
By taking the polynomial interpretation
[0] = [1] = [2] = [3] = [4] = [5] = [6] = [7] = [8] = [9] = 1,
[+](x,y) = [c](x,y) = x + y + 1
and [C](x,y) = y + 1,
the rules in {2,22,31,32,40-42,49-52,58-62,67-72,76-82,85-92,94-104}
are weakly decreasing and
the rules in {1,3-21,23-30,33-39,43-48,53-57,63-66,73-75,83,84,93,207}
are strictly decreasing.


- Consider the SCC {317,318,320,321}.
There are no usable rules.
By taking the polynomial interpretation
[*#](x,y) = [c](x,y) = x + y + 1,
the rules in {317,318,320,321}
are strictly decreasing.

Hence the TRS is terminating.