Certification Problem

Input (TPDB TRS_Standard/Der95/01)

The rewrite relation of the following TRS is considered.

\(x,x) e (1)
/(x,x) e (2)
.(e,x) x (3)
.(x,e) x (4)
\(e,x) x (5)
/(x,e) x (6)
.(x,\(x,y)) y (7)
.(/(y,x),x) y (8)
\(x,.(x,y)) y (9)
/(.(y,x),x) y (10)
/(x,\(y,x)) y (11)
\(/(x,y),x) y (12)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(e) = 0 weight(e) = 2
prec(\) = 1 weight(\) = 0
prec(/) = 2 weight(/) = 0
prec(.) = 3 weight(.) = 0
all of the following rules can be deleted.
\(x,x) e (1)
/(x,x) e (2)
.(e,x) x (3)
.(x,e) x (4)
\(e,x) x (5)
/(x,e) x (6)
.(x,\(x,y)) y (7)
.(/(y,x),x) y (8)
\(x,.(x,y)) y (9)
/(.(y,x),x) y (10)
/(x,\(y,x)) y (11)
\(/(x,y),x) y (12)

1.1 R is empty

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