Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z045)

The rewrite relation of the following TRS is considered.

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

→

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

final states:

{4}

transitions:

25	→	59
102	→	61
32	→	4
32	→	21
34	→	20
40	→	20
58	→	24
72	→	21
88	→	46
4	→	19
28	→	33
100	→	119
30	→	39
30	→	45
132	→	64
70	→	87
56	→	89
b₂(51)	→	52
b₂(67)	→	68
b₂(65)	→	66
b₂(53)	→	54
b₂(95)	→	96
b₂(98)	→	99
b₂(91)	→	92
b₂(61)	→	62
b₂(50)	→	51
b₂(56)	→	57
b₂(64)	→	65
b₂(68)	→	69
b₂(70)	→	71
b₂(94)	→	95
b₂(97)	→	98
b₂(47)	→	48
b₂(100)	→	101
b₂(54)	→	55
c₂(46)	→	47
c₂(60)	→	61
c₂(93)	→	94
c₂(63)	→	64
c₂(90)	→	91
c₂(49)	→	50
a₂(59)	→	60
a₂(45)	→	46
a₂(99)	→	100
a₂(92)	→	93
a₂(55)	→	56
a₂(87)	→	88
a₂(69)	→	70
a₂(57)	→	58
a₂(96)	→	97
a₂(101)	→	102
a₂(71)	→	72
a₂(62)	→	63
a₂(48)	→	49
a₂(66)	→	67
a₂(89)	→	90
a₂(52)	→	53
a₀(4)	→	4
b₀(4)	→	4
a₃(122)	→	123
a₃(129)	→	130
a₃(119)	→	120
a₃(131)	→	132
a₃(126)	→	127
b₃(121)	→	122
b₃(128)	→	129
b₃(130)	→	131
b₃(125)	→	126
b₃(127)	→	128
b₃(124)	→	125
c₀(4)	→	4
b₁(28)	→	29
b₁(24)	→	25
b₁(25)	→	26
b₁(27)	→	28
b₁(30)	→	31
b₁(21)	→	22
c₁(23)	→	24
c₁(20)	→	21
c₃(123)	→	124
c₃(120)	→	121
a₁(22)	→	23
a₁(26)	→	27
a₁(29)	→	30
a₁(33)	→	34
a₁(31)	→	32
a₁(39)	→	40
a₁(19)	→	20

The automaton is closed under rewriting as it is compatible.