YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{21, 1}

transitions:

202 → 116

202 → 158

202 → 203

15 → 27

134 → 72

134 → 159

134 → 116

134 → 158

9 → 71

34 → 183

90 → 28

90 → 113

1 → 8

1 → 3

1 → 207

40 → 157

208 → 28

21 → 8

21 → 3

204 → 129

114 → 85

69 → 115

46 → 9

46 → 69

46 → 208

158 → 116

160 → 129

70 → 41

f6₀ → 2

2₂(130) → 131

2₂(184) → 185

2₂(116) → 117

2₂(124) → 125

2₂(192) → 193

2₂(198) → 199

3₂(131) → 132

3₂(125) → 126

3₂(185) → 186

3₂(193) → 194

3₂(117) → 118

3₂(199) → 200

0₀(9) → 10

0₀(1) → 22

0₀(15) → 16

2₁(72) → 73

2₁(86) → 87

2₁(28) → 29

2₁(36) → 37

2₁(80) → 81

2₁(42) → 43

0₁(34) → 35

0₁(84) → 85

0₁(113) → 114

0₁(69) → 70

0₁(40) → 41

0₁(78) → 79

4₀(19) → 20

4₀(25) → 26

4₀(13) → 14

4₀(5) → 6

1₁(32) → 33

1₁(85) → 86

1₁(33) → 34

1₁(35) → 36

1₁(207) → 208

1₁(77) → 78

1₁(41) → 42

1₁(76) → 77

1₁(79) → 80

1₁(71) → 72

1₁(27) → 28

0₂(190) → 191

0₂(159) → 160

0₂(203) → 204

0₂(128) → 129

0₂(196) → 197

0₂(122) → 123

3₀(24) → 25

3₀(18) → 19

3₀(4) → 5

3₀(12) → 13

5₁(39) → 40

5₁(89) → 90

5₁(31) → 32

5₁(45) → 46

5₁(75) → 76

5₁(83) → 84

2₀(11) → 12

2₀(23) → 24

2₀(17) → 18

2₀(3) → 4

5₀(26) → 21

5₀(6) → 7

5₀(14) → 15

5₀(20) → 1

4₁(82) → 83

4₁(74) → 75

4₁(88) → 89

4₁(30) → 31

4₁(38) → 39

4₁(44) → 45

3₁(37) → 38

3₁(73) → 74

3₁(87) → 88

3₁(29) → 30

3₁(43) → 44

3₁(81) → 82

1₂(157) → 158

1₂(123) → 124

1₂(189) → 190

1₂(191) → 192

1₂(121) → 122

1₂(129) → 130

1₂(120) → 121

1₂(183) → 184

1₂(115) → 116

1₂(188) → 189

1₂(197) → 198

4₂(186) → 187

4₂(132) → 133

4₂(200) → 201

4₂(194) → 195

4₂(126) → 127

4₂(118) → 119

1₀(8) → 9

1₀(7) → 8

1₀(10) → 11

1₀(22) → 23

1₀(16) → 17

1₀(2) → 3

5₂(201) → 202

5₂(133) → 134

5₂(195) → 196

5₂(127) → 128

5₂(187) → 188

5₂(119) → 120

202	→	116
202	→	158
202	→	203
15	→	27
134	→	72
134	→	159
134	→	116
134	→	158
9	→	71
34	→	183
90	→	28
90	→	113
1	→	8
1	→	3
1	→	207
40	→	157
208	→	28
21	→	8
21	→	3
204	→	129
114	→	85
69	→	115
46	→	9
46	→	69
46	→	208
158	→	116
160	→	129
70	→	41
f6₀	→	2
2₂(130)	→	131
2₂(184)	→	185
2₂(116)	→	117
2₂(124)	→	125
2₂(192)	→	193
2₂(198)	→	199
3₂(131)	→	132
3₂(125)	→	126
3₂(185)	→	186
3₂(193)	→	194
3₂(117)	→	118
3₂(199)	→	200
0₀(9)	→	10
0₀(1)	→	22
0₀(15)	→	16
2₁(72)	→	73
2₁(86)	→	87
2₁(28)	→	29
2₁(36)	→	37
2₁(80)	→	81
2₁(42)	→	43
0₁(34)	→	35
0₁(84)	→	85
0₁(113)	→	114
0₁(69)	→	70
0₁(40)	→	41
0₁(78)	→	79
4₀(19)	→	20
4₀(25)	→	26
4₀(13)	→	14
4₀(5)	→	6
1₁(32)	→	33
1₁(85)	→	86
1₁(33)	→	34
1₁(35)	→	36
1₁(207)	→	208
1₁(77)	→	78
1₁(41)	→	42
1₁(76)	→	77
1₁(79)	→	80
1₁(71)	→	72
1₁(27)	→	28
0₂(190)	→	191
0₂(159)	→	160
0₂(203)	→	204
0₂(128)	→	129
0₂(196)	→	197
0₂(122)	→	123
3₀(24)	→	25
3₀(18)	→	19
3₀(4)	→	5
3₀(12)	→	13
5₁(39)	→	40
5₁(89)	→	90
5₁(31)	→	32
5₁(45)	→	46
5₁(75)	→	76
5₁(83)	→	84
2₀(11)	→	12
2₀(23)	→	24
2₀(17)	→	18
2₀(3)	→	4
5₀(26)	→	21
5₀(6)	→	7
5₀(14)	→	15
5₀(20)	→	1
4₁(82)	→	83
4₁(74)	→	75
4₁(88)	→	89
4₁(30)	→	31
4₁(38)	→	39
4₁(44)	→	45
3₁(37)	→	38
3₁(73)	→	74
3₁(87)	→	88
3₁(29)	→	30
3₁(43)	→	44
3₁(81)	→	82
1₂(157)	→	158
1₂(123)	→	124
1₂(189)	→	190
1₂(191)	→	192
1₂(121)	→	122
1₂(129)	→	130
1₂(120)	→	121
1₂(183)	→	184
1₂(115)	→	116
1₂(188)	→	189
1₂(197)	→	198
4₂(186)	→	187
4₂(132)	→	133
4₂(200)	→	201
4₂(194)	→	195
4₂(126)	→	127
4₂(118)	→	119
1₀(8)	→	9
1₀(7)	→	8
1₀(10)	→	11
1₀(22)	→	23
1₀(16)	→	17
1₀(2)	→	3
5₂(201)	→	202
5₂(133)	→	134
5₂(195)	→	196
5₂(127)	→	128
5₂(187)	→	188
5₂(119)	→	120