YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{142, 138, 135, 131, 129, 127, 124, 120, 118, 114, 111, 108, 106, 103, 99, 96, 92, 87, 82, 76, 74, 69, 68, 65, 64, 63, 62, 61, 57, 53, 52, 47, 46, 41, 38, 34, 32, 28, 24, 20, 14, 11, 7, 6, 1}

transitions:

111 → 77

32 → 83

129 → 77

41 → 83

120 → 77

57 → 77

187 → 139

34 → 83

65 → 21

65 → 146

55 → 183

20 → 77

62 → 77

1 → 83

127 → 77

135 → 77

76 → 83

38 → 83

178 → 106

138 → 21

138 → 146

6 → 83

124 → 88

124 → 77

174 → 163

174 → 175

53 → 88

53 → 77

2 → 145

11 → 83

28 → 58

28 → 21

28 → 146

118 → 77

114 → 77

14 → 77

63 → 77

7 → 83

69 → 70

69 → 147

69 → 21

69 → 146

64 → 58

64 → 21

64 → 146

46 → 83

48 → 77

47 → 83

168 → 106

68 → 21

68 → 146

142 → 21

142 → 146

131 → 77

74 → 83

24 → 77

166 → 106

166 → 167

151 → 104

151 → 163

151 → 173

0₁(167) → 168

0₁(149) → 150

0₁(165) → 166

0₁(175) → 176

5₁(145) → 146

5₁(186) → 187

5₁(146) → 147

3₁(185) → 186

4₁(147) → 148

1₀(19) → 14

1₀(73) → 69

1₀(3) → 4

1₀(33) → 32

1₀(77) → 78

1₀(48) → 49

1₀(121) → 122

1₀(21) → 48

1₀(143) → 144

1₀(8) → 9

1₀(134) → 131

1₀(29) → 30

1₀(128) → 127

1₀(56) → 53

1₀(18) → 33

1₀(27) → 130

1₀(79) → 80

1₀(60) → 57

1₀(119) → 118

1₀(136) → 137

1₀(5) → 39

1₀(117) → 114

1₀(28) → 61

1₀(36) → 37

1₀(43) → 44

1₀(116) → 117

1₀(2) → 3

1₀(23) → 20

1₀(17) → 66

1₀(104) → 107

1₀(100) → 101

1₀(12) → 13

3₀(20) → 68

3₀(2) → 77

3₀(78) → 132

3₀(42) → 121

3₀(28) → 62

3₀(37) → 34

3₀(59) → 60

3₀(115) → 116

3₀(85) → 86

3₀(89) → 90

3₀(1) → 75

3₀(55) → 56

3₀(141) → 138

3₀(93) → 112

3₀(125) → 126

3₀(18) → 19

3₀(27) → 128

3₀(97) → 98

3₀(66) → 67

3₀(39) → 40

3₀(130) → 129

3₀(3) → 25

3₀(29) → 88

3₀(101) → 102

3₀(30) → 31

3₀(22) → 23

3₀(35) → 115

2₀(26) → 109

2₀(42) → 43

2₀(78) → 79

2₀(59) → 97

2₀(112) → 113

2₀(105) → 103

2₀(3) → 8

2₀(140) → 141

2₀(116) → 119

2₀(9) → 10

2₀(80) → 81

2₀(15) → 16

2₀(27) → 24

2₀(49) → 50

2₀(13) → 11

2₀(71) → 72

2₀(17) → 143

2₀(93) → 94

2₀(2) → 29

2₀(4) → 5

2₀(44) → 45

2₀(22) → 54

4₀(25) → 93

4₀(21) → 22

4₀(58) → 59

4₀(88) → 89

4₀(26) → 27

4₀(84) → 85

4₀(6) → 46

4₀(20) → 63

4₀(139) → 140

4₀(3) → 42

4₀(31) → 125

4₀(102) → 99

4₀(133) → 134

4₀(70) → 71

4₀(137) → 135

4₀(126) → 124

4₀(23) → 136

4₀(104) → 105

4₀(2) → 15

5₀(90) → 91

5₀(31) → 28

5₀(132) → 133

5₀(88) → 139

5₀(21) → 70

5₀(94) → 95

5₀(84) → 104

5₀(144) → 142

5₀(83) → 84

5₀(2) → 21

5₀(3) → 58

5₀(28) → 64

5₀(35) → 36

5₀(67) → 65

5₀(25) → 26

f6₀ → 2

0₀(51) → 47

0₀(123) → 120

0₀(91) → 87

0₀(10) → 7

0₀(54) → 55

0₀(110) → 108

0₀(98) → 96

0₀(50) → 51

0₀(95) → 92

0₀(113) → 111

0₀(107) → 106

0₀(8) → 12

0₀(3) → 83

0₀(17) → 18

0₀(86) → 82

0₀(81) → 76

0₀(1) → 6

0₀(29) → 35

0₀(35) → 100

0₀(45) → 41

0₀(75) → 74

0₀(20) → 52

0₀(40) → 38

0₀(16) → 17

0₀(109) → 110

0₀(5) → 1

0₀(72) → 73

0₀(122) → 123

2₁(177) → 178

2₁(164) → 165

2₁(148) → 149

2₁(183) → 184

2₁(173) → 174

1₁(176) → 177

1₁(163) → 164

1₁(150) → 151

1₁(184) → 185

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