Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z043)

The rewrite relation of the following TRS is considered.

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

→

a(a(b(a(a(b(c(b(a(c(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 3. This is shown by the following automaton.

final states:

{4}

transitions:

25	→	33
25	→	59
81	→	83
57	→	70
34	→	17
71	→	60
26	→	4
26	→	17
58	→	17
58	→	28
21	→	48
105	→	107
67	→	72
82	→	49
117	→	76
4	→	16
28	→	17
106	→	73
93	→	52
69	→	20
64	→	96
24	→	27
b₂(74)	→	75
b₂(66)	→	67
b₂(61)	→	62
b₂(50)	→	51
b₂(52)	→	53
b₂(79)	→	80
b₂(55)	→	56
b₂(76)	→	77
b₂(63)	→	64
c₂(72)	→	73
c₂(51)	→	52
c₂(48)	→	49
c₂(59)	→	60
c₂(70)	→	71
c₂(62)	→	63
c₂(75)	→	76
a₂(65)	→	66
a₂(73)	→	74
a₂(81)	→	82
a₂(78)	→	79
a₂(60)	→	61
a₂(77)	→	78
a₂(56)	→	57
a₂(64)	→	65
a₂(57)	→	58
a₂(54)	→	55
a₂(80)	→	81
a₂(49)	→	50
a₂(53)	→	54
a₂(67)	→	68
a₂(68)	→	69
b₀(4)	→	4
a₀(4)	→	4
a₃(108)	→	109
a₃(101)	→	102
a₃(112)	→	113
a₃(97)	→	98
a₃(88)	→	89
a₃(84)	→	85
a₃(92)	→	93
a₃(89)	→	90
a₃(116)	→	117
a₃(102)	→	103
a₃(91)	→	92
a₃(115)	→	116
a₃(104)	→	105
a₃(105)	→	106
a₃(113)	→	114
b₃(90)	→	91
b₃(87)	→	88
b₃(98)	→	99
b₃(114)	→	115
b₃(109)	→	110
b₃(85)	→	86
b₃(111)	→	112
b₃(103)	→	104
b₃(100)	→	101
c₀(4)	→	4
b₁(18)	→	19
b₁(23)	→	24
b₁(20)	→	21
c₁(19)	→	20
c₁(33)	→	34
c₁(27)	→	28
c₁(16)	→	17
c₃(99)	→	100
c₃(110)	→	111
c₃(96)	→	97
c₃(107)	→	108
c₃(86)	→	87
c₃(83)	→	84
a₁(22)	→	23
a₁(24)	→	25
a₁(17)	→	18
a₁(21)	→	22
a₁(25)	→	26

The automaton is closed under rewriting as it is compatible.