Certification Problem
Input (TPDB TRS_Standard/AProVE_08/round_nonterm)
The rewrite relation of the following TRS is considered.
f
(
s
(
x
),
x
)
→
f
(
s
(
x
),
round
(
x
))
(1)
round
(
0
)
→
0
(2)
round
(
0
)
→
s
(
0
)
(3)
round
(
s
(
0
))
→
s
(
0
)
(4)
round
(
s
(
s
(
x
)))
→
s
(
s
(
round
(
x
)))
(5)
Property / Task
Prove or disprove termination.
Answer / Result
No.
Proof (by ttt2 @ termCOMP 2023)
1 Loop
The following loop proves nontermination.
t
0
=
f
(
s
(
0
),
0
)
→
f
(
s
(
0
),
round
(
0
))
→
f
(
s
(
0
),
0
)
=
t
2
where t
2
= t
0