YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(1(2(x0))))	→	3(4(4(2(x0))))
2(1(0(2(5(5(x0))))))	→	4(0(5(2(5(x0)))))
4(2(0(3(1(2(x0))))))	→	5(5(0(5(2(5(x0))))))
0(1(5(0(4(4(5(x0)))))))	→	3(0(0(4(5(0(x0))))))
0(4(1(2(2(4(5(x0)))))))	→	0(0(1(5(4(5(x0))))))
3(5(4(0(0(4(0(x0)))))))	→	0(0(0(5(4(0(x0))))))
2(3(4(3(1(0(2(4(x0))))))))	→	0(4(5(3(1(4(x0))))))
2(5(2(4(4(3(1(0(0(x0)))))))))	→	4(2(5(5(4(5(5(0(x0))))))))
5(4(1(5(5(5(3(3(0(x0)))))))))	→	5(3(5(0(4(3(5(4(0(x0)))))))))
4(0(5(1(2(1(3(3(0(5(3(x0)))))))))))	→	1(2(1(4(4(3(2(5(0(2(3(x0)))))))))))
4(5(2(5(0(0(2(2(0(4(1(x0)))))))))))	→	4(4(4(3(3(1(3(5(5(1(1(x0)))))))))))
1(2(3(1(4(1(3(2(0(5(1(4(x0))))))))))))	→	1(0(4(4(5(1(2(4(3(3(0(1(x0))))))))))))
1(1(5(1(4(3(4(1(1(5(1(2(5(x0)))))))))))))	→	5(0(0(3(3(0(5(5(5(4(2(3(x0))))))))))))
1(4(0(0(1(3(4(3(3(0(3(0(4(5(x0))))))))))))))	→	5(5(3(3(5(0(4(5(4(1(5(0(0(x0)))))))))))))
2(1(0(3(2(0(2(0(3(3(2(3(4(0(5(x0)))))))))))))))	→	2(2(3(3(5(5(5(3(1(4(0(5(0(2(2(x0)))))))))))))))
0(5(5(4(0(5(3(1(5(4(4(2(2(5(3(4(x0))))))))))))))))	→	0(4(2(1(2(0(2(2(4(3(3(2(2(4(4(3(3(4(x0))))))))))))))))))
2(4(4(5(0(1(5(0(3(5(1(1(5(2(0(4(4(x0)))))))))))))))))	→	2(5(2(4(3(5(4(2(4(3(4(1(3(4(5(5(4(1(2(4(x0))))))))))))))))))))
1(2(2(2(5(0(0(3(3(5(2(4(5(1(1(0(4(3(x0))))))))))))))))))	→	1(1(3(0(0(0(3(1(5(1(0(2(3(0(0(x0)))))))))))))))
0(2(1(4(1(2(5(0(0(1(3(1(5(5(5(5(1(3(4(x0)))))))))))))))))))	→	3(5(5(1(3(2(2(2(5(2(5(5(5(2(0(4(1(1(4(4(x0))))))))))))))))))))
1(3(1(0(2(2(4(4(1(3(4(2(0(5(2(1(3(5(4(x0)))))))))))))))))))	→	1(4(2(0(2(0(5(5(2(2(0(5(4(3(4(4(4(x0)))))))))))))))))
1(3(2(0(0(1(1(5(5(3(1(3(0(2(3(4(5(5(5(x0)))))))))))))))))))	→	3(0(0(5(2(5(2(2(1(4(2(2(0(0(2(5(5(3(0(2(x0))))))))))))))))))))
2(2(2(5(1(3(5(5(0(4(0(4(5(1(1(2(0(2(5(x0)))))))))))))))))))	→	3(2(4(4(2(3(3(1(1(2(0(3(3(1(1(4(5(x0)))))))))))))))))
2(5(3(4(5(1(1(5(5(1(2(1(3(3(3(5(4(5(1(x0)))))))))))))))))))	→	5(4(5(4(5(1(1(0(4(2(5(4(1(2(0(1(3(1(x0))))))))))))))))))
3(2(1(3(3(5(5(5(4(2(4(4(5(1(5(1(3(0(4(x0)))))))))))))))))))	→	0(4(4(3(0(1(1(3(0(4(2(2(3(3(0(4(0(1(x0))))))))))))))))))
2(5(5(2(2(0(1(2(0(3(3(5(1(3(2(2(0(2(3(4(3(x0)))))))))))))))))))))	→	4(4(0(4(1(1(4(5(2(5(1(0(1(4(4(1(1(3(3(x0)))))))))))))))))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

2(1(1(0(x0))))	→	2(4(4(3(x0))))
5(5(2(0(1(2(x0))))))	→	5(2(5(0(4(x0)))))
2(1(3(0(2(4(x0))))))	→	5(2(5(0(5(5(x0))))))
5(4(4(0(5(1(0(x0)))))))	→	0(5(4(0(0(3(x0))))))
5(4(2(2(1(4(0(x0)))))))	→	5(4(5(1(0(0(x0))))))
0(4(0(0(4(5(3(x0)))))))	→	0(4(5(0(0(0(x0))))))
4(2(0(1(3(4(3(2(x0))))))))	→	4(1(3(5(4(0(x0))))))
0(0(1(3(4(4(2(5(2(x0)))))))))	→	0(5(5(4(5(5(2(4(x0))))))))
0(3(3(5(5(5(1(4(5(x0)))))))))	→	0(4(5(3(4(0(5(3(5(x0)))))))))
3(5(0(3(3(1(2(1(5(0(4(x0)))))))))))	→	3(2(0(5(2(3(4(4(1(2(1(x0)))))))))))
1(4(0(2(2(0(0(5(2(5(4(x0)))))))))))	→	1(1(5(5(3(1(3(3(4(4(4(x0)))))))))))
4(1(5(0(2(3(1(4(1(3(2(1(x0))))))))))))	→	1(0(3(3(4(2(1(5(4(4(0(1(x0))))))))))))
5(2(1(5(1(1(4(3(4(1(5(1(1(x0)))))))))))))	→	3(2(4(5(5(5(0(3(3(0(0(5(x0))))))))))))
5(4(0(3(0(3(3(4(3(1(0(0(4(1(x0))))))))))))))	→	0(0(5(1(4(5(4(0(5(3(3(5(5(x0)))))))))))))
5(0(4(3(2(3(3(0(2(0(2(3(0(1(2(x0)))))))))))))))	→	2(2(0(5(0(4(1(3(5(5(5(3(3(2(2(x0)))))))))))))))
4(3(5(2(2(4(4(5(1(3(5(0(4(5(5(0(x0))))))))))))))))	→	4(3(3(4(4(2(2(3(3(4(2(2(0(2(1(2(4(0(x0))))))))))))))))))
4(4(0(2(5(1(1(5(3(0(5(1(0(5(4(4(2(x0)))))))))))))))))	→	4(2(1(4(5(5(4(3(1(4(3(4(2(4(5(3(4(2(5(2(x0))))))))))))))))))))
3(4(0(1(1(5(4(2(5(3(3(0(0(5(2(2(2(1(x0))))))))))))))))))	→	0(0(3(2(0(1(5(1(3(0(0(0(3(1(1(x0)))))))))))))))
4(3(1(5(5(5(5(1(3(1(0(0(5(2(1(4(1(2(0(x0)))))))))))))))))))	→	4(4(1(1(4(0(2(5(5(5(2(5(2(2(2(3(1(5(5(3(x0))))))))))))))))))))
4(5(3(1(2(5(0(2(4(3(1(4(4(2(2(0(1(3(1(x0)))))))))))))))))))	→	4(4(4(3(4(5(0(2(2(5(5(0(2(0(2(4(1(x0)))))))))))))))))
5(5(5(4(3(2(0(3(1(3(5(5(1(1(0(0(2(3(1(x0)))))))))))))))))))	→	2(0(3(5(5(2(0(0(2(2(4(1(2(2(5(2(5(0(0(3(x0))))))))))))))))))))
5(2(0(2(1(1(5(4(0(4(0(5(5(3(1(5(2(2(2(x0)))))))))))))))))))	→	5(4(1(1(3(3(0(2(1(1(3(3(2(4(4(2(3(x0)))))))))))))))))
1(5(4(5(3(3(3(1(2(1(5(5(1(1(5(4(3(5(2(x0)))))))))))))))))))	→	1(3(1(0(2(1(4(5(2(4(0(1(1(5(4(5(4(5(x0))))))))))))))))))
4(0(3(1(5(1(5(4(4(2(4(5(5(5(3(3(1(2(3(x0)))))))))))))))))))	→	1(0(4(0(3(3(2(2(4(0(3(1(1(0(3(4(4(0(x0))))))))))))))))))
3(4(3(2(0(2(2(3(1(5(3(3(0(2(1(0(2(2(5(5(2(x0)))))))))))))))))))))	→	3(3(1(1(4(4(1(0(1(5(2(5(4(1(1(4(0(4(4(x0)))))))))))))))))))

1.1 Bounds

The given TRS is match-bounded by 0. This is shown by the following automaton.

final states:

{271, 255, 238, 222, 205, 189, 170, 156, 137, 121, 106, 95, 84, 73, 63, 52, 44, 37, 32, 28, 22, 17, 11, 6, 1}

transitions:

32 → 7

205 → 13

205 → 12

271 → 3

84 → 138

84 → 12

37 → 24

37 → 23

95 → 34

95 → 12

255 → 33

255 → 7

1 → 54

1 → 107

222 → 138

222 → 12

44 → 18

44 → 23

73 → 190

73 → 7

170 → 4

170 → 7

121 → 4

121 → 7

6 → 13

6 → 12

52 → 45

52 → 3

22 → 12

11 → 54

11 → 107

28 → 8

28 → 23

106 → 9

106 → 12

63 → 53

137 → 256

137 → 64

137 → 7

189 → 239

189 → 7

17 → 12

156 → 3

238 → 53

f6₀ → 2

1₀(235) → 236

1₀(274) → 275

1₀(284) → 285

1₀(147) → 148

1₀(77) → 78

1₀(229) → 230

1₀(53) → 157

1₀(185) → 186

1₀(72) → 63

1₀(273) → 274

1₀(24) → 25

1₀(172) → 173

1₀(270) → 255

1₀(258) → 259

1₀(54) → 55

1₀(243) → 244

1₀(242) → 243

1₀(114) → 115

1₀(186) → 187

1₀(252) → 253

1₀(71) → 72

1₀(279) → 280

1₀(162) → 163

1₀(83) → 73

1₀(281) → 282

1₀(2) → 53

1₀(228) → 229

1₀(122) → 123

1₀(35) → 36

1₀(210) → 211

1₀(164) → 165

1₀(259) → 260

1₀(102) → 103

1₀(234) → 235

1₀(285) → 286

1₀(254) → 238

1₀(67) → 68

1₀(153) → 154

1₀(249) → 250

4₀(33) → 256

4₀(23) → 33

4₀(245) → 246

4₀(200) → 201

4₀(26) → 27

4₀(272) → 273

4₀(30) → 31

4₀(144) → 145

4₀(19) → 20

4₀(142) → 143

4₀(7) → 64

4₀(136) → 121

4₀(132) → 133

4₀(262) → 263

4₀(99) → 100

4₀(203) → 204

4₀(79) → 80

4₀(187) → 188

4₀(152) → 153

4₀(149) → 150

4₀(155) → 137

4₀(283) → 284

4₀(92) → 93

4₀(202) → 203

4₀(55) → 56

4₀(56) → 57

4₀(268) → 269

4₀(75) → 76

4₀(282) → 283

4₀(36) → 32

4₀(3) → 4

4₀(47) → 48

4₀(40) → 41

4₀(139) → 140

4₀(64) → 65

4₀(184) → 185

4₀(204) → 189

4₀(236) → 237

4₀(12) → 239

4₀(101) → 102

4₀(248) → 249

4₀(50) → 51

4₀(146) → 147

4₀(224) → 225

4₀(275) → 276

4₀(127) → 128

4₀(223) → 224

4₀(115) → 116

4₀(74) → 75

4₀(53) → 190

4₀(133) → 134

4₀(2) → 7

4₀(4) → 5

4₀(188) → 170

4₀(211) → 212

4₀(240) → 241

3₀(260) → 261

3₀(65) → 66

3₀(173) → 174

3₀(157) → 158

3₀(227) → 228

3₀(86) → 87

3₀(129) → 130

3₀(253) → 254

3₀(66) → 67

3₀(48) → 49

3₀(135) → 136

3₀(80) → 81

3₀(167) → 168

3₀(87) → 88

3₀(286) → 287

3₀(256) → 257

3₀(134) → 135

3₀(140) → 141

3₀(108) → 109

3₀(128) → 129

3₀(68) → 69

3₀(113) → 114

3₀(201) → 202

3₀(287) → 271

3₀(94) → 84

3₀(96) → 97

3₀(145) → 146

3₀(109) → 110

3₀(62) → 52

3₀(148) → 149

3₀(161) → 162

3₀(233) → 234

3₀(13) → 96

3₀(81) → 82

3₀(265) → 266

3₀(2) → 3

3₀(57) → 58

3₀(266) → 267

3₀(34) → 35

3₀(226) → 227

3₀(12) → 45

3₀(232) → 233

3₀(219) → 220

5₀(41) → 42

5₀(111) → 112

5₀(20) → 21

5₀(2) → 12

5₀(25) → 26

5₀(45) → 46

5₀(117) → 118

5₀(177) → 178

5₀(179) → 180

5₀(19) → 206

5₀(110) → 111

5₀(16) → 11

5₀(247) → 248

5₀(103) → 104

5₀(42) → 43

5₀(59) → 60

5₀(112) → 113

5₀(76) → 77

5₀(100) → 101

5₀(218) → 219

5₀(150) → 151

5₀(70) → 71

5₀(12) → 13

5₀(8) → 9

5₀(89) → 90

5₀(91) → 92

5₀(207) → 208

5₀(199) → 200

5₀(141) → 142

5₀(181) → 182

5₀(14) → 15

5₀(195) → 196

5₀(27) → 22

5₀(163) → 164

5₀(217) → 218

5₀(97) → 98

5₀(276) → 277

5₀(107) → 138

5₀(90) → 91

5₀(69) → 70

5₀(39) → 40

5₀(241) → 242

5₀(180) → 181

5₀(38) → 39

5₀(49) → 50

5₀(33) → 34

5₀(237) → 222

5₀(3) → 171

5₀(10) → 6

5₀(29) → 30

5₀(171) → 172

5₀(278) → 279

5₀(194) → 195

5₀(239) → 240

5₀(151) → 152

2₀(2) → 107

2₀(250) → 251

2₀(196) → 197

2₀(123) → 124

2₀(263) → 264

2₀(9) → 10

2₀(230) → 231

2₀(175) → 176

2₀(197) → 198

2₀(277) → 278

2₀(213) → 214

2₀(246) → 247

2₀(166) → 167

2₀(225) → 226

2₀(131) → 132

2₀(107) → 108

2₀(61) → 62

2₀(138) → 139

2₀(178) → 179

2₀(206) → 207

2₀(3) → 223

2₀(264) → 265

2₀(192) → 193

2₀(176) → 177

2₀(53) → 54

2₀(216) → 217

2₀(125) → 126

2₀(221) → 205

2₀(208) → 209

2₀(130) → 131

2₀(7) → 38

2₀(33) → 122

2₀(15) → 16

2₀(93) → 94

2₀(120) → 106

2₀(126) → 127

2₀(174) → 175

2₀(143) → 144

2₀(154) → 155

2₀(212) → 213

2₀(209) → 210

2₀(78) → 79

2₀(190) → 191

2₀(58) → 59

2₀(5) → 1

2₀(119) → 120

2₀(182) → 183

0₀(21) → 17

0₀(191) → 192

0₀(160) → 161

0₀(244) → 245

0₀(82) → 83

0₀(46) → 47

0₀(88) → 89

0₀(98) → 99

0₀(257) → 258

0₀(53) → 74

0₀(124) → 125

0₀(269) → 270

0₀(169) → 156

0₀(60) → 61

0₀(198) → 199

0₀(7) → 8

0₀(43) → 37

0₀(13) → 14

0₀(118) → 119

0₀(280) → 281

0₀(220) → 221

0₀(116) → 117

0₀(251) → 252

0₀(193) → 194

0₀(159) → 160

0₀(267) → 268

0₀(3) → 18

0₀(165) → 166

0₀(31) → 28

0₀(261) → 262

0₀(158) → 159

0₀(18) → 19

0₀(183) → 184

0₀(85) → 86

0₀(24) → 29

0₀(51) → 44

0₀(64) → 272

0₀(214) → 215

0₀(23) → 24

0₀(104) → 105

0₀(12) → 85

0₀(231) → 232

0₀(105) → 95

0₀(215) → 216

0₀(2) → 23

0₀(168) → 169

32	→	7
205	→	13
205	→	12
271	→	3
84	→	138
84	→	12
37	→	24
37	→	23
95	→	34
95	→	12
255	→	33
255	→	7
1	→	54
1	→	107
222	→	138
222	→	12
44	→	18
44	→	23
73	→	190
73	→	7
170	→	4
170	→	7
121	→	4
121	→	7
6	→	13
6	→	12
52	→	45
52	→	3
22	→	12
11	→	54
11	→	107
28	→	8
28	→	23
106	→	9
106	→	12
63	→	53
137	→	256
137	→	64
137	→	7
189	→	239
189	→	7
17	→	12
156	→	3
238	→	53
f6₀	→	2
1₀(235)	→	236
1₀(274)	→	275
1₀(284)	→	285
1₀(147)	→	148
1₀(77)	→	78
1₀(229)	→	230
1₀(53)	→	157
1₀(185)	→	186
1₀(72)	→	63
1₀(273)	→	274
1₀(24)	→	25
1₀(172)	→	173
1₀(270)	→	255
1₀(258)	→	259
1₀(54)	→	55
1₀(243)	→	244
1₀(242)	→	243
1₀(114)	→	115
1₀(186)	→	187
1₀(252)	→	253
1₀(71)	→	72
1₀(279)	→	280
1₀(162)	→	163
1₀(83)	→	73
1₀(281)	→	282
1₀(2)	→	53
1₀(228)	→	229
1₀(122)	→	123
1₀(35)	→	36
1₀(210)	→	211
1₀(164)	→	165
1₀(259)	→	260
1₀(102)	→	103
1₀(234)	→	235
1₀(285)	→	286
1₀(254)	→	238
1₀(67)	→	68
1₀(153)	→	154
1₀(249)	→	250
4₀(33)	→	256
4₀(23)	→	33
4₀(245)	→	246
4₀(200)	→	201
4₀(26)	→	27
4₀(272)	→	273
4₀(30)	→	31
4₀(144)	→	145
4₀(19)	→	20
4₀(142)	→	143
4₀(7)	→	64
4₀(136)	→	121
4₀(132)	→	133
4₀(262)	→	263
4₀(99)	→	100
4₀(203)	→	204
4₀(79)	→	80
4₀(187)	→	188
4₀(152)	→	153
4₀(149)	→	150
4₀(155)	→	137
4₀(283)	→	284
4₀(92)	→	93
4₀(202)	→	203
4₀(55)	→	56
4₀(56)	→	57
4₀(268)	→	269
4₀(75)	→	76
4₀(282)	→	283
4₀(36)	→	32
4₀(3)	→	4
4₀(47)	→	48
4₀(40)	→	41
4₀(139)	→	140
4₀(64)	→	65
4₀(184)	→	185
4₀(204)	→	189
4₀(236)	→	237
4₀(12)	→	239
4₀(101)	→	102
4₀(248)	→	249
4₀(50)	→	51
4₀(146)	→	147
4₀(224)	→	225
4₀(275)	→	276
4₀(127)	→	128
4₀(223)	→	224
4₀(115)	→	116
4₀(74)	→	75
4₀(53)	→	190
4₀(133)	→	134
4₀(2)	→	7
4₀(4)	→	5
4₀(188)	→	170
4₀(211)	→	212
4₀(240)	→	241
3₀(260)	→	261
3₀(65)	→	66
3₀(173)	→	174
3₀(157)	→	158
3₀(227)	→	228
3₀(86)	→	87
3₀(129)	→	130
3₀(253)	→	254
3₀(66)	→	67
3₀(48)	→	49
3₀(135)	→	136
3₀(80)	→	81
3₀(167)	→	168
3₀(87)	→	88
3₀(286)	→	287
3₀(256)	→	257
3₀(134)	→	135
3₀(140)	→	141
3₀(108)	→	109
3₀(128)	→	129
3₀(68)	→	69
3₀(113)	→	114
3₀(201)	→	202
3₀(287)	→	271
3₀(94)	→	84
3₀(96)	→	97
3₀(145)	→	146
3₀(109)	→	110
3₀(62)	→	52
3₀(148)	→	149
3₀(161)	→	162
3₀(233)	→	234
3₀(13)	→	96
3₀(81)	→	82
3₀(265)	→	266
3₀(2)	→	3
3₀(57)	→	58
3₀(266)	→	267
3₀(34)	→	35
3₀(226)	→	227
3₀(12)	→	45
3₀(232)	→	233
3₀(219)	→	220
5₀(41)	→	42
5₀(111)	→	112
5₀(20)	→	21
5₀(2)	→	12
5₀(25)	→	26
5₀(45)	→	46
5₀(117)	→	118
5₀(177)	→	178
5₀(179)	→	180
5₀(19)	→	206
5₀(110)	→	111
5₀(16)	→	11
5₀(247)	→	248
5₀(103)	→	104
5₀(42)	→	43
5₀(59)	→	60
5₀(112)	→	113
5₀(76)	→	77
5₀(100)	→	101
5₀(218)	→	219
5₀(150)	→	151
5₀(70)	→	71
5₀(12)	→	13
5₀(8)	→	9
5₀(89)	→	90
5₀(91)	→	92
5₀(207)	→	208
5₀(199)	→	200
5₀(141)	→	142
5₀(181)	→	182
5₀(14)	→	15
5₀(195)	→	196
5₀(27)	→	22
5₀(163)	→	164
5₀(217)	→	218
5₀(97)	→	98
5₀(276)	→	277
5₀(107)	→	138
5₀(90)	→	91
5₀(69)	→	70
5₀(39)	→	40
5₀(241)	→	242
5₀(180)	→	181
5₀(38)	→	39
5₀(49)	→	50
5₀(33)	→	34
5₀(237)	→	222
5₀(3)	→	171
5₀(10)	→	6
5₀(29)	→	30
5₀(171)	→	172
5₀(278)	→	279
5₀(194)	→	195
5₀(239)	→	240
5₀(151)	→	152
2₀(2)	→	107
2₀(250)	→	251
2₀(196)	→	197
2₀(123)	→	124
2₀(263)	→	264
2₀(9)	→	10
2₀(230)	→	231
2₀(175)	→	176
2₀(197)	→	198
2₀(277)	→	278
2₀(213)	→	214
2₀(246)	→	247
2₀(166)	→	167
2₀(225)	→	226
2₀(131)	→	132
2₀(107)	→	108
2₀(61)	→	62
2₀(138)	→	139
2₀(178)	→	179
2₀(206)	→	207
2₀(3)	→	223
2₀(264)	→	265
2₀(192)	→	193
2₀(176)	→	177
2₀(53)	→	54
2₀(216)	→	217
2₀(125)	→	126
2₀(221)	→	205
2₀(208)	→	209
2₀(130)	→	131
2₀(7)	→	38
2₀(33)	→	122
2₀(15)	→	16
2₀(93)	→	94
2₀(120)	→	106
2₀(126)	→	127
2₀(174)	→	175
2₀(143)	→	144
2₀(154)	→	155
2₀(212)	→	213
2₀(209)	→	210
2₀(78)	→	79
2₀(190)	→	191
2₀(58)	→	59
2₀(5)	→	1
2₀(119)	→	120
2₀(182)	→	183
0₀(21)	→	17
0₀(191)	→	192
0₀(160)	→	161
0₀(244)	→	245
0₀(82)	→	83
0₀(46)	→	47
0₀(88)	→	89
0₀(98)	→	99
0₀(257)	→	258
0₀(53)	→	74
0₀(124)	→	125
0₀(269)	→	270
0₀(169)	→	156
0₀(60)	→	61
0₀(198)	→	199
0₀(7)	→	8
0₀(43)	→	37
0₀(13)	→	14
0₀(118)	→	119
0₀(280)	→	281
0₀(220)	→	221
0₀(116)	→	117
0₀(251)	→	252
0₀(193)	→	194
0₀(159)	→	160
0₀(267)	→	268
0₀(3)	→	18
0₀(165)	→	166
0₀(31)	→	28
0₀(261)	→	262
0₀(158)	→	159
0₀(18)	→	19
0₀(183)	→	184
0₀(85)	→	86
0₀(24)	→	29
0₀(51)	→	44
0₀(64)	→	272
0₀(214)	→	215
0₀(23)	→	24
0₀(104)	→	105
0₀(12)	→	85
0₀(231)	→	232
0₀(105)	→	95
0₀(215)	→	216
0₀(2)	→	23
0₀(168)	→	169