Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z039)

The rewrite relation of the following TRS is considered.

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

→

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

→

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

78	→	34
23	→	31
23	→	75
32	→	16
18	→	77
37	→	63
37	→	95
26	→	16
76	→	34
72	→	17
4	→	15
104	→	35
104	→	65
104	→	97
42	→	16
42	→	17
42	→	26
42	→	34
42	→	64
42	→	35
42	→	96
24	→	4
24	→	16
24	→	26
24	→	34
19	→	25
19	→	33
b₂(35)	→	36
b₂(65)	→	66
b₂(70)	→	71
b₂(40)	→	41
a₂(34)	→	35
a₂(77)	→	78
a₂(68)	→	69
a₂(64)	→	65
a₂(63)	→	64
a₂(69)	→	70
a₂(39)	→	40
a₂(38)	→	39
a₂(33)	→	34
a₂(75)	→	76
c₂(41)	→	42
c₂(37)	→	38
c₂(36)	→	37
c₂(71)	→	72
c₂(67)	→	68
c₂(66)	→	67
c₀(4)	→	4
b₀(4)	→	4
c₃(99)	→	100
c₃(98)	→	99
c₃(103)	→	104
b₃(97)	→	98
b₃(102)	→	103
a₀(4)	→	4
b₁(22)	→	23
b₁(17)	→	18
a₁(25)	→	26
a₁(21)	→	22
a₁(15)	→	16
a₁(20)	→	21
a₁(16)	→	17
a₁(31)	→	32
a₃(100)	→	101
a₃(96)	→	97
a₃(101)	→	102
a₃(95)	→	96
c₁(18)	→	19
c₁(19)	→	20
c₁(23)	→	24

The automaton is closed under rewriting as it is compatible.