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(1(3(2(x0))))
0(1(2(x0)))	→	0(2(1(0(x0))))
0(1(2(x0)))	→	0(2(1(3(x0))))
0(1(2(x0)))	→	0(2(2(1(x0))))
0(1(2(x0)))	→	0(2(2(1(4(x0)))))
0(1(2(x0)))	→	5(1(0(5(2(3(x0))))))
0(2(4(x0)))	→	0(2(1(4(3(x0)))))
0(4(2(x0)))	→	4(0(2(3(x0))))
0(4(2(x0)))	→	4(0(5(5(2(x0)))))
0(0(4(2(x0))))	→	0(0(2(2(3(4(x0))))))
0(1(2(2(x0))))	→	0(2(1(0(2(x0)))))
0(1(2(2(x0))))	→	1(3(0(2(2(x0)))))
0(1(2(4(x0))))	→	0(1(4(2(3(x0)))))
0(1(2(4(x0))))	→	4(0(2(2(1(1(x0))))))
0(1(2(4(x0))))	→	4(0(5(5(2(1(x0))))))
0(1(2(5(x0))))	→	3(5(5(2(1(0(x0))))))
0(1(4(2(x0))))	→	0(5(2(1(4(x0)))))
0(1(5(2(x0))))	→	1(5(0(2(3(x0)))))
0(1(5(2(x0))))	→	0(2(2(1(0(5(x0))))))
0(1(5(2(x0))))	→	5(5(0(2(1(3(x0))))))
0(2(4(2(x0))))	→	0(5(4(3(2(2(x0))))))
0(3(1(2(x0))))	→	0(2(1(3(2(x0)))))
0(3(1(2(x0))))	→	1(0(2(5(3(x0)))))
0(3(1(2(x0))))	→	1(5(0(2(3(x0)))))
0(3(1(2(x0))))	→	3(0(2(2(1(x0)))))
0(3(1(2(x0))))	→	3(2(2(1(0(x0)))))
0(3(1(2(x0))))	→	0(3(2(3(1(3(x0))))))
0(3(4(2(x0))))	→	0(2(2(3(4(x0)))))
5(0(1(2(x0))))	→	1(3(2(5(0(x0)))))
5(0(1(2(x0))))	→	5(0(2(1(3(3(x0))))))
0(1(1(2(5(x0)))))	→	5(0(2(5(1(1(x0))))))
0(2(3(4(2(x0)))))	→	3(2(2(3(4(0(x0))))))
0(3(1(2(5(x0)))))	→	2(3(1(3(0(5(x0))))))
0(3(1(5(2(x0)))))	→	0(3(2(5(1(2(x0))))))
0(3(4(1(4(x0)))))	→	0(5(3(1(4(4(x0))))))
0(3(5(1(2(x0)))))	→	5(5(3(2(1(0(x0))))))
0(4(0(4(2(x0)))))	→	4(4(0(0(2(2(x0))))))
0(4(1(1(2(x0)))))	→	3(1(4(0(2(1(x0))))))
0(4(1(2(2(x0)))))	→	4(1(0(2(2(3(x0))))))
0(4(1(2(5(x0)))))	→	3(4(1(0(2(5(x0))))))
0(4(2(1(2(x0)))))	→	4(1(3(2(0(2(x0))))))
0(4(2(1(4(x0)))))	→	0(2(1(4(4(4(x0))))))
0(4(2(5(2(x0)))))	→	5(4(3(2(2(0(x0))))))
0(4(5(1(2(x0)))))	→	1(4(2(0(5(5(x0))))))
0(4(5(1(2(x0)))))	→	4(0(2(5(1(1(x0))))))
5(0(1(2(2(x0)))))	→	5(0(2(2(1(2(x0))))))
5(0(2(4(2(x0)))))	→	0(2(2(5(1(4(x0))))))
5(0(4(4(2(x0)))))	→	0(5(2(5(4(4(x0))))))

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{167, 164, 161, 158, 153, 148, 146, 142, 137, 132, 127, 122, 118, 114, 111, 105, 102, 99, 94, 91, 89, 84, 80, 76, 72, 71, 67, 62, 60, 56, 52, 46, 45, 42, 39, 34, 33, 28, 25, 21, 19, 13, 12, 10, 9, 6, 1}

transitions:

33 → 106

111 → 106

25 → 106

102 → 106

89 → 106

80 → 106

10 → 106

84 → 106

167 → 106

122 → 106

39 → 22

146 → 154

146 → 22

9 → 106

34 → 106

175 → 41

99 → 14

62 → 106

1 → 106

71 → 106

127 → 106

13 → 106

60 → 106

76 → 106

91 → 106

161 → 106

21 → 106

72 → 106

6 → 106

153 → 106

52 → 155

52 → 106

105 → 14

67 → 106

2 → 170

28 → 106

118 → 106

45 → 22

114 → 154

114 → 22

12 → 106

42 → 22

137 → 14

46 → 14

158 → 106

164 → 106

148 → 106

132 → 106

142 → 106

19 → 22

56 → 106

94 → 106

1₁(173) → 174

0₁(170) → 171

5₁(171) → 172

1₀(115) → 116

1₀(65) → 66

1₀(11) → 10

1₀(162) → 163

1₀(120) → 121

1₀(112) → 113

1₀(3) → 4

1₀(7) → 8

1₀(25) → 45

1₀(44) → 42

1₀(50) → 51

1₀(87) → 88

1₀(165) → 166

1₀(159) → 160

1₀(138) → 139

1₀(82) → 83

1₀(131) → 127

1₀(79) → 76

1₀(96) → 97

1₀(101) → 99

1₀(107) → 108

1₀(14) → 15

1₀(160) → 158

1₀(43) → 44

1₀(47) → 128

1₀(22) → 133

1₀(2) → 35

1₀(100) → 101

1₀(54) → 55

0₀(109) → 110

0₀(2) → 3

0₀(155) → 156

0₀(124) → 125

0₀(152) → 148

0₀(129) → 130

0₀(51) → 46

0₀(133) → 134

0₀(144) → 145

0₀(83) → 80

0₀(47) → 77

0₀(8) → 6

0₀(123) → 124

0₀(36) → 37

0₀(93) → 91

0₀(14) → 95

0₀(139) → 140

0₀(57) → 58

0₀(63) → 64

0₀(121) → 118

0₀(15) → 16

0₀(3) → 29

0₀(10) → 61

0₀(104) → 102

0₀(22) → 23

0₀(35) → 73

3₀(98) → 94

3₀(106) → 107

3₀(41) → 39

3₀(63) → 119

3₀(59) → 56

3₀(86) → 87

3₀(108) → 109

3₀(136) → 132

3₀(35) → 36

3₀(8) → 9

3₀(11) → 90

3₀(149) → 150

3₀(88) → 84

3₀(75) → 72

3₀(18) → 13

3₀(82) → 103

3₀(3) → 85

3₀(97) → 98

3₀(20) → 19

3₀(53) → 115

3₀(31) → 32

3₀(133) → 143

3₀(2) → 47

3₀(4) → 5

3₀(24) → 21

3₀(68) → 69

3₀(66) → 62

4₀(8) → 20

4₀(47) → 138

4₀(53) → 68

4₀(117) → 114

4₀(169) → 167

4₀(128) → 129

4₀(4) → 40

4₀(90) → 89

4₀(10) → 12

4₀(22) → 123

4₀(147) → 146

4₀(20) → 147

4₀(166) → 164

4₀(116) → 117

4₀(14) → 149

4₀(103) → 104

4₀(35) → 154

4₀(32) → 28

4₀(55) → 52

4₀(2) → 22

4₀(168) → 169

5₀(48) → 49

5₀(16) → 17

5₀(156) → 157

5₀(96) → 100

5₀(24) → 159

5₀(157) → 153

5₀(92) → 93

5₀(54) → 168

5₀(61) → 60

5₀(23) → 26

5₀(11) → 165

5₀(74) → 75

5₀(14) → 63

5₀(2) → 14

5₀(3) → 53

5₀(26) → 27

5₀(35) → 57

5₀(110) → 105

5₀(47) → 48

5₀(86) → 112

5₀(141) → 137

f6₀ → 2

2₀(2) → 106

2₀(163) → 161

2₀(9) → 71

2₀(134) → 135

2₀(49) → 50

2₀(95) → 96

2₀(64) → 65

2₀(113) → 111

2₀(30) → 31

2₀(36) → 92

2₀(24) → 43

2₀(37) → 38

2₀(151) → 152

2₀(150) → 151

2₀(38) → 34

2₀(96) → 162

2₀(3) → 7

2₀(17) → 18

2₀(135) → 136

2₀(6) → 33

2₀(53) → 54

2₀(140) → 141

2₀(70) → 67

2₀(23) → 24

2₀(125) → 126

2₀(81) → 82

2₀(29) → 30

2₀(130) → 131

2₀(7) → 11

2₀(27) → 25

2₀(85) → 86

2₀(40) → 41

2₀(126) → 122

2₀(73) → 74

2₀(143) → 144

2₀(154) → 155

2₀(78) → 79

2₀(58) → 59

2₀(5) → 1

2₀(145) → 142

2₀(77) → 78

2₀(119) → 120

2₀(47) → 81

2₀(69) → 70

2₁(172) → 173

4₁(174) → 175

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