Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_AG01/#4.13)

The rewrite relation of the following TRS is considered.

f(0,1,x) → f(x,x,x) (1)
f(x,y,z) → 2 (2)
0 → 2 (3)
1 → 2 (4)
g(x,x,y) → y (5)
g(x,y,y) → x (6)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(0,1,x) → f#(x,x,x) (7)
It remains to prove infiniteness of the resulting DP problem.

1.1 Loop

The following loop proves infiniteness of the DP problem.

t0 = f#(g(1,0,0),g(1,0,0),g(1,0,0))
→R f#(g(1,0,0),1,g(1,0,0))
→R f#(g(1,2,0),1,g(1,0,0))
→R f#(g(2,2,0),1,g(1,0,0))
→R f#(0,1,g(1,0,0))
→P f#(g(1,0,0),g(1,0,0),g(1,0,0))
= t5
where t5 = t0