Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_mixed_05/test9)

The rewrite relation of the following TRS is considered.

f(0,1,X) h(X,X) (1)
h(0,X) f(0,X,X) (2)
g(X,Y) X (3)
g(X,Y) Y (4)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = h(0,g(1,0))
f(0,g(1,0),g(1,0))
f(0,1,g(1,0))
h(g(1,0),g(1,0))
h(0,g(1,0))
= t4
where t4 = t0