YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(b(a(a(a(b(x0))))))	→	c(c(a(x0)))
c(x0)	→	b(a(a(a(b(x0)))))

Proof

1 Bounds

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

final states:

{5, 1}

transitions:

157 → 119

176 → 214

81 → 26

81 → 9

271 → 237

87 → 68

87 → 35

87 → 49

80 → 126

229 → 220

229 → 175

229 → 224

229 → 114

149 → 196

119 → 79

227 → 248

3 → 22

50 → 78

50 → 226

225 → 176

219 → 177

37 → 25

37 → 8

37 → 47

37 → 223

37 → 113

110 → 174

55 → 25

55 → 37

175 → 220

49 → 35

1 → 24

1 → 7

1 → 22

1 → 3

1 → 222

1 → 112

73 → 36

235 → 278

253 → 228

79 → 132

36 → 50

201 → 150

177 → 149

21 → 1

150 → 190

173 → 118

22 → 46

237 → 227

283 → 236

82 → 148

117 → 168

4 → 16

118 → 152

16 → 34

236 → 266

137 → 80

35 → 68

115 → 48

48 → 82

47 → 110

68 → 116

68 → 234

131 → 81

195 → 151

27 → 4

151 → 117

151 → 235

228 → 242

247 → 229

b₀(9) → 5

b₀(2) → 6

a₃(70) → 71

a₃(135) → 136

a₃(53) → 54

a₃(128) → 129

a₃(133) → 134

a₃(69) → 70

a₃(84) → 85

a₃(71) → 72

a₃(127) → 128

a₃(85) → 86

a₃(111) → 112

a₃(83) → 84

a₃(113) → 114

a₃(129) → 130

a₃(116) → 117

a₃(52) → 53

a₃(134) → 135

a₃(51) → 52

a₃(112) → 113

c₄(235) → 236

c₄(236) → 237

c₄(227) → 228

c₄(175) → 176

c₄(228) → 229

c₄(176) → 177

c₄(150) → 151

c₄(149) → 150

c₀(4) → 1

c₀(3) → 4

a₅(223) → 224

a₅(197) → 198

a₅(268) → 269

a₅(216) → 217

a₅(251) → 252

a₅(280) → 281

a₅(191) → 192

a₅(193) → 194

a₅(215) → 216

a₅(249) → 250

a₅(222) → 223

a₅(221) → 222

a₅(244) → 245

a₅(269) → 270

a₅(192) → 193

a₅(279) → 280

a₅(245) → 246

a₅(199) → 200

a₅(198) → 199

a₅(243) → 244

a₅(217) → 218

a₅(281) → 282

a₅(250) → 251

a₅(267) → 268

a₁(23) → 24

a₁(19) → 20

a₁(18) → 19

a₁(25) → 26

a₁(17) → 18

a₁(24) → 25

b₅(278) → 279

b₅(220) → 221

b₅(246) → 247

b₅(248) → 249

b₅(242) → 243

b₅(252) → 253

b₅(214) → 215

b₅(200) → 201

b₅(190) → 191

b₅(224) → 225

b₅(194) → 195

b₅(270) → 271

b₅(218) → 219

b₅(196) → 197

b₅(266) → 267

b₅(282) → 283

c₂(35) → 36

c₂(48) → 49

c₂(80) → 81

c₂(79) → 80

c₂(36) → 37

c₂(47) → 48

c₃(118) → 119

c₃(117) → 118

a₂(78) → 79

a₂(46) → 47

a₂(34) → 35

b₁(26) → 27

b₁(22) → 23

b₁(20) → 21

b₁(16) → 17

b₄(156) → 157

b₄(168) → 169

b₄(172) → 173

b₄(152) → 153

a₄(154) → 155

a₄(169) → 170

a₄(153) → 154

a₄(234) → 235

a₄(148) → 149

a₄(226) → 227

a₄(155) → 156

a₄(171) → 172

a₄(170) → 171

a₄(174) → 175

f3₀ → 2

b₃(132) → 133

b₃(82) → 83

b₃(86) → 87

b₃(50) → 51

b₃(136) → 137

b₃(54) → 55

b₃(72) → 73

b₃(110) → 111

b₃(114) → 115

b₃(126) → 127

b₃(130) → 131

b₃(68) → 69

a₀(8) → 9

a₀(6) → 7

a₀(2) → 3

a₀(7) → 8

157	→	119
176	→	214
81	→	26
81	→	9
271	→	237
87	→	68
87	→	35
87	→	49
80	→	126
229	→	220
229	→	175
229	→	224
229	→	114
149	→	196
119	→	79
227	→	248
3	→	22
50	→	78
50	→	226
225	→	176
219	→	177
37	→	25
37	→	8
37	→	47
37	→	223
37	→	113
110	→	174
55	→	25
55	→	37
175	→	220
49	→	35
1	→	24
1	→	7
1	→	22
1	→	3
1	→	222
1	→	112
73	→	36
235	→	278
253	→	228
79	→	132
36	→	50
201	→	150
177	→	149
21	→	1
150	→	190
173	→	118
22	→	46
237	→	227
283	→	236
82	→	148
117	→	168
4	→	16
118	→	152
16	→	34
236	→	266
137	→	80
35	→	68
115	→	48
48	→	82
47	→	110
68	→	116
68	→	234
131	→	81
195	→	151
27	→	4
151	→	117
151	→	235
228	→	242
247	→	229
b₀(9)	→	5
b₀(2)	→	6
a₃(70)	→	71
a₃(135)	→	136
a₃(53)	→	54
a₃(128)	→	129
a₃(133)	→	134
a₃(69)	→	70
a₃(84)	→	85
a₃(71)	→	72
a₃(127)	→	128
a₃(85)	→	86
a₃(111)	→	112
a₃(83)	→	84
a₃(113)	→	114
a₃(129)	→	130
a₃(116)	→	117
a₃(52)	→	53
a₃(134)	→	135
a₃(51)	→	52
a₃(112)	→	113
c₄(235)	→	236
c₄(236)	→	237
c₄(227)	→	228
c₄(175)	→	176
c₄(228)	→	229
c₄(176)	→	177
c₄(150)	→	151
c₄(149)	→	150
c₀(4)	→	1
c₀(3)	→	4
a₅(223)	→	224
a₅(197)	→	198
a₅(268)	→	269
a₅(216)	→	217
a₅(251)	→	252
a₅(280)	→	281
a₅(191)	→	192
a₅(193)	→	194
a₅(215)	→	216
a₅(249)	→	250
a₅(222)	→	223
a₅(221)	→	222
a₅(244)	→	245
a₅(269)	→	270
a₅(192)	→	193
a₅(279)	→	280
a₅(245)	→	246
a₅(199)	→	200
a₅(198)	→	199
a₅(243)	→	244
a₅(217)	→	218
a₅(281)	→	282
a₅(250)	→	251
a₅(267)	→	268
a₁(23)	→	24
a₁(19)	→	20
a₁(18)	→	19
a₁(25)	→	26
a₁(17)	→	18
a₁(24)	→	25
b₅(278)	→	279
b₅(220)	→	221
b₅(246)	→	247
b₅(248)	→	249
b₅(242)	→	243
b₅(252)	→	253
b₅(214)	→	215
b₅(200)	→	201
b₅(190)	→	191
b₅(224)	→	225
b₅(194)	→	195
b₅(270)	→	271
b₅(218)	→	219
b₅(196)	→	197
b₅(266)	→	267
b₅(282)	→	283
c₂(35)	→	36
c₂(48)	→	49
c₂(80)	→	81
c₂(79)	→	80
c₂(36)	→	37
c₂(47)	→	48
c₃(118)	→	119
c₃(117)	→	118
a₂(78)	→	79
a₂(46)	→	47
a₂(34)	→	35
b₁(26)	→	27
b₁(22)	→	23
b₁(20)	→	21
b₁(16)	→	17
b₄(156)	→	157
b₄(168)	→	169
b₄(172)	→	173
b₄(152)	→	153
a₄(154)	→	155
a₄(169)	→	170
a₄(153)	→	154
a₄(234)	→	235
a₄(148)	→	149
a₄(226)	→	227
a₄(155)	→	156
a₄(171)	→	172
a₄(170)	→	171
a₄(174)	→	175
f3₀	→	2
b₃(132)	→	133
b₃(82)	→	83
b₃(86)	→	87
b₃(50)	→	51
b₃(136)	→	137
b₃(54)	→	55
b₃(72)	→	73
b₃(110)	→	111
b₃(114)	→	115
b₃(126)	→	127
b₃(130)	→	131
b₃(68)	→	69
a₀(8)	→	9
a₀(6)	→	7
a₀(2)	→	3
a₀(7)	→	8