Certification Problem

Input (TPDB TRS_Standard/Der95/02)

The rewrite relation of the following TRS is considered.

.(1,x) x (1)
.(x,1) x (2)
.(i(x),x) 1 (3)
.(x,i(x)) 1 (4)
i(1) 1 (5)
i(i(x)) x (6)
.(i(y),.(y,z)) z (7)
.(y,.(i(y),z)) z (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(i) = 0 weight(i) = 4
prec(.) = 3 weight(.) = 0
prec(1) = 2 weight(1) = 6
all of the following rules can be deleted.
.(1,x) x (1)
.(x,1) x (2)
.(i(x),x) 1 (3)
.(x,i(x)) 1 (4)
i(1) 1 (5)
i(i(x)) x (6)
.(i(y),.(y,z)) z (7)
.(y,.(i(y),z)) z (8)

1.1 R is empty

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