Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_Zan97_GM)

The rewrite relation of the following TRS is considered.

a__g(X)	→	a__h(X)	(1)
a__c	→	d	(2)
a__h(d)	→	a__g(c)	(3)
mark(g(X))	→	a__g(X)	(4)
mark(h(X))	→	a__h(X)	(5)
mark(c)	→	a__c	(6)
mark(d)	→	d	(7)
a__g(X)	→	g(X)	(8)
a__h(X)	→	h(X)	(9)
a__c	→	c	(10)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Bounds

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

final states:

{0, 1, 2, 3, 4, 5, 6, 7}

transitions:

a__g₀(0)	→	0
a__g₀(1)	→	0
a__g₀(2)	→	0
a__g₀(3)	→	0
a__g₀(4)	→	0
a__g₀(5)	→	0
a__g₀(6)	→	0
a__g₀(7)	→	0
a__h₀(0)	→	1
a__h₀(1)	→	1
a__h₀(2)	→	1
a__h₀(3)	→	1
a__h₀(4)	→	1
a__h₀(5)	→	1
a__h₀(6)	→	1
a__h₀(7)	→	1
a__c₀	→	2
d₀	→	3
c₀	→	4
mark₀(0)	→	5
mark₀(1)	→	5
mark₀(2)	→	5
mark₀(3)	→	5
mark₀(4)	→	5
mark₀(5)	→	5
mark₀(6)	→	5
mark₀(7)	→	5
g₀(0)	→	6
g₀(1)	→	6
g₀(2)	→	6
g₀(3)	→	6
g₀(4)	→	6
g₀(5)	→	6
g₀(6)	→	6
g₀(7)	→	6
h₀(0)	→	7
h₀(1)	→	7
h₀(2)	→	7
h₀(3)	→	7
h₀(4)	→	7
h₀(5)	→	7
h₀(6)	→	7
h₀(7)	→	7
a__h₁(0)	→	0
a__h₁(1)	→	0
a__h₁(2)	→	0
a__h₁(3)	→	0
a__h₁(4)	→	0
a__h₁(5)	→	0
a__h₁(6)	→	0
a__h₁(7)	→	0
d₁	→	2
c₁	→	8
a__g₁(8)	→	1
a__g₁(0)	→	5
a__g₁(1)	→	5
a__g₁(2)	→	5
a__g₁(3)	→	5
a__g₁(4)	→	5
a__g₁(5)	→	5
a__g₁(6)	→	5
a__g₁(7)	→	5
a__c₁	→	0
g₁(0)	→	0
g₁(1)	→	0
g₁(3)	→	0
g₁(4)	→	0
g₁(5)	→	0
g₁(6)	→	0
g₁(7)	→	0
h₁(0)	→	1
h₁(1)	→	1
h₁(3)	→	1
h₁(4)	→	1
h₁(5)	→	1
h₁(6)	→	1
h₁(7)	→	1
a__h₂(8)	→	1
a__h₂(0)	→	0
a__h₂(1)	→	0
a__h₂(3)	→	0
a__h₂(4)	→	0
a__h₂(5)	→	0
a__h₂(6)	→	0
a__h₂(7)	→	0
d₂	→	0
c₂	→	9
a__g₂(9)	→	0
g₂(8)	→	1
g₂(0)	→	0
g₂(3)	→	0
g₂(4)	→	0
g₂(5)	→	0
g₂(6)	→	0
g₂(7)	→	0
h₂(0)	→	0
h₂(3)	→	0
h₂(4)	→	0
h₂(5)	→	0
h₂(6)	→	0
h₂(7)	→	0
a__h₃(9)	→	0
c₃	→	10
a__g₃(10)	→	0
g₃(9)	→	0
h₃(8)	→	0
h₃(0)	→	0
h₃(3)	→	0
h₃(4)	→	0
h₃(5)	→	0
h₃(6)	→	0
h₃(7)	→	0
a__h₄(10)	→	0
g₄(10)	→	0
h₄(9)	→	0
a__g₁(10)	→	0
h₅(10)	→	0
a__h₂(10)	→	0
g₂(10)	→	0
a__h₁(10)	→	0
h₂(10)	→	0
h₃(10)	→	0
0	→	5
0	→	1
2	→	0
8	→	2
1	→	0
9	→	0