Certification Problem

Input (TPDB TRS_Standard/Various_04/06)

The rewrite relation of the following TRS is considered.

f(x,y) → g1(x,x,y) (1)
f(x,y) → g1(y,x,x) (2)
f(x,y) → g2(x,y,y) (3)
f(x,y) → g2(y,y,x) (4)
g1(x,x,y) → h(x,y) (5)
g1(y,x,x) → h(x,y) (6)
g2(x,y,y) → h(x,y) (7)
g2(y,y,x) → h(x,y) (8)
h(x,x) → x (9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[g1(x1, x2, x3)] =
3 2
1 5
· x1 +
1 0
0 0
· x2 +
3 2
1 5
· x3 +
4 0
2 0
[h(x1, x2)] =
1 0
1 0
· x1 +
3 0
1 2
· x2 +
0 0
0 0
[f(x1, x2)] =
4 2
1 5
· x1 +
3 2
1 5
· x2 +
4 0
2 0
[g2(x1, x2, x3)] =
1 0
1 5
· x1 +
2 0
0 0
· x2 +
1 0
1 4
· x3 +
4 0
0 0
all of the following rules can be deleted.
g1(x,x,y) → h(x,y) (5)
g1(y,x,x) → h(x,y) (6)
g2(x,y,y) → h(x,y) (7)
g2(y,y,x) → h(x,y) (8)

1.1 Rule Removal

Using the Weighted Path Order with the following precedence and status
prec(h) = 0 status(h) = [2, 1] list-extension(h) = Lex
prec(g2) = 0 status(g2) = [1, 2, 3] list-extension(g2) = Lex
prec(g1) = 0 status(g1) = [1, 3, 2] list-extension(g1) = Lex
prec(f) = 1 status(f) = [2, 1] list-extension(f) = Lex
and the following Max-polynomial interpretation
[h(x1, x2)] = max(0, 1 + 1 · x1, 0 + 1 · x2)
[g2(x1, x2, x3)] = max(0, 0 + 1 · x1, 0 + 1 · x2, 0 + 1 · x3)
[g1(x1, x2, x3)] = max(0, 0 + 1 · x1, 0 + 1 · x2, 0 + 1 · x3)
[f(x1, x2)] = max(4, 0 + 1 · x1, 0 + 1 · x2)
all of the following rules can be deleted.
f(x,y) → g1(x,x,y) (1)
f(x,y) → g1(y,x,x) (2)
f(x,y) → g2(x,y,y) (3)
f(x,y) → g2(y,y,x) (4)
h(x,x) → x (9)

1.1.1 R is empty

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