Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z047)

The rewrite relation of the following TRS is considered.

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

→

a(b(a(a(c(a(b(c(a(b(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(a(c(x1))))

→

b(a(c(b(a(c(a(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:

23	→	31
23	→	33
32	→	17
89	→	47
37	→	90
20	→	46
40	→	79
26	→	4
26	→	19
26	→	17
4	→	16
100	→	80
43	→	17
43	→	20
56	→	32
56	→	34
a₂(51)	→	52
a₂(35)	→	36
a₂(46)	→	47
a₂(49)	→	50
a₂(41)	→	42
a₂(33)	→	34
a₂(48)	→	49
a₂(36)	→	37
a₂(54)	→	55
a₂(38)	→	39
c₂(50)	→	51
c₂(37)	→	38
c₂(53)	→	54
c₂(40)	→	41
b₂(42)	→	43
b₂(34)	→	35
b₂(55)	→	56
b₂(47)	→	48
b₂(39)	→	40
b₂(52)	→	53
b₀(4)	→	4
c₀(4)	→	4
b₃(99)	→	100
b₃(88)	→	89
b₃(96)	→	97
b₃(80)	→	81
b₃(85)	→	86
b₃(91)	→	92
a₃(90)	→	91
a₃(93)	→	94
a₃(87)	→	88
a₃(79)	→	80
a₃(95)	→	96
a₃(98)	→	99
a₃(92)	→	93
a₃(84)	→	85
a₃(82)	→	83
a₃(81)	→	82
a₀(4)	→	4
a₁(19)	→	20
a₁(18)	→	19
a₁(24)	→	25
a₁(16)	→	17
a₁(31)	→	32
a₁(21)	→	22
c₁(23)	→	24
c₁(20)	→	21
c₃(97)	→	98
c₃(86)	→	87
c₃(94)	→	95
c₃(83)	→	84
b₁(22)	→	23
b₁(17)	→	18
b₁(25)	→	26

The automaton is closed under rewriting as it is compatible.