Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z048)

The rewrite relation of the following TRS is considered.

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

→

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

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 String Reversal

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

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

→

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

(2)

1.1 Bounds

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

final states:

{4}

transitions:

20	→	33
26	→	4
26	→	17
26	→	28
26	→	47
38	→	68
38	→	83
21	→	27
21	→	46
4	→	16
28	→	17
93	→	49
69	→	47
43	→	17
43	→	28
43	→	47
56	→	19
56	→	49
a₂(35)	→	36
a₂(46)	→	47
a₂(41)	→	42
a₂(33)	→	34
a₂(48)	→	49
a₂(52)	→	53
a₂(68)	→	69
a₂(39)	→	40
a₂(54)	→	55
b₂(51)	→	52
b₂(50)	→	51
b₂(37)	→	38
b₂(34)	→	35
b₂(47)	→	48
b₂(38)	→	39
b₂(53)	→	54
b₂(40)	→	41
c₂(42)	→	43
c₂(55)	→	56
c₂(36)	→	37
c₂(49)	→	50
b₀(4)	→	4
c₀(4)	→	4
c₃(86)	→	87
c₃(92)	→	93
a₃(91)	→	92
a₃(85)	→	86
a₃(83)	→	84
a₃(89)	→	90
a₀(4)	→	4
a₁(22)	→	23
a₁(18)	→	19
a₁(24)	→	25
a₁(16)	→	17
a₁(27)	→	28
b₁(21)	→	22
b₁(17)	→	18
b₁(23)	→	24
b₁(20)	→	21
b₃(88)	→	89
b₃(84)	→	85
b₃(90)	→	91
b₃(87)	→	88
c₁(19)	→	20
c₁(25)	→	26

The automaton is closed under rewriting as it is compatible.