YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{172, 167, 164, 163, 161, 156, 154, 150, 149, 146, 142, 137, 136, 132, 128, 123, 117, 111, 107, 104, 101, 98, 95, 93, 88, 84, 79, 78, 73, 68, 64, 61, 57, 52, 46, 41, 37, 33, 30, 27, 23, 19, 14, 10, 7, 1}

transitions:

78 → 80

33 → 69

33 → 47

23 → 69

23 → 47

111 → 69

111 → 47

61 → 69

61 → 47

128 → 69

128 → 47

98 → 69

98 → 47

10 → 69

10 → 47

84 → 80

167 → 80

149 → 80

41 → 69

41 → 47

41 → 138

41 → 80

57 → 69

57 → 47

146 → 80

37 → 69

37 → 47

95 → 69

95 → 47

107 → 69

107 → 47

1 → 69

1 → 47

123 → 69

123 → 47

101 → 69

101 → 47

73 → 69

73 → 47

79 → 80

161 → 69

150 → 69

138 → 80

172 → 80

88 → 80

52 → 69

52 → 47

117 → 69

117 → 47

14 → 69

14 → 47

93 → 80

104 → 69

104 → 47

7 → 69

7 → 47

69 → 47

30 → 69

30 → 47

137 → 80

64 → 69

64 → 47

46 → 69

46 → 47

164 → 69

154 → 69

68 → 69

68 → 47

132 → 80

142 → 47

19 → 69

19 → 47

27 → 69

27 → 47

156 → 80

1₀(74) → 75

1₀(53) → 54

1₀(11) → 34

1₀(92) → 88

1₀(49) → 50

1₀(112) → 113

1₀(3) → 4

1₀(44) → 78

1₀(80) → 124

1₀(134) → 135

1₀(138) → 139

1₀(82) → 83

1₀(118) → 119

1₀(15) → 89

1₀(47) → 53

1₀(2) → 15

1₀(147) → 148

1₀(85) → 86

1₀(69) → 70

1₀(20) → 38

1₀(12) → 13

3₀(2) → 112

3₀(21) → 22

3₀(102) → 103

3₀(113) → 114

3₀(58) → 62

3₀(48) → 49

3₀(16) → 17

3₀(50) → 51

3₀(4) → 151

3₀(34) → 35

3₀(119) → 120

3₀(70) → 71

3₀(8) → 9

3₀(106) → 104

3₀(108) → 109

3₀(36) → 33

3₀(13) → 10

3₀(53) → 58

3₀(15) → 24

3₀(29) → 155

3₀(75) → 76

3₀(65) → 66

0₀(124) → 125

0₀(42) → 43

0₀(63) → 61

0₀(159) → 160

0₀(144) → 145

0₀(58) → 59

0₀(38) → 39

0₀(60) → 57

0₀(77) → 73

0₀(129) → 130

0₀(90) → 91

0₀(87) → 84

0₀(82) → 147

0₀(28) → 29

0₀(47) → 48

0₀(139) → 140

0₀(113) → 133

0₀(54) → 55

0₀(94) → 93

0₀(80) → 81

0₀(15) → 16

0₀(20) → 21

0₀(53) → 108

0₀(71) → 72

0₀(2) → 3

0₀(4) → 5

0₀(24) → 25

0₀(66) → 67

4₀(125) → 126

4₀(140) → 141

4₀(160) → 156

4₀(47) → 74

4₀(5) → 31

4₀(157) → 158

4₀(43) → 44

4₀(39) → 40

4₀(16) → 143

4₀(3) → 168

4₀(80) → 85

4₀(133) → 134

4₀(81) → 82

4₀(173) → 174

4₀(130) → 131

4₀(91) → 92

4₀(55) → 56

4₀(2) → 118

5₀(135) → 132

5₀(87) → 94

5₀(53) → 65

5₀(72) → 68

5₀(152) → 153

5₀(24) → 99

5₀(175) → 172

5₀(97) → 95

5₀(169) → 170

5₀(114) → 115

5₀(145) → 142

5₀(148) → 146

5₀(171) → 167

5₀(83) → 79

5₀(89) → 90

5₀(2) → 80

5₀(170) → 171

5₀(168) → 173

5₀(122) → 117

5₀(58) → 165

5₀(29) → 162

5₀(78) → 149

5₀(101) → 163

5₀(110) → 107

5₀(47) → 138

5₀(15) → 42

5₀(158) → 159

5₀(86) → 87

5₀(141) → 137

5₀(112) → 157

f6₀ → 2

2₀(2) → 47

2₀(51) → 46

2₀(18) → 14

2₀(56) → 52

2₀(9) → 7

2₀(105) → 106

2₀(95) → 136

2₀(67) → 64

2₀(99) → 100

2₀(166) → 164

2₀(24) → 28

2₀(131) → 128

2₀(25) → 26

2₀(43) → 105

2₀(4) → 8

2₀(124) → 129

2₀(26) → 23

2₀(155) → 154

2₀(151) → 152

2₀(76) → 77

2₀(96) → 97

2₀(3) → 11

2₀(17) → 18

2₀(11) → 12

2₀(6) → 1

2₀(100) → 98

2₀(62) → 63

2₀(32) → 30

2₀(121) → 122

2₀(29) → 27

2₀(15) → 20

2₀(165) → 166

2₀(35) → 36

2₀(45) → 41

2₀(22) → 19

2₀(103) → 101

2₀(127) → 123

2₀(42) → 102

2₀(120) → 121

2₀(40) → 37

2₀(126) → 127

2₀(174) → 175

2₀(143) → 144

2₀(162) → 161

2₀(44) → 45

2₀(16) → 96

2₀(59) → 60

2₀(109) → 110

2₀(31) → 32

2₀(5) → 6

2₀(115) → 116

2₀(116) → 111

2₀(47) → 69

2₀(168) → 169

2₀(153) → 150

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