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

Proof

1 Bounds

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

final states:

{33, 26, 19, 12, 1}

transitions:

33 → 5

25 → 174

61 → 8

32 → 178

89 → 81

87 → 15

167 → 159

18 → 170

39 → 182

57 → 62

175 → 52

1 → 5

165 → 36

183 → 52

60 → 77

139 → 29

135 → 140

179 → 52

26 → 5

86 → 103

161 → 166

141 → 133

138 → 155

171 → 52

109 → 114

11 → 51

63 → 55

12 → 5

112 → 129

113 → 22

115 → 107

83 → 88

19 → 5

0₁(53) → 54

0₁(157) → 158

0₁(105) → 106

0₁(134) → 135

0₁(108) → 109

0₁(56) → 57

0₁(82) → 83

0₁(131) → 132

0₁(79) → 80

0₁(160) → 161

2₁(114) → 115

2₁(182) → 183

2₁(106) → 107

2₁(137) → 138

2₁(170) → 171

2₁(59) → 60

2₁(166) → 167

2₁(85) → 86

2₁(178) → 179

2₁(51) → 52

2₁(174) → 175

2₁(132) → 133

2₁(77) → 78

2₁(155) → 156

2₁(158) → 159

2₁(129) → 130

2₁(88) → 89

2₁(140) → 141

2₁(111) → 112

2₁(163) → 164

2₁(54) → 55

2₁(80) → 81

2₁(62) → 63

2₁(103) → 104

f3₀ → 2

1₀(20) → 21

1₀(37) → 38

1₀(29) → 30

1₀(9) → 10

1₀(8) → 9

1₀(32) → 26

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

1₀(13) → 14

1₀(22) → 23

1₀(34) → 35

0₀(28) → 29

0₀(14) → 15

0₀(7) → 8

0₀(4) → 5

0₀(35) → 36

0₀(21) → 22

1₁(156) → 157

1₁(133) → 134

1₁(110) → 111

1₁(55) → 56

1₁(107) → 108

1₁(159) → 160

1₁(104) → 105

1₁(138) → 139

1₁(164) → 165

1₁(84) → 85

1₁(86) → 87

1₁(135) → 136

1₁(83) → 84

1₁(136) → 137

1₁(81) → 82

1₁(161) → 162

1₁(112) → 113

1₁(130) → 131

1₁(52) → 53

1₁(57) → 58

1₁(60) → 61

1₁(162) → 163

1₁(78) → 79

1₁(109) → 110

1₁(58) → 59

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₀(5) → 6

2₀(31) → 32

2₀(2) → 3

33	→	5
25	→	174
61	→	8
32	→	178
89	→	81
87	→	15
167	→	159
18	→	170
39	→	182
57	→	62
175	→	52
1	→	5
165	→	36
183	→	52
60	→	77
139	→	29
135	→	140
179	→	52
26	→	5
86	→	103
161	→	166
141	→	133
138	→	155
171	→	52
109	→	114
11	→	51
63	→	55
12	→	5
112	→	129
113	→	22
115	→	107
83	→	88
19	→	5
0₁(53)	→	54
0₁(157)	→	158
0₁(105)	→	106
0₁(134)	→	135
0₁(108)	→	109
0₁(56)	→	57
0₁(82)	→	83
0₁(131)	→	132
0₁(79)	→	80
0₁(160)	→	161
2₁(114)	→	115
2₁(182)	→	183
2₁(106)	→	107
2₁(137)	→	138
2₁(170)	→	171
2₁(59)	→	60
2₁(166)	→	167
2₁(85)	→	86
2₁(178)	→	179
2₁(51)	→	52
2₁(174)	→	175
2₁(132)	→	133
2₁(77)	→	78
2₁(155)	→	156
2₁(158)	→	159
2₁(129)	→	130
2₁(88)	→	89
2₁(140)	→	141
2₁(111)	→	112
2₁(163)	→	164
2₁(54)	→	55
2₁(80)	→	81
2₁(62)	→	63
2₁(103)	→	104
f3₀	→	2
1₀(20)	→	21
1₀(37)	→	38
1₀(29)	→	30
1₀(9)	→	10
1₀(8)	→	9
1₀(32)	→	26
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₀(3)	→	4
1₀(13)	→	14
1₀(22)	→	23
1₀(34)	→	35
0₀(28)	→	29
0₀(14)	→	15
0₀(7)	→	8
0₀(4)	→	5
0₀(35)	→	36
0₀(21)	→	22
1₁(156)	→	157
1₁(133)	→	134
1₁(110)	→	111
1₁(55)	→	56
1₁(107)	→	108
1₁(159)	→	160
1₁(104)	→	105
1₁(138)	→	139
1₁(164)	→	165
1₁(84)	→	85
1₁(86)	→	87
1₁(135)	→	136
1₁(83)	→	84
1₁(136)	→	137
1₁(81)	→	82
1₁(161)	→	162
1₁(112)	→	113
1₁(130)	→	131
1₁(52)	→	53
1₁(57)	→	58
1₁(60)	→	61
1₁(162)	→	163
1₁(78)	→	79
1₁(109)	→	110
1₁(58)	→	59
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₀(5)	→	6
2₀(31)	→	32
2₀(2)	→	3