Certification Problem
Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM04_L)
The rewrite relation of the following TRS is considered.
hd
(
cons
)
→
X
(1)
tl
(
cons
)
→
Y
(2)
nats
→
adx
(
zeros
)
(3)
zeros
→
cons
(4)
incr
(
cons
)
→
cons
(5)
adx
(
cons
)
→
incr
(
cons
)
(6)
Property / Task
Prove or disprove termination.
Answer / Result
No.
Proof (by ttt2 @ termCOMP 2023)
1 Loop
The following loop proves nontermination.
t
0
=
hd
(
cons
)
→
hd
(
cons
)
=
t
1
where t
1
= t
0
σ and σ = {
X
/
hd
(
cons
)}