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(b(x0)))))	→	c(c(c(c(a(x0)))))
c(x0)	→	b(a(a(b(x0))))

Proof

1 Bounds

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

final states:

{7, 1}

transitions:

61 → 85

89 → 49

89 → 62

15 → 5

84 → 60

122 → 209

120 → 61

3 → 46

50 → 4

218 → 172

213 → 123

146 → 68

5 → 26

59 → 80

65 → 147

243 → 169

193 → 126

62 → 49

62 → 10

62 → 239

62 → 168

62 → 242

31 → 57

1 → 48

1 → 9

1 → 46

1 → 3

1 → 241

123 → 194

60 → 116

26 → 63

125 → 189

233 → 170

58 → 100

170 → 224

177 → 125

141 → 67

172 → 122

171 → 214

6 → 31

124 → 173

67 → 142

11 → 121

4 → 11

66 → 137

169 → 229

104 → 59

126 → 64

30 → 6

64 → 152

46 → 167

35 → 1

198 → 124

168 → 239

68 → 58

151 → 66

228 → 171

156 → 65

c₂(67) → 68

c₂(65) → 66

c₂(169) → 170

c₂(125) → 126

c₂(66) → 67

c₂(58) → 59

c₂(123) → 124

c₂(61) → 62

c₂(170) → 171

c₂(64) → 65

c₂(59) → 60

c₂(60) → 61

c₂(171) → 172

c₂(124) → 125

c₂(122) → 123

c₂(168) → 169

a₂(167) → 168

a₂(57) → 58

a₂(63) → 64

a₂(121) → 122

a₁(33) → 34

a₁(32) → 33

a₁(28) → 29

a₁(47) → 48

a₁(12) → 13

a₁(27) → 28

a₁(13) → 14

a₁(48) → 49

f3₀ → 2

c₀(5) → 6

c₀(6) → 1

c₀(4) → 5

c₀(3) → 4

b₃(140) → 141

b₃(100) → 101

b₃(142) → 143

b₃(192) → 193

b₃(227) → 228

b₃(88) → 89

b₃(152) → 153

b₃(242) → 243

b₃(239) → 240

b₃(147) → 148

b₃(155) → 156

b₃(209) → 210

b₃(83) → 84

b₃(116) → 117

b₃(232) → 233

b₃(194) → 195

b₃(119) → 120

b₃(103) → 104

b₃(145) → 146

b₃(189) → 190

b₃(80) → 81

b₃(217) → 218

b₃(137) → 138

b₃(224) → 225

b₃(197) → 198

b₃(229) → 230

b₃(150) → 151

b₃(176) → 177

b₃(173) → 174

b₃(85) → 86

b₃(214) → 215

b₃(212) → 213

a₃(138) → 139

a₃(87) → 88

a₃(230) → 231

a₃(175) → 176

a₃(118) → 119

a₃(139) → 140

a₃(211) → 212

a₃(225) → 226

a₃(190) → 191

a₃(191) → 192

a₃(215) → 216

a₃(117) → 118

a₃(241) → 242

a₃(144) → 145

a₃(216) → 217

a₃(148) → 149

a₃(240) → 241

a₃(82) → 83

a₃(174) → 175

a₃(231) → 232

a₃(143) → 144

a₃(210) → 211

a₃(149) → 150

a₃(101) → 102

a₃(226) → 227

a₃(196) → 197

a₃(102) → 103

a₃(153) → 154

a₃(86) → 87

a₃(154) → 155

a₃(81) → 82

a₃(195) → 196

b₀(10) → 7

b₀(2) → 8

b₁(46) → 47

b₁(49) → 50

b₁(26) → 27

b₁(11) → 12

b₁(14) → 15

b₁(29) → 30

b₁(34) → 35

b₁(31) → 32

a₀(8) → 9

a₀(2) → 3

a₀(9) → 10

61	→	85
89	→	49
89	→	62
15	→	5
84	→	60
122	→	209
120	→	61
3	→	46
50	→	4
218	→	172
213	→	123
146	→	68
5	→	26
59	→	80
65	→	147
243	→	169
193	→	126
62	→	49
62	→	10
62	→	239
62	→	168
62	→	242
31	→	57
1	→	48
1	→	9
1	→	46
1	→	3
1	→	241
123	→	194
60	→	116
26	→	63
125	→	189
233	→	170
58	→	100
170	→	224
177	→	125
141	→	67
172	→	122
171	→	214
6	→	31
124	→	173
67	→	142
11	→	121
4	→	11
66	→	137
169	→	229
104	→	59
126	→	64
30	→	6
64	→	152
46	→	167
35	→	1
198	→	124
168	→	239
68	→	58
151	→	66
228	→	171
156	→	65
c₂(67)	→	68
c₂(65)	→	66
c₂(169)	→	170
c₂(125)	→	126
c₂(66)	→	67
c₂(58)	→	59
c₂(123)	→	124
c₂(61)	→	62
c₂(170)	→	171
c₂(64)	→	65
c₂(59)	→	60
c₂(60)	→	61
c₂(171)	→	172
c₂(124)	→	125
c₂(122)	→	123
c₂(168)	→	169
a₂(167)	→	168
a₂(57)	→	58
a₂(63)	→	64
a₂(121)	→	122
a₁(33)	→	34
a₁(32)	→	33
a₁(28)	→	29
a₁(47)	→	48
a₁(12)	→	13
a₁(27)	→	28
a₁(13)	→	14
a₁(48)	→	49
f3₀	→	2
c₀(5)	→	6
c₀(6)	→	1
c₀(4)	→	5
c₀(3)	→	4
b₃(140)	→	141
b₃(100)	→	101
b₃(142)	→	143
b₃(192)	→	193
b₃(227)	→	228
b₃(88)	→	89
b₃(152)	→	153
b₃(242)	→	243
b₃(239)	→	240
b₃(147)	→	148
b₃(155)	→	156
b₃(209)	→	210
b₃(83)	→	84
b₃(116)	→	117
b₃(232)	→	233
b₃(194)	→	195
b₃(119)	→	120
b₃(103)	→	104
b₃(145)	→	146
b₃(189)	→	190
b₃(80)	→	81
b₃(217)	→	218
b₃(137)	→	138
b₃(224)	→	225
b₃(197)	→	198
b₃(229)	→	230
b₃(150)	→	151
b₃(176)	→	177
b₃(173)	→	174
b₃(85)	→	86
b₃(214)	→	215
b₃(212)	→	213
a₃(138)	→	139
a₃(87)	→	88
a₃(230)	→	231
a₃(175)	→	176
a₃(118)	→	119
a₃(139)	→	140
a₃(211)	→	212
a₃(225)	→	226
a₃(190)	→	191
a₃(191)	→	192
a₃(215)	→	216
a₃(117)	→	118
a₃(241)	→	242
a₃(144)	→	145
a₃(216)	→	217
a₃(148)	→	149
a₃(240)	→	241
a₃(82)	→	83
a₃(174)	→	175
a₃(231)	→	232
a₃(143)	→	144
a₃(210)	→	211
a₃(149)	→	150
a₃(101)	→	102
a₃(226)	→	227
a₃(196)	→	197
a₃(102)	→	103
a₃(153)	→	154
a₃(86)	→	87
a₃(154)	→	155
a₃(81)	→	82
a₃(195)	→	196
b₀(10)	→	7
b₀(2)	→	8
b₁(46)	→	47
b₁(49)	→	50
b₁(26)	→	27
b₁(11)	→	12
b₁(14)	→	15
b₁(29)	→	30
b₁(34)	→	35
b₁(31)	→	32
a₀(8)	→	9
a₀(2)	→	3
a₀(9)	→	10