Consider the TRS R consisting of the rewrite rules

1: 0 + 0 -> 0
2: 0 + 1 -> 1
3: 0 + 2 -> 2
4: 0 + 3 -> 3
5: 0 + 4 -> 4
6: 0 + 5 -> 5
7: 0 + 6 -> 6
8: 0 + 7 -> 7
9: 0 + 8 -> 8
10: 0 + 9 -> 9
11: 1 + 0 -> 1
12: 1 + 1 -> 2
13: 1 + 2 -> 3
14: 1 + 3 -> 4
15: 1 + 4 -> 5
16: 1 + 5 -> 6
17: 1 + 6 -> 7
18: 1 + 7 -> 8
19: 1 + 8 -> 9
20: 1 + 9 -> c(1,0)
21: 2 + 0 -> 2
22: 2 + 1 -> 3
23: 2 + 2 -> 4
24: 2 + 3 -> 5
25: 2 + 4 -> 6
26: 2 + 5 -> 7
27: 2 + 6 -> 8
28: 2 + 7 -> 9
29: 2 + 8 -> c(1,0)
30: 2 + 9 -> c(1,1)
31: 3 + 0 -> 3
32: 3 + 1 -> 4
33: 3 + 2 -> 5
34: 3 + 3 -> 6
35: 3 + 4 -> 7
36: 3 + 5 -> 8
37: 3 + 6 -> 9
38: 3 + 7 -> c(1,0)
39: 3 + 8 -> c(1,1)
40: 3 + 9 -> c(1,2)
41: 4 + 0 -> 4
42: 4 + 1 -> 5
43: 4 + 2 -> 6
44: 4 + 3 -> 7
45: 4 + 4 -> 8
46: 4 + 5 -> 9
47: 4 + 6 -> c(1,0)
48: 4 + 7 -> c(1,1)
49: 4 + 8 -> c(1,2)
50: 4 + 9 -> c(1,3)
51: 5 + 0 -> 5
52: 5 + 1 -> 6
53: 5 + 2 -> 7
54: 5 + 3 -> 8
55: 5 + 4 -> 9
56: 5 + 5 -> c(1,0)
57: 5 + 6 -> c(1,1)
58: 5 + 7 -> c(1,2)
59: 5 + 8 -> c(1,3)
60: 5 + 9 -> c(1,4)
61: 6 + 0 -> 6
62: 6 + 1 -> 7
63: 6 + 2 -> 8
64: 6 + 3 -> 9
65: 6 + 4 -> c(1,0)
66: 6 + 5 -> c(1,1)
67: 6 + 6 -> c(1,2)
68: 6 + 7 -> c(1,3)
69: 6 + 8 -> c(1,4)
70: 6 + 9 -> c(1,5)
71: 7 + 0 -> 7
72: 7 + 1 -> 8
73: 7 + 2 -> 9
74: 7 + 3 -> c(1,0)
75: 7 + 4 -> c(1,1)
76: 7 + 5 -> c(1,2)
77: 7 + 6 -> c(1,3)
78: 7 + 7 -> c(1,4)
79: 7 + 8 -> c(1,5)
80: 7 + 9 -> c(1,6)
81: 8 + 0 -> 8
82: 8 + 1 -> 9
83: 8 + 2 -> c(1,0)
84: 8 + 3 -> c(1,1)
85: 8 + 4 -> c(1,2)
86: 8 + 5 -> c(1,3)
87: 8 + 6 -> c(1,4)
88: 8 + 7 -> c(1,5)
89: 8 + 8 -> c(1,6)
90: 8 + 9 -> c(1,7)
91: 9 + 0 -> 9
92: 9 + 1 -> c(1,0)
93: 9 + 2 -> c(1,1)
94: 9 + 3 -> c(1,2)
95: 9 + 4 -> c(1,3)
96: 9 + 5 -> c(1,4)
97: 9 + 6 -> c(1,5)
98: 9 + 7 -> c(1,6)
99: 9 + 8 -> c(1,7)
100: 9 + 9 -> c(1,8)
101: x + c(y,z) -> c(y,x + z)
102: c(x,y) + z -> c(x,y + z)
103: c(0,x) -> x
104: c(x,c(y,z)) -> c(x + y,z)

There are 51 dependency pairs:

105: 1 +# 9 -> C(1,0)
106: 2 +# 8 -> C(1,0)
107: 2 +# 9 -> C(1,1)
108: 3 +# 7 -> C(1,0)
109: 3 +# 8 -> C(1,1)
110: 3 +# 9 -> C(1,2)
111: 4 +# 6 -> C(1,0)
112: 4 +# 7 -> C(1,1)
113: 4 +# 8 -> C(1,2)
114: 4 +# 9 -> C(1,3)
115: 5 +# 5 -> C(1,0)
116: 5 +# 6 -> C(1,1)
117: 5 +# 7 -> C(1,2)
118: 5 +# 8 -> C(1,3)
119: 5 +# 9 -> C(1,4)
120: 6 +# 4 -> C(1,0)
121: 6 +# 5 -> C(1,1)
122: 6 +# 6 -> C(1,2)
123: 6 +# 7 -> C(1,3)
124: 6 +# 8 -> C(1,4)
125: 6 +# 9 -> C(1,5)
126: 7 +# 3 -> C(1,0)
127: 7 +# 4 -> C(1,1)
128: 7 +# 5 -> C(1,2)
129: 7 +# 6 -> C(1,3)
130: 7 +# 7 -> C(1,4)
131: 7 +# 8 -> C(1,5)
132: 7 +# 9 -> C(1,6)
133: 8 +# 2 -> C(1,0)
134: 8 +# 3 -> C(1,1)
135: 8 +# 4 -> C(1,2)
136: 8 +# 5 -> C(1,3)
137: 8 +# 6 -> C(1,4)
138: 8 +# 7 -> C(1,5)
139: 8 +# 8 -> C(1,6)
140: 8 +# 9 -> C(1,7)
141: 9 +# 1 -> C(1,0)
142: 9 +# 2 -> C(1,1)
143: 9 +# 3 -> C(1,2)
144: 9 +# 4 -> C(1,3)
145: 9 +# 5 -> C(1,4)
146: 9 +# 6 -> C(1,5)
147: 9 +# 7 -> C(1,6)
148: 9 +# 8 -> C(1,7)
149: 9 +# 9 -> C(1,8)
150: x +# c(y,z) -> C(y,x + z)
151: x +# c(y,z) -> x +# z
152: c(x,y) +# z -> C(x,y + z)
153: c(x,y) +# z -> y +# z
154: C(x,c(y,z)) -> C(x + y,z)
155: C(x,c(y,z)) -> x +# y

The approximated dependency graph contains one SCC:
{150-155}.

- Consider the SCC {150-155}.
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 {20,29,30,38-40,47-50,56-60,65-70,74-80,83-90,92-102,104,150,152,154}
are weakly decreasing and
the rules in {1-19,21-28,31-37,41-46,51-55,61-64,71-73,81,82,91,103,151,153,155}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {154}.
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 {20,29,30,38-40,47-50,56-60,65-70,74-80,83-90,92-102,104}
are weakly decreasing and
the rules in {1-19,21-28,31-37,41-46,51-55,61-64,71-73,81,82,91,103,154}
are strictly decreasing.


Hence the TRS is terminating.