Certification Problem

Input (TPDB TRS_Standard/Der95/18)

The rewrite relation of the following TRS is considered.

*(x,+(y,z)) → +(*(x,y),*(x,z)) (1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(*) = 1 stat(*) = lex
prec(+) = 0 stat(+) = lex

π(*) = [1,2]
π(+) = [2,1]

all of the following rules can be deleted.
*(x,+(y,z)) → +(*(x,y),*(x,z)) (1)

1.1 R is empty

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