Certification Problem

Input (TPDB SRS_Relative/Mixed_relative_SRS/zr03)

The relative rewrite relation R/S is considered where R is the following TRS

a(a(x1))

→

a(b(a(x1)))

(1)

and S is the following TRS.

b(x1)

→

b(b(x1))

(2)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[b(x₁)]

=

1	1	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a(x₁)]

=

1	1	1
1	1	0
0	0	0

· x₁ +

0	0	0
1	0	0
1	0	0

all of the following rules can be deleted.

a(a(x1))

→

a(b(a(x1)))

(1)

1.1 R is empty

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