YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

b(a(b(a(a(x0)))))

→

a(a(a(b(a(b(a(b(x0))))))))

Proof

1 String Reversal

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

a(a(b(a(b(x0)))))

→

b(a(b(a(b(a(a(a(x0))))))))

1.1 Bounds

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

final states:

{1}

transitions:

33 → 64

9 → 28

5 → 55

99 → 31

1 → 4

1 → 3

60 → 91

135 → 92

36 → 20

72 → 22

141 → 172

171 → 94

116 → 127

117 → 57

117 → 58

180 → 130

63 → 29

112 → 136

7 → 19

132 → 163

24 → 109

144 → 128

27 → 5

27 → 56

a₁(19) → 20

a₁(61) → 62

a₁(28) → 29

a₁(23) → 24

a₁(29) → 30

a₁(57) → 58

a₁(59) → 60

a₁(55) → 56

a₁(25) → 26

a₁(34) → 35

a₁(20) → 21

a₁(56) → 57

a₁(32) → 33

a₁(30) → 31

a₁(21) → 22

a₀(8) → 9

a₀(2) → 3

a₀(6) → 7

a₀(4) → 5

a₀(3) → 4

a₂(65) → 66

a₂(70) → 71

a₂(91) → 92

a₂(95) → 96

a₂(110) → 111

a₂(92) → 93

a₂(131) → 132

a₂(129) → 130

a₂(109) → 110

a₂(97) → 98

a₂(64) → 65

a₂(113) → 114

a₂(111) → 112

a₂(128) → 129

a₂(127) → 128

a₂(115) → 116

a₂(133) → 134

a₂(93) → 94

a₂(68) → 69

a₂(66) → 67

b₃(175) → 176

b₃(166) → 167

b₃(141) → 142

b₃(143) → 144

b₃(170) → 171

b₃(179) → 180

b₃(177) → 178

b₃(139) → 140

b₃(168) → 169

a₃(167) → 168

a₃(136) → 137

a₃(173) → 174

a₃(174) → 175

a₃(140) → 141

a₃(165) → 166

a₃(164) → 165

a₃(176) → 177

a₃(172) → 173

a₃(163) → 164

a₃(137) → 138

a₃(169) → 170

a₃(138) → 139

a₃(142) → 143

a₃(178) → 179

b₂(114) → 115

b₂(134) → 135

b₂(98) → 99

b₂(67) → 68

b₂(71) → 72

b₂(96) → 97

b₂(94) → 95

b₂(132) → 133

b₂(112) → 113

b₂(130) → 131

b₂(116) → 117

b₂(69) → 70

b₀(9) → 1

b₀(7) → 8

b₀(5) → 6

f2₀ → 2

b₁(22) → 23

b₁(24) → 25

b₁(58) → 59

b₁(26) → 27

b₁(60) → 61

b₁(33) → 34

b₁(35) → 36

b₁(31) → 32

b₁(62) → 63

33	→	64
9	→	28
5	→	55
99	→	31
1	→	4
1	→	3
60	→	91
135	→	92
36	→	20
72	→	22
141	→	172
171	→	94
116	→	127
117	→	57
117	→	58
180	→	130
63	→	29
112	→	136
7	→	19
132	→	163
24	→	109
144	→	128
27	→	5
27	→	56
a₁(19)	→	20
a₁(61)	→	62
a₁(28)	→	29
a₁(23)	→	24
a₁(29)	→	30
a₁(57)	→	58
a₁(59)	→	60
a₁(55)	→	56
a₁(25)	→	26
a₁(34)	→	35
a₁(20)	→	21
a₁(56)	→	57
a₁(32)	→	33
a₁(30)	→	31
a₁(21)	→	22
a₀(8)	→	9
a₀(2)	→	3
a₀(6)	→	7
a₀(4)	→	5
a₀(3)	→	4
a₂(65)	→	66
a₂(70)	→	71
a₂(91)	→	92
a₂(95)	→	96
a₂(110)	→	111
a₂(92)	→	93
a₂(131)	→	132
a₂(129)	→	130
a₂(109)	→	110
a₂(97)	→	98
a₂(64)	→	65
a₂(113)	→	114
a₂(111)	→	112
a₂(128)	→	129
a₂(127)	→	128
a₂(115)	→	116
a₂(133)	→	134
a₂(93)	→	94
a₂(68)	→	69
a₂(66)	→	67
b₃(175)	→	176
b₃(166)	→	167
b₃(141)	→	142
b₃(143)	→	144
b₃(170)	→	171
b₃(179)	→	180
b₃(177)	→	178
b₃(139)	→	140
b₃(168)	→	169
a₃(167)	→	168
a₃(136)	→	137
a₃(173)	→	174
a₃(174)	→	175
a₃(140)	→	141
a₃(165)	→	166
a₃(164)	→	165
a₃(176)	→	177
a₃(172)	→	173
a₃(163)	→	164
a₃(137)	→	138
a₃(169)	→	170
a₃(138)	→	139
a₃(142)	→	143
a₃(178)	→	179
b₂(114)	→	115
b₂(134)	→	135
b₂(98)	→	99
b₂(67)	→	68
b₂(71)	→	72
b₂(96)	→	97
b₂(94)	→	95
b₂(132)	→	133
b₂(112)	→	113
b₂(130)	→	131
b₂(116)	→	117
b₂(69)	→	70
b₀(9)	→	1
b₀(7)	→	8
b₀(5)	→	6
f2₀	→	2
b₁(22)	→	23
b₁(24)	→	25
b₁(58)	→	59
b₁(26)	→	27
b₁(60)	→	61
b₁(33)	→	34
b₁(35)	→	36
b₁(31)	→	32
b₁(62)	→	63