YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(x0))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(x0)))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))

Proof

1 Bounds

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

final states:

{47, 40, 33, 26, 19, 12, 1}

transitions:

33 → 5

25 → 240

205 → 43

32 → 244

103 → 95

152 → 169

97 → 102

181 → 173

129 → 121

149 → 154

18 → 236

227 → 232

39 → 248

241 → 66

175 → 180

1 → 5

123 → 128

40 → 5

71 → 76

127 → 22

101 → 15

179 → 36

26 → 5

253 → 66

233 → 225

201 → 206

178 → 195

207 → 199

257 → 66

153 → 29

75 → 8

237 → 66

249 → 66

204 → 221

53 → 256

11 → 65

12 → 5

77 → 69

100 → 117

126 → 143

46 → 252

231 → 50

245 → 66

47 → 5

74 → 91

19 → 5

155 → 147

0₁(67) → 68

0₁(200) → 201

0₁(174) → 175

0₁(93) → 94

0₁(197) → 198

0₁(70) → 71

0₁(96) → 97

0₁(145) → 146

0₁(119) → 120

0₁(148) → 149

0₁(171) → 172

0₁(122) → 123

0₁(223) → 224

0₁(226) → 227

2₁(244) → 245

2₁(65) → 66

2₁(151) → 152

2₁(177) → 178

2₁(73) → 74

2₁(206) → 207

2₁(76) → 77

2₁(91) → 92

2₁(252) → 253

2₁(169) → 170

2₁(125) → 126

2₁(143) → 144

2₁(99) → 100

2₁(203) → 204

2₁(120) → 121

2₁(195) → 196

2₁(172) → 173

2₁(154) → 155

2₁(221) → 222

2₁(232) → 233

2₁(236) → 237

2₁(248) → 249

2₁(128) → 129

2₁(146) → 147

2₁(94) → 95

2₁(180) → 181

2₁(224) → 225

2₁(102) → 103

2₁(117) → 118

2₁(256) → 257

2₁(68) → 69

2₁(229) → 230

2₁(198) → 199

2₁(240) → 241

f3₀ → 2

1₀(20) → 21

1₀(51) → 52

1₀(37) → 38

1₀(29) → 30

1₀(43) → 44

1₀(9) → 10

1₀(8) → 9

1₀(32) → 26

1₀(41) → 42

1₀(15) → 16

1₀(18) → 12

1₀(16) → 17

1₀(27) → 28

1₀(25) → 19

1₀(23) → 24

1₀(6) → 7

1₀(39) → 33

1₀(36) → 37

1₀(30) → 31

1₀(11) → 1

1₀(44) → 45

1₀(46) → 40

1₀(50) → 51

1₀(3) → 4

1₀(13) → 14

1₀(48) → 49

1₀(22) → 23

1₀(34) → 35

1₀(53) → 47

0₀(28) → 29

0₀(14) → 15

0₀(7) → 8

0₀(49) → 50

0₀(4) → 5

0₀(42) → 43

0₀(35) → 36

0₀(21) → 22

1₁(149) → 150

1₁(196) → 197

1₁(123) → 124

1₁(227) → 228

1₁(204) → 205

1₁(230) → 231

1₁(175) → 176

1₁(202) → 203

1₁(98) → 99

1₁(95) → 96

1₁(170) → 171

1₁(225) → 226

1₁(152) → 153

1₁(71) → 72

1₁(92) → 93

1₁(124) → 125

1₁(222) → 223

1₁(74) → 75

1₁(150) → 151

1₁(178) → 179

1₁(147) → 148

1₁(176) → 177

1₁(100) → 101

1₁(118) → 119

1₁(66) → 67

1₁(121) → 122

1₁(173) → 174

1₁(228) → 229

1₁(201) → 202

1₁(126) → 127

1₁(97) → 98

1₁(144) → 145

1₁(199) → 200

1₁(72) → 73

1₁(69) → 70

2₀(22) → 27

2₀(38) → 39

2₀(24) → 25

2₀(8) → 13

2₀(10) → 11

2₀(15) → 20

2₀(29) → 34

2₀(17) → 18

2₀(45) → 46

2₀(5) → 6

2₀(31) → 32

2₀(2) → 3

2₀(52) → 53

2₀(36) → 41

2₀(43) → 48

33	→	5
25	→	240
205	→	43
32	→	244
103	→	95
152	→	169
97	→	102
181	→	173
129	→	121
149	→	154
18	→	236
227	→	232
39	→	248
241	→	66
175	→	180
1	→	5
123	→	128
40	→	5
71	→	76
127	→	22
101	→	15
179	→	36
26	→	5
253	→	66
233	→	225
201	→	206
178	→	195
207	→	199
257	→	66
153	→	29
75	→	8
237	→	66
249	→	66
204	→	221
53	→	256
11	→	65
12	→	5
77	→	69
100	→	117
126	→	143
46	→	252
231	→	50
245	→	66
47	→	5
74	→	91
19	→	5
155	→	147
0₁(67)	→	68
0₁(200)	→	201
0₁(174)	→	175
0₁(93)	→	94
0₁(197)	→	198
0₁(70)	→	71
0₁(96)	→	97
0₁(145)	→	146
0₁(119)	→	120
0₁(148)	→	149
0₁(171)	→	172
0₁(122)	→	123
0₁(223)	→	224
0₁(226)	→	227
2₁(244)	→	245
2₁(65)	→	66
2₁(151)	→	152
2₁(177)	→	178
2₁(73)	→	74
2₁(206)	→	207
2₁(76)	→	77
2₁(91)	→	92
2₁(252)	→	253
2₁(169)	→	170
2₁(125)	→	126
2₁(143)	→	144
2₁(99)	→	100
2₁(203)	→	204
2₁(120)	→	121
2₁(195)	→	196
2₁(172)	→	173
2₁(154)	→	155
2₁(221)	→	222
2₁(232)	→	233
2₁(236)	→	237
2₁(248)	→	249
2₁(128)	→	129
2₁(146)	→	147
2₁(94)	→	95
2₁(180)	→	181
2₁(224)	→	225
2₁(102)	→	103
2₁(117)	→	118
2₁(256)	→	257
2₁(68)	→	69
2₁(229)	→	230
2₁(198)	→	199
2₁(240)	→	241
f3₀	→	2
1₀(20)	→	21
1₀(51)	→	52
1₀(37)	→	38
1₀(29)	→	30
1₀(43)	→	44
1₀(9)	→	10
1₀(8)	→	9
1₀(32)	→	26
1₀(41)	→	42
1₀(15)	→	16
1₀(18)	→	12
1₀(16)	→	17
1₀(27)	→	28
1₀(25)	→	19
1₀(23)	→	24
1₀(6)	→	7
1₀(39)	→	33
1₀(36)	→	37
1₀(30)	→	31
1₀(11)	→	1
1₀(44)	→	45
1₀(46)	→	40
1₀(50)	→	51
1₀(3)	→	4
1₀(13)	→	14
1₀(48)	→	49
1₀(22)	→	23
1₀(34)	→	35
1₀(53)	→	47
0₀(28)	→	29
0₀(14)	→	15
0₀(7)	→	8
0₀(49)	→	50
0₀(4)	→	5
0₀(42)	→	43
0₀(35)	→	36
0₀(21)	→	22
1₁(149)	→	150
1₁(196)	→	197
1₁(123)	→	124
1₁(227)	→	228
1₁(204)	→	205
1₁(230)	→	231
1₁(175)	→	176
1₁(202)	→	203
1₁(98)	→	99
1₁(95)	→	96
1₁(170)	→	171
1₁(225)	→	226
1₁(152)	→	153
1₁(71)	→	72
1₁(92)	→	93
1₁(124)	→	125
1₁(222)	→	223
1₁(74)	→	75
1₁(150)	→	151
1₁(178)	→	179
1₁(147)	→	148
1₁(176)	→	177
1₁(100)	→	101
1₁(118)	→	119
1₁(66)	→	67
1₁(121)	→	122
1₁(173)	→	174
1₁(228)	→	229
1₁(201)	→	202
1₁(126)	→	127
1₁(97)	→	98
1₁(144)	→	145
1₁(199)	→	200
1₁(72)	→	73
1₁(69)	→	70
2₀(22)	→	27
2₀(38)	→	39
2₀(24)	→	25
2₀(8)	→	13
2₀(10)	→	11
2₀(15)	→	20
2₀(29)	→	34
2₀(17)	→	18
2₀(45)	→	46
2₀(5)	→	6
2₀(31)	→	32
2₀(2)	→	3
2₀(52)	→	53
2₀(36)	→	41
2₀(43)	→	48