Certification Problem

Input (TPDB TRS_Standard/SK90/2.59)

The rewrite relation of the following TRS is considered.

f(g(x),y,y) → g(f(x,x,y)) (1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(f) = 1 stat(f) = mul
prec(g) = 0 stat(g) = mul

π(f) = [1,2,3]
π(g) = [1]

all of the following rules can be deleted.
f(g(x),y,y) → g(f(x,x,y)) (1)

1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.