YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{179, 175, 171, 167, 163, 159, 158, 153, 149, 145, 140, 136, 131, 128, 126, 122, 118, 116, 115, 110, 106, 101, 96, 93, 90, 86, 84, 81, 77, 74, 71, 70, 65, 61, 58, 53, 49, 46, 42, 38, 34, 28, 24, 20, 17, 15, 10, 6, 1}

transitions:

61 → 66

128 → 66

81 → 3

10 → 3

15 → 3

96 → 3

84 → 3

136 → 66

167 → 66

149 → 3

145 → 66

122 → 66

110 → 66

34 → 66

65 → 66

175 → 66

90 → 37

90 → 3

20 → 3

49 → 66

1 → 3

71 → 66

101 → 3

179 → 66

38 → 66

86 → 3

58 → 66

171 → 66

6 → 3

116 → 66

153 → 3

53 → 66

28 → 3

118 → 66

106 → 66

93 → 3

77 → 66

140 → 66

126 → 66

42 → 66

46 → 66

158 → 3

115 → 66

17 → 3

159 → 3

131 → 66

74 → 66

24 → 3

70 → 66

163 → 66

f6₀ → 2

5₀(138) → 139

5₀(147) → 148

5₀(48) → 70

5₀(105) → 101

5₀(172) → 173

5₀(7) → 25

5₀(130) → 128

5₀(73) → 71

5₀(66) → 180

5₀(85) → 84

5₀(117) → 116

5₀(80) → 77

5₀(148) → 145

5₀(162) → 159

5₀(2) → 11

5₀(3) → 102

5₀(75) → 76

5₀(37) → 94

5₀(143) → 144

5₀(35) → 62

5₀(164) → 165

5₀(134) → 135

5₀(33) → 28

5₀(67) → 68

2₀(182) → 183

2₀(137) → 138

2₀(177) → 178

2₀(170) → 167

2₀(26) → 27

2₀(123) → 124

2₀(91) → 92

2₀(63) → 64

2₀(160) → 161

2₀(108) → 109

2₀(7) → 8

2₀(51) → 52

2₀(35) → 36

2₀(132) → 133

2₀(112) → 113

2₀(43) → 44

2₀(79) → 80

2₀(120) → 121

2₀(176) → 177

2₀(55) → 56

2₀(36) → 168

2₀(40) → 41

2₀(154) → 155

2₀(54) → 107

2₀(12) → 91

2₀(50) → 51

2₀(146) → 147

2₀(72) → 73

2₀(13) → 14

2₀(31) → 32

2₀(133) → 134

2₀(103) → 104

2₀(119) → 120

2₀(2) → 66

2₀(141) → 142

2₀(4) → 5

2₀(39) → 47

1₀(35) → 54

1₀(180) → 181

1₀(19) → 17

1₀(11) → 12

1₀(78) → 79

1₀(157) → 153

1₀(144) → 140

1₀(95) → 93

1₀(174) → 171

1₀(3) → 4

1₀(125) → 122

1₀(66) → 111

1₀(123) → 137

1₀(150) → 151

1₀(135) → 131

1₀(89) → 86

1₀(29) → 39

1₀(111) → 112

1₀(9) → 6

1₀(82) → 83

1₀(99) → 100

1₀(94) → 95

1₀(62) → 63

1₀(39) → 40

1₀(76) → 74

1₀(43) → 72

1₀(22) → 23

1₀(2) → 35

1₀(69) → 65

1₀(54) → 78

3₀(2) → 7

3₀(132) → 176

3₀(21) → 22

3₀(102) → 103

3₀(44) → 45

3₀(48) → 46

3₀(87) → 88

3₀(37) → 34

3₀(83) → 81

3₀(8) → 18

3₀(11) → 97

3₀(36) → 164

3₀(54) → 55

3₀(56) → 57

3₀(156) → 157

3₀(107) → 108

3₀(62) → 160

3₀(66) → 146

3₀(121) → 118

3₀(3) → 154

3₀(75) → 115

3₀(43) → 50

3₀(127) → 126

3₀(30) → 31

3₀(5) → 16

3₀(151) → 152

3₀(35) → 132

0₀(2) → 3

0₀(18) → 19

0₀(54) → 150

0₀(64) → 61

0₀(67) → 172

0₀(166) → 163

0₀(113) → 114

0₀(36) → 37

0₀(152) → 149

0₀(55) → 85

0₀(107) → 129

0₀(92) → 90

0₀(8) → 9

0₀(124) → 125

0₀(14) → 10

0₀(100) → 96

0₀(23) → 20

0₀(161) → 162

0₀(29) → 30

0₀(27) → 24

0₀(52) → 49

0₀(45) → 42

0₀(75) → 127

0₀(183) → 179

0₀(57) → 53

0₀(41) → 38

0₀(44) → 75

0₀(16) → 15

0₀(59) → 60

0₀(109) → 106

0₀(5) → 1

0₀(88) → 89

0₀(47) → 48

0₀(168) → 169

4₀(29) → 123

4₀(25) → 26

4₀(8) → 21

4₀(47) → 59

4₀(142) → 143

4₀(97) → 98

4₀(5) → 117

4₀(98) → 99

4₀(129) → 130

4₀(169) → 170

4₀(11) → 141

4₀(66) → 67

4₀(60) → 58

4₀(36) → 87

4₀(181) → 182

4₀(139) → 136

4₀(15) → 158

4₀(155) → 156

4₀(35) → 43

4₀(165) → 166

4₀(62) → 119

4₀(32) → 33

4₀(173) → 174

4₀(114) → 110

4₀(37) → 82

4₀(68) → 69

4₀(104) → 105

4₀(12) → 13

4₀(178) → 175

4₀(2) → 29

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