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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{165, 160, 155, 154, 151, 148, 145, 140, 135, 134, 129, 127, 123, 119, 114, 108, 104, 101, 99, 98, 95, 93, 89, 86, 83, 81, 79, 77, 74, 70, 66, 63, 59, 54, 50, 44, 42, 39, 36, 31, 28, 24, 21, 16, 15, 14, 10, 6, 1}

transitions:

89 → 109

81 → 56

81 → 55

98 → 136

98 → 55

10 → 3

15 → 109

129 → 55

119 → 156

119 → 7

145 → 7

39 → 166

39 → 45

50 → 136

50 → 55

108 → 109

134 → 3

95 → 55

59 → 55

99 → 25

99 → 17

31 → 109

1 → 55

123 → 109

165 → 109

127 → 109

101 → 45

44 → 109

135 → 3

86 → 109

79 → 136

79 → 55

36 → 109

21 → 115

21 → 45

6 → 109

54 → 3

28 → 109

66 → 136

66 → 55

16 → 17

114 → 71

114 → 45

14 → 3

93 → 7

63 → 55

77 → 136

77 → 55

104 → 115

104 → 45

140 → 109

42 → 109

83 → 109

160 → 55

154 → 55

148 → 109

74 → 109

24 → 115

24 → 45

70 → 109

151 → 115

151 → 45

155 → 109

0₀(112) → 113

0₀(3) → 11

0₀(7) → 32

0₀(45) → 46

0₀(58) → 54

0₀(121) → 122

0₀(8) → 64

0₀(52) → 84

0₀(138) → 139

0₀(96) → 100

0₀(63) → 134

0₀(117) → 118

0₀(139) → 135

0₀(2) → 3

0₀(17) → 18

0₀(1) → 14

4₀(72) → 73

4₀(2) → 17

4₀(78) → 77

4₀(167) → 168

4₀(71) → 72

4₀(51) → 52

4₀(110) → 111

4₀(100) → 99

4₀(12) → 43

4₀(47) → 102

4₀(60) → 61

4₀(141) → 142

4₀(9) → 152

4₀(13) → 82

4₀(156) → 157

4₀(67) → 68

4₀(3) → 25

4₀(7) → 8

2₀(106) → 107

2₀(142) → 143

2₀(7) → 136

2₀(130) → 131

2₀(51) → 124

2₀(8) → 9

2₀(11) → 12

2₀(32) → 33

2₀(158) → 159

2₀(55) → 56

2₀(18) → 19

2₀(82) → 81

2₀(3) → 4

2₀(64) → 65

2₀(113) → 108

2₀(163) → 164

2₀(25) → 26

2₀(61) → 62

2₀(72) → 80

2₀(17) → 161

2₀(2) → 55

2₀(68) → 69

2₀(52) → 53

3₀(25) → 105

3₀(17) → 67

3₀(120) → 121

3₀(46) → 47

3₀(94) → 93

3₀(11) → 29

3₀(157) → 158

3₀(7) → 141

3₀(118) → 114

3₀(147) → 145

3₀(72) → 146

3₀(52) → 149

3₀(3) → 51

3₀(57) → 58

3₀(45) → 156

3₀(111) → 112

3₀(55) → 130

3₀(2) → 7

3₀(168) → 169

5₀(90) → 91

5₀(132) → 133

5₀(105) → 106

5₀(137) → 138

5₀(53) → 50

5₀(55) → 115

5₀(24) → 154

5₀(166) → 167

5₀(19) → 87

5₀(7) → 71

5₀(91) → 92

5₀(9) → 78

5₀(126) → 123

5₀(62) → 59

5₀(144) → 140

5₀(4) → 22

5₀(162) → 163

5₀(2) → 45

5₀(26) → 96

5₀(41) → 39

5₀(75) → 76

5₀(107) → 104

5₀(27) → 24

5₀(122) → 119

5₀(35) → 98

5₀(103) → 101

5₀(161) → 162

5₀(17) → 166

5₀(153) → 151

f6₀ → 2

1₀(2) → 109

1₀(18) → 37

1₀(149) → 150

1₀(56) → 57

1₀(9) → 6

1₀(65) → 63

1₀(128) → 127

1₀(133) → 129

1₀(49) → 44

1₀(146) → 147

1₀(48) → 49

1₀(67) → 75

1₀(19) → 20

1₀(80) → 79

1₀(30) → 28

1₀(152) → 153

1₀(55) → 60

1₀(131) → 132

1₀(25) → 40

1₀(43) → 42

1₀(92) → 89

1₀(4) → 5

1₀(159) → 155

1₀(124) → 125

1₀(26) → 27

1₀(37) → 38

1₀(76) → 74

1₀(150) → 148

1₀(38) → 36

1₀(96) → 97

1₀(164) → 160

1₀(11) → 90

1₀(84) → 85

1₀(87) → 88

1₀(53) → 94

1₀(136) → 137

1₀(23) → 21

1₀(125) → 126

1₀(1) → 15

1₀(29) → 30

1₀(33) → 34

1₀(35) → 31

1₀(22) → 23

1₀(85) → 83

1₀(20) → 16

1₀(40) → 41

1₀(12) → 13

1₀(73) → 70

1₀(143) → 144

1₀(97) → 95

1₀(60) → 120

1₀(34) → 35

1₀(78) → 128

1₀(109) → 110

1₀(5) → 1

1₀(13) → 10

1₀(88) → 86

1₀(169) → 165

1₀(115) → 116

1₀(116) → 117

1₀(47) → 48

1₀(102) → 103

1₀(69) → 66

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