YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{147, 141, 138, 135, 131, 127, 124, 120, 116, 112, 107, 102, 97, 93, 89, 84, 81, 75, 70, 67, 63, 59, 53, 49, 45, 40, 35, 30, 28, 24, 18, 14, 8, 1}

transitions:

102 → 19

89 → 9

81 → 143

81 → 3

97 → 9

84 → 143

84 → 3

18 → 142

120 → 54

147 → 54

59 → 19

107 → 19

49 → 143

49 → 3

1 → 142

40 → 142

8 → 142

127 → 143

127 → 3

135 → 54

141 → 19

138 → 54

116 → 54

75 → 143

75 → 3

124 → 142

67 → 142

82 → 150

53 → 9

28 → 142

45 → 142

14 → 142

93 → 9

63 → 54

112 → 19

30 → 142

35 → 142

131 → 9

24 → 142

70 → 9

156 → 36

f6₀ → 2

4₀(34) → 30

4₀(19) → 71

4₀(98) → 113

4₀(114) → 115

4₀(76) → 77

4₀(85) → 86

4₀(144) → 148

4₀(83) → 81

4₀(2) → 54

4₀(36) → 46

4₀(41) → 60

4₀(103) → 104

4₀(108) → 109

4₀(134) → 131

4₀(136) → 137

3₁(150) → 151

1₀(100) → 101

1₀(41) → 42

1₀(144) → 145

1₀(37) → 38

1₀(86) → 87

1₀(108) → 132

1₀(142) → 143

1₀(6) → 7

1₀(60) → 61

1₀(43) → 44

1₀(109) → 125

1₀(88) → 84

1₀(64) → 65

1₀(9) → 85

1₀(50) → 51

1₀(27) → 24

1₀(13) → 8

1₀(21) → 68

1₀(48) → 45

1₀(17) → 14

1₀(122) → 123

1₀(10) → 25

1₀(2) → 3

1₀(39) → 35

1₀(66) → 63

3₀(130) → 127

3₀(95) → 96

3₀(105) → 106

3₀(3) → 4

3₀(25) → 26

3₀(129) → 130

3₀(98) → 99

3₀(77) → 90

3₀(58) → 53

3₀(61) → 62

3₀(21) → 139

3₀(52) → 49

3₀(9) → 98

3₀(82) → 83

3₀(110) → 111

3₀(109) → 110

3₀(62) → 59

3₀(42) → 43

3₀(4) → 5

3₀(22) → 23

3₀(2) → 19

3₀(57) → 58

3₀(104) → 105

2₁(154) → 155

2₁(155) → 156

2₁(153) → 154

5₀(41) → 64

5₀(2) → 142

5₀(31) → 32

5₀(21) → 22

5₀(117) → 118

5₀(80) → 75

5₀(76) → 108

5₀(126) → 124

5₀(11) → 12

5₀(128) → 129

5₀(69) → 67

5₀(33) → 34

0₀(2) → 76

0₀(46) → 47

0₀(9) → 41

0₀(65) → 66

0₀(133) → 134

0₀(10) → 11

0₀(54) → 55

0₀(79) → 80

0₀(113) → 114

0₀(71) → 72

0₀(25) → 136

0₀(38) → 39

0₀(96) → 93

0₀(3) → 31

0₀(87) → 88

0₀(118) → 119

0₀(140) → 138

0₀(23) → 18

0₀(132) → 133

0₀(125) → 126

0₀(32) → 33

0₀(121) → 122

0₀(111) → 107

0₀(29) → 28

0₀(7) → 1

0₀(15) → 16

0₀(22) → 29

0₀(103) → 117

0₀(85) → 128

0₀(20) → 21

0₀(12) → 13

0₀(143) → 144

0₀(108) → 121

0₀(78) → 79

0₀(44) → 40

0₀(16) → 17

0₀(5) → 6

0₀(106) → 102

0₀(68) → 69

0₀(119) → 116

0₁(152) → 153

4₁(151) → 152

2₀(19) → 20

2₀(101) → 97

2₀(47) → 48

2₀(78) → 82

2₀(99) → 100

2₀(123) → 120

2₀(94) → 95

2₀(26) → 27

2₀(36) → 37

2₀(146) → 141

2₀(4) → 15

2₀(56) → 57

2₀(90) → 91

2₀(10) → 50

2₀(148) → 149

2₀(41) → 94

2₀(92) → 89

2₀(139) → 140

2₀(9) → 10

2₀(149) → 147

2₀(72) → 73

2₀(145) → 146

2₀(3) → 36

2₀(74) → 70

2₀(137) → 135

2₀(51) → 52

2₀(77) → 78

2₀(76) → 103

2₀(91) → 92

2₀(115) → 112

2₀(55) → 56

2₀(2) → 9

2₀(73) → 74

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