Certification Problem
Input (TPDB SRS_Standard/Zantema_04/z096)
The rewrite relation of the following TRS is considered.
a
(
a
(
b
(
b
(
x1
))))
→
b
(
b
(
b
(
b
(
b
(
a
(
a
(
a
(
a
(
a
(
x1
))))))))))
(1)
Property / Task
Prove or disprove termination.
Answer / Result
No.
Proof (by ttt2 @ termCOMP 2023)
1 Loop
The following loop proves nontermination.
t
0
=
a
(
a
(
b
(
b
(
b
(
b
(
x18
))))))
→
b
(
b
(
b
(
b
(
b
(
a
(
a
(
a
(
a
(
a
(
b
(
b
(
x18
))))))))))))
→
b
(
b
(
b
(
b
(
b
(
a
(
a
(
a
(
b
(
b
(
b
(
b
(
b
(
a
(
a
(
a
(
a
(
a
(
x18
))))))))))))))))))
=
t
2
where t
2
= C[t
0
σ] and σ = {
x18
/
b
(
a
(
a
(
a
(
a
(
a
(
x18
))))))} and C =
b
(
b
(
b
(
b
(
b
(
a
(
☐
))))))