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