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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{173, 170, 166, 161, 155, 151, 148, 143, 138, 134, 130, 125, 120, 116, 112, 108, 103, 99, 96, 91, 88, 84, 79, 74, 70, 66, 60, 56, 52, 48, 46, 41, 37, 33, 27, 26, 25, 22, 19, 15, 10, 8, 6, 1}

transitions:

33 → 157

33 → 61

25 → 162

25 → 61

103 → 92

103 → 156

10 → 92

10 → 156

10 → 11

15 → 156

96 → 61

84 → 92

84 → 156

41 → 92

41 → 156

120 → 157

120 → 61

108 → 92

108 → 156

134 → 156

37 → 156

130 → 156

99 → 61

1 → 92

1 → 156

8 → 92

8 → 156

60 → 92

60 → 156

26 → 162

26 → 61

125 → 156

79 → 156

79 → 71

79 → 29

91 → 92

91 → 156

170 → 156

161 → 156

138 → 157

138 → 61

173 → 156

6 → 92

6 → 156

116 → 62

116 → 156

88 → 156

52 → 92

52 → 156

22 → 156

143 → 162

143 → 61

66 → 157

66 → 61

112 → 156

46 → 157

46 → 61

48 → 92

48 → 156

148 → 92

148 → 156

74 → 61

19 → 156

27 → 156

70 → 35

70 → 62

70 → 156

166 → 156

56 → 29

56 → 156

151 → 29

151 → 156

155 → 92

155 → 156

f6₀ → 2

4₀(131) → 149

4₀(16) → 144

4₀(137) → 134

4₀(97) → 98

4₀(169) → 166

4₀(109) → 110

4₀(11) → 38

4₀(63) → 64

4₀(2) → 11

4₀(75) → 117

4₀(142) → 138

4₀(28) → 42

4₀(115) → 112

4₀(158) → 159

0₀(81) → 82

0₀(35) → 36

0₀(34) → 131

0₀(105) → 106

0₀(11) → 57

0₀(95) → 91

0₀(167) → 168

0₀(77) → 78

0₀(92) → 93

0₀(131) → 132

0₀(29) → 30

0₀(28) → 75

0₀(3) → 4

0₀(164) → 165

0₀(57) → 58

0₀(54) → 55

0₀(12) → 152

0₀(101) → 102

0₀(146) → 147

0₀(80) → 81

0₀(72) → 73

0₀(127) → 128

0₀(49) → 85

0₀(20) → 21

0₀(13) → 14

0₀(53) → 54

0₀(71) → 72

0₀(62) → 113

0₀(67) → 68

0₀(17) → 18

0₀(2) → 28

0₀(4) → 5

0₀(68) → 69

0₀(39) → 40

0₀(16) → 17

1₀(175) → 176

1₀(16) → 121

1₀(65) → 60

1₀(11) → 53

1₀(3) → 49

1₀(44) → 45

1₀(93) → 94

1₀(159) → 160

1₀(64) → 65

1₀(62) → 67

1₀(126) → 127

1₀(76) → 77

1₀(28) → 104

1₀(2) → 3

1₀(17) → 109

1₀(100) → 101

1₀(12) → 13

1₀(38) → 39

3₀(73) → 70

3₀(20) → 167

3₀(2) → 61

3₀(78) → 74

3₀(82) → 83

3₀(21) → 26

3₀(117) → 118

3₀(177) → 173

3₀(102) → 99

3₀(113) → 114

3₀(58) → 59

3₀(110) → 111

3₀(147) → 143

3₀(16) → 162

3₀(162) → 163

3₀(28) → 139

3₀(4) → 7

3₀(144) → 145

3₀(140) → 141

3₀(47) → 46

3₀(123) → 124

3₀(135) → 136

3₀(36) → 33

3₀(18) → 25

3₀(128) → 129

3₀(23) → 24

3₀(54) → 89

3₀(139) → 140

3₀(17) → 23

3₀(156) → 157

3₀(107) → 103

3₀(69) → 66

3₀(121) → 135

3₀(3) → 34

3₀(75) → 76

3₀(149) → 150

3₀(30) → 31

3₀(122) → 123

3₀(5) → 9

3₀(153) → 154

2₀(2) → 156

2₀(157) → 158

2₀(163) → 164

2₀(51) → 48

2₀(18) → 15

2₀(28) → 29

2₀(9) → 8

2₀(50) → 51

2₀(152) → 153

2₀(55) → 52

2₀(24) → 22

2₀(4) → 71

2₀(21) → 19

2₀(124) → 120

2₀(61) → 62

2₀(150) → 148

2₀(89) → 90

2₀(3) → 92

2₀(86) → 87

2₀(135) → 171

2₀(14) → 10

2₀(87) → 84

2₀(83) → 79

2₀(118) → 119

2₀(141) → 142

2₀(136) → 137

2₀(23) → 47

2₀(132) → 133

2₀(121) → 122

2₀(111) → 108

2₀(7) → 6

2₀(165) → 161

2₀(45) → 41

2₀(129) → 125

2₀(172) → 170

2₀(85) → 86

2₀(40) → 37

2₀(154) → 151

2₀(34) → 35

2₀(59) → 56

2₀(5) → 1

2₀(106) → 107

2₀(168) → 169

2₀(171) → 172

5₀(42) → 43

5₀(160) → 155

5₀(98) → 96

5₀(94) → 95

5₀(11) → 12

5₀(28) → 126

5₀(7) → 97

5₀(43) → 44

5₀(90) → 88

5₀(156) → 174

5₀(49) → 50

5₀(119) → 116

5₀(16) → 20

5₀(145) → 146

5₀(3) → 80

5₀(31) → 32

5₀(133) → 130

5₀(62) → 63

5₀(32) → 27

5₀(176) → 177

5₀(114) → 115

5₀(174) → 175

5₀(104) → 105

5₀(12) → 100

5₀(2) → 16

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