Certification Problem

Input (TPDB TRS_Standard/TCT_12/polycounter-10)

The rewrite relation of the following TRS is considered.

f(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10) → f(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) (1)
f(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10) → f(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10) (2)
f(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10) → f(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10) (3)
f(0,0,0,s(x4),x5,x6,x7,x8,x9,x10) → f(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10) (4)
f(0,0,0,0,s(x5),x6,x7,x8,x9,x10) → f(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10) (5)
f(0,0,0,0,0,s(x6),x7,x8,x9,x10) → f(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10) (6)
f(0,0,0,0,0,0,s(x7),x8,x9,x10) → f(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10) (7)
f(0,0,0,0,0,0,0,s(x8),x9,x10) → f(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10) (8)
f(0,0,0,0,0,0,0,0,s(x9),x10) → f(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10) (9)
f(0,0,0,0,0,0,0,0,0,s(x10)) → f(x10,x10,x10,x10,x10,x10,x10,x10,x10,x10) (10)
f(0,0,0,0,0,0,0,0,0,0) → 0 (11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[f(x1,...,x10)] = 5 · x1 + 2 · x2 + 1 · x3 + 1 · x4 + 3 · x5 + 5 · x6 + 2 · x7 + 5 · x8 + 3 · x9 + 4 · x10 + 3
[s(x1)] = 12 · x1 + 16
[0] = 0
all of the following rules can be deleted.
f(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10) → f(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) (1)
f(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10) → f(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10) (2)
f(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10) → f(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10) (3)
f(0,0,0,s(x4),x5,x6,x7,x8,x9,x10) → f(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10) (4)
f(0,0,0,0,s(x5),x6,x7,x8,x9,x10) → f(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10) (5)
f(0,0,0,0,0,s(x6),x7,x8,x9,x10) → f(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10) (6)
f(0,0,0,0,0,0,s(x7),x8,x9,x10) → f(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10) (7)
f(0,0,0,0,0,0,0,s(x8),x9,x10) → f(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10) (8)
f(0,0,0,0,0,0,0,0,s(x9),x10) → f(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10) (9)
f(0,0,0,0,0,0,0,0,0,s(x10)) → f(x10,x10,x10,x10,x10,x10,x10,x10,x10,x10) (10)
f(0,0,0,0,0,0,0,0,0,0) → 0 (11)

1.1 R is empty

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