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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{123, 119, 118, 114, 109, 104, 101, 96, 94, 93, 91, 86, 83, 80, 74, 69, 65, 55, 64, 62, 60, 56, 50, 47, 43, 42, 39, 38, 37, 36, 34, 32, 29, 25, 22, 21, 19, 17, 16, 11, 9, 6, 1}

transitions:

78 → 209

111 → 190

25 → 51

32 → 7

32 → 158

32 → 51

29 → 124

80 → 75

96 → 26

119 → 52

39 → 26

3 → 170

50 → 66

213 → 48

9 → 51

37 → 76

37 → 51

34 → 27

34 → 51

65 → 66

199 → 27

55 → 44

62 → 51

1 → 51

123 → 7

123 → 158

123 → 51

135 → 153

179 → 86

86 → 75

91 → 66

36 → 26

21 → 124

138 → 73

6 → 51

109 → 124

88 → 175

22 → 124

22 → 27

22 → 51

174 → 61

143 → 45

53 → 205

2 → 139

11 → 26

4 → 195

28 → 10

28 → 159

16 → 51

114 → 26

93 → 26

140 → 157

104 → 124

69 → 51

42 → 27

42 → 51

64 → 66

83 → 66

17 → 26

47 → 124

160 → 45

206 → 157

74 → 27

74 → 51

19 → 75

43 → 124

194 → 109

70 → 134

56 → 124

94 → 105

94 → 124

156 → 73

f6₀ → 2

5₀(99) → 100

5₀(20) → 19

5₀(128) → 123

5₀(24) → 64

5₀(95) → 94

5₀(6) → 37

5₀(117) → 114

5₀(82) → 80

5₀(2) → 75

5₀(3) → 70

5₀(41) → 39

5₀(35) → 42

5₀(102) → 103

5₀(17) → 38

5₀(81) → 82

4₁(195) → 196

4₁(175) → 176

4₁(170) → 171

4₁(209) → 210

4₁(190) → 191

4₁(205) → 206

2₀(106) → 107

2₀(126) → 127

2₀(26) → 27

2₀(85) → 83

2₀(58) → 63

2₀(120) → 121

2₀(92) → 91

2₀(90) → 86

2₀(75) → 76

2₀(3) → 7

2₀(40) → 61

2₀(113) → 109

2₀(12) → 23

2₀(72) → 73

2₀(27) → 48

2₀(13) → 81

2₀(103) → 101

2₀(2) → 51

2₀(4) → 5

2₀(44) → 45

0₁(134) → 135

0₁(140) → 141

0₁(139) → 140

0₁(135) → 136

0₀(51) → 57

0₀(3) → 4

0₀(66) → 67

0₀(77) → 78

0₀(24) → 36

0₀(26) → 97

0₀(87) → 88

0₀(52) → 53

0₀(70) → 71

0₀(84) → 85

0₀(110) → 111

0₀(75) → 87

0₀(15) → 11

0₀(97) → 115

0₀(107) → 108

0₀(124) → 125

0₀(14) → 15

0₀(2) → 3

0₀(100) → 96

1₁(212) → 213

1₁(198) → 199

1₁(159) → 160

1₁(178) → 179

1₁(193) → 194

1₁(173) → 174

1₁(155) → 156

3₀(26) → 66

3₀(71) → 72

3₀(58) → 84

3₀(51) → 52

3₀(48) → 49

3₀(4) → 30

3₀(112) → 113

3₀(12) → 40

3₀(8) → 6

3₀(89) → 90

3₀(55) → 50

3₀(9) → 95

3₀(68) → 65

3₀(18) → 17

3₀(27) → 28

3₀(23) → 24

3₀(54) → 55

3₀(13) → 102

3₀(63) → 62

3₀(79) → 74

3₀(121) → 122

3₀(3) → 44

3₀(40) → 41

3₀(5) → 16

3₀(22) → 118

3₀(7) → 10

1₀(2) → 124

1₀(51) → 105

1₀(18) → 20

1₀(46) → 43

1₀(28) → 25

1₀(10) → 9

1₀(49) → 47

1₀(105) → 106

1₀(98) → 99

1₀(30) → 31

1₀(24) → 22

1₀(8) → 21

1₀(61) → 60

1₀(76) → 77

1₀(23) → 35

1₀(1) → 33

1₀(7) → 8

1₀(33) → 32

1₀(35) → 34

1₀(45) → 46

1₀(127) → 128

1₀(75) → 110

1₀(12) → 13

1₀(73) → 69

1₀(59) → 56

1₀(31) → 29

1₀(58) → 59

1₀(5) → 1

1₀(13) → 14

1₀(116) → 117

1₀(122) → 119

3₁(137) → 138

3₁(192) → 193

3₁(158) → 159

3₁(154) → 155

3₁(172) → 173

3₁(177) → 178

3₁(142) → 143

3₁(197) → 198

3₁(211) → 212

2₁(136) → 137

2₁(153) → 154

2₁(196) → 197

2₁(191) → 192

2₁(176) → 177

2₁(157) → 158

2₁(171) → 172

2₁(141) → 142

2₁(210) → 211

4₀(125) → 126

4₀(108) → 104

4₀(42) → 93

4₀(97) → 98

4₀(78) → 79

4₀(88) → 89

4₀(53) → 54

4₀(4) → 18

4₀(41) → 92

4₀(67) → 68

4₀(3) → 12

4₀(57) → 58

4₀(115) → 116

4₀(12) → 120

4₀(111) → 112

4₀(2) → 26

78	→	209
111	→	190
25	→	51
32	→	7
32	→	158
32	→	51
29	→	124
80	→	75
96	→	26
119	→	52
39	→	26
3	→	170
50	→	66
213	→	48
9	→	51
37	→	76
37	→	51
34	→	27
34	→	51
65	→	66
199	→	27
55	→	44
62	→	51
1	→	51
123	→	7
123	→	158
123	→	51
135	→	153
179	→	86
86	→	75
91	→	66
36	→	26
21	→	124
138	→	73
6	→	51
109	→	124
88	→	175
22	→	124
22	→	27
22	→	51
174	→	61
143	→	45
53	→	205
2	→	139
11	→	26
4	→	195
28	→	10
28	→	159
16	→	51
114	→	26
93	→	26
140	→	157
104	→	124
69	→	51
42	→	27
42	→	51
64	→	66
83	→	66
17	→	26
47	→	124
160	→	45
206	→	157
74	→	27
74	→	51
19	→	75
43	→	124
194	→	109
70	→	134
56	→	124
94	→	105
94	→	124
156	→	73
f6₀	→	2
5₀(99)	→	100
5₀(20)	→	19
5₀(128)	→	123
5₀(24)	→	64
5₀(95)	→	94
5₀(6)	→	37
5₀(117)	→	114
5₀(82)	→	80
5₀(2)	→	75
5₀(3)	→	70
5₀(41)	→	39
5₀(35)	→	42
5₀(102)	→	103
5₀(17)	→	38
5₀(81)	→	82
4₁(195)	→	196
4₁(175)	→	176
4₁(170)	→	171
4₁(209)	→	210
4₁(190)	→	191
4₁(205)	→	206
2₀(106)	→	107
2₀(126)	→	127
2₀(26)	→	27
2₀(85)	→	83
2₀(58)	→	63
2₀(120)	→	121
2₀(92)	→	91
2₀(90)	→	86
2₀(75)	→	76
2₀(3)	→	7
2₀(40)	→	61
2₀(113)	→	109
2₀(12)	→	23
2₀(72)	→	73
2₀(27)	→	48
2₀(13)	→	81
2₀(103)	→	101
2₀(2)	→	51
2₀(4)	→	5
2₀(44)	→	45
0₁(134)	→	135
0₁(140)	→	141
0₁(139)	→	140
0₁(135)	→	136
0₀(51)	→	57
0₀(3)	→	4
0₀(66)	→	67
0₀(77)	→	78
0₀(24)	→	36
0₀(26)	→	97
0₀(87)	→	88
0₀(52)	→	53
0₀(70)	→	71
0₀(84)	→	85
0₀(110)	→	111
0₀(75)	→	87
0₀(15)	→	11
0₀(97)	→	115
0₀(107)	→	108
0₀(124)	→	125
0₀(14)	→	15
0₀(2)	→	3
0₀(100)	→	96
1₁(212)	→	213
1₁(198)	→	199
1₁(159)	→	160
1₁(178)	→	179
1₁(193)	→	194
1₁(173)	→	174
1₁(155)	→	156
3₀(26)	→	66
3₀(71)	→	72
3₀(58)	→	84
3₀(51)	→	52
3₀(48)	→	49
3₀(4)	→	30
3₀(112)	→	113
3₀(12)	→	40
3₀(8)	→	6
3₀(89)	→	90
3₀(55)	→	50
3₀(9)	→	95
3₀(68)	→	65
3₀(18)	→	17
3₀(27)	→	28
3₀(23)	→	24
3₀(54)	→	55
3₀(13)	→	102
3₀(63)	→	62
3₀(79)	→	74
3₀(121)	→	122
3₀(3)	→	44
3₀(40)	→	41
3₀(5)	→	16
3₀(22)	→	118
3₀(7)	→	10
1₀(2)	→	124
1₀(51)	→	105
1₀(18)	→	20
1₀(46)	→	43
1₀(28)	→	25
1₀(10)	→	9
1₀(49)	→	47
1₀(105)	→	106
1₀(98)	→	99
1₀(30)	→	31
1₀(24)	→	22
1₀(8)	→	21
1₀(61)	→	60
1₀(76)	→	77
1₀(23)	→	35
1₀(1)	→	33
1₀(7)	→	8
1₀(33)	→	32
1₀(35)	→	34
1₀(45)	→	46
1₀(127)	→	128
1₀(75)	→	110
1₀(12)	→	13
1₀(73)	→	69
1₀(59)	→	56
1₀(31)	→	29
1₀(58)	→	59
1₀(5)	→	1
1₀(13)	→	14
1₀(116)	→	117
1₀(122)	→	119
3₁(137)	→	138
3₁(192)	→	193
3₁(158)	→	159
3₁(154)	→	155
3₁(172)	→	173
3₁(177)	→	178
3₁(142)	→	143
3₁(197)	→	198
3₁(211)	→	212
2₁(136)	→	137
2₁(153)	→	154
2₁(196)	→	197
2₁(191)	→	192
2₁(176)	→	177
2₁(157)	→	158
2₁(171)	→	172
2₁(141)	→	142
2₁(210)	→	211
4₀(125)	→	126
4₀(108)	→	104
4₀(42)	→	93
4₀(97)	→	98
4₀(78)	→	79
4₀(88)	→	89
4₀(53)	→	54
4₀(4)	→	18
4₀(41)	→	92
4₀(67)	→	68
4₀(3)	→	12
4₀(57)	→	58
4₀(115)	→	116
4₀(12)	→	120
4₀(111)	→	112
4₀(2)	→	26