Certification Problem

Input (TPDB TRS_Standard/Der95/28)

The rewrite relation of the following TRS is considered.

if(if(x,y,z),u,v)

→

if(x,if(y,u,v),if(z,u,v))

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(if)

=

0

stat(if)

=

lex

π(if)

=

[1,2,3]

all of the following rules can be deleted.

if(if(x,y,z),u,v)

→

if(x,if(y,u,v),if(z,u,v))

(1)

1.1 R is empty

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