Certification Problem

Input (TPDB TRS_Standard/SK90/4.08)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[*(x1, x2)] = 2 + 1 · x1 + 1 · x2
all of the following rules can be deleted.
*(x,x) → x (2)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[*(x1, x2)] = 1 + 1 · x1 + 2 · x2
all of the following rules can be deleted.
*(x,*(y,z)) → *(*(x,y),z) (1)

1.1.1 R is empty

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