YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{161, 156, 152, 148, 145, 140, 135, 131, 126, 122, 119, 114, 111, 109, 104, 103, 99, 94, 91, 88, 83, 80, 77, 73, 70, 67, 63, 62, 59, 58, 52, 50, 45, 41, 35, 33, 29, 26, 23, 19, 18, 14, 11, 6, 1}

transitions:

103 → 24

103 → 53

152 → 54

152 → 3

122 → 115

18 → 115

18 → 53

184 → 115

50 → 53

59 → 115

99 → 54

99 → 3

62 → 115

1 → 115

91 → 3

58 → 115

208 → 167

161 → 53

186 → 181

150 → 189

150 → 202

6 → 115

52 → 115

11 → 115

14 → 115

63 → 115

169 → 115

85 → 64

85 → 53

104 → 24

104 → 53

206 → 168

148 → 3

92 → 165

92 → 180

19 → 115

166 → 185

94 → 3

192 → 168

192 → 207

156 → 53

0₁(166) → 167

0₁(207) → 208

0₁(204) → 205

0₁(191) → 192

0₁(182) → 183

3₁(165) → 166

3₁(203) → 204

1₁(168) → 169

1₁(185) → 186

1₁(189) → 190

1₁(180) → 181

1₁(205) → 206

2₀(31) → 51

2₀(137) → 138

2₀(53) → 95

2₀(105) → 106

2₀(3) → 4

2₀(86) → 87

2₀(24) → 25

2₀(142) → 143

2₀(128) → 129

2₀(64) → 65

2₀(84) → 149

2₀(42) → 43

2₀(55) → 56

2₀(36) → 37

2₀(116) → 117

2₀(2) → 7

2₀(154) → 155

2₀(34) → 33

2₀(69) → 67

2₀(20) → 21

2₀(100) → 101

2₀(54) → 55

2₀(153) → 154

2₀(132) → 133

3₀(2) → 15

3₀(78) → 79

3₀(74) → 112

3₀(124) → 125

3₀(129) → 130

3₀(144) → 140

3₀(108) → 104

3₀(18) → 110

3₀(54) → 68

3₀(17) → 89

3₀(138) → 139

3₀(38) → 146

3₀(53) → 84

3₀(15) → 46

3₀(3) → 27

3₀(30) → 123

3₀(5) → 71

3₀(7) → 8

0₀(106) → 107

0₀(65) → 66

0₀(30) → 74

0₀(159) → 160

0₀(37) → 38

0₀(118) → 114

0₀(7) → 30

0₀(130) → 126

0₀(8) → 9

0₀(84) → 85

0₀(112) → 113

0₀(143) → 144

0₀(95) → 96

0₀(38) → 39

0₀(134) → 131

0₀(43) → 44

0₀(110) → 109

0₀(149) → 150

0₀(155) → 152

0₀(158) → 159

0₀(56) → 57

0₀(46) → 47

0₀(87) → 83

0₀(28) → 120

0₀(3) → 115

0₀(139) → 135

0₀(57) → 52

0₀(25) → 23

0₀(101) → 102

0₀(72) → 70

0₀(15) → 16

0₀(27) → 28

0₀(21) → 22

0₀(117) → 118

0₀(48) → 49

0₀(133) → 134

0₀(5) → 12

0₀(4) → 5

0₀(68) → 69

4₀(47) → 48

4₀(82) → 80

4₀(164) → 161

4₀(123) → 124

4₀(5) → 18

4₀(53) → 127

4₀(44) → 41

4₀(36) → 157

4₀(157) → 158

4₀(1) → 103

4₀(28) → 26

4₀(39) → 40

4₀(22) → 19

4₀(92) → 93

4₀(107) → 108

4₀(15) → 64

4₀(16) → 17

4₀(3) → 24

4₀(31) → 32

4₀(74) → 75

4₀(30) → 31

4₀(102) → 99

4₀(163) → 164

4₀(121) → 119

4₀(12) → 13

4₀(71) → 72

4₀(2) → 53

5₀(31) → 81

5₀(146) → 147

5₀(16) → 60

5₀(53) → 141

5₀(79) → 77

5₀(97) → 98

5₀(95) → 132

5₀(98) → 94

5₀(120) → 121

5₀(127) → 128

5₀(85) → 86

5₀(49) → 45

5₀(89) → 90

5₀(2) → 36

5₀(75) → 76

5₀(37) → 42

5₀(1) → 58

5₀(8) → 162

5₀(115) → 116

5₀(47) → 92

5₀(160) → 156

f6₀ → 2

1₀(2) → 3

1₀(51) → 50

1₀(9) → 10

1₀(90) → 88

1₀(10) → 6

1₀(54) → 153

1₀(113) → 111

1₀(36) → 136

1₀(4) → 100

1₀(61) → 59

1₀(151) → 148

1₀(76) → 73

1₀(150) → 151

1₀(96) → 97

1₀(3) → 105

1₀(17) → 14

1₀(147) → 145

1₀(53) → 54

1₀(141) → 142

1₀(66) → 63

1₀(136) → 137

1₀(23) → 62

1₀(125) → 122

1₀(32) → 29

1₀(81) → 82

1₀(15) → 20

1₀(93) → 91

1₀(40) → 35

1₀(60) → 61

1₀(162) → 163

1₀(16) → 78

1₀(31) → 34

1₀(5) → 1

1₀(13) → 11

2₁(181) → 182

2₁(202) → 203

2₁(190) → 191

4₁(183) → 184

4₁(167) → 168

103	→	24
103	→	53
152	→	54
152	→	3
122	→	115
18	→	115
18	→	53
184	→	115
50	→	53
59	→	115
99	→	54
99	→	3
62	→	115
1	→	115
91	→	3
58	→	115
208	→	167
161	→	53
186	→	181
150	→	189
150	→	202
6	→	115
52	→	115
11	→	115
14	→	115
63	→	115
169	→	115
85	→	64
85	→	53
104	→	24
104	→	53
206	→	168
148	→	3
92	→	165
92	→	180
19	→	115
166	→	185
94	→	3
192	→	168
192	→	207
156	→	53
0₁(166)	→	167
0₁(207)	→	208
0₁(204)	→	205
0₁(191)	→	192
0₁(182)	→	183
3₁(165)	→	166
3₁(203)	→	204
1₁(168)	→	169
1₁(185)	→	186
1₁(189)	→	190
1₁(180)	→	181
1₁(205)	→	206
2₀(31)	→	51
2₀(137)	→	138
2₀(53)	→	95
2₀(105)	→	106
2₀(3)	→	4
2₀(86)	→	87
2₀(24)	→	25
2₀(142)	→	143
2₀(128)	→	129
2₀(64)	→	65
2₀(84)	→	149
2₀(42)	→	43
2₀(55)	→	56
2₀(36)	→	37
2₀(116)	→	117
2₀(2)	→	7
2₀(154)	→	155
2₀(34)	→	33
2₀(69)	→	67
2₀(20)	→	21
2₀(100)	→	101
2₀(54)	→	55
2₀(153)	→	154
2₀(132)	→	133
3₀(2)	→	15
3₀(78)	→	79
3₀(74)	→	112
3₀(124)	→	125
3₀(129)	→	130
3₀(144)	→	140
3₀(108)	→	104
3₀(18)	→	110
3₀(54)	→	68
3₀(17)	→	89
3₀(138)	→	139
3₀(38)	→	146
3₀(53)	→	84
3₀(15)	→	46
3₀(3)	→	27
3₀(30)	→	123
3₀(5)	→	71
3₀(7)	→	8
0₀(106)	→	107
0₀(65)	→	66
0₀(30)	→	74
0₀(159)	→	160
0₀(37)	→	38
0₀(118)	→	114
0₀(7)	→	30
0₀(130)	→	126
0₀(8)	→	9
0₀(84)	→	85
0₀(112)	→	113
0₀(143)	→	144
0₀(95)	→	96
0₀(38)	→	39
0₀(134)	→	131
0₀(43)	→	44
0₀(110)	→	109
0₀(149)	→	150
0₀(155)	→	152
0₀(158)	→	159
0₀(56)	→	57
0₀(46)	→	47
0₀(87)	→	83
0₀(28)	→	120
0₀(3)	→	115
0₀(139)	→	135
0₀(57)	→	52
0₀(25)	→	23
0₀(101)	→	102
0₀(72)	→	70
0₀(15)	→	16
0₀(27)	→	28
0₀(21)	→	22
0₀(117)	→	118
0₀(48)	→	49
0₀(133)	→	134
0₀(5)	→	12
0₀(4)	→	5
0₀(68)	→	69
4₀(47)	→	48
4₀(82)	→	80
4₀(164)	→	161
4₀(123)	→	124
4₀(5)	→	18
4₀(53)	→	127
4₀(44)	→	41
4₀(36)	→	157
4₀(157)	→	158
4₀(1)	→	103
4₀(28)	→	26
4₀(39)	→	40
4₀(22)	→	19
4₀(92)	→	93
4₀(107)	→	108
4₀(15)	→	64
4₀(16)	→	17
4₀(3)	→	24
4₀(31)	→	32
4₀(74)	→	75
4₀(30)	→	31
4₀(102)	→	99
4₀(163)	→	164
4₀(121)	→	119
4₀(12)	→	13
4₀(71)	→	72
4₀(2)	→	53
5₀(31)	→	81
5₀(146)	→	147
5₀(16)	→	60
5₀(53)	→	141
5₀(79)	→	77
5₀(97)	→	98
5₀(95)	→	132
5₀(98)	→	94
5₀(120)	→	121
5₀(127)	→	128
5₀(85)	→	86
5₀(49)	→	45
5₀(89)	→	90
5₀(2)	→	36
5₀(75)	→	76
5₀(37)	→	42
5₀(1)	→	58
5₀(8)	→	162
5₀(115)	→	116
5₀(47)	→	92
5₀(160)	→	156
f6₀	→	2
1₀(2)	→	3
1₀(51)	→	50
1₀(9)	→	10
1₀(90)	→	88
1₀(10)	→	6
1₀(54)	→	153
1₀(113)	→	111
1₀(36)	→	136
1₀(4)	→	100
1₀(61)	→	59
1₀(151)	→	148
1₀(76)	→	73
1₀(150)	→	151
1₀(96)	→	97
1₀(3)	→	105
1₀(17)	→	14
1₀(147)	→	145
1₀(53)	→	54
1₀(141)	→	142
1₀(66)	→	63
1₀(136)	→	137
1₀(23)	→	62
1₀(125)	→	122
1₀(32)	→	29
1₀(81)	→	82
1₀(15)	→	20
1₀(93)	→	91
1₀(40)	→	35
1₀(60)	→	61
1₀(162)	→	163
1₀(16)	→	78
1₀(31)	→	34
1₀(5)	→	1
1₀(13)	→	11
2₁(181)	→	182
2₁(202)	→	203
2₁(190)	→	191
4₁(183)	→	184
4₁(167)	→	168