Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z032)

The rewrite relation of the following TRS is considered.

b(a(b(a(a(x1)))))

→

a(a(b(b(a(b(a(b(a(x1)))))))))

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 4. This is shown by the following automaton.

final states:

{3}

transitions:

33	→	18
33	→	20
33	→	28
23	→	3
23	→	18
23	→	42
23	→	16
32	→	58
87	→	30
145	→	166
3	→	14
213	→	198
146	→	63
37	→	16
65	→	78
55	→	25
165	→	141
86	→	110
21	→	54
173	→	194
172	→	204
116	→	156
109	→	28
109	→	82
22	→	24
22	→	36
174	→	102
118	→	59
118	→	138
66	→	26
66	→	16
66	→	37
66	→	76
77	→	26
64	→	100
203	→	106
43	→	16
a₄(211)	→	212
a₄(212)	→	213
a₄(158)	→	159
a₄(206)	→	207
a₄(208)	→	209
a₄(201)	→	202
a₄(198)	→	199
a₄(204)	→	205
a₄(196)	→	197
a₄(202)	→	203
a₄(160)	→	161
a₄(163)	→	164
a₄(164)	→	165
a₄(194)	→	195
a₄(156)	→	157
b₄(159)	→	160
b₄(161)	→	162
b₄(205)	→	206
b₄(157)	→	158
b₄(162)	→	163
b₄(209)	→	210
b₄(207)	→	208
b₄(199)	→	200
b₄(210)	→	211
b₄(195)	→	196
b₄(200)	→	201
b₄(197)	→	198
b₃(114)	→	115
b₃(106)	→	107
b₃(170)	→	171
b₃(81)	→	82
b₃(166)	→	167
b₃(142)	→	143
b₃(84)	→	85
b₃(112)	→	113
b₃(105)	→	106
b₃(143)	→	144
b₃(168)	→	169
b₃(79)	→	80
b₃(110)	→	111
b₃(140)	→	141
b₃(101)	→	102
b₃(83)	→	84
b₃(115)	→	116
b₃(103)	→	104
b₃(138)	→	139
b₃(171)	→	172
a₁(16)	→	17
a₁(22)	→	23
a₁(14)	→	15
a₁(21)	→	22
a₁(18)	→	19
b₁(20)	→	21
b₁(17)	→	18
b₁(19)	→	20
b₁(15)	→	16
b₁(36)	→	37
b₁(42)	→	43
a₀(3)	→	3
b₂(29)	→	30
b₂(76)	→	77
b₂(63)	→	64
b₂(58)	→	59
b₂(25)	→	26
b₂(27)	→	28
b₂(60)	→	61
b₂(62)	→	63
b₂(30)	→	31
a₃(167)	→	168
a₃(117)	→	118
a₃(80)	→	81
a₃(113)	→	114
a₃(107)	→	108
a₃(104)	→	105
a₃(86)	→	87
a₃(100)	→	101
a₃(141)	→	142
a₃(111)	→	112
a₃(173)	→	174
a₃(139)	→	140
a₃(172)	→	173
a₃(85)	→	86
a₃(82)	→	83
a₃(108)	→	109
a₃(78)	→	79
a₃(145)	→	146
a₃(144)	→	145
a₃(169)	→	170
a₃(116)	→	117
a₃(102)	→	103
b₀(3)	→	3
a₂(64)	→	65
a₂(24)	→	25
a₂(54)	→	55
a₂(26)	→	27
a₂(28)	→	29
a₂(59)	→	60
a₂(31)	→	32
a₂(61)	→	62
a₂(32)	→	33
a₂(65)	→	66

The automaton is closed under rewriting as it is compatible.