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)))))))))))))))))))))))))

Proof

1 Bounds

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

final states:

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

transitions:

33 → 5

25 → 207

200 → 192

32 → 211

96 → 88

119 → 136

145 → 162

122 → 114

18 → 203

120 → 22

39 → 215

146 → 29

90 → 95

1 → 5

40 → 5

26 → 5

208 → 59

172 → 36

171 → 188

116 → 121

220 → 59

174 → 166

67 → 84

204 → 59

11 → 58

212 → 59

93 → 110

12 → 5

64 → 69

216 → 59

46 → 219

198 → 43

168 → 173

68 → 8

148 → 140

142 → 147

19 → 5

194 → 199

70 → 62

94 → 15

0₁(190) → 191

0₁(115) → 116

0₁(141) → 142

0₁(112) → 113

0₁(193) → 194

0₁(86) → 87

0₁(167) → 168

0₁(89) → 90

0₁(138) → 139

0₁(60) → 61

0₁(63) → 64

0₁(164) → 165

2₁(219) → 220

2₁(165) → 166

2₁(170) → 171

2₁(144) → 145

2₁(147) → 148

2₁(199) → 200

2₁(118) → 119

2₁(173) → 174

2₁(58) → 59

2₁(207) → 208

2₁(136) → 137

2₁(84) → 85

2₁(95) → 96

2₁(203) → 204

2₁(110) → 111

2₁(92) → 93

2₁(87) → 88

2₁(139) → 140

2₁(69) → 70

2₁(121) → 122

2₁(113) → 114

2₁(191) → 192

2₁(196) → 197

2₁(162) → 163

2₁(61) → 62

2₁(215) → 216

2₁(188) → 189

2₁(211) → 212

2₁(66) → 67

f3₀ → 2

1₀(20) → 21

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₀(3) → 4

1₀(13) → 14

1₀(22) → 23

1₀(34) → 35

0₀(28) → 29

0₀(14) → 15

0₀(7) → 8

0₀(4) → 5

0₀(42) → 43

0₀(35) → 36

0₀(21) → 22

1₁(163) → 164

1₁(114) → 115

1₁(117) → 118

1₁(91) → 92

1₁(90) → 91

1₁(65) → 66

1₁(197) → 198

1₁(64) → 65

1₁(67) → 68

1₁(166) → 167

1₁(189) → 190

1₁(192) → 193

1₁(140) → 141

1₁(62) → 63

1₁(111) → 112

1₁(137) → 138

1₁(93) → 94

1₁(195) → 196

1₁(85) → 86

1₁(143) → 144

1₁(142) → 143

1₁(59) → 60

1₁(145) → 146

1₁(88) → 89

1₁(169) → 170

1₁(116) → 117

1₁(194) → 195

1₁(119) → 120

1₁(168) → 169

1₁(171) → 172

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₀(36) → 41

33	→	5
25	→	207
200	→	192
32	→	211
96	→	88
119	→	136
145	→	162
122	→	114
18	→	203
120	→	22
39	→	215
146	→	29
90	→	95
1	→	5
40	→	5
26	→	5
208	→	59
172	→	36
171	→	188
116	→	121
220	→	59
174	→	166
67	→	84
204	→	59
11	→	58
212	→	59
93	→	110
12	→	5
64	→	69
216	→	59
46	→	219
198	→	43
168	→	173
68	→	8
148	→	140
142	→	147
19	→	5
194	→	199
70	→	62
94	→	15
0₁(190)	→	191
0₁(115)	→	116
0₁(141)	→	142
0₁(112)	→	113
0₁(193)	→	194
0₁(86)	→	87
0₁(167)	→	168
0₁(89)	→	90
0₁(138)	→	139
0₁(60)	→	61
0₁(63)	→	64
0₁(164)	→	165
2₁(219)	→	220
2₁(165)	→	166
2₁(170)	→	171
2₁(144)	→	145
2₁(147)	→	148
2₁(199)	→	200
2₁(118)	→	119
2₁(173)	→	174
2₁(58)	→	59
2₁(207)	→	208
2₁(136)	→	137
2₁(84)	→	85
2₁(95)	→	96
2₁(203)	→	204
2₁(110)	→	111
2₁(92)	→	93
2₁(87)	→	88
2₁(139)	→	140
2₁(69)	→	70
2₁(121)	→	122
2₁(113)	→	114
2₁(191)	→	192
2₁(196)	→	197
2₁(162)	→	163
2₁(61)	→	62
2₁(215)	→	216
2₁(188)	→	189
2₁(211)	→	212
2₁(66)	→	67
f3₀	→	2
1₀(20)	→	21
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₀(3)	→	4
1₀(13)	→	14
1₀(22)	→	23
1₀(34)	→	35
0₀(28)	→	29
0₀(14)	→	15
0₀(7)	→	8
0₀(4)	→	5
0₀(42)	→	43
0₀(35)	→	36
0₀(21)	→	22
1₁(163)	→	164
1₁(114)	→	115
1₁(117)	→	118
1₁(91)	→	92
1₁(90)	→	91
1₁(65)	→	66
1₁(197)	→	198
1₁(64)	→	65
1₁(67)	→	68
1₁(166)	→	167
1₁(189)	→	190
1₁(192)	→	193
1₁(140)	→	141
1₁(62)	→	63
1₁(111)	→	112
1₁(137)	→	138
1₁(93)	→	94
1₁(195)	→	196
1₁(85)	→	86
1₁(143)	→	144
1₁(142)	→	143
1₁(59)	→	60
1₁(145)	→	146
1₁(88)	→	89
1₁(169)	→	170
1₁(116)	→	117
1₁(194)	→	195
1₁(119)	→	120
1₁(168)	→	169
1₁(171)	→	172
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₀(36)	→	41